zabsmul - examples/peano.mm1

Step	Hyp	Ref	Expression
1		eor	(m = b0 (zabs m) -> zabs (m Z n) = zabs m zabs n) -> (m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n) -> m = b0 (zabs m) \/ m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
2		eqtr4	zabs (b0 (zabs m) Z n) = zabs m zabs n -> zabs (b0 (zabs m)) * zabs n = zabs m * zabs n -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n
3		eor	(n = b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n) -> (n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n) -> n = b0 (zabs n) \/ n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
4		eqtr	zabs (b0 (zabs m) Z b0 (zabs n)) = zabs (b0 (zabs m zabs n)) -> zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n)) -> zabs (b0 (zabs m) Z b0 (zabs n)) = zabs m zabs (b0 (zabs n))
5		zabseq	b0 (zabs m) Z b0 (zabs n) = b0 (zabs m zabs n) -> zabs (b0 (zabs m) Z b0 (zabs n)) = zabs (b0 (zabs m zabs n))
6		zmulb0	b0 (zabs m) Z b0 (zabs n) = b0 (zabs m zabs n)
7	5, 6	ax_mp	zabs (b0 (zabs m) Z b0 (zabs n)) = zabs (b0 (zabs m zabs n))
8	4, 7	ax_mp	zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n)) -> zabs (b0 (zabs m) Z b0 (zabs n)) = zabs m zabs (b0 (zabs n))
9		eqtr4	zabs (b0 (zabs m * zabs n)) = zabs m * zabs n -> zabs m * zabs (b0 (zabs n)) = zabs m * zabs n -> zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n))
10		zabsb0	zabs (b0 (zabs m * zabs n)) = zabs m * zabs n
11	9, 10	ax_mp	zabs m * zabs (b0 (zabs n)) = zabs m * zabs n -> zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n))
12		muleq2	zabs (b0 (zabs n)) = zabs n -> zabs m * zabs (b0 (zabs n)) = zabs m * zabs n
13		zabsb0	zabs (b0 (zabs n)) = zabs n
14	12, 13	ax_mp	zabs m * zabs (b0 (zabs n)) = zabs m * zabs n
15	11, 14	ax_mp	zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n))
16	8, 15	ax_mp	zabs (b0 (zabs m) Z b0 (zabs n)) = zabs m zabs (b0 (zabs n))
17		id	n = b0 (zabs n) -> n = b0 (zabs n)
18	17	zmuleq2d	n = b0 (zabs n) -> b0 (zabs m) Z n = b0 (zabs m) Z b0 (zabs n)
19	18	zabseqd	n = b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m) Z b0 (zabs n))
20	17	zabseqd	n = b0 (zabs n) -> zabs n = zabs (b0 (zabs n))
21	20	muleq2d	n = b0 (zabs n) -> zabs m * zabs n = zabs m * zabs (b0 (zabs n))
22	19, 21	eqeqd	n = b0 (zabs n) -> (zabs (b0 (zabs m) Z n) = zabs m zabs n <-> zabs (b0 (zabs m) Z b0 (zabs n)) = zabs m zabs (b0 (zabs n)))
23	16, 22	mpbiri	n = b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
24	3, 23	ax_mp	(n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n) -> n = b0 (zabs n) \/ n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
25		eqtr	zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) -> zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs m zabs (-uZ b0 (zabs n)) -> zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs m zabs (-uZ b0 (zabs n))
26		zabseq	b0 (zabs m) Z -uZ b0 (zabs n) = -uZ (b0 (zabs m) Z b0 (zabs n)) -> zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) Z b0 (zabs n)))
27		zmulneg2	b0 (zabs m) Z -uZ b0 (zabs n) = -uZ (b0 (zabs m) Z b0 (zabs n))
28	26, 27	ax_mp	zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) Z b0 (zabs n)))
29	25, 28	ax_mp	zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs m zabs (-uZ b0 (zabs n)) -> zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs m zabs (-uZ b0 (zabs n))
30		eqtr4	zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs (b0 (zabs m) Z b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) Z b0 (zabs n)) -> zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n))
31		zabsneg	zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs (b0 (zabs m) Z b0 (zabs n))
32	30, 31	ax_mp	zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) Z b0 (zabs n)) -> zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n))
33		eqtr4	zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n)) -> zabs (b0 (zabs m) Z b0 (zabs n)) = zabs m zabs (b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))
34		muleq2	zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n))
35		zabsneg	zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs n))
36	34, 35	ax_mp	zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n))
37	33, 36	ax_mp	zabs (b0 (zabs m) Z b0 (zabs n)) = zabs m zabs (b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))
38	37, 16	ax_mp	zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))
39	32, 38	ax_mp	zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs m zabs (-uZ b0 (zabs n))
40	29, 39	ax_mp	zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs m zabs (-uZ b0 (zabs n))
41		id	n = -uZ b0 (zabs n) -> n = -uZ b0 (zabs n)
42	41	zmuleq2d	n = -uZ b0 (zabs n) -> b0 (zabs m) Z n = b0 (zabs m) Z -uZ b0 (zabs n)
43	42	zabseqd	n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m) Z -uZ b0 (zabs n))
44	41	zabseqd	n = -uZ b0 (zabs n) -> zabs n = zabs (-uZ b0 (zabs n))
45	44	muleq2d	n = -uZ b0 (zabs n) -> zabs m * zabs n = zabs m * zabs (-uZ b0 (zabs n))
46	43, 45	eqeqd	n = -uZ b0 (zabs n) -> (zabs (b0 (zabs m) Z n) = zabs m zabs n <-> zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs m zabs (-uZ b0 (zabs n)))
47	40, 46	mpbiri	n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
48	24, 47	ax_mp	n = b0 (zabs n) \/ n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
49		zb0orb0	n = b0 (zabs n) \/ n = -uZ b0 (zabs n)
50	48, 49	ax_mp	zabs (b0 (zabs m) Z n) = zabs m zabs n
51	2, 50	ax_mp	zabs (b0 (zabs m)) * zabs n = zabs m * zabs n -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n
52		muleq1	zabs (b0 (zabs m)) = zabs m -> zabs (b0 (zabs m)) * zabs n = zabs m * zabs n
53		zabsb0	zabs (b0 (zabs m)) = zabs m
54	52, 53	ax_mp	zabs (b0 (zabs m)) * zabs n = zabs m * zabs n
55	51, 54	ax_mp	zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n
56		id	m = b0 (zabs m) -> m = b0 (zabs m)
57	56	zmuleq1d	m = b0 (zabs m) -> m Z n = b0 (zabs m) Z n
58	57	zabseqd	m = b0 (zabs m) -> zabs (m Z n) = zabs (b0 (zabs m) Z n)
59	56	zabseqd	m = b0 (zabs m) -> zabs m = zabs (b0 (zabs m))
60	59	muleq1d	m = b0 (zabs m) -> zabs m * zabs n = zabs (b0 (zabs m)) * zabs n
61	58, 60	eqeqd	m = b0 (zabs m) -> (zabs (m Z n) = zabs m zabs n <-> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n)
62	55, 61	mpbiri	m = b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
63	1, 62	ax_mp	(m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n) -> m = b0 (zabs m) \/ m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
64		eqtr	zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ (b0 (zabs m) Z n)) -> zabs (-uZ (b0 (zabs m) Z n)) = zabs (-uZ b0 (zabs m)) zabs n -> zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ b0 (zabs m)) zabs n
65		zabseq	-uZ b0 (zabs m) Z n = -uZ (b0 (zabs m) Z n) -> zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ (b0 (zabs m) Z n))
66		zmulneg1	-uZ b0 (zabs m) Z n = -uZ (b0 (zabs m) Z n)
67	65, 66	ax_mp	zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ (b0 (zabs m) Z n))
68	64, 67	ax_mp	zabs (-uZ (b0 (zabs m) Z n)) = zabs (-uZ b0 (zabs m)) zabs n -> zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ b0 (zabs m)) zabs n
69		eqtr4	zabs (-uZ (b0 (zabs m) Z n)) = zabs (b0 (zabs m) Z n) -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) Z n) -> zabs (-uZ (b0 (zabs m) Z n)) = zabs (-uZ b0 (zabs m)) * zabs n
70		zabsneg	zabs (-uZ (b0 (zabs m) Z n)) = zabs (b0 (zabs m) Z n)
71	69, 70	ax_mp	zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) Z n) -> zabs (-uZ (b0 (zabs m) Z n)) = zabs (-uZ b0 (zabs m)) * zabs n
72		eqtr4	zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)
73		muleq1	zabs (-uZ b0 (zabs m)) = zabs (b0 (zabs m)) -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n
74		zabsneg	zabs (-uZ b0 (zabs m)) = zabs (b0 (zabs m))
75	73, 74	ax_mp	zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n
76	72, 75	ax_mp	zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)
77	76, 55	ax_mp	zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)
78	71, 77	ax_mp	zabs (-uZ (b0 (zabs m) Z n)) = zabs (-uZ b0 (zabs m)) zabs n
79	68, 78	ax_mp	zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ b0 (zabs m)) zabs n
80		id	m = -uZ b0 (zabs m) -> m = -uZ b0 (zabs m)
81	80	zmuleq1d	m = -uZ b0 (zabs m) -> m Z n = -uZ b0 (zabs m) Z n
82	81	zabseqd	m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs (-uZ b0 (zabs m) Z n)
83	80	zabseqd	m = -uZ b0 (zabs m) -> zabs m = zabs (-uZ b0 (zabs m))
84	83	muleq1d	m = -uZ b0 (zabs m) -> zabs m * zabs n = zabs (-uZ b0 (zabs m)) * zabs n
85	82, 84	eqeqd	m = -uZ b0 (zabs m) -> (zabs (m Z n) = zabs m zabs n <-> zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ b0 (zabs m)) zabs n)
86	79, 85	mpbiri	m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
87	63, 86	ax_mp	m = b0 (zabs m) \/ m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
88		zb0orb0	m = b0 (zabs m) \/ m = -uZ b0 (zabs m)
89	87, 88	ax_mp	zabs (m Z n) = zabs m zabs n

