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		eqidd	n = b0 (zabs n) -> b0 (zabs m) = b0 (zabs m)
18		id	n = b0 (zabs n) -> n = b0 (zabs n)
19	17, 18	zmuleqd	n = b0 (zabs n) -> b0 (zabs m) Z n = b0 (zabs m) Z b0 (zabs n)
20	19	zabseqd	n = b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m) Z b0 (zabs n))
21		eqidd	n = b0 (zabs n) -> zabs m = zabs m
22	18	zabseqd	n = b0 (zabs n) -> zabs n = zabs (b0 (zabs n))
23	21, 22	muleqd	n = b0 (zabs n) -> zabs m * zabs n = zabs m * zabs (b0 (zabs n))
24	20, 23	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)))
25	16, 24	mpbiri	n = b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
26	3, 25	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
27		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))
28		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)))
29		zmulneg2	b0 (zabs m) Z -uZ b0 (zabs n) = -uZ (b0 (zabs m) Z b0 (zabs n))
30	28, 29	ax_mp	zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs (-uZ (b0 (zabs m) Z b0 (zabs n)))
31	27, 30	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))
32		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))
33		zabsneg	zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs (b0 (zabs m) Z b0 (zabs n))
34	32, 33	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))
35		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))
36		muleq2	zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs n)) -> zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n))
37		zabsneg	zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs n))
38	36, 37	ax_mp	zabs m * zabs (-uZ b0 (zabs n)) = zabs m * zabs (b0 (zabs n))
39	35, 38	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))
40	39, 16	ax_mp	zabs m * zabs (-uZ b0 (zabs n)) = zabs (b0 (zabs m) *Z b0 (zabs n))
41	34, 40	ax_mp	zabs (-uZ (b0 (zabs m) Z b0 (zabs n))) = zabs m zabs (-uZ b0 (zabs n))
42	31, 41	ax_mp	zabs (b0 (zabs m) Z -uZ b0 (zabs n)) = zabs m zabs (-uZ b0 (zabs n))
43		eqidd	n = -uZ b0 (zabs n) -> b0 (zabs m) = b0 (zabs m)
44		id	n = -uZ b0 (zabs n) -> n = -uZ b0 (zabs n)
45	43, 44	zmuleqd	n = -uZ b0 (zabs n) -> b0 (zabs m) Z n = b0 (zabs m) Z -uZ b0 (zabs n)
46	45	zabseqd	n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m) Z -uZ b0 (zabs n))
47		eqidd	n = -uZ b0 (zabs n) -> zabs m = zabs m
48	44	zabseqd	n = -uZ b0 (zabs n) -> zabs n = zabs (-uZ b0 (zabs n))
49	47, 48	muleqd	n = -uZ b0 (zabs n) -> zabs m * zabs n = zabs m * zabs (-uZ b0 (zabs n))
50	46, 49	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)))
51	42, 50	mpbiri	n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
52	26, 51	ax_mp	n = b0 (zabs n) \/ n = -uZ b0 (zabs n) -> zabs (b0 (zabs m) Z n) = zabs m zabs n
53		zb0orb0	n = b0 (zabs n) \/ n = -uZ b0 (zabs n)
54	52, 53	ax_mp	zabs (b0 (zabs m) Z n) = zabs m zabs n
55	2, 54	ax_mp	zabs (b0 (zabs m)) * zabs n = zabs m * zabs n -> zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n
56		muleq1	zabs (b0 (zabs m)) = zabs m -> zabs (b0 (zabs m)) * zabs n = zabs m * zabs n
57		zabsb0	zabs (b0 (zabs m)) = zabs m
58	56, 57	ax_mp	zabs (b0 (zabs m)) * zabs n = zabs m * zabs n
59	55, 58	ax_mp	zabs (b0 (zabs m) Z n) = zabs (b0 (zabs m)) zabs n
60		id	m = b0 (zabs m) -> m = b0 (zabs m)
61		eqidd	m = b0 (zabs m) -> n = n
62	60, 61	zmuleqd	m = b0 (zabs m) -> m Z n = b0 (zabs m) Z n
63	62	zabseqd	m = b0 (zabs m) -> zabs (m Z n) = zabs (b0 (zabs m) Z n)
64	60	zabseqd	m = b0 (zabs m) -> zabs m = zabs (b0 (zabs m))
65		eqidd	m = b0 (zabs m) -> zabs n = zabs n
66	64, 65	muleqd	m = b0 (zabs m) -> zabs m * zabs n = zabs (b0 (zabs m)) * zabs n
67	63, 66	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)
68	59, 67	mpbiri	m = b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
69	1, 68	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
70		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
71		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))
72		zmulneg1	-uZ b0 (zabs m) Z n = -uZ (b0 (zabs m) Z n)
73	71, 72	ax_mp	zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ (b0 (zabs m) Z n))
74	70, 73	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
75		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
76		zabsneg	zabs (-uZ (b0 (zabs m) Z n)) = zabs (b0 (zabs m) Z n)
77	75, 76	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
78		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)
79		muleq1	zabs (-uZ b0 (zabs m)) = zabs (b0 (zabs m)) -> zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n
80		zabsneg	zabs (-uZ b0 (zabs m)) = zabs (b0 (zabs m))
81	79, 80	ax_mp	zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m)) * zabs n
82	78, 81	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)
83	82, 59	ax_mp	zabs (-uZ b0 (zabs m)) * zabs n = zabs (b0 (zabs m) *Z n)
84	77, 83	ax_mp	zabs (-uZ (b0 (zabs m) Z n)) = zabs (-uZ b0 (zabs m)) zabs n
85	74, 84	ax_mp	zabs (-uZ b0 (zabs m) Z n) = zabs (-uZ b0 (zabs m)) zabs n
86		id	m = -uZ b0 (zabs m) -> m = -uZ b0 (zabs m)
87		eqidd	m = -uZ b0 (zabs m) -> n = n
88	86, 87	zmuleqd	m = -uZ b0 (zabs m) -> m Z n = -uZ b0 (zabs m) Z n
89	88	zabseqd	m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs (-uZ b0 (zabs m) Z n)
90	86	zabseqd	m = -uZ b0 (zabs m) -> zabs m = zabs (-uZ b0 (zabs m))
91		eqidd	m = -uZ b0 (zabs m) -> zabs n = zabs n
92	90, 91	muleqd	m = -uZ b0 (zabs m) -> zabs m * zabs n = zabs (-uZ b0 (zabs m)) * zabs n
93	89, 92	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)
94	85, 93	mpbiri	m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
95	69, 94	ax_mp	m = b0 (zabs m) \/ m = -uZ b0 (zabs m) -> zabs (m Z n) = zabs m zabs n
96		zb0orb0	m = b0 (zabs m) \/ m = -uZ b0 (zabs m)
97	95, 96	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

