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

Theorem nnc3n3p1 6278
Description: Three times a natural is not one more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
Assertion
Ref Expression
nnc3n3p1 ((A Nn B Nn ) → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c))

Proof of Theorem nnc3n3p1
Dummy variables a m n p q x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2862 . . . . . . . 8 a V
21elcompl 3225 . . . . . . 7 (a ∼ (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) ↔ ¬ a (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ))
3 elima 4754 . . . . . . . . 9 (a (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) ↔ n Nn nran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))a)
4 df-br 4640 . . . . . . . . . . 11 (nran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))an, a ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))))
5 elrn 4896 . . . . . . . . . . . 12 (n, a ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ p p(ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))n, a)
6 df-br 4640 . . . . . . . . . . . . . . 15 (p(ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))n, ap, n, a (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))))
7 oteltxp 5782 . . . . . . . . . . . . . . 15 (p, n, a (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ (p, n ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) p, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))))
86, 7bitri 240 . . . . . . . . . . . . . 14 (p(ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))n, a ↔ (p, n ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) p, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))))
9 elrn2 4897 . . . . . . . . . . . . . . . 16 (p, n ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ qq, p, n (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))))
10 oteltxp 5782 . . . . . . . . . . . . . . . . . 18 (q, p, n (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ (q, p ( AddC (1st (2nd “ {1c}))) q, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))))
11 opelco 4884 . . . . . . . . . . . . . . . . . . . 20 (q, p ( AddC (1st (2nd “ {1c}))) ↔ x(q(1st (2nd “ {1c}))x x AddC p))
12 brcnv 4892 . . . . . . . . . . . . . . . . . . . . . . . . 25 (q(1st (2nd “ {1c}))xx(1st (2nd “ {1c}))q)
13 brres 4949 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x(1st (2nd “ {1c}))q ↔ (x1st q x (2nd “ {1c})))
1412, 13bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (q(1st (2nd “ {1c}))x ↔ (x1st q x (2nd “ {1c})))
15 eliniseg 5020 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x (2nd “ {1c}) ↔ x2nd 1c)
1615anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . 24 ((x1st q x (2nd “ {1c})) ↔ (x1st q x2nd 1c))
17 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . 25 q V
18 1cex 4142 . . . . . . . . . . . . . . . . . . . . . . . . 25 1c V
1917, 18op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . 24 ((x1st q x2nd 1c) ↔ x = q, 1c)
2014, 16, 193bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (q(1st (2nd “ {1c}))xx = q, 1c)
2120anbi1i 676 . . . . . . . . . . . . . . . . . . . . . 22 ((q(1st (2nd “ {1c}))x x AddC p) ↔ (x = q, 1c x AddC p))
2221exbii 1582 . . . . . . . . . . . . . . . . . . . . 21 (x(q(1st (2nd “ {1c}))x x AddC p) ↔ x(x = q, 1c x AddC p))
2317, 18opex 4588 . . . . . . . . . . . . . . . . . . . . . 22 q, 1c V
24 breq1 4642 . . . . . . . . . . . . . . . . . . . . . 22 (x = q, 1c → (x AddC pq, 1c AddC p))
2523, 24ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . 21 (x(x = q, 1c x AddC p) ↔ q, 1c AddC p)
2622, 25bitri 240 . . . . . . . . . . . . . . . . . . . 20 (x(q(1st (2nd “ {1c}))x x AddC p) ↔ q, 1c AddC p)
2717, 18braddcfn 5826 . . . . . . . . . . . . . . . . . . . . 21 (q, 1c AddC p ↔ (q +c 1c) = p)
28 eqcom 2355 . . . . . . . . . . . . . . . . . . . . 21 ((q +c 1c) = pp = (q +c 1c))
2927, 28bitri 240 . . . . . . . . . . . . . . . . . . . 20 (q, 1c AddC pp = (q +c 1c))
3011, 26, 293bitri 262 . . . . . . . . . . . . . . . . . . 19 (q, p ( AddC (1st (2nd “ {1c}))) ↔ p = (q +c 1c))
31 opelcnv 4893 . . . . . . . . . . . . . . . . . . . 20 (q, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ n, q ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))
32 nncdiv3lem1 6275 . . . . . . . . . . . . . . . . . . . 20 (n, q ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ q = ((n +c n) +c n))
3331, 32bitri 240 . . . . . . . . . . . . . . . . . . 19 (q, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ q = ((n +c n) +c n))
3430, 33anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((q, p ( AddC (1st (2nd “ {1c}))) q, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ (p = (q +c 1c) q = ((n +c n) +c n)))
35 ancom 437 . . . . . . . . . . . . . . . . . 18 ((p = (q +c 1c) q = ((n +c n) +c n)) ↔ (q = ((n +c n) +c n) p = (q +c 1c)))
3610, 34, 353bitri 262 . . . . . . . . . . . . . . . . 17 (q, p, n (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ (q = ((n +c n) +c n) p = (q +c 1c)))
3736exbii 1582 . . . . . . . . . . . . . . . 16 (qq, p, n (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ q(q = ((n +c n) +c n) p = (q +c 1c)))
38 vex 2862 . . . . . . . . . . . . . . . . . . 19 n V
3938, 38addcex 4394 . . . . . . . . . . . . . . . . . 18 (n +c n) V
4039, 38addcex 4394 . . . . . . . . . . . . . . . . 17 ((n +c n) +c n) V
41 addceq1 4383 . . . . . . . . . . . . . . . . . 18 (q = ((n +c n) +c n) → (q +c 1c) = (((n +c n) +c n) +c 1c))
4241eqeq2d 2364 . . . . . . . . . . . . . . . . 17 (q = ((n +c n) +c n) → (p = (q +c 1c) ↔ p = (((n +c n) +c n) +c 1c)))
4340, 42ceqsexv 2894 . . . . . . . . . . . . . . . 16 (q(q = ((n +c n) +c n) p = (q +c 1c)) ↔ p = (((n +c n) +c n) +c 1c))
449, 37, 433bitri 262 . . . . . . . . . . . . . . 15 (p, n ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ p = (((n +c n) +c n) +c 1c))
45 opelcnv 4893 . . . . . . . . . . . . . . . 16 (p, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ a, p ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))
46 nncdiv3lem1 6275 . . . . . . . . . . . . . . . 16 (a, p ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ p = ((a +c a) +c a))
4745, 46bitri 240 . . . . . . . . . . . . . . 15 (p, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ p = ((a +c a) +c a))
4844, 47anbi12i 678 . . . . . . . . . . . . . 14 ((p, n ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) p, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ (p = (((n +c n) +c n) +c 1c) p = ((a +c a) +c a)))
49 ancom 437 . . . . . . . . . . . . . 14 ((p = (((n +c n) +c n) +c 1c) p = ((a +c a) +c a)) ↔ (p = ((a +c a) +c a) p = (((n +c n) +c n) +c 1c)))
508, 48, 493bitri 262 . . . . . . . . . . . . 13 (p(ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))n, a ↔ (p = ((a +c a) +c a) p = (((n +c n) +c n) +c 1c)))
5150exbii 1582 . . . . . . . . . . . 12 (p p(ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))n, ap(p = ((a +c a) +c a) p = (((n +c n) +c n) +c 1c)))
521, 1addcex 4394 . . . . . . . . . . . . . 14 (a +c a) V
5352, 1addcex 4394 . . . . . . . . . . . . 13 ((a +c a) +c a) V
54 eqeq1 2359 . . . . . . . . . . . . 13 (p = ((a +c a) +c a) → (p = (((n +c n) +c n) +c 1c) ↔ ((a +c a) +c a) = (((n +c n) +c n) +c 1c)))
5553, 54ceqsexv 2894 . . . . . . . . . . . 12 (p(p = ((a +c a) +c a) p = (((n +c n) +c n) +c 1c)) ↔ ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
565, 51, 553bitri 262 . . . . . . . . . . 11 (n, a ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ↔ ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
574, 56bitri 240 . . . . . . . . . 10 (nran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))a ↔ ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
5857rexbii 2639 . . . . . . . . 9 (n Nn nran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))an Nn ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
59 dfrex2 2627 . . . . . . . . 9 (n Nn ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ¬ n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
603, 58, 593bitrri 263 . . . . . . . 8 n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ a (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ))
6160con1bii 321 . . . . . . 7 a (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) ↔ n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
622, 61bitri 240 . . . . . 6 (a ∼ (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) ↔ n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c))
6362abbi2i 2464 . . . . 5 ∼ (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) = {a n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c)}
64 addcfnex 5824 . . . . . . . . . . . 12 AddC V
65 1stex 4739 . . . . . . . . . . . . . 14 1st V
66 2ndex 5112 . . . . . . . . . . . . . . . 16 2nd V
6766cnvex 5102 . . . . . . . . . . . . . . 15 2nd V
68 snex 4111 . . . . . . . . . . . . . . 15 {1c} V
6967, 68imaex 4747 . . . . . . . . . . . . . 14 (2nd “ {1c}) V
7065, 69resex 5117 . . . . . . . . . . . . 13 (1st (2nd “ {1c})) V
7170cnvex 5102 . . . . . . . . . . . 12 (1st (2nd “ {1c})) V
7264, 71coex 4750 . . . . . . . . . . 11 ( AddC (1st (2nd “ {1c}))) V
7365cnvex 5102 . . . . . . . . . . . . . . . . . . . 20 1st V
7465, 66inex 4105 . . . . . . . . . . . . . . . . . . . 20 (1st ∩ 2nd ) V
7573, 74txpex 5785 . . . . . . . . . . . . . . . . . . 19 (1st ⊗ (1st ∩ 2nd )) V
7675rnex 5107 . . . . . . . . . . . . . . . . . 18 ran (1st ⊗ (1st ∩ 2nd )) V
7776, 66txpex 5785 . . . . . . . . . . . . . . . . 17 (ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) V
7877, 64imaex 4747 . . . . . . . . . . . . . . . 16 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
7978cnvex 5102 . . . . . . . . . . . . . . 15 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
8079ins3ex 5798 . . . . . . . . . . . . . 14 Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
8165, 65coex 4750 . . . . . . . . . . . . . . . 16 (1st 1st ) V
8266, 65coex 4750 . . . . . . . . . . . . . . . . 17 (2nd 1st ) V
8382, 66txpex 5785 . . . . . . . . . . . . . . . 16 ((2nd 1st ) ⊗ 2nd ) V
8481, 83txpex 5785 . . . . . . . . . . . . . . 15 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) V
8584, 64imaex 4747 . . . . . . . . . . . . . 14 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ) V
8680, 85inex 4105 . . . . . . . . . . . . 13 ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
8786rnex 5107 . . . . . . . . . . . 12 ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
8887cnvex 5102 . . . . . . . . . . 11 ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
8972, 88txpex 5785 . . . . . . . . . 10 (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) V
9089rnex 5107 . . . . . . . . 9 ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) V
9190, 88txpex 5785 . . . . . . . 8 (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) V
9291rnex 5107 . . . . . . 7 ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) V
93 nncex 4396 . . . . . . 7 Nn V
9492, 93imaex 4747 . . . . . 6 (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) V
9594complex 4104 . . . . 5 ∼ (ran (ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) “ Nn ) V
9663, 95eqeltrri 2424 . . . 4 {a n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c)} V
97 addceq12 4385 . . . . . . . . . 10 ((a = 0c a = 0c) → (a +c a) = (0c +c 0c))
9897anidms 626 . . . . . . . . 9 (a = 0c → (a +c a) = (0c +c 0c))
99 id 19 . . . . . . . . 9 (a = 0ca = 0c)
10098, 99addceq12d 4391 . . . . . . . 8 (a = 0c → ((a +c a) +c a) = ((0c +c 0c) +c 0c))
101 addcid1 4405 . . . . . . . . 9 ((0c +c 0c) +c 0c) = (0c +c 0c)
102 addcid2 4407 . . . . . . . . 9 (0c +c 0c) = 0c
103101, 102eqtri 2373 . . . . . . . 8 ((0c +c 0c) +c 0c) = 0c
104100, 103syl6eq 2401 . . . . . . 7 (a = 0c → ((a +c a) +c a) = 0c)
105104eqeq1d 2361 . . . . . 6 (a = 0c → (((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ 0c = (((n +c n) +c n) +c 1c)))
106105notbid 285 . . . . 5 (a = 0c → (¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ¬ 0c = (((n +c n) +c n) +c 1c)))
107106ralbidv 2634 . . . 4 (a = 0c → (n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ n Nn ¬ 0c = (((n +c n) +c n) +c 1c)))
108 addceq12 4385 . . . . . . . . 9 ((a = m a = m) → (a +c a) = (m +c m))
109108anidms 626 . . . . . . . 8 (a = m → (a +c a) = (m +c m))
110 id 19 . . . . . . . 8 (a = ma = m)
111109, 110addceq12d 4391 . . . . . . 7 (a = m → ((a +c a) +c a) = ((m +c m) +c m))
112111eqeq1d 2361 . . . . . 6 (a = m → (((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)))
113112notbid 285 . . . . 5 (a = m → (¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)))
114113ralbidv 2634 . . . 4 (a = m → (n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)))
115 addceq12 4385 . . . . . . . . . 10 ((a = (m +c 1c) a = (m +c 1c)) → (a +c a) = ((m +c 1c) +c (m +c 1c)))
116115anidms 626 . . . . . . . . 9 (a = (m +c 1c) → (a +c a) = ((m +c 1c) +c (m +c 1c)))
117 id 19 . . . . . . . . 9 (a = (m +c 1c) → a = (m +c 1c))
118116, 117addceq12d 4391 . . . . . . . 8 (a = (m +c 1c) → ((a +c a) +c a) = (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)))
119118eqeq1d 2361 . . . . . . 7 (a = (m +c 1c) → (((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((n +c n) +c n) +c 1c)))
120119notbid 285 . . . . . 6 (a = (m +c 1c) → (¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((n +c n) +c n) +c 1c)))
121120ralbidv 2634 . . . . 5 (a = (m +c 1c) → (n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ n Nn ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((n +c n) +c n) +c 1c)))
122 addceq12 4385 . . . . . . . . . . 11 ((n = p n = p) → (n +c n) = (p +c p))
123122anidms 626 . . . . . . . . . 10 (n = p → (n +c n) = (p +c p))
124 id 19 . . . . . . . . . 10 (n = pn = p)
125123, 124addceq12d 4391 . . . . . . . . 9 (n = p → ((n +c n) +c n) = ((p +c p) +c p))
126125addceq1d 4389 . . . . . . . 8 (n = p → (((n +c n) +c n) +c 1c) = (((p +c p) +c p) +c 1c))
127126eqeq2d 2364 . . . . . . 7 (n = p → ((((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((n +c n) +c n) +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
128127notbid 285 . . . . . 6 (n = p → (¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((n +c n) +c n) +c 1c) ↔ ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
129128cbvralv 2835 . . . . 5 (n Nn ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((n +c n) +c n) +c 1c) ↔ p Nn ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c))
130121, 129syl6bb 252 . . . 4 (a = (m +c 1c) → (n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ p Nn ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
131 addceq12 4385 . . . . . . . . 9 ((a = A a = A) → (a +c a) = (A +c A))
132131anidms 626 . . . . . . . 8 (a = A → (a +c a) = (A +c A))
133 id 19 . . . . . . . 8 (a = Aa = A)
134132, 133addceq12d 4391 . . . . . . 7 (a = A → ((a +c a) +c a) = ((A +c A) +c A))
135134eqeq1d 2361 . . . . . 6 (a = A → (((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ((A +c A) +c A) = (((n +c n) +c n) +c 1c)))
136135notbid 285 . . . . 5 (a = A → (¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ ¬ ((A +c A) +c A) = (((n +c n) +c n) +c 1c)))
137136ralbidv 2634 . . . 4 (a = A → (n Nn ¬ ((a +c a) +c a) = (((n +c n) +c n) +c 1c) ↔ n Nn ¬ ((A +c A) +c A) = (((n +c n) +c n) +c 1c)))
138 1ne0c 6241 . . . . . . . 8 1c ≠ 0c
139 df-ne 2518 . . . . . . . 8 (1c ≠ 0c ↔ ¬ 1c = 0c)
140138, 139mpbi 199 . . . . . . 7 ¬ 1c = 0c
141140intnan 880 . . . . . 6 ¬ (((n +c n) +c n) = 0c 1c = 0c)
142 eqcom 2355 . . . . . . 7 (0c = (((n +c n) +c n) +c 1c) ↔ (((n +c n) +c n) +c 1c) = 0c)
143 nncaddccl 4419 . . . . . . . . . . 11 ((n Nn n Nn ) → (n +c n) Nn )
144143anidms 626 . . . . . . . . . 10 (n Nn → (n +c n) Nn )
145 nncaddccl 4419 . . . . . . . . . 10 (((n +c n) Nn n Nn ) → ((n +c n) +c n) Nn )
146144, 145mpancom 650 . . . . . . . . 9 (n Nn → ((n +c n) +c n) Nn )
147 nnnc 6146 . . . . . . . . 9 (((n +c n) +c n) Nn → ((n +c n) +c n) NC )
148146, 147syl 15 . . . . . . . 8 (n Nn → ((n +c n) +c n) NC )
149 1cnc 6139 . . . . . . . 8 1c NC
150 addceq0 6219 . . . . . . . 8 ((((n +c n) +c n) NC 1c NC ) → ((((n +c n) +c n) +c 1c) = 0c ↔ (((n +c n) +c n) = 0c 1c = 0c)))
151148, 149, 150sylancl 643 . . . . . . 7 (n Nn → ((((n +c n) +c n) +c 1c) = 0c ↔ (((n +c n) +c n) = 0c 1c = 0c)))
152142, 151syl5bb 248 . . . . . 6 (n Nn → (0c = (((n +c n) +c n) +c 1c) ↔ (((n +c n) +c n) = 0c 1c = 0c)))
153141, 152mtbiri 294 . . . . 5 (n Nn → ¬ 0c = (((n +c n) +c n) +c 1c))
154153rgen 2679 . . . 4 n Nn ¬ 0c = (((n +c n) +c n) +c 1c)
155 nnc0suc 4412 . . . . . . 7 (p Nn ↔ (p = 0c q Nn p = (q +c 1c)))
156 0cnsuc 4401 . . . . . . . . . . . . . . 15 ((((m +c 1c) +c m) +c m) +c 1c) ≠ 0c
157 df-ne 2518 . . . . . . . . . . . . . . 15 (((((m +c 1c) +c m) +c m) +c 1c) ≠ 0c ↔ ¬ ((((m +c 1c) +c m) +c m) +c 1c) = 0c)
158156, 157mpbi 199 . . . . . . . . . . . . . 14 ¬ ((((m +c 1c) +c m) +c m) +c 1c) = 0c
159158a1i 10 . . . . . . . . . . . . 13 (m Nn → ¬ ((((m +c 1c) +c m) +c m) +c 1c) = 0c)
160 addcass 4415 . . . . . . . . . . . . . . . 16 (((m +c 1c) +c m) +c 1c) = ((m +c 1c) +c (m +c 1c))
161160addceq1i 4386 . . . . . . . . . . . . . . 15 ((((m +c 1c) +c m) +c 1c) +c m) = (((m +c 1c) +c (m +c 1c)) +c m)
162 addc32 4416 . . . . . . . . . . . . . . 15 ((((m +c 1c) +c m) +c 1c) +c m) = ((((m +c 1c) +c m) +c m) +c 1c)
163161, 162eqtr3i 2375 . . . . . . . . . . . . . 14 (((m +c 1c) +c (m +c 1c)) +c m) = ((((m +c 1c) +c m) +c m) +c 1c)
164163eqeq1i 2360 . . . . . . . . . . . . 13 ((((m +c 1c) +c (m +c 1c)) +c m) = 0c ↔ ((((m +c 1c) +c m) +c m) +c 1c) = 0c)
165159, 164sylnibr 296 . . . . . . . . . . . 12 (m Nn → ¬ (((m +c 1c) +c (m +c 1c)) +c m) = 0c)
166 peano2 4403 . . . . . . . . . . . . . . 15 (m Nn → (m +c 1c) Nn )
167 nncaddccl 4419 . . . . . . . . . . . . . . . 16 (((m +c 1c) Nn (m +c 1c) Nn ) → ((m +c 1c) +c (m +c 1c)) Nn )
168167anidms 626 . . . . . . . . . . . . . . 15 ((m +c 1c) Nn → ((m +c 1c) +c (m +c 1c)) Nn )
169166, 168syl 15 . . . . . . . . . . . . . 14 (m Nn → ((m +c 1c) +c (m +c 1c)) Nn )
170 nncaddccl 4419 . . . . . . . . . . . . . 14 ((((m +c 1c) +c (m +c 1c)) Nn m Nn ) → (((m +c 1c) +c (m +c 1c)) +c m) Nn )
171169, 170mpancom 650 . . . . . . . . . . . . 13 (m Nn → (((m +c 1c) +c (m +c 1c)) +c m) Nn )
172 peano1 4402 . . . . . . . . . . . . 13 0c Nn
173 suc11nnc 4558 . . . . . . . . . . . . 13 (((((m +c 1c) +c (m +c 1c)) +c m) Nn 0c Nn ) → (((((m +c 1c) +c (m +c 1c)) +c m) +c 1c) = (0c +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c m) = 0c))
174171, 172, 173sylancl 643 . . . . . . . . . . . 12 (m Nn → (((((m +c 1c) +c (m +c 1c)) +c m) +c 1c) = (0c +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c m) = 0c))
175165, 174mtbird 292 . . . . . . . . . . 11 (m Nn → ¬ ((((m +c 1c) +c (m +c 1c)) +c m) +c 1c) = (0c +c 1c))
176 addcass 4415 . . . . . . . . . . . 12 ((((m +c 1c) +c (m +c 1c)) +c m) +c 1c) = (((m +c 1c) +c (m +c 1c)) +c (m +c 1c))
177176eqeq1i 2360 . . . . . . . . . . 11 (((((m +c 1c) +c (m +c 1c)) +c m) +c 1c) = (0c +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (0c +c 1c))
178175, 177sylnib 295 . . . . . . . . . 10 (m Nn → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (0c +c 1c))
179 addceq12 4385 . . . . . . . . . . . . . . . 16 ((p = 0c p = 0c) → (p +c p) = (0c +c 0c))
180179anidms 626 . . . . . . . . . . . . . . 15 (p = 0c → (p +c p) = (0c +c 0c))
181 id 19 . . . . . . . . . . . . . . 15 (p = 0cp = 0c)
182180, 181addceq12d 4391 . . . . . . . . . . . . . 14 (p = 0c → ((p +c p) +c p) = ((0c +c 0c) +c 0c))
183182, 103syl6eq 2401 . . . . . . . . . . . . 13 (p = 0c → ((p +c p) +c p) = 0c)
184183addceq1d 4389 . . . . . . . . . . . 12 (p = 0c → (((p +c p) +c p) +c 1c) = (0c +c 1c))
185184eqeq2d 2364 . . . . . . . . . . 11 (p = 0c → ((((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (0c +c 1c)))
186185notbid 285 . . . . . . . . . 10 (p = 0c → (¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c) ↔ ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (0c +c 1c)))
187178, 186syl5ibrcom 213 . . . . . . . . 9 (m Nn → (p = 0c → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
188187adantr 451 . . . . . . . 8 ((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) → (p = 0c → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
189 addceq12 4385 . . . . . . . . . . . . . . . . . . . 20 ((n = q n = q) → (n +c n) = (q +c q))
190189anidms 626 . . . . . . . . . . . . . . . . . . 19 (n = q → (n +c n) = (q +c q))
191 id 19 . . . . . . . . . . . . . . . . . . 19 (n = qn = q)
192190, 191addceq12d 4391 . . . . . . . . . . . . . . . . . 18 (n = q → ((n +c n) +c n) = ((q +c q) +c q))
193192addceq1d 4389 . . . . . . . . . . . . . . . . 17 (n = q → (((n +c n) +c n) +c 1c) = (((q +c q) +c q) +c 1c))
194193eqeq2d 2364 . . . . . . . . . . . . . . . 16 (n = q → (((m +c m) +c m) = (((n +c n) +c n) +c 1c) ↔ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
195194notbid 285 . . . . . . . . . . . . . . 15 (n = q → (¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c) ↔ ¬ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
196195rspcv 2951 . . . . . . . . . . . . . 14 (q Nn → (n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c) → ¬ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
197196adantl 452 . . . . . . . . . . . . 13 ((m Nn q Nn ) → (n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c) → ¬ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
198 addc6 4418 . . . . . . . . . . . . . . . 16 (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((m +c m) +c m) +c ((1c +c 1c) +c 1c))
199 addc6 4418 . . . . . . . . . . . . . . . . . 18 (((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) = (((q +c q) +c q) +c ((1c +c 1c) +c 1c))
200199addceq1i 4386 . . . . . . . . . . . . . . . . 17 ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c) = ((((q +c q) +c q) +c ((1c +c 1c) +c 1c)) +c 1c)
201 addc32 4416 . . . . . . . . . . . . . . . . 17 ((((q +c q) +c q) +c ((1c +c 1c) +c 1c)) +c 1c) = ((((q +c q) +c q) +c 1c) +c ((1c +c 1c) +c 1c))
202200, 201eqtri 2373 . . . . . . . . . . . . . . . 16 ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c) = ((((q +c q) +c q) +c 1c) +c ((1c +c 1c) +c 1c))
203198, 202eqeq12i 2366 . . . . . . . . . . . . . . 15 ((((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c) ↔ (((m +c m) +c m) +c ((1c +c 1c) +c 1c)) = ((((q +c q) +c q) +c 1c) +c ((1c +c 1c) +c 1c)))
204 nncaddccl 4419 . . . . . . . . . . . . . . . . . 18 ((m Nn m Nn ) → (m +c m) Nn )
205204anidms 626 . . . . . . . . . . . . . . . . 17 (m Nn → (m +c m) Nn )
206 nncaddccl 4419 . . . . . . . . . . . . . . . . 17 (((m +c m) Nn m Nn ) → ((m +c m) +c m) Nn )
207205, 206mpancom 650 . . . . . . . . . . . . . . . 16 (m Nn → ((m +c m) +c m) Nn )
208 nncaddccl 4419 . . . . . . . . . . . . . . . . . . 19 ((q Nn q Nn ) → (q +c q) Nn )
209208anidms 626 . . . . . . . . . . . . . . . . . 18 (q Nn → (q +c q) Nn )
210 nncaddccl 4419 . . . . . . . . . . . . . . . . . 18 (((q +c q) Nn q Nn ) → ((q +c q) +c q) Nn )
211209, 210mpancom 650 . . . . . . . . . . . . . . . . 17 (q Nn → ((q +c q) +c q) Nn )
212 peano2 4403 . . . . . . . . . . . . . . . . 17 (((q +c q) +c q) Nn → (((q +c q) +c q) +c 1c) Nn )
213211, 212syl 15 . . . . . . . . . . . . . . . 16 (q Nn → (((q +c q) +c q) +c 1c) Nn )
214 1cnnc 4408 . . . . . . . . . . . . . . . . . . 19 1c Nn
215 nncaddccl 4419 . . . . . . . . . . . . . . . . . . 19 ((1c Nn 1c Nn ) → (1c +c 1c) Nn )
216214, 214, 215mp2an 653 . . . . . . . . . . . . . . . . . 18 (1c +c 1c) Nn
217 nncaddccl 4419 . . . . . . . . . . . . . . . . . 18 (((1c +c 1c) Nn 1c Nn ) → ((1c +c 1c) +c 1c) Nn )
218216, 214, 217mp2an 653 . . . . . . . . . . . . . . . . 17 ((1c +c 1c) +c 1c) Nn
219 addccan1 4560 . . . . . . . . . . . . . . . . 17 ((((m +c m) +c m) Nn (((q +c q) +c q) +c 1c) Nn ((1c +c 1c) +c 1c) Nn ) → ((((m +c m) +c m) +c ((1c +c 1c) +c 1c)) = ((((q +c q) +c q) +c 1c) +c ((1c +c 1c) +c 1c)) ↔ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
220218, 219mp3an3 1266 . . . . . . . . . . . . . . . 16 ((((m +c m) +c m) Nn (((q +c q) +c q) +c 1c) Nn ) → ((((m +c m) +c m) +c ((1c +c 1c) +c 1c)) = ((((q +c q) +c q) +c 1c) +c ((1c +c 1c) +c 1c)) ↔ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
221207, 213, 220syl2an 463 . . . . . . . . . . . . . . 15 ((m Nn q Nn ) → ((((m +c m) +c m) +c ((1c +c 1c) +c 1c)) = ((((q +c q) +c q) +c 1c) +c ((1c +c 1c) +c 1c)) ↔ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
222203, 221syl5bb 248 . . . . . . . . . . . . . 14 ((m Nn q Nn ) → ((((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c) ↔ ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
223222biimpd 198 . . . . . . . . . . . . 13 ((m Nn q Nn ) → ((((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c) → ((m +c m) +c m) = (((q +c q) +c q) +c 1c)))
224197, 223nsyld 132 . . . . . . . . . . . 12 ((m Nn q Nn ) → (n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c) → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c)))
225224imp 418 . . . . . . . . . . 11 (((m Nn q Nn ) n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c))
226225an32s 779 . . . . . . . . . 10 (((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) q Nn ) → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c))
227 addceq12 4385 . . . . . . . . . . . . . . 15 ((p = (q +c 1c) p = (q +c 1c)) → (p +c p) = ((q +c 1c) +c (q +c 1c)))
228227anidms 626 . . . . . . . . . . . . . 14 (p = (q +c 1c) → (p +c p) = ((q +c 1c) +c (q +c 1c)))
229 id 19 . . . . . . . . . . . . . 14 (p = (q +c 1c) → p = (q +c 1c))
230228, 229addceq12d 4391 . . . . . . . . . . . . 13 (p = (q +c 1c) → ((p +c p) +c p) = (((q +c 1c) +c (q +c 1c)) +c (q +c 1c)))
231230addceq1d 4389 . . . . . . . . . . . 12 (p = (q +c 1c) → (((p +c p) +c p) +c 1c) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c))
232231eqeq2d 2364 . . . . . . . . . . 11 (p = (q +c 1c) → ((((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c) ↔ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c)))
233232notbid 285 . . . . . . . . . 10 (p = (q +c 1c) → (¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c) ↔ ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = ((((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) +c 1c)))
234226, 233syl5ibrcom 213 . . . . . . . . 9 (((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) q Nn ) → (p = (q +c 1c) → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
235234rexlimdva 2738 . . . . . . . 8 ((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) → (q Nn p = (q +c 1c) → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
236188, 235jaod 369 . . . . . . 7 ((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) → ((p = 0c q Nn p = (q +c 1c)) → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
237155, 236syl5bi 208 . . . . . 6 ((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) → (p Nn → ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
238237ralrimiv 2696 . . . . 5 ((m Nn n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c)) → p Nn ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c))
239238ex 423 . . . 4 (m Nn → (n Nn ¬ ((m +c m) +c m) = (((n +c n) +c n) +c 1c) → p Nn ¬ (((m +c 1c) +c (m +c 1c)) +c (m +c 1c)) = (((p +c p) +c p) +c 1c)))
24096, 107, 114, 130, 137, 154, 239finds 4411 . . 3 (A Nnn Nn ¬ ((A +c A) +c A) = (((n +c n) +c n) +c 1c))
241 addceq12 4385 . . . . . . . . 9 ((n = B n = B) → (n +c n) = (B +c B))
242241anidms 626 . . . . . . . 8 (n = B → (n +c n) = (B +c B))
243 id 19 . . . . . . . 8 (n = Bn = B)
244242, 243addceq12d 4391 . . . . . . 7 (n = B → ((n +c n) +c n) = ((B +c B) +c B))
245244addceq1d 4389 . . . . . 6 (n = B → (((n +c n) +c n) +c 1c) = (((B +c B) +c B) +c 1c))
246245eqeq2d 2364 . . . . 5 (n = B → (((A +c A) +c A) = (((n +c n) +c n) +c 1c) ↔ ((A +c A) +c A) = (((B +c B) +c B) +c 1c)))
247246notbid 285 . . . 4 (n = B → (¬ ((A +c A) +c A) = (((n +c n) +c n) +c 1c) ↔ ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c)))
248247rspccv 2952 . . 3 (n Nn ¬ ((A +c A) +c A) = (((n +c n) +c n) +c 1c) → (B Nn → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c)))
249240, 248syl 15 . 2 (A Nn → (B Nn → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c)))
250249imp 418 1 ((A Nn B Nn ) → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wo 357   wa 358  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wne 2516  wral 2614  wrex 2615  Vcvv 2859  ccompl 3205  cin 3208  {csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   +c cplc 4375  cop 4561   class class class wbr 4639  1st c1st 4717   ccom 4721  cima 4722  ccnv 4771  ran crn 4773   cres 4774  2nd c2nd 4783  ctxp 5735   AddC caddcfn 5745   Ins3 cins3 5751   NC cncs 6088
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-13 1712  ax-14 1714  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-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-csb 3137  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  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-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-cup 5742  df-disj 5744  df-addcfn 5746  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-trans 5899  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-en 6029  df-ncs 6098  df-lec 6099  df-nc 6101
This theorem is referenced by:  nnc3n3p2  6279  nnc3p1n3p2  6280  nchoicelem1  6289
  Copyright terms: Public domain W3C validator