1

(m = b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n) ->
  (m = -uZ b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n) ->
  m = b0 (zabs m) \/ m = -uZ b0 (zabs m) ->
  zabs (m *Z n) = zabs m * zabs n

2

eqtr4

zabs (b0 (zabs m) *Z n) = zabs m * zabs n -> zabs (b0 (zabs m)) * zabs n = zabs m * zabs n -> zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m)) * zabs n

3

eor

(n = b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n) ->
  (n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n) ->
  n = b0 (zabs n) \/ n = -uZ b0 (zabs n) ->
  zabs (b0 (zabs m) *Z n) = zabs m * zabs n

4

eqtr

zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs (b0 (zabs m * zabs n)) ->
  zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n)) ->
  zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs m * zabs (b0 (zabs n))

5

zabseq

b0 (zabs m) *Z b0 (zabs n) = b0 (zabs m * zabs n) -> zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs (b0 (zabs m * zabs n))

6

zmulb0

b0 (zabs m) *Z b0 (zabs n) = b0 (zabs m * zabs n)

7

5, 6

ax_mp

zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs (b0 (zabs m * zabs n))

8

4, 7

ax_mp

zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n)) -> zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs m * zabs (b0 (zabs n))

9

eqtr4

zabs (b0 (zabs m * zabs n)) = zabs m * zabs n -> zabs m * zabs (b0 (zabs n)) = zabs m * zabs n -> zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n))