eqidd

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

18

id

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

19

17, 18

zmuleqd

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

20

19

zabseqd

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

21

eqidd

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

22

18

zabseqd

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

23

21, 22

muleqd

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

24

20, 23

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)))

25

16, 24

mpbiri

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

26

3, 25

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

27

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))

28

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)))

29

zmulneg2

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

30

28, 29

ax_mp

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

31

27, 30

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))

32

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))

33

zabsneg

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

34

32, 33

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))

35

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))

36

muleq2

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

37

zabsneg

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

38

36, 37

ax_mp

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

39

35, 38

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))

40

39, 16

ax_mp

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

41

34, 40

ax_mp

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

42

31, 41

ax_mp

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

43

eqidd

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

44

id

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

45

43, 44

zmuleqd

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

46

45

zabseqd

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

47

eqidd

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

48

44

zabseqd

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

49

47, 48

muleqd

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

50

46, 49

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)))

51

42, 50

mpbiri

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

52

26, 51

ax_mp

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

53

zb0orb0

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

54

52, 53

ax_mp

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

55

2, 54

ax_mp

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

56

muleq1

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

57

zabsb0

zabs (b0 (zabs m)) = zabs m

58

56, 57

ax_mp

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

59

55, 58

ax_mp

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

60

id

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

61

eqidd

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

62

60, 61

zmuleqd

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

63

62

zabseqd

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

64

60

zabseqd

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

65

eqidd

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

66

64, 65

muleqd

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

67

63, 66

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)

68

59, 67

mpbiri

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

69

1, 68

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

70

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

71

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))

72

zmulneg1

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

73

71, 72

ax_mp

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

74

70, 73

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

75

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

76

zabsneg

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

77

75, 76

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

78

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)

79

muleq1

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

80

zabsneg

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

81

79, 80

ax_mp

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

82

78, 81

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)

83

82, 59

ax_mp

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

84

77, 83

ax_mp

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

85

74, 84

ax_mp

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

86

id

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

87

eqidd

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

88

86, 87

zmuleqd

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

89

88

zabseqd

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

90

86

zabseqd

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

91

eqidd

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

92

90, 91

muleqd

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

93

89, 92

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)

94

85, 93

mpbiri

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

95

69, 94

ax_mp

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

96

zb0orb0

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

97

95, 96

ax_mp

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

Theorem zabsmul ≪ | index | src | ≫

Axiom use