NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  evenodddisj GIF version

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 ( EvenfinOddfin ) =

Proof of Theorem evenodddisj
Dummy variables m n x k p q j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfevenfin2 4512 . . . 4 Evenfin = {x k Nn (x = (k +c k) (k +c k) ≠ )}
2 dfoddfin2 4513 . . . 4 Oddfin = {x n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )}
31, 2ineq12i 3455 . . 3 ( EvenfinOddfin ) = ({x k Nn (x = (k +c k) (k +c k) ≠ )} ∩ {x n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )})
4 inab 3522 . . 3 ({x k Nn (x = (k +c k) (k +c k) ≠ )} ∩ {x n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )}) = {x (k Nn (x = (k +c k) (k +c k) ≠ ) n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))}
53, 4eqtri 2373 . 2 ( EvenfinOddfin ) = {x (k Nn (x = (k +c k) (k +c k) ≠ ) n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))}
6 evenodddisjlem1 4515 . . . . . . . . 9 {j ((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)))} V
7 addceq12 4385 . . . . . . . . . . . . 13 ((j = 0c j = 0c) → (j +c j) = (0c +c 0c))
87anidms 626 . . . . . . . . . . . 12 (j = 0c → (j +c j) = (0c +c 0c))
9 addcid2 4407 . . . . . . . . . . . 12 (0c +c 0c) = 0c
108, 9syl6eq 2401 . . . . . . . . . . 11 (j = 0c → (j +c j) = 0c)
1110neeq1d 2529 . . . . . . . . . 10 (j = 0c → ((j +c j) ≠ ↔ 0c))
1210neeq1d 2529 . . . . . . . . . . . 12 (j = 0c → ((j +c j) ≠ ((n +c n) +c 1c) ↔ 0c ≠ ((n +c n) +c 1c)))
1312imbi2d 307 . . . . . . . . . . 11 (j = 0c → ((((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ → 0c ≠ ((n +c n) +c 1c))))
1413ralbidv 2634 . . . . . . . . . 10 (j = 0c → (n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ n Nn (((n +c n) +c 1c) ≠ → 0c ≠ ((n +c n) +c 1c))))
1511, 14imbi12d 311 . . . . . . . . 9 (j = 0c → (((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ (0cn Nn (((n +c n) +c 1c) ≠ → 0c ≠ ((n +c n) +c 1c)))))
16 addceq12 4385 . . . . . . . . . . . 12 ((j = m j = m) → (j +c j) = (m +c m))
1716anidms 626 . . . . . . . . . . 11 (j = m → (j +c j) = (m +c m))
1817neeq1d 2529 . . . . . . . . . 10 (j = m → ((j +c j) ≠ ↔ (m +c m) ≠ ))
1917neeq1d 2529 . . . . . . . . . . . . 13 (j = m → ((j +c j) ≠ ((n +c n) +c 1c) ↔ (m +c m) ≠ ((n +c n) +c 1c)))
2019imbi2d 307 . . . . . . . . . . . 12 (j = m → ((((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ → (m +c m) ≠ ((n +c n) +c 1c))))
2120ralbidv 2634 . . . . . . . . . . 11 (j = m → (n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ n Nn (((n +c n) +c 1c) ≠ → (m +c m) ≠ ((n +c n) +c 1c))))
22 addceq12 4385 . . . . . . . . . . . . . . . 16 ((n = p n = p) → (n +c n) = (p +c p))
2322anidms 626 . . . . . . . . . . . . . . 15 (n = p → (n +c n) = (p +c p))
2423addceq1d 4389 . . . . . . . . . . . . . 14 (n = p → ((n +c n) +c 1c) = ((p +c p) +c 1c))
2524neeq1d 2529 . . . . . . . . . . . . 13 (n = p → (((n +c n) +c 1c) ≠ ↔ ((p +c p) +c 1c) ≠ ))
2624neeq2d 2530 . . . . . . . . . . . . 13 (n = p → ((m +c m) ≠ ((n +c n) +c 1c) ↔ (m +c m) ≠ ((p +c p) +c 1c)))
2725, 26imbi12d 311 . . . . . . . . . . . 12 (n = p → ((((n +c n) +c 1c) ≠ → (m +c m) ≠ ((n +c n) +c 1c)) ↔ (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))))
2827cbvralv 2835 . . . . . . . . . . 11 (n Nn (((n +c n) +c 1c) ≠ → (m +c m) ≠ ((n +c n) +c 1c)) ↔ p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)))
2921, 28syl6bb 252 . . . . . . . . . 10 (j = m → (n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))))
3018, 29imbi12d 311 . . . . . . . . 9 (j = m → (((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ ((m +c m) ≠ p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)))))
31 addceq12 4385 . . . . . . . . . . . . 13 ((j = (m +c 1c) j = (m +c 1c)) → (j +c j) = ((m +c 1c) +c (m +c 1c)))
3231anidms 626 . . . . . . . . . . . 12 (j = (m +c 1c) → (j +c j) = ((m +c 1c) +c (m +c 1c)))
33 addcass 4415 . . . . . . . . . . . . 13 (((m +c 1c) +c m) +c 1c) = ((m +c 1c) +c (m +c 1c))
34 addc32 4416 . . . . . . . . . . . . . 14 ((m +c 1c) +c m) = ((m +c m) +c 1c)
3534addceq1i 4386 . . . . . . . . . . . . 13 (((m +c 1c) +c m) +c 1c) = (((m +c m) +c 1c) +c 1c)
3633, 35eqtr3i 2375 . . . . . . . . . . . 12 ((m +c 1c) +c (m +c 1c)) = (((m +c m) +c 1c) +c 1c)
3732, 36syl6eq 2401 . . . . . . . . . . 11 (j = (m +c 1c) → (j +c j) = (((m +c m) +c 1c) +c 1c))
3837neeq1d 2529 . . . . . . . . . 10 (j = (m +c 1c) → ((j +c j) ≠ ↔ (((m +c m) +c 1c) +c 1c) ≠ ))
3937neeq1d 2529 . . . . . . . . . . . 12 (j = (m +c 1c) → ((j +c j) ≠ ((n +c n) +c 1c) ↔ (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
4039imbi2d 307 . . . . . . . . . . 11 (j = (m +c 1c) → ((((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
4140ralbidv 2634 . . . . . . . . . 10 (j = (m +c 1c) → (n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
4238, 41imbi12d 311 . . . . . . . . 9 (j = (m +c 1c) → (((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ ((((m +c m) +c 1c) +c 1c) ≠ n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))))
43 addceq12 4385 . . . . . . . . . . . 12 ((j = k j = k) → (j +c j) = (k +c k))
4443anidms 626 . . . . . . . . . . 11 (j = k → (j +c j) = (k +c k))
4544neeq1d 2529 . . . . . . . . . 10 (j = k → ((j +c j) ≠ ↔ (k +c k) ≠ ))
4644neeq1d 2529 . . . . . . . . . . . 12 (j = k → ((j +c j) ≠ ((n +c n) +c 1c) ↔ (k +c k) ≠ ((n +c n) +c 1c)))
4746imbi2d 307 . . . . . . . . . . 11 (j = k → ((((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c))))
4847ralbidv 2634 . . . . . . . . . 10 (j = k → (n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)) ↔ n Nn (((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c))))
4945, 48imbi12d 311 . . . . . . . . 9 (j = k → (((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c))) ↔ ((k +c k) ≠ n Nn (((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c)))))
50 0cnsuc 4401 . . . . . . . . . . . . 13 ((n +c n) +c 1c) ≠ 0c
5150necomi 2598 . . . . . . . . . . . 12 0c ≠ ((n +c n) +c 1c)
5251a1i 10 . . . . . . . . . . 11 (((n +c n) +c 1c) ≠ → 0c ≠ ((n +c n) +c 1c))
5352rgenw 2681 . . . . . . . . . 10 n Nn (((n +c n) +c 1c) ≠ → 0c ≠ ((n +c n) +c 1c))
5453a1i 10 . . . . . . . . 9 (0cn Nn (((n +c n) +c 1c) ≠ → 0c ≠ ((n +c n) +c 1c)))
55 addcass 4415 . . . . . . . . . . . . . . 15 (((m +c m) +c 1c) +c 1c) = ((m +c m) +c (1c +c 1c))
5655neeq1i 2526 . . . . . . . . . . . . . 14 ((((m +c m) +c 1c) +c 1c) ≠ ↔ ((m +c m) +c (1c +c 1c)) ≠ )
57 addcnnul 4453 . . . . . . . . . . . . . . 15 (((m +c m) +c (1c +c 1c)) ≠ → ((m +c m) ≠ (1c +c 1c) ≠ ))
5857simpld 445 . . . . . . . . . . . . . 14 (((m +c m) +c (1c +c 1c)) ≠ → (m +c m) ≠ )
5956, 58sylbi 187 . . . . . . . . . . . . 13 ((((m +c m) +c 1c) +c 1c) ≠ → (m +c m) ≠ )
6059adantl 452 . . . . . . . . . . . 12 ((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) → (m +c m) ≠ )
61 simprl 732 . . . . . . . . . . . . . . . . . 18 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → n Nn )
62 nnc0suc 4412 . . . . . . . . . . . . . . . . . 18 (n Nn ↔ (n = 0c q Nn n = (q +c 1c)))
6361, 62sylib 188 . . . . . . . . . . . . . . . . 17 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → (n = 0c q Nn n = (q +c 1c)))
64 0cnsuc 4401 . . . . . . . . . . . . . . . . . . . 20 ((m +c m) +c 1c) ≠ 0c
65 addceq12 4385 . . . . . . . . . . . . . . . . . . . . . . 23 ((n = 0c n = 0c) → (n +c n) = (0c +c 0c))
6665anidms 626 . . . . . . . . . . . . . . . . . . . . . 22 (n = 0c → (n +c n) = (0c +c 0c))
6766, 9syl6eq 2401 . . . . . . . . . . . . . . . . . . . . 21 (n = 0c → (n +c n) = 0c)
6867neeq2d 2530 . . . . . . . . . . . . . . . . . . . 20 (n = 0c → (((m +c m) +c 1c) ≠ (n +c n) ↔ ((m +c m) +c 1c) ≠ 0c))
6964, 68mpbiri 224 . . . . . . . . . . . . . . . . . . 19 (n = 0c → ((m +c m) +c 1c) ≠ (n +c n))
7069a1i 10 . . . . . . . . . . . . . . . . . 18 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → (n = 0c → ((m +c m) +c 1c) ≠ (n +c n)))
71 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn ) → q Nn )
7271adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → q Nn )
73 addceq12 4385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((p = q p = q) → (p +c p) = (q +c q))
7473anidms 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (p = q → (p +c p) = (q +c q))
7574addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (p = q → ((p +c p) +c 1c) = ((q +c q) +c 1c))
7675neeq1d 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (p = q → (((p +c p) +c 1c) ≠ ↔ ((q +c q) +c 1c) ≠ ))
7775neeq2d 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (p = q → ((m +c m) ≠ ((p +c p) +c 1c) ↔ (m +c m) ≠ ((q +c q) +c 1c)))
7876, 77imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (p = q → ((((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) ↔ (((q +c q) +c 1c) ≠ → (m +c m) ≠ ((q +c q) +c 1c))))
7978rspcv 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (q Nn → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → (((q +c q) +c 1c) ≠ → (m +c m) ≠ ((q +c q) +c 1c))))
8072, 79syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → (((q +c q) +c 1c) ≠ → (m +c m) ≠ ((q +c q) +c 1c))))
81 addc4 4417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((q +c 1c) +c (q +c 1c)) = ((q +c q) +c (1c +c 1c))
8281addceq1i 4386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((q +c 1c) +c (q +c 1c)) +c 1c) = (((q +c q) +c (1c +c 1c)) +c 1c)
83 addc32 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((q +c q) +c (1c +c 1c)) +c 1c) = (((q +c q) +c 1c) +c (1c +c 1c))
8482, 83eqtri 2373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((q +c 1c) +c (q +c 1c)) +c 1c) = (((q +c q) +c 1c) +c (1c +c 1c))
8584neeq1i 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ↔ (((q +c q) +c 1c) +c (1c +c 1c)) ≠ )
86 addcnnul 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((q +c q) +c 1c) +c (1c +c 1c)) ≠ → (((q +c q) +c 1c) ≠ (1c +c 1c) ≠ ))
8786simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((q +c q) +c 1c) +c (1c +c 1c)) ≠ → ((q +c q) +c 1c) ≠ )
8885, 87sylbi 187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ → ((q +c q) +c 1c) ≠ )
8988adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn ) → ((q +c q) +c 1c) ≠ )
9089adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → ((q +c q) +c 1c) ≠ )
91 addc32 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((q +c q) +c 1c) = ((q +c 1c) +c q)
9291addceq1i 4386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((q +c q) +c 1c) +c 1c) = (((q +c 1c) +c q) +c 1c)
93 addcass 4415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((q +c 1c) +c q) +c 1c) = ((q +c 1c) +c (q +c 1c))
9492, 93eqtri 2373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((q +c q) +c 1c) +c 1c) = ((q +c 1c) +c (q +c 1c))
9594eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c) ↔ ((m +c m) +c 1c) = ((q +c 1c) +c (q +c 1c)))
96 simplll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → m Nn )
97 nncaddccl 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((m Nn m Nn ) → (m +c m) Nn )
9897anidms 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (m Nn → (m +c m) Nn )
9996, 98syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → (m +c m) Nn )
100 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → q Nn )
101 nncaddccl 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((q Nn q Nn ) → (q +c q) Nn )
102101anidms 626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (q Nn → (q +c q) Nn )
103 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((q +c q) Nn → ((q +c q) +c 1c) Nn )
104100, 102, 1033syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → ((q +c q) +c 1c) Nn )
105 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c))
106 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → (((m +c m) +c 1c) +c 1c) ≠ )
107 addcnnul 4453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((m +c m) +c 1c) +c 1c) ≠ → (((m +c m) +c 1c) ≠ 1c))
108107simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((m +c m) +c 1c) +c 1c) ≠ → ((m +c m) +c 1c) ≠ )
109106, 108syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → ((m +c m) +c 1c) ≠ )
110 prepeano4 4451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((m +c m) Nn ((q +c q) +c 1c) Nn ) (((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c) ((m +c m) +c 1c) ≠ )) → (m +c m) = ((q +c q) +c 1c))
11199, 104, 105, 109, 110syl22anc 1183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) ((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c)) → (m +c m) = ((q +c q) +c 1c))
112111ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → (((m +c m) +c 1c) = (((q +c q) +c 1c) +c 1c) → (m +c m) = ((q +c q) +c 1c)))
11395, 112syl5bir 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → (((m +c m) +c 1c) = ((q +c 1c) +c (q +c 1c)) → (m +c m) = ((q +c q) +c 1c)))
114113necon3d 2554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → ((m +c m) ≠ ((q +c q) +c 1c) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
11590, 114embantd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → ((((q +c q) +c 1c) ≠ → (m +c m) ≠ ((q +c q) +c 1c)) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
11680, 115syld 40 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ q Nn )) → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
117116expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ) → (q Nn → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c)))))
118117com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ) → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → (q Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c)))))
119118ex 423 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) → ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → (q Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))))
120119com23 72 . . . . . . . . . . . . . . . . . . . . . . . 24 ((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → ((((q +c 1c) +c (q +c 1c)) +c 1c) ≠ → (q Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))))
121120imp31 421 . . . . . . . . . . . . . . . . . . . . . . 23 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ) → (q Nn → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
122121com12 27 . . . . . . . . . . . . . . . . . . . . . 22 (q Nn → ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
123 addceq12 4385 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((n = (q +c 1c) n = (q +c 1c)) → (n +c n) = ((q +c 1c) +c (q +c 1c)))
124123anidms 626 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (n = (q +c 1c) → (n +c n) = ((q +c 1c) +c (q +c 1c)))
125124addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . 25 (n = (q +c 1c) → ((n +c n) +c 1c) = (((q +c 1c) +c (q +c 1c)) +c 1c))
126125neeq1d 2529 . . . . . . . . . . . . . . . . . . . . . . . 24 (n = (q +c 1c) → (((n +c n) +c 1c) ≠ ↔ (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ))
127126anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . 23 (n = (q +c 1c) → ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) ((n +c n) +c 1c) ≠ ) ↔ (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ )))
128124neeq2d 2530 . . . . . . . . . . . . . . . . . . . . . . 23 (n = (q +c 1c) → (((m +c m) +c 1c) ≠ (n +c n) ↔ ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c))))
129127, 128imbi12d 311 . . . . . . . . . . . . . . . . . . . . . 22 (n = (q +c 1c) → (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) ((n +c n) +c 1c) ≠ ) → ((m +c m) +c 1c) ≠ (n +c n)) ↔ ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (((q +c 1c) +c (q +c 1c)) +c 1c) ≠ ) → ((m +c m) +c 1c) ≠ ((q +c 1c) +c (q +c 1c)))))
130122, 129syl5ibrcom 213 . . . . . . . . . . . . . . . . . . . . 21 (q Nn → (n = (q +c 1c) → ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) ((n +c n) +c 1c) ≠ ) → ((m +c m) +c 1c) ≠ (n +c n))))
131130rexlimiv 2732 . . . . . . . . . . . . . . . . . . . 20 (q Nn n = (q +c 1c) → ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) ((n +c n) +c 1c) ≠ ) → ((m +c m) +c 1c) ≠ (n +c n)))
132131com12 27 . . . . . . . . . . . . . . . . . . 19 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) ((n +c n) +c 1c) ≠ ) → (q Nn n = (q +c 1c) → ((m +c m) +c 1c) ≠ (n +c n)))
133132adantrl 696 . . . . . . . . . . . . . . . . . 18 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → (q Nn n = (q +c 1c) → ((m +c m) +c 1c) ≠ (n +c n)))
13470, 133jaod 369 . . . . . . . . . . . . . . . . 17 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → ((n = 0c q Nn n = (q +c 1c)) → ((m +c m) +c 1c) ≠ (n +c n)))
13563, 134mpd 14 . . . . . . . . . . . . . . . 16 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → ((m +c m) +c 1c) ≠ (n +c n))
136 simplll 734 . . . . . . . . . . . . . . . . . . . . 21 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → m Nn )
137136adantr 451 . . . . . . . . . . . . . . . . . . . 20 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → m Nn )
138 peano2 4403 . . . . . . . . . . . . . . . . . . . 20 ((m +c m) Nn → ((m +c m) +c 1c) Nn )
139137, 98, 1383syl 18 . . . . . . . . . . . . . . . . . . 19 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → ((m +c m) +c 1c) Nn )
140 simplrl 736 . . . . . . . . . . . . . . . . . . . 20 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → n Nn )
141 nncaddccl 4419 . . . . . . . . . . . . . . . . . . . . 21 ((n Nn n Nn ) → (n +c n) Nn )
142141anidms 626 . . . . . . . . . . . . . . . . . . . 20 (n Nn → (n +c n) Nn )
143140, 142syl 15 . . . . . . . . . . . . . . . . . . 19 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → (n +c n) Nn )
144 simpr 447 . . . . . . . . . . . . . . . . . . 19 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c))
145 simpllr 735 . . . . . . . . . . . . . . . . . . . 20 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → (((m +c m) +c 1c) +c 1c) ≠ )
146145adantr 451 . . . . . . . . . . . . . . . . . . 19 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → (((m +c m) +c 1c) +c 1c) ≠ )
147 prepeano4 4451 . . . . . . . . . . . . . . . . . . 19 (((((m +c m) +c 1c) Nn (n +c n) Nn ) ((((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c) (((m +c m) +c 1c) +c 1c) ≠ )) → ((m +c m) +c 1c) = (n +c n))
148139, 143, 144, 146, 147syl22anc 1183 . . . . . . . . . . . . . . . . . 18 (((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) (((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c)) → ((m +c m) +c 1c) = (n +c n))
149148ex 423 . . . . . . . . . . . . . . . . 17 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → ((((m +c m) +c 1c) +c 1c) = ((n +c n) +c 1c) → ((m +c m) +c 1c) = (n +c n)))
150149necon3d 2554 . . . . . . . . . . . . . . . 16 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → (((m +c m) +c 1c) ≠ (n +c n) → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
151135, 150mpd 14 . . . . . . . . . . . . . . 15 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) (n Nn ((n +c n) +c 1c) ≠ )) → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))
152151expr 598 . . . . . . . . . . . . . 14 ((((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) n Nn ) → (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
153152ralrimiva 2697 . . . . . . . . . . . . 13 (((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) → n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))
154153ex 423 . . . . . . . . . . . 12 ((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) → (p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c)) → n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
15560, 154embantd 50 . . . . . . . . . . 11 ((m Nn (((m +c m) +c 1c) +c 1c) ≠ ) → (((m +c m) ≠ p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) → n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c))))
156155ex 423 . . . . . . . . . 10 (m Nn → ((((m +c m) +c 1c) +c 1c) ≠ → (((m +c m) ≠ p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) → n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))))
157156com23 72 . . . . . . . . 9 (m Nn → (((m +c m) ≠ p Nn (((p +c p) +c 1c) ≠ → (m +c m) ≠ ((p +c p) +c 1c))) → ((((m +c m) +c 1c) +c 1c) ≠ n Nn (((n +c n) +c 1c) ≠ → (((m +c m) +c 1c) +c 1c) ≠ ((n +c n) +c 1c)))))
1586, 15, 30, 42, 49, 54, 157finds 4411 . . . . . . . 8 (k Nn → ((k +c k) ≠ n Nn (((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c))))
159 df-ne 2518 . . . . . . . . . . . . 13 ((k +c k) ≠ ((n +c n) +c 1c) ↔ ¬ (k +c k) = ((n +c n) +c 1c))
160159imbi2i 303 . . . . . . . . . . . 12 ((((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ (((n +c n) +c 1c) ≠ → ¬ (k +c k) = ((n +c n) +c 1c)))
161 con2b 324 . . . . . . . . . . . 12 ((((n +c n) +c 1c) ≠ → ¬ (k +c k) = ((n +c n) +c 1c)) ↔ ((k +c k) = ((n +c n) +c 1c) → ¬ ((n +c n) +c 1c) ≠ ))
162160, 161bitri 240 . . . . . . . . . . 11 ((((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ((k +c k) = ((n +c n) +c 1c) → ¬ ((n +c n) +c 1c) ≠ ))
163 imnan 411 . . . . . . . . . . 11 (((k +c k) = ((n +c n) +c 1c) → ¬ ((n +c n) +c 1c) ≠ ) ↔ ¬ ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
164162, 163bitri 240 . . . . . . . . . 10 ((((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ¬ ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
165164ralbii 2638 . . . . . . . . 9 (n Nn (((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ n Nn ¬ ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
166 ralnex 2624 . . . . . . . . 9 (n Nn ¬ ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ) ↔ ¬ n Nn ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
167165, 166bitri 240 . . . . . . . 8 (n Nn (((n +c n) +c 1c) ≠ → (k +c k) ≠ ((n +c n) +c 1c)) ↔ ¬ n Nn ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
168158, 167syl6ib 217 . . . . . . 7 (k Nn → ((k +c k) ≠ → ¬ n Nn ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )))
169 eqeq1 2359 . . . . . . . . . . 11 (x = (k +c k) → (x = ((n +c n) +c 1c) ↔ (k +c k) = ((n +c n) +c 1c)))
170169anbi1d 685 . . . . . . . . . 10 (x = (k +c k) → ((x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ) ↔ ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )))
171170rexbidv 2635 . . . . . . . . 9 (x = (k +c k) → (n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ) ↔ n Nn ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )))
172171notbid 285 . . . . . . . 8 (x = (k +c k) → (¬ n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ) ↔ ¬ n Nn ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )))
173172imbi2d 307 . . . . . . 7 (x = (k +c k) → (((k +c k) ≠ → ¬ n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )) ↔ ((k +c k) ≠ → ¬ n Nn ((k +c k) = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))))
174168, 173syl5ibrcom 213 . . . . . 6 (k Nn → (x = (k +c k) → ((k +c k) ≠ → ¬ n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))))
175174imp3a 420 . . . . 5 (k Nn → ((x = (k +c k) (k +c k) ≠ ) → ¬ n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )))
176175rexlimiv 2732 . . . 4 (k Nn (x = (k +c k) (k +c k) ≠ ) → ¬ n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
177 imnan 411 . . . 4 ((k Nn (x = (k +c k) (k +c k) ≠ ) → ¬ n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )) ↔ ¬ (k Nn (x = (k +c k) (k +c k) ≠ ) n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )))
178176, 177mpbi 199 . . 3 ¬ (k Nn (x = (k +c k) (k +c k) ≠ ) n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))
179178abf 3584 . 2 {x (k Nn (x = (k +c k) (k +c k) ≠ ) n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ ))} =
1805, 179eqtri 2373 1 ( EvenfinOddfin ) =
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wo 357   wa 358   = wceq 1642   wcel 1710  {cab 2339  wne 2516  wral 2614  wrex 2615  cin 3208  c0 3550  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375   Evenfin cevenfin 4436   Oddfin coddfin 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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
  Copyright terms: Public domain W3C validator