10

zabsb0

zabs (b0 (zabs m * zabs n)) = zabs m * zabs n

11

9, 10

ax_mp

zabs m * zabs (b0 (zabs n)) = zabs m * zabs n -> zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n))

12

muleq2

zabs (b0 (zabs n)) = zabs n -> zabs m * zabs (b0 (zabs n)) = zabs m * zabs n

13

zabsb0

zabs (b0 (zabs n)) = zabs n

14

12, 13

ax_mp

zabs m * zabs (b0 (zabs n)) = zabs m * zabs n

15

11, 14

ax_mp

zabs (b0 (zabs m * zabs n)) = zabs m * zabs (b0 (zabs n))

16

8, 15

ax_mp

zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs m * zabs (b0 (zabs n))

17

id

n = b0 (zabs n) -> n = b0 (zabs n)

18

17

zmuleq2d

n = b0 (zabs n) -> b0 (zabs m) *Z n = b0 (zabs m) *Z b0 (zabs n)

19

18

zabseqd

n = b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m) *Z b0 (zabs n))

20

17

zabseqd

n = b0 (zabs n) -> zabs n = zabs (b0 (zabs n))

21

20

muleq2d

n = b0 (zabs n) -> zabs m * zabs n = zabs m * zabs (b0 (zabs n))

22

19, 21

eqeqd

n = b0 (zabs n) -> (zabs (b0 (zabs m) *Z n) = zabs m * zabs n <-> zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs m * zabs (b0 (zabs n)))

23

16, 22

mpbiri

n = b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n

24

3, 23

ax_mp

(n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n) -> n = b0 (zabs n) \/ n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n

25

eqtr

zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) ->
  zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n)) ->
  zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs m * zabs (-uZ b0 (zabs n))

26

zabseq

b0 (zabs m) *Z -uZ b0 (zabs n) = -uZ (b0 (zabs m) *Z b0 (zabs n)) -> zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) *Z b0 (zabs n)))

27

zmulneg2

b0 (zabs m) *Z -uZ b0 (zabs n) = -uZ (b0 (zabs m) *Z b0 (zabs n))

28

26, 27

ax_mp

zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) *Z b0 (zabs n)))

29

25, 28

ax_mp

zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n)) -> zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs m * zabs (-uZ b0 (zabs n))

30

eqtr4

zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs (b0 (zabs m) *Z b0 (zabs n)) ->
  zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n)) ->
  zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n))

31

zabsneg

zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs (b0 (zabs m) *Z b0 (zabs n))

32

30, 31

ax_mp

zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n)) -> zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n))

33

eqtr4

zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n)) ->
  zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs m * zabs (b0 (zabs n)) ->
  zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))

34

muleq2

zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n))

35

zabsneg

zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs n))

36

34, 35

ax_mp

zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n))

37

33, 36

ax_mp

zabs (b0 (zabs m) *Z b0 (zabs n)) = zabs m * zabs (b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))

38

37, 16

ax_mp

zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))

39

32, 38

ax_mp

zabs (-uZ (b0 (zabs m) *Z b0 (zabs n))) = zabs m * zabs (-uZ b0 (zabs n))

40

29, 39

ax_mp

zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs m * zabs (-uZ b0 (zabs n))

41

id

n = -uZ b0 (zabs n) -> n = -uZ b0 (zabs n)

42

41

zmuleq2d

n = -uZ b0 (zabs n) -> b0 (zabs m) *Z n = b0 (zabs m) *Z -uZ b0 (zabs n)

43

42

zabseqd

n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m) *Z -uZ b0 (zabs n))

44

41

zabseqd

n = -uZ b0 (zabs n) -> zabs n = zabs (-uZ b0 (zabs n))

45

44

muleq2d

n = -uZ b0 (zabs n) -> zabs m * zabs n = zabs m * zabs (-uZ b0 (zabs n))

46

43, 45

eqeqd

n = -uZ b0 (zabs n) -> (zabs (b0 (zabs m) *Z n) = zabs m * zabs n <-> zabs (b0 (zabs m) *Z -uZ b0 (zabs n)) = zabs m * zabs (-uZ b0 (zabs n)))

47

40, 46

mpbiri

n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n

48

24, 47

ax_mp

n = b0 (zabs n) \/ n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) *Z n) = zabs m * zabs n

49

zb0orb0

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

50

48, 49

ax_mp

zabs (b0 (zabs m) *Z n) = zabs m * zabs n

51

2, 50

ax_mp

zabs (b0 (zabs m)) * zabs n = zabs m * zabs n -> zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m)) * zabs n

52

muleq1

zabs (b0 (zabs m)) = zabs m -> zabs (b0 (zabs m)) * zabs n = zabs m * zabs n

53

zabsb0

zabs (b0 (zabs m)) = zabs m

54

52, 53

ax_mp

zabs (b0 (zabs m)) * zabs n = zabs m * zabs n

55

51, 54

ax_mp

zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m)) * zabs n

56

id

m = b0 (zabs m) -> m = b0 (zabs m)

57

56

zmuleq1d

m = b0 (zabs m) -> m *Z n = b0 (zabs m) *Z n

