zdvddef - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		eor	(a = b0 (zabs a) -> a \|Z b -> E. c c Z a = b) -> (a = -uZ b0 (zabs a) -> a \|Z b -> E. c c Z a = b) -> a = b0 (zabs a) \/ a = -uZ b0 (zabs a) -> a \|Z b -> E. c c *Z a = b
2		zb0orb0	b = b0 (zabs b) \/ b = -uZ b0 (zabs b)
3		zdvdb0	b0 (zabs a) \|Z b0 (zabs b) <-> zabs a \|\| zabs b
4		zmuleq1	c = b0 (zabs b // zabs a) -> c Z b0 (zabs a) = b0 (zabs b // zabs a) Z b0 (zabs a)
5	4	eqeq1d	c = b0 (zabs b // zabs a) -> (c Z b0 (zabs a) = b0 (zabs b) <-> b0 (zabs b // zabs a) Z b0 (zabs a) = b0 (zabs b))
6	5	iexe	b0 (zabs b // zabs a) Z b0 (zabs a) = b0 (zabs b) -> E. c c Z b0 (zabs a) = b0 (zabs b)
7		zmulb0	b0 (zabs b // zabs a) Z b0 (zabs a) = b0 (zabs b // zabs a zabs a)
8		divmul	zabs a \|\| zabs b -> zabs b // zabs a * zabs a = zabs b
9	8	b0eqd	zabs a \|\| zabs b -> b0 (zabs b // zabs a * zabs a) = b0 (zabs b)
10	7, 9	syl5eq	zabs a \|\| zabs b -> b0 (zabs b // zabs a) *Z b0 (zabs a) = b0 (zabs b)
11	6, 10	syl	zabs a \|\| zabs b -> E. c c *Z b0 (zabs a) = b0 (zabs b)
12	3, 11	sylbi	b0 (zabs a) \|Z b0 (zabs b) -> E. c c *Z b0 (zabs a) = b0 (zabs b)
13		anl	a = b0 (zabs a) /\ b = b0 (zabs b) -> a = b0 (zabs a)
14		anr	a = b0 (zabs a) /\ b = b0 (zabs b) -> b = b0 (zabs b)
15	13, 14	zdvdeqd	a = b0 (zabs a) /\ b = b0 (zabs b) -> (a \|Z b <-> b0 (zabs a) \|Z b0 (zabs b))
16	13	zmuleq2d	a = b0 (zabs a) /\ b = b0 (zabs b) -> c Z a = c Z b0 (zabs a)
17	16, 14	eqeqd	a = b0 (zabs a) /\ b = b0 (zabs b) -> (c Z a = b <-> c Z b0 (zabs a) = b0 (zabs b))
18	17	exeqd	a = b0 (zabs a) /\ b = b0 (zabs b) -> (E. c c Z a = b <-> E. c c Z b0 (zabs a) = b0 (zabs b))
19	15, 18	imeqd	a = b0 (zabs a) /\ b = b0 (zabs b) -> (a \|Z b -> E. c c Z a = b <-> b0 (zabs a) \|Z b0 (zabs b) -> E. c c Z b0 (zabs a) = b0 (zabs b))
20	12, 19	mpbiri	a = b0 (zabs a) /\ b = b0 (zabs b) -> a \|Z b -> E. c c *Z a = b
21		zdvdneg2	b0 (zabs a) \|Z -uZ b0 (zabs b) <-> b0 (zabs a) \|Z b0 (zabs b)
22		zmuleq1	c = -uZ b0 (zabs b // zabs a) -> c Z b0 (zabs a) = -uZ b0 (zabs b // zabs a) Z b0 (zabs a)
23	22	eqeq1d	c = -uZ b0 (zabs b // zabs a) -> (c Z b0 (zabs a) = -uZ b0 (zabs b) <-> -uZ b0 (zabs b // zabs a) Z b0 (zabs a) = -uZ b0 (zabs b))
24	23	iexe	-uZ b0 (zabs b // zabs a) Z b0 (zabs a) = -uZ b0 (zabs b) -> E. c c Z b0 (zabs a) = -uZ b0 (zabs b)
25		zmulneg1	-uZ b0 (zabs b // zabs a) Z b0 (zabs a) = -uZ (b0 (zabs b // zabs a) Z b0 (zabs a))
26	10	znegeqd	zabs a \|\| zabs b -> -uZ (b0 (zabs b // zabs a) *Z b0 (zabs a)) = -uZ b0 (zabs b)
27	25, 26	syl5eq	zabs a \|\| zabs b -> -uZ b0 (zabs b // zabs a) *Z b0 (zabs a) = -uZ b0 (zabs b)
28	24, 27	syl	zabs a \|\| zabs b -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)
29	3, 28	sylbi	b0 (zabs a) \|Z b0 (zabs b) -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)
30	21, 29	sylbi	b0 (zabs a) \|Z -uZ b0 (zabs b) -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)
31		anl	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a = b0 (zabs a)
32		anr	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> b = -uZ b0 (zabs b)
33	31, 32	zdvdeqd	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a \|Z b <-> b0 (zabs a) \|Z -uZ b0 (zabs b))
34	31	zmuleq2d	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> c Z a = c Z b0 (zabs a)
35	34, 32	eqeqd	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (c Z a = b <-> c Z b0 (zabs a) = -uZ b0 (zabs b))
36	35	exeqd	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (E. c c Z a = b <-> E. c c Z b0 (zabs a) = -uZ b0 (zabs b))
37	33, 36	imeqd	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a \|Z b -> E. c c Z a = b <-> b0 (zabs a) \|Z -uZ b0 (zabs b) -> E. c c Z b0 (zabs a) = -uZ b0 (zabs b))
38	30, 37	mpbiri	a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a \|Z b -> E. c c *Z a = b
39	20, 38	eorda	a = b0 (zabs a) -> b = b0 (zabs b) \/ b = -uZ b0 (zabs b) -> a \|Z b -> E. c c *Z a = b
40	2, 39	mpi	a = b0 (zabs a) -> a \|Z b -> E. c c *Z a = b
41	1, 40	ax_mp	(a = -uZ b0 (zabs a) -> a \|Z b -> E. c c Z a = b) -> a = b0 (zabs a) \/ a = -uZ b0 (zabs a) -> a \|Z b -> E. c c Z a = b
42		zdvdneg1	-uZ b0 (zabs a) \|Z b0 (zabs b) <-> b0 (zabs a) \|Z b0 (zabs b)
43		zmuleq1	c = -uZ b0 (zabs b // zabs a) -> c Z -uZ b0 (zabs a) = -uZ b0 (zabs b // zabs a) Z -uZ b0 (zabs a)
44	43	eqeq1d	c = -uZ b0 (zabs b // zabs a) -> (c Z -uZ b0 (zabs a) = b0 (zabs b) <-> -uZ b0 (zabs b // zabs a) Z -uZ b0 (zabs a) = b0 (zabs b))
45	44	iexe	-uZ b0 (zabs b // zabs a) Z -uZ b0 (zabs a) = b0 (zabs b) -> E. c c Z -uZ b0 (zabs a) = b0 (zabs b)
46		zmul2neg	-uZ b0 (zabs b // zabs a) Z -uZ b0 (zabs a) = b0 (zabs b // zabs a) Z b0 (zabs a)
47	46, 10	syl5eq	zabs a \|\| zabs b -> -uZ b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = b0 (zabs b)
48	45, 47	syl	zabs a \|\| zabs b -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)
49	3, 48	sylbi	b0 (zabs a) \|Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)
50	42, 49	sylbi	-uZ b0 (zabs a) \|Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)
51		anl	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> a = -uZ b0 (zabs a)
52		anr	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> b = b0 (zabs b)
53	51, 52	zdvdeqd	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (a \|Z b <-> -uZ b0 (zabs a) \|Z b0 (zabs b))
54	51	zmuleq2d	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> c Z a = c Z -uZ b0 (zabs a)
55	54, 52	eqeqd	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (c Z a = b <-> c Z -uZ b0 (zabs a) = b0 (zabs b))
56	55	exeqd	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (E. c c Z a = b <-> E. c c Z -uZ b0 (zabs a) = b0 (zabs b))
57	53, 56	imeqd	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (a \|Z b -> E. c c Z a = b <-> -uZ b0 (zabs a) \|Z b0 (zabs b) -> E. c c Z -uZ b0 (zabs a) = b0 (zabs b))
58	50, 57	mpbiri	a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> a \|Z b -> E. c c *Z a = b
59		zdvdneg2	-uZ b0 (zabs a) \|Z -uZ b0 (zabs b) <-> -uZ b0 (zabs a) \|Z b0 (zabs b)
60		zmuleq1	c = b0 (zabs b // zabs a) -> c Z -uZ b0 (zabs a) = b0 (zabs b // zabs a) Z -uZ b0 (zabs a)
61	60	eqeq1d	c = b0 (zabs b // zabs a) -> (c Z -uZ b0 (zabs a) = -uZ b0 (zabs b) <-> b0 (zabs b // zabs a) Z -uZ b0 (zabs a) = -uZ b0 (zabs b))
62	61	iexe	b0 (zabs b // zabs a) Z -uZ b0 (zabs a) = -uZ b0 (zabs b) -> E. c c Z -uZ b0 (zabs a) = -uZ b0 (zabs b)
63		zmulneg2	b0 (zabs b // zabs a) Z -uZ b0 (zabs a) = -uZ (b0 (zabs b // zabs a) Z b0 (zabs a))
64	63, 26	syl5eq	zabs a \|\| zabs b -> b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)
65	62, 64	syl	zabs a \|\| zabs b -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)
66	3, 65	sylbi	b0 (zabs a) \|Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)
67	42, 66	sylbi	-uZ b0 (zabs a) \|Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)
68	59, 67	sylbi	-uZ b0 (zabs a) \|Z -uZ b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)
69		anl	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a = -uZ b0 (zabs a)
70		anr	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> b = -uZ b0 (zabs b)
71	69, 70	zdvdeqd	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a \|Z b <-> -uZ b0 (zabs a) \|Z -uZ b0 (zabs b))
72	69	zmuleq2d	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> c Z a = c Z -uZ b0 (zabs a)
73	72, 70	eqeqd	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (c Z a = b <-> c Z -uZ b0 (zabs a) = -uZ b0 (zabs b))
74	73	exeqd	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (E. c c Z a = b <-> E. c c Z -uZ b0 (zabs a) = -uZ b0 (zabs b))
75	71, 74	imeqd	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a \|Z b -> E. c c Z a = b <-> -uZ b0 (zabs a) \|Z -uZ b0 (zabs b) -> E. c c Z -uZ b0 (zabs a) = -uZ b0 (zabs b))
76	68, 75	mpbiri	a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a \|Z b -> E. c c *Z a = b
77	58, 76	eorda	a = -uZ b0 (zabs a) -> b = b0 (zabs b) \/ b = -uZ b0 (zabs b) -> a \|Z b -> E. c c *Z a = b
78	2, 77	mpi	a = -uZ b0 (zabs a) -> a \|Z b -> E. c c *Z a = b
79	41, 78	ax_mp	a = b0 (zabs a) \/ a = -uZ b0 (zabs a) -> a \|Z b -> E. c c *Z a = b
80		zb0orb0	a = b0 (zabs a) \/ a = -uZ b0 (zabs a)
81	79, 80	ax_mp	a \|Z b -> E. c c *Z a = b
82		izdvd	c *Z a = b -> a \|Z b
83	82	eex	E. c c *Z a = b -> a \|Z b
84	81, 83	ibii	a \|Z b <-> E. c c *Z a = b

1

(a = b0 (zabs a) -> a |Z b -> E. c c *Z a = b) ->
  (a = -uZ b0 (zabs a) -> a |Z b -> E. c c *Z a = b) ->
  a = b0 (zabs a) \/ a = -uZ b0 (zabs a) ->
  a |Z b ->
  E. c c *Z a = b

2

zb0orb0

b = b0 (zabs b) \/ b = -uZ b0 (zabs b)

3

zdvdb0

b0 (zabs a) |Z b0 (zabs b) <-> zabs a || zabs b

4

zmuleq1

c = b0 (zabs b // zabs a) -> c *Z b0 (zabs a) = b0 (zabs b // zabs a) *Z b0 (zabs a)

5

4

eqeq1d

c = b0 (zabs b // zabs a) -> (c *Z b0 (zabs a) = b0 (zabs b) <-> b0 (zabs b // zabs a) *Z b0 (zabs a) = b0 (zabs b))

6

5

iexe

b0 (zabs b // zabs a) *Z b0 (zabs a) = b0 (zabs b) -> E. c c *Z b0 (zabs a) = b0 (zabs b)

7

zmulb0

b0 (zabs b // zabs a) *Z b0 (zabs a) = b0 (zabs b // zabs a * zabs a)

8

divmul

zabs a || zabs b -> zabs b // zabs a * zabs a = zabs b

9

8

b0eqd

zabs a || zabs b -> b0 (zabs b // zabs a * zabs a) = b0 (zabs b)

10

7, 9

syl5eq

zabs a || zabs b -> b0 (zabs b // zabs a) *Z b0 (zabs a) = b0 (zabs b)

11

6, 10

syl

zabs a || zabs b -> E. c c *Z b0 (zabs a) = b0 (zabs b)

12

3, 11

sylbi

b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z b0 (zabs a) = b0 (zabs b)

13

anl

a = b0 (zabs a) /\ b = b0 (zabs b) -> a = b0 (zabs a)

14

anr

a = b0 (zabs a) /\ b = b0 (zabs b) -> b = b0 (zabs b)

15

13, 14

zdvdeqd

a = b0 (zabs a) /\ b = b0 (zabs b) -> (a |Z b <-> b0 (zabs a) |Z b0 (zabs b))

16

13

zmuleq2d

a = b0 (zabs a) /\ b = b0 (zabs b) -> c *Z a = c *Z b0 (zabs a)

17

16, 14

eqeqd

a = b0 (zabs a) /\ b = b0 (zabs b) -> (c *Z a = b <-> c *Z b0 (zabs a) = b0 (zabs b))

18

17

exeqd

a = b0 (zabs a) /\ b = b0 (zabs b) -> (E. c c *Z a = b <-> E. c c *Z b0 (zabs a) = b0 (zabs b))

19

15, 18

imeqd

a = b0 (zabs a) /\ b = b0 (zabs b) -> (a |Z b -> E. c c *Z a = b <-> b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z b0 (zabs a) = b0 (zabs b))

20

12, 19

mpbiri

a = b0 (zabs a) /\ b = b0 (zabs b) -> a |Z b -> E. c c *Z a = b

21

zdvdneg2

b0 (zabs a) |Z -uZ b0 (zabs b) <-> b0 (zabs a) |Z b0 (zabs b)

22

zmuleq1

c = -uZ b0 (zabs b // zabs a) -> c *Z b0 (zabs a) = -uZ b0 (zabs b // zabs a) *Z b0 (zabs a)

23

22

eqeq1d

c = -uZ b0 (zabs b // zabs a) -> (c *Z b0 (zabs a) = -uZ b0 (zabs b) <-> -uZ b0 (zabs b // zabs a) *Z b0 (zabs a) = -uZ b0 (zabs b))

24

23

iexe

-uZ b0 (zabs b // zabs a) *Z b0 (zabs a) = -uZ b0 (zabs b) -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)

25

zmulneg1

-uZ b0 (zabs b // zabs a) *Z b0 (zabs a) = -uZ (b0 (zabs b // zabs a) *Z b0 (zabs a))

26

10

znegeqd

zabs a || zabs b -> -uZ (b0 (zabs b // zabs a) *Z b0 (zabs a)) = -uZ b0 (zabs b)

27

25, 26

syl5eq

zabs a || zabs b -> -uZ b0 (zabs b // zabs a) *Z b0 (zabs a) = -uZ b0 (zabs b)

28

24, 27

syl

zabs a || zabs b -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)

29

3, 28

sylbi

b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)

30

21, 29

sylbi

b0 (zabs a) |Z -uZ b0 (zabs b) -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b)

31

anl

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a = b0 (zabs a)

32

anr

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> b = -uZ b0 (zabs b)

33

31, 32

zdvdeqd

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a |Z b <-> b0 (zabs a) |Z -uZ b0 (zabs b))

34

31

zmuleq2d

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> c *Z a = c *Z b0 (zabs a)

35

34, 32

eqeqd

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (c *Z a = b <-> c *Z b0 (zabs a) = -uZ b0 (zabs b))

36

35

exeqd

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (E. c c *Z a = b <-> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b))

37

33, 36

imeqd

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a |Z b -> E. c c *Z a = b <-> b0 (zabs a) |Z -uZ b0 (zabs b) -> E. c c *Z b0 (zabs a) = -uZ b0 (zabs b))

38

30, 37

mpbiri

a = b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a |Z b -> E. c c *Z a = b

39

20, 38

eorda

a = b0 (zabs a) -> b = b0 (zabs b) \/ b = -uZ b0 (zabs b) -> a |Z b -> E. c c *Z a = b

40

2, 39

mpi

a = b0 (zabs a) -> a |Z b -> E. c c *Z a = b

41

1, 40

ax_mp

(a = -uZ b0 (zabs a) -> a |Z b -> E. c c *Z a = b) -> a = b0 (zabs a) \/ a = -uZ b0 (zabs a) -> a |Z b -> E. c c *Z a = b

42

zdvdneg1

-uZ b0 (zabs a) |Z b0 (zabs b) <-> b0 (zabs a) |Z b0 (zabs b)

43

zmuleq1

c = -uZ b0 (zabs b // zabs a) -> c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b // zabs a) *Z -uZ b0 (zabs a)

44

43

eqeq1d

c = -uZ b0 (zabs b // zabs a) -> (c *Z -uZ b0 (zabs a) = b0 (zabs b) <-> -uZ b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = b0 (zabs b))

45

44

iexe

-uZ b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)

46

zmul2neg

-uZ b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = b0 (zabs b // zabs a) *Z b0 (zabs a)

47

46, 10

syl5eq

zabs a || zabs b -> -uZ b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = b0 (zabs b)

48

45, 47

syl

zabs a || zabs b -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)

49

3, 48

sylbi

b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)

50

42, 49

sylbi

-uZ b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b)

51

anl

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> a = -uZ b0 (zabs a)

52

anr

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> b = b0 (zabs b)

53

51, 52

zdvdeqd

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (a |Z b <-> -uZ b0 (zabs a) |Z b0 (zabs b))

54

51

zmuleq2d

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> c *Z a = c *Z -uZ b0 (zabs a)

55

54, 52

eqeqd

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (c *Z a = b <-> c *Z -uZ b0 (zabs a) = b0 (zabs b))

56

55

exeqd

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (E. c c *Z a = b <-> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b))

57

53, 56

imeqd

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> (a |Z b -> E. c c *Z a = b <-> -uZ b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = b0 (zabs b))

58

50, 57

mpbiri

a = -uZ b0 (zabs a) /\ b = b0 (zabs b) -> a |Z b -> E. c c *Z a = b

59

zdvdneg2

-uZ b0 (zabs a) |Z -uZ b0 (zabs b) <-> -uZ b0 (zabs a) |Z b0 (zabs b)

60

zmuleq1

c = b0 (zabs b // zabs a) -> c *Z -uZ b0 (zabs a) = b0 (zabs b // zabs a) *Z -uZ b0 (zabs a)

61

60

eqeq1d

c = b0 (zabs b // zabs a) -> (c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b) <-> b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = -uZ b0 (zabs b))

62

61

iexe

b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = -uZ b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)

63

zmulneg2

b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = -uZ (b0 (zabs b // zabs a) *Z b0 (zabs a))

64

63, 26

syl5eq

zabs a || zabs b -> b0 (zabs b // zabs a) *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)

65

62, 64

syl

zabs a || zabs b -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)

66

3, 65

sylbi

b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)

67

42, 66

sylbi

-uZ b0 (zabs a) |Z b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)

68

59, 67

sylbi

-uZ b0 (zabs a) |Z -uZ b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b)

69

anl

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a = -uZ b0 (zabs a)

70

anr

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> b = -uZ b0 (zabs b)

71

69, 70

zdvdeqd

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a |Z b <-> -uZ b0 (zabs a) |Z -uZ b0 (zabs b))

72

69

zmuleq2d

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> c *Z a = c *Z -uZ b0 (zabs a)

73

72, 70

eqeqd

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (c *Z a = b <-> c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b))

74

73

exeqd

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (E. c c *Z a = b <-> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b))

75

71, 74

imeqd

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> (a |Z b -> E. c c *Z a = b <-> -uZ b0 (zabs a) |Z -uZ b0 (zabs b) -> E. c c *Z -uZ b0 (zabs a) = -uZ b0 (zabs b))

76

68, 75

mpbiri

a = -uZ b0 (zabs a) /\ b = -uZ b0 (zabs b) -> a |Z b -> E. c c *Z a = b

77

58, 76

eorda

a = -uZ b0 (zabs a) -> b = b0 (zabs b) \/ b = -uZ b0 (zabs b) -> a |Z b -> E. c c *Z a = b

78

2, 77

mpi

a = -uZ b0 (zabs a) -> a |Z b -> E. c c *Z a = b

79

41, 78

ax_mp

a = b0 (zabs a) \/ a = -uZ b0 (zabs a) -> a |Z b -> E. c c *Z a = b

80

zb0orb0

a = b0 (zabs a) \/ a = -uZ b0 (zabs a)

81

79, 80

ax_mp

a |Z b -> E. c c *Z a = b

82

izdvd

c *Z a = b -> a |Z b

83

82

eex

E. c c *Z a = b -> a |Z b

84

81, 83

ibii

a |Z b <-> E. c c *Z a = b

Theorem zdvddef ≪ | index | src | ≫

Axiom use