Theorem evenodddisj 4516

Description: The even finite cardinals and the odd ones are disjoint. Theorem X.1.36 of [Rosser] p. 529. (Contributed by SF, 22-Jan-2015.)

Assertion

Ref	Expression
evenodddisj	|- ( Evenfin i^i Oddfin ) = (/)

Proof of Theorem evenodddisj

Dummy variables m n x k p q j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfevenfin2 4512	. . . 4 |- Evenfin = {x | E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/))}
2		dfoddfin2 4513	. . . 4 |- Oddfin = {x | E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))}
3	1, 2	ineq12i 3455	. . 3 |- ( Evenfin i^i Oddfin ) = ({x | E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/))} i^i {x | E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))})
4		inab 3522	. . 3 |- ({x | E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/))} i^i {x | E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))}) = {x | (E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) /\ E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))}
5	3, 4	eqtri 2373	. 2 |- ( Evenfin i^i Oddfin ) = {x | (E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) /\ E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))}
6		evenodddisjlem1 4515	. . . . . . . . 9 |- {j | ((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)))} e. _V
7		addceq12 4385	. . . . . . . . . . . . 13 |- ((j = 0c /\ j = 0c) -> (j +o j) = (0c +o 0c))
8	7	anidms 626	. . . . . . . . . . . 12 |- (j = 0c -> (j +o j) = (0c +o 0c))
9		addcid2 4407	. . . . . . . . . . . 12 |- (0c +o 0c) = 0c
10	8, 9	syl6eq 2401	. . . . . . . . . . 11 |- (j = 0c -> (j +o j) = 0c)
11	10	neeq1d 2529	. . . . . . . . . 10 |- (j = 0c -> ((j +o j) =/= (/) <-> 0c =/= (/)))
12	10	neeq1d 2529	. . . . . . . . . . . 12 |- (j = 0c -> ((j +o j) =/= ((n +o n) +o 1c) <-> 0c =/= ((n +o n) +o 1c)))
13	12	imbi2d 307	. . . . . . . . . . 11 |- (j = 0c -> ((((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> (((n +o n) +o 1c) =/= (/) -> 0c =/= ((n +o n) +o 1c))))
14	13	ralbidv 2634	. . . . . . . . . 10 |- (j = 0c -> (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> 0c =/= ((n +o n) +o 1c))))
15	11, 14	imbi12d 311	. . . . . . . . 9 |- (j = 0c -> (((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c))) <-> (0c =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> 0c =/= ((n +o n) +o 1c)))))
16		addceq12 4385	. . . . . . . . . . . 12 |- ((j = m /\ j = m) -> (j +o j) = (m +o m))
17	16	anidms 626	. . . . . . . . . . 11 |- (j = m -> (j +o j) = (m +o m))
18	17	neeq1d 2529	. . . . . . . . . 10 |- (j = m -> ((j +o j) =/= (/) <-> (m +o m) =/= (/)))
19	17	neeq1d 2529	. . . . . . . . . . . . 13 |- (j = m -> ((j +o j) =/= ((n +o n) +o 1c) <-> (m +o m) =/= ((n +o n) +o 1c)))
20	19	imbi2d 307	. . . . . . . . . . . 12 |- (j = m -> ((((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> (((n +o n) +o 1c) =/= (/) -> (m +o m) =/= ((n +o n) +o 1c))))
21	20	ralbidv 2634	. . . . . . . . . . 11 |- (j = m -> (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (m +o m) =/= ((n +o n) +o 1c))))
22		addceq12 4385	. . . . . . . . . . . . . . . 16 |- ((n = p /\ n = p) -> (n +o n) = (p +o p))
23	22	anidms 626	. . . . . . . . . . . . . . 15 |- (n = p -> (n +o n) = (p +o p))
24	23	addceq1d 4389	. . . . . . . . . . . . . 14 |- (n = p -> ((n +o n) +o 1c) = ((p +o p) +o 1c))
25	24	neeq1d 2529	. . . . . . . . . . . . 13 |- (n = p -> (((n +o n) +o 1c) =/= (/) <-> ((p +o p) +o 1c) =/= (/)))
26	24	neeq2d 2530	. . . . . . . . . . . . 13 |- (n = p -> ((m +o m) =/= ((n +o n) +o 1c) <-> (m +o m) =/= ((p +o p) +o 1c)))
27	25, 26	imbi12d 311	. . . . . . . . . . . 12 |- (n = p -> ((((n +o n) +o 1c) =/= (/) -> (m +o m) =/= ((n +o n) +o 1c)) <-> (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))))
28	27	cbvralv 2835	. . . . . . . . . . 11 |- (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (m +o m) =/= ((n +o n) +o 1c)) <-> A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)))
29	21, 28	syl6bb 252	. . . . . . . . . 10 |- (j = m -> (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))))
30	18, 29	imbi12d 311	. . . . . . . . 9 |- (j = m -> (((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c))) <-> ((m +o m) =/= (/) -> A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)))))
31		addceq12 4385	. . . . . . . . . . . . 13 |- ((j = (m +o 1c) /\ j = (m +o 1c)) -> (j +o j) = ((m +o 1c) +o (m +o 1c)))
32	31	anidms 626	. . . . . . . . . . . 12 |- (j = (m +o 1c) -> (j +o j) = ((m +o 1c) +o (m +o 1c)))
33		addcass 4415	. . . . . . . . . . . . 13 |- (((m +o 1c) +o m) +o 1c) = ((m +o 1c) +o (m +o 1c))
34		addc32 4416	. . . . . . . . . . . . . 14 |- ((m +o 1c) +o m) = ((m +o m) +o 1c)
35	34	addceq1i 4386	. . . . . . . . . . . . 13 |- (((m +o 1c) +o m) +o 1c) = (((m +o m) +o 1c) +o 1c)
36	33, 35	eqtr3i 2375	. . . . . . . . . . . 12 |- ((m +o 1c) +o (m +o 1c)) = (((m +o m) +o 1c) +o 1c)
37	32, 36	syl6eq 2401	. . . . . . . . . . 11 |- (j = (m +o 1c) -> (j +o j) = (((m +o m) +o 1c) +o 1c))
38	37	neeq1d 2529	. . . . . . . . . 10 |- (j = (m +o 1c) -> ((j +o j) =/= (/) <-> (((m +o m) +o 1c) +o 1c) =/= (/)))
39	37	neeq1d 2529	. . . . . . . . . . . 12 |- (j = (m +o 1c) -> ((j +o j) =/= ((n +o n) +o 1c) <-> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))
40	39	imbi2d 307	. . . . . . . . . . 11 |- (j = (m +o 1c) -> ((((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c))))
41	40	ralbidv 2634	. . . . . . . . . 10 |- (j = (m +o 1c) -> (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c))))
42	38, 41	imbi12d 311	. . . . . . . . 9 |- (j = (m +o 1c) -> (((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c))) <-> ((((m +o m) +o 1c) +o 1c) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))))
43		addceq12 4385	. . . . . . . . . . . 12 |- ((j = k /\ j = k) -> (j +o j) = (k +o k))
44	43	anidms 626	. . . . . . . . . . 11 |- (j = k -> (j +o j) = (k +o k))
45	44	neeq1d 2529	. . . . . . . . . 10 |- (j = k -> ((j +o j) =/= (/) <-> (k +o k) =/= (/)))
46	44	neeq1d 2529	. . . . . . . . . . . 12 |- (j = k -> ((j +o j) =/= ((n +o n) +o 1c) <-> (k +o k) =/= ((n +o n) +o 1c)))
47	46	imbi2d 307	. . . . . . . . . . 11 |- (j = k -> ((((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> (((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c))))
48	47	ralbidv 2634	. . . . . . . . . 10 |- (j = k -> (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c)) <-> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c))))
49	45, 48	imbi12d 311	. . . . . . . . 9 |- (j = k -> (((j +o j) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (j +o j) =/= ((n +o n) +o 1c))) <-> ((k +o k) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c)))))
50		0cnsuc 4401	. . . . . . . . . . . . 13 |- ((n +o n) +o 1c) =/= 0c
51	50	necomi 2598	. . . . . . . . . . . 12 |- 0c =/= ((n +o n) +o 1c)
52	51	a1i 10	. . . . . . . . . . 11 |- (((n +o n) +o 1c) =/= (/) -> 0c =/= ((n +o n) +o 1c))
53	52	rgenw 2681	. . . . . . . . . 10 |- A.n e. Nn (((n +o n) +o 1c) =/= (/) -> 0c =/= ((n +o n) +o 1c))
54	53	a1i 10	. . . . . . . . 9 |- (0c =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> 0c =/= ((n +o n) +o 1c)))
55		addcass 4415	. . . . . . . . . . . . . . 15 |- (((m +o m) +o 1c) +o 1c) = ((m +o m) +o (1c +o 1c))
56	55	neeq1i 2526	. . . . . . . . . . . . . 14 |- ((((m +o m) +o 1c) +o 1c) =/= (/) <-> ((m +o m) +o (1c +o 1c)) =/= (/))
57		addcnnul 4453	. . . . . . . . . . . . . . 15 |- (((m +o m) +o (1c +o 1c)) =/= (/) -> ((m +o m) =/= (/) /\ (1c +o 1c) =/= (/)))
58	57	simpld 445	. . . . . . . . . . . . . 14 |- (((m +o m) +o (1c +o 1c)) =/= (/) -> (m +o m) =/= (/))
59	56, 58	sylbi 187	. . . . . . . . . . . . 13 |- ((((m +o m) +o 1c) +o 1c) =/= (/) -> (m +o m) =/= (/))
60	59	adantl 452	. . . . . . . . . . . 12 |- ((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) -> (m +o m) =/= (/))
61		simprl 732	. . . . . . . . . . . . . . . . . 18 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> n e. Nn )
62		nnc0suc 4412	. . . . . . . . . . . . . . . . . 18 |- (n e. Nn <-> (n = 0c \/ E.q e. Nn n = (q +o 1c)))
63	61, 62	sylib 188	. . . . . . . . . . . . . . . . 17 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> (n = 0c \/ E.q e. Nn n = (q +o 1c)))
64		0cnsuc 4401	. . . . . . . . . . . . . . . . . . . 20 |- ((m +o m) +o 1c) =/= 0c
65		addceq12 4385	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n = 0c /\ n = 0c) -> (n +o n) = (0c +o 0c))
66	65	anidms 626	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = 0c -> (n +o n) = (0c +o 0c))
67	66, 9	syl6eq 2401	. . . . . . . . . . . . . . . . . . . . 21 |- (n = 0c -> (n +o n) = 0c)
68	67	neeq2d 2530	. . . . . . . . . . . . . . . . . . . 20 |- (n = 0c -> (((m +o m) +o 1c) =/= (n +o n) <-> ((m +o m) +o 1c) =/= 0c))
69	64, 68	mpbiri 224	. . . . . . . . . . . . . . . . . . 19 |- (n = 0c -> ((m +o m) +o 1c) =/= (n +o n))
70	69	a1i 10	. . . . . . . . . . . . . . . . . 18 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> (n = 0c -> ((m +o m) +o 1c) =/= (n +o n)))
71		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn ) -> q e. Nn )
72	71	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> q e. Nn )
73		addceq12 4385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((p = q /\ p = q) -> (p +o p) = (q +o q))
74	73	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (p = q -> (p +o p) = (q +o q))
75	74	addceq1d 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (p = q -> ((p +o p) +o 1c) = ((q +o q) +o 1c))
76	75	neeq1d 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (p = q -> (((p +o p) +o 1c) =/= (/) <-> ((q +o q) +o 1c) =/= (/)))
77	75	neeq2d 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (p = q -> ((m +o m) =/= ((p +o p) +o 1c) <-> (m +o m) =/= ((q +o q) +o 1c)))
78	76, 77	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (p = q -> ((((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) <-> (((q +o q) +o 1c) =/= (/) -> (m +o m) =/= ((q +o q) +o 1c))))
79	78	rspcv 2951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (q e. Nn -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> (((q +o q) +o 1c) =/= (/) -> (m +o m) =/= ((q +o q) +o 1c))))
80	72, 79	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> (((q +o q) +o 1c) =/= (/) -> (m +o m) =/= ((q +o q) +o 1c))))
81		addc4 4417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((q +o 1c) +o (q +o 1c)) = ((q +o q) +o (1c +o 1c))
82	81	addceq1i 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((q +o 1c) +o (q +o 1c)) +o 1c) = (((q +o q) +o (1c +o 1c)) +o 1c)
83		addc32 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((q +o q) +o (1c +o 1c)) +o 1c) = (((q +o q) +o 1c) +o (1c +o 1c))
84	82, 83	eqtri 2373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((q +o 1c) +o (q +o 1c)) +o 1c) = (((q +o q) +o 1c) +o (1c +o 1c))
85	84	neeq1i 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) <-> (((q +o q) +o 1c) +o (1c +o 1c)) =/= (/))
86		addcnnul 4453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((q +o q) +o 1c) +o (1c +o 1c)) =/= (/) -> (((q +o q) +o 1c) =/= (/) /\ (1c +o 1c) =/= (/)))
87	86	simpld 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((q +o q) +o 1c) +o (1c +o 1c)) =/= (/) -> ((q +o q) +o 1c) =/= (/))
88	85, 87	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) -> ((q +o q) +o 1c) =/= (/))
89	88	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn ) -> ((q +o q) +o 1c) =/= (/))
90	89	adantl 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> ((q +o q) +o 1c) =/= (/))
91		addc32 4416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((q +o q) +o 1c) = ((q +o 1c) +o q)
92	91	addceq1i 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((q +o q) +o 1c) +o 1c) = (((q +o 1c) +o q) +o 1c)
93		addcass 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((q +o 1c) +o q) +o 1c) = ((q +o 1c) +o (q +o 1c))
94	92, 93	eqtri 2373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((q +o q) +o 1c) +o 1c) = ((q +o 1c) +o (q +o 1c))
95	94	eqeq2i 2363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c) <-> ((m +o m) +o 1c) = ((q +o 1c) +o (q +o 1c)))
96		simplll 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> m e. Nn )
97		nncaddccl 4419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((m e. Nn /\ m e. Nn ) -> (m +o m) e. Nn )
98	97	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (m e. Nn -> (m +o m) e. Nn )
99	96, 98	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> (m +o m) e. Nn )
100		simplrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> q e. Nn )
101		nncaddccl 4419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((q e. Nn /\ q e. Nn ) -> (q +o q) e. Nn )
102	101	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (q e. Nn -> (q +o q) e. Nn )
103		peano2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((q +o q) e. Nn -> ((q +o q) +o 1c) e. Nn )
104	100, 102, 103	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> ((q +o q) +o 1c) e. Nn )
105		simpr 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c))
106		simpllr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> (((m +o m) +o 1c) +o 1c) =/= (/))
107		addcnnul 4453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((m +o m) +o 1c) +o 1c) =/= (/) -> (((m +o m) +o 1c) =/= (/) /\ 1c =/= (/)))
108	107	simpld 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((m +o m) +o 1c) +o 1c) =/= (/) -> ((m +o m) +o 1c) =/= (/))
109	106, 108	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> ((m +o m) +o 1c) =/= (/))
110		prepeano4 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((m +o m) e. Nn /\ ((q +o q) +o 1c) e. Nn ) /\ (((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c) /\ ((m +o m) +o 1c) =/= (/))) -> (m +o m) = ((q +o q) +o 1c))
111	99, 104, 105, 109, 110	syl22anc 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) /\ ((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c)) -> (m +o m) = ((q +o q) +o 1c))
112	111	ex 423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> (((m +o m) +o 1c) = (((q +o q) +o 1c) +o 1c) -> (m +o m) = ((q +o q) +o 1c)))
113	95, 112	syl5bir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> (((m +o m) +o 1c) = ((q +o 1c) +o (q +o 1c)) -> (m +o m) = ((q +o q) +o 1c)))
114	113	necon3d 2554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> ((m +o m) =/= ((q +o q) +o 1c) -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))
115	90, 114	embantd 50	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> ((((q +o q) +o 1c) =/= (/) -> (m +o m) =/= ((q +o q) +o 1c)) -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))
116	80, 115	syld 40	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) /\ q e. Nn )) -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))
117	116	expr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/)) -> (q e. Nn -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c)))))
118	117	com23 72	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/)) -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> (q e. Nn -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c)))))
119	118	ex 423	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) -> ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> (q e. Nn -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))))
120	119	com23 72	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> ((((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/) -> (q e. Nn -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))))
121	120	imp31 421	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/)) -> (q e. Nn -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))
122	121	com12 27	. . . . . . . . . . . . . . . . . . . . . 22 |- (q e. Nn -> ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/)) -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))
123		addceq12 4385	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((n = (q +o 1c) /\ n = (q +o 1c)) -> (n +o n) = ((q +o 1c) +o (q +o 1c)))
124	123	anidms 626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (n = (q +o 1c) -> (n +o n) = ((q +o 1c) +o (q +o 1c)))
125	124	addceq1d 4389	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (n = (q +o 1c) -> ((n +o n) +o 1c) = (((q +o 1c) +o (q +o 1c)) +o 1c))
126	125	neeq1d 2529	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n = (q +o 1c) -> (((n +o n) +o 1c) =/= (/) <-> (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/)))
127	126	anbi2d 684	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = (q +o 1c) -> ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ ((n +o n) +o 1c) =/= (/)) <-> (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/))))
128	124	neeq2d 2530	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n = (q +o 1c) -> (((m +o m) +o 1c) =/= (n +o n) <-> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c))))
129	127, 128	imbi12d 311	. . . . . . . . . . . . . . . . . . . . . 22 |- (n = (q +o 1c) -> (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ ((n +o n) +o 1c) =/= (/)) -> ((m +o m) +o 1c) =/= (n +o n)) <-> ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (((q +o 1c) +o (q +o 1c)) +o 1c) =/= (/)) -> ((m +o m) +o 1c) =/= ((q +o 1c) +o (q +o 1c)))))
130	122, 129	syl5ibrcom 213	. . . . . . . . . . . . . . . . . . . . 21 |- (q e. Nn -> (n = (q +o 1c) -> ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ ((n +o n) +o 1c) =/= (/)) -> ((m +o m) +o 1c) =/= (n +o n))))
131	130	rexlimiv 2732	. . . . . . . . . . . . . . . . . . . 20 |- (E.q e. Nn n = (q +o 1c) -> ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ ((n +o n) +o 1c) =/= (/)) -> ((m +o m) +o 1c) =/= (n +o n)))
132	131	com12 27	. . . . . . . . . . . . . . . . . . 19 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ ((n +o n) +o 1c) =/= (/)) -> (E.q e. Nn n = (q +o 1c) -> ((m +o m) +o 1c) =/= (n +o n)))
133	132	adantrl 696	. . . . . . . . . . . . . . . . . 18 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> (E.q e. Nn n = (q +o 1c) -> ((m +o m) +o 1c) =/= (n +o n)))
134	70, 133	jaod 369	. . . . . . . . . . . . . . . . 17 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> ((n = 0c \/ E.q e. Nn n = (q +o 1c)) -> ((m +o m) +o 1c) =/= (n +o n)))
135	63, 134	mpd 14	. . . . . . . . . . . . . . . 16 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> ((m +o m) +o 1c) =/= (n +o n))
136		simplll 734	. . . . . . . . . . . . . . . . . . . . 21 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> m e. Nn )
137	136	adantr 451	. . . . . . . . . . . . . . . . . . . 20 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> m e. Nn )
138		peano2 4403	. . . . . . . . . . . . . . . . . . . 20 |- ((m +o m) e. Nn -> ((m +o m) +o 1c) e. Nn )
139	137, 98, 138	3syl 18	. . . . . . . . . . . . . . . . . . 19 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> ((m +o m) +o 1c) e. Nn )
140		simplrl 736	. . . . . . . . . . . . . . . . . . . 20 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> n e. Nn )
141		nncaddccl 4419	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. Nn /\ n e. Nn ) -> (n +o n) e. Nn )
142	141	anidms 626	. . . . . . . . . . . . . . . . . . . 20 |- (n e. Nn -> (n +o n) e. Nn )
143	140, 142	syl 15	. . . . . . . . . . . . . . . . . . 19 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> (n +o n) e. Nn )
144		simpr 447	. . . . . . . . . . . . . . . . . . 19 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c))
145		simpllr 735	. . . . . . . . . . . . . . . . . . . 20 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> (((m +o m) +o 1c) +o 1c) =/= (/))
146	145	adantr 451	. . . . . . . . . . . . . . . . . . 19 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> (((m +o m) +o 1c) +o 1c) =/= (/))
147		prepeano4 4451	. . . . . . . . . . . . . . . . . . 19 |- (((((m +o m) +o 1c) e. Nn /\ (n +o n) e. Nn ) /\ ((((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c) /\ (((m +o m) +o 1c) +o 1c) =/= (/))) -> ((m +o m) +o 1c) = (n +o n))
148	139, 143, 144, 146, 147	syl22anc 1183	. . . . . . . . . . . . . . . . . 18 |- (((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) /\ (((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c)) -> ((m +o m) +o 1c) = (n +o n))
149	148	ex 423	. . . . . . . . . . . . . . . . 17 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> ((((m +o m) +o 1c) +o 1c) = ((n +o n) +o 1c) -> ((m +o m) +o 1c) = (n +o n)))
150	149	necon3d 2554	. . . . . . . . . . . . . . . 16 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> (((m +o m) +o 1c) =/= (n +o n) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))
151	135, 150	mpd 14	. . . . . . . . . . . . . . 15 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ (n e. Nn /\ ((n +o n) +o 1c) =/= (/))) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c))
152	151	expr 598	. . . . . . . . . . . . . 14 |- ((((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) /\ n e. Nn ) -> (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))
153	152	ralrimiva 2697	. . . . . . . . . . . . 13 |- (((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) /\ A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))
154	153	ex 423	. . . . . . . . . . . 12 |- ((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) -> (A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c)) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c))))
155	60, 154	embantd 50	. . . . . . . . . . 11 |- ((m e. Nn /\ (((m +o m) +o 1c) +o 1c) =/= (/)) -> (((m +o m) =/= (/) -> A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c))))
156	155	ex 423	. . . . . . . . . 10 |- (m e. Nn -> ((((m +o m) +o 1c) +o 1c) =/= (/) -> (((m +o m) =/= (/) -> A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))))
157	156	com23 72	. . . . . . . . 9 |- (m e. Nn -> (((m +o m) =/= (/) -> A.p e. Nn (((p +o p) +o 1c) =/= (/) -> (m +o m) =/= ((p +o p) +o 1c))) -> ((((m +o m) +o 1c) +o 1c) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (((m +o m) +o 1c) +o 1c) =/= ((n +o n) +o 1c)))))
158	6, 15, 30, 42, 49, 54, 157	finds 4411	. . . . . . . 8 |- (k e. Nn -> ((k +o k) =/= (/) -> A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c))))
159		df-ne 2518	. . . . . . . . . . . . 13 |- ((k +o k) =/= ((n +o n) +o 1c) <-> -. (k +o k) = ((n +o n) +o 1c))
160	159	imbi2i 303	. . . . . . . . . . . 12 |- ((((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c)) <-> (((n +o n) +o 1c) =/= (/) -> -. (k +o k) = ((n +o n) +o 1c)))
161		con2b 324	. . . . . . . . . . . 12 |- ((((n +o n) +o 1c) =/= (/) -> -. (k +o k) = ((n +o n) +o 1c)) <-> ((k +o k) = ((n +o n) +o 1c) -> -. ((n +o n) +o 1c) =/= (/)))
162	160, 161	bitri 240	. . . . . . . . . . 11 |- ((((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c)) <-> ((k +o k) = ((n +o n) +o 1c) -> -. ((n +o n) +o 1c) =/= (/)))
163		imnan 411	. . . . . . . . . . 11 |- (((k +o k) = ((n +o n) +o 1c) -> -. ((n +o n) +o 1c) =/= (/)) <-> -. ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
164	162, 163	bitri 240	. . . . . . . . . 10 |- ((((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c)) <-> -. ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
165	164	ralbii 2638	. . . . . . . . 9 |- (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c)) <-> A.n e. Nn -. ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
166		ralnex 2624	. . . . . . . . 9 |- (A.n e. Nn -. ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)) <-> -. E.n e. Nn ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
167	165, 166	bitri 240	. . . . . . . 8 |- (A.n e. Nn (((n +o n) +o 1c) =/= (/) -> (k +o k) =/= ((n +o n) +o 1c)) <-> -. E.n e. Nn ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
168	158, 167	syl6ib 217	. . . . . . 7 |- (k e. Nn -> ((k +o k) =/= (/) -> -. E.n e. Nn ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))))
169		eqeq1 2359	. . . . . . . . . . 11 |- (x = (k +o k) -> (x = ((n +o n) +o 1c) <-> (k +o k) = ((n +o n) +o 1c)))
170	169	anbi1d 685	. . . . . . . . . 10 |- (x = (k +o k) -> ((x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)) <-> ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))))
171	170	rexbidv 2635	. . . . . . . . 9 |- (x = (k +o k) -> (E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)) <-> E.n e. Nn ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))))
172	171	notbid 285	. . . . . . . 8 |- (x = (k +o k) -> (-. E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)) <-> -. E.n e. Nn ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))))
173	172	imbi2d 307	. . . . . . 7 |- (x = (k +o k) -> (((k +o k) =/= (/) -> -. E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))) <-> ((k +o k) =/= (/) -> -. E.n e. Nn ((k +o k) = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))))
174	168, 173	syl5ibrcom 213	. . . . . 6 |- (k e. Nn -> (x = (k +o k) -> ((k +o k) =/= (/) -> -. E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))))
175	174	imp3a 420	. . . . 5 |- (k e. Nn -> ((x = (k +o k) /\ (k +o k) =/= (/)) -> -. E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))))
176	175	rexlimiv 2732	. . . 4 |- (E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) -> -. E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
177		imnan 411	. . . 4 |- ((E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) -> -. E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))) <-> -. (E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) /\ E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/))))
178	176, 177	mpbi 199	. . 3 |- -. (E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) /\ E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))
179	178	abf 3584	. 2 |- {x | (E.k e. Nn (x = (k +o k) /\ (k +o k) =/= (/)) /\ E.n e. Nn (x = ((n +o n) +o 1c) /\ ((n +o n) +o 1c) =/= (/)))} = (/)
180	5, 179	eqtri 2373	1 |- ( Evenfin i^i Oddfin ) = (/)

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357   /\ wa 358   = wceq 1642   e. wcel 1710  {cab 2339   =/= wne 2516  A.wral 2614  E.wrex 2615   i^i cin 3208  (/)c0 3550  1_cc1c 4134   Nn cnnc 4373  0_cc0c 4374   +o cplc 4375   Even_fin cevenfin 4436   Odd_fin coddfin 4437

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379  df-evenfin 4444  df-oddfin 4445

This theorem is referenced by:  vinf  4555