58

57

zabseqd

m = b0 (zabs m) -> zabs (m *Z n) = zabs (b0 (zabs m) *Z n)

59

56

zabseqd

m = b0 (zabs m) -> zabs m = zabs (b0 (zabs m))

60

59

muleq1d

m = b0 (zabs m) -> zabs m * zabs n = zabs (b0 (zabs m)) * zabs n

61

58, 60

eqeqd

m = b0 (zabs m) -> (zabs (m *Z n) = zabs m * zabs n <-> zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m)) * zabs n)

62

55, 61

mpbiri

m = b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n

63

1, 62

ax_mp

(m = -uZ b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n) -> m = b0 (zabs m) \/ m = -uZ b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n

64

eqtr

zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ (b0 (zabs m) *Z n)) ->
  zabs (-uZ (b0 (zabs m) *Z n)) = zabs (-uZ b0 (zabs m)) * zabs n ->
  zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ b0 (zabs m)) * zabs n

65

zabseq

-uZ b0 (zabs m) *Z n = -uZ (b0 (zabs m) *Z n) -> zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ (b0 (zabs m) *Z n))

66

zmulneg1

-uZ b0 (zabs m) *Z n = -uZ (b0 (zabs m) *Z n)

67

65, 66

ax_mp

zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ (b0 (zabs m) *Z n))

68

64, 67

ax_mp

zabs (-uZ (b0 (zabs m) *Z n)) = zabs (-uZ b0 (zabs m)) * zabs n -> zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ b0 (zabs m)) * zabs n

69

eqtr4

zabs (-uZ (b0 (zabs m) *Z n)) = zabs (b0 (zabs m) *Z n) ->
  zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n) ->
  zabs (-uZ (b0 (zabs m) *Z n)) = zabs (-uZ b0 (zabs m)) * zabs n

70

zabsneg

zabs (-uZ (b0 (zabs m) *Z n)) = zabs (b0 (zabs m) *Z n)

71

69, 70

ax_mp

zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n) -> zabs (-uZ (b0 (zabs m) *Z n)) = zabs (-uZ b0 (zabs m)) * zabs n

72

eqtr4

zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n ->
  zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m)) * zabs n ->
  zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)

73

muleq1

zabs (-uZ b0 (zabs m)) = zabs (b0 (zabs m)) -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n

74

zabsneg

zabs (-uZ b0 (zabs m)) = zabs (b0 (zabs m))

75

73, 74

ax_mp

zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n

76

72, 75

ax_mp

zabs (b0 (zabs m) *Z n) = zabs (b0 (zabs m)) * zabs n -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)

77

76, 55

ax_mp

zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)

78

71, 77

ax_mp

zabs (-uZ (b0 (zabs m) *Z n)) = zabs (-uZ b0 (zabs m)) * zabs n

79

68, 78

ax_mp

zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ b0 (zabs m)) * zabs n

80

id

m = -uZ b0 (zabs m) -> m = -uZ b0 (zabs m)

81

80

zmuleq1d

m = -uZ b0 (zabs m) -> m *Z n = -uZ b0 (zabs m) *Z n

82

81

zabseqd

m = -uZ b0 (zabs m) -> zabs (m *Z n) = zabs (-uZ b0 (zabs m) *Z n)

83

80

zabseqd

m = -uZ b0 (zabs m) -> zabs m = zabs (-uZ b0 (zabs m))

84

83

muleq1d

m = -uZ b0 (zabs m) -> zabs m * zabs n = zabs (-uZ b0 (zabs m)) * zabs n

85

82, 84

eqeqd

m = -uZ b0 (zabs m) -> (zabs (m *Z n) = zabs m * zabs n <-> zabs (-uZ b0 (zabs m) *Z n) = zabs (-uZ b0 (zabs m)) * zabs n)

86

79, 85

mpbiri

m = -uZ b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n

87

63, 86

ax_mp

m = b0 (zabs m) \/ m = -uZ b0 (zabs m) -> zabs (m *Z n) = zabs m * zabs n

88

zb0orb0

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

89

87, 88

ax_mp

zabs (m *Z n) = zabs m * zabs n

Theorem zabsmul ≪ | index | src | ≫

Axiom use