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

Theorem nnc3n3p1 6279
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 2863 . . . . . . . 8 a V
21elcompl 3226 . . . . . . 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 4755 . . . . . . . . 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 4641 . . . . . . . . . . 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 4897 . . . . . . . . . . . 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 4641 . . . . . . . . . . . . . . 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 5783 . . . . . . . . . . . . . . 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 4898 . . . . . . . . . . . . . . . 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 5783 . . . . . . . . . . . . . . . . . 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 4885 . . . . . . . . . . . . . . . . . . . 20 (q, p ( AddC (1st (2nd “ {1c}))) ↔ x(q(1st (2nd “ {1c}))x x AddC p))
12 brcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . 25 (q(1st (2nd “ {1c}))xx(1st (2nd “ {1c}))q)
13 brres 4950 . . . . . . . . . . . . . . . . . . . . . . . . 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 5021 . . . . . . . . . . . . . . . . . . . . . . . . 25 (x (2nd “ {1c}) ↔ x2nd 1c)
1615anbi2i 675 . . . . . . . . . . . . . . . . . . . . . . . 24 ((x1st q x (2nd “ {1c})) ↔ (x1st q x2nd 1c))
17 vex 2863 . . . . . . . . . . . . . . . . . . . . . . . . 25 q V
18 1cex 4143 . . . . . . . . . . . . . . . . . . . . . . . . 25 1c V
1917, 18op1st2nd 5791 . . . . . . . . . . . . . . . . . . . . . . . 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 4589 . . . . . . . . . . . . . . . . . . . . . 22 q, 1c V
24 breq1 4643 . . . . . . . . . . . . . . . . . . . . . 22 (x = q, 1c → (x AddC pq, 1c AddC p))
2523, 24ceqsexv 2895 . . . . . . . . . . . . . . . . . . . . 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 5827 . . . . . . . . . . . . . . . . . . . . 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 4894 . . . . . . . . . . . . . . . . . . . 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 6276 . . . . . . . . . . . . . . . . . . . 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 2863 . . . . . . . . . . . . . . . . . . 19 n V
3938, 38addcex 4395 . . . . . . . . . . . . . . . . . 18 (n +c n) V
4039, 38addcex 4395 . . . . . . . . . . . . . . . . 17 ((n +c n) +c n) V
41 addceq1 4384 . . . . . . . . . . . . . . . . . 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 2895 . . . . . . . . . . . . . . . 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 4894 . . . . . . . . . . . . . . . 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 6276 . . . . . . . . . . . . . . . 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 4395 . . . . . . . . . . . . . 14 (a +c a) V
5352, 1addcex 4395 . . . . . . . . . . . . 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 2895 . . . . . . . . . . . 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 2640 . . . . . . . . 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 2628 . . . . . . . . 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 2465 . . . . 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 5825 . . . . . . . . . . . 12 AddC V
65 1stex 4740 . . . . . . . . . . . . . 14 1st V
66 2ndex 5113 . . . . . . . . . . . . . . . 16 2nd V
6766cnvex 5103 . . . . . . . . . . . . . . 15 2nd V
68 snex 4112 . . . . . . . . . . . . . . 15 {1c} V
6967, 68imaex 4748 . . . . . . . . . . . . . 14 (2nd “ {1c}) V
7065, 69resex 5118 . . . . . . . . . . . . 13 (1st (2nd “ {1c})) V
7170cnvex 5103 . . . . . . . . . . . 12 (1st (2nd “ {1c})) V
7264, 71coex 4751 . . . . . . . . . . 11 ( AddC (1st (2nd “ {1c}))) V
7365cnvex 5103 . . . . . . . . . . . . . . . . . . . 20 1st V
7465, 66inex 4106 . . . . . . . . . . . . . . . . . . . 20 (1st ∩ 2nd ) V
7573, 74txpex 5786 . . . . . . . . . . . . . . . . . . 19 (1st ⊗ (1st ∩ 2nd )) V
7675rnex 5108 . . . . . . . . . . . . . . . . . 18 ran (1st ⊗ (1st ∩ 2nd )) V
7776, 66txpex 5786 . . . . . . . . . . . . . . . . 17 (ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) V
7877, 64imaex 4748 . . . . . . . . . . . . . . . 16 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
7978cnvex 5103 . . . . . . . . . . . . . . 15 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
8079ins3ex 5799 . . . . . . . . . . . . . 14 Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
8165, 65coex 4751 . . . . . . . . . . . . . . . 16 (1st 1st ) V
8266, 65coex 4751 . . . . . . . . . . . . . . . . 17 (2nd 1st ) V
8382, 66txpex 5786 . . . . . . . . . . . . . . . 16 ((2nd 1st ) ⊗ 2nd ) V
8481, 83txpex 5786 . . . . . . . . . . . . . . 15 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) V
8584, 64imaex 4748 . . . . . . . . . . . . . 14 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ) V
8680, 85inex 4106 . . . . . . . . . . . . 13 ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
8786rnex 5108 . . . . . . . . . . . 12 ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
8887cnvex 5103 . . . . . . . . . . 11 ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
8972, 88txpex 5786 . . . . . . . . . 10 (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) V
9089rnex 5108 . . . . . . . . 9 ran (( AddC (1st (2nd “ {1c}))) ⊗ ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ))) V
9190, 88txpex 5786 . . . . . . . 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 5108 . . . . . . 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 4397 . . . . . . 7 Nn V
9492, 93imaex 4748 . . . . . 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 4105 . . . . 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 4386 . . . . . . . . . 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 4392 . . . . . . . 8 (a = 0c → ((a +c a) +c a) = ((0c +c 0c) +c 0c))
101 addcid1 4406 . . . . . . . . 9 ((0c +c 0c) +c 0c) = (0c +c 0c)
102 addcid2 4408 . . . . . . . . 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 2635 . . . 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 4386 . . . . . . . . 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 4392 . . . . . . 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 2635 . . . 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 4386 . . . . . . . . . 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 4392 . . . . . . . 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 2635 . . . . 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 4386 . . . . . . . . . . 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 4392 . . . . . . . . 9 (n = p → ((n +c n) +c n) = ((p +c p) +c p))
126125addceq1d 4390 . . . . . . . 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 2836 . . . . 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 4386 . . . . . . . . 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 4392 . . . . . . 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 2635 . . . 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 6242 . . . . . . . 8 1c ≠ 0c
139 df-ne 2519 . . . . . . . 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 4420 . . . . . . . . . . 11 ((n Nn n Nn ) → (n +c n) Nn )
144143anidms 626 . . . . . . . . . 10 (n Nn → (n +c n) Nn )
145 nncaddccl 4420 . . . . . . . . . 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 6147 . . . . . . . . 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 6140 . . . . . . . 8 1c NC
150 addceq0 6220 . . . . . . . 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 2680 . . . 4 n Nn ¬ 0c = (((n +c n) +c n) +c 1c)
155 nnc0suc 4413 . . . . . . 7 (p Nn ↔ (p = 0c q Nn p = (q +c 1c)))
156 0cnsuc 4402 . . . . . . . . . . . . . . 15 ((((m +c 1c) +c m) +c m) +c 1c) ≠ 0c
157 df-ne 2519 . . . . . . . . . . . . . . 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 4416 . . . . . . . . . . . . . . . 16 (((m +c 1c) +c m) +c 1c) = ((m +c 1c) +c (m +c 1c))
161160addceq1i 4387 . . . . . . . . . . . . . . 15 ((((m +c 1c) +c m) +c 1c) +c m) = (((m +c 1c) +c (m +c 1c)) +c m)
162 addc32 4417 . . . . . . . . . . . . . . 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 4404 . . . . . . . . . . . . . . 15 (m Nn → (m +c 1c) Nn )
167 nncaddccl 4420 . . . . . . . . . . . . . . . 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 4420 . . . . . . . . . . . . . 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 4403 . . . . . . . . . . . . 13 0c Nn
173 suc11nnc 4559 . . . . . . . . . . . . 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 4416 . . . . . . . . . . . 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 4386 . . . . . . . . . . . . . . . 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 4392 . . . . . . . . . . . . . 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 4390 . . . . . . . . . . . 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 4386 . . . . . . . . . . . . . . . . . . . 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 4392 . . . . . . . . . . . . . . . . . 18 (n = q → ((n +c n) +c n) = ((q +c q) +c q))
193192addceq1d 4390 . . . . . . . . . . . . . . . . 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 2952 . . . . . . . . . . . . . 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 4419 . . . . . . . . . . . . . . . 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 4419 . . . . . . . . . . . . . . . . . 18 (((q +c 1c) +c (q +c 1c)) +c (q +c 1c)) = (((q +c q) +c q) +c ((1c +c 1c) +c 1c))
200199addceq1i 4387 . . . . . . . . . . . . . . . . 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 4417 . . . . . . . . . . . . . . . . 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 4420 . . . . . . . . . . . . . . . . . 18 ((m Nn m Nn ) → (m +c m) Nn )
205204anidms 626 . . . . . . . . . . . . . . . . 17 (m Nn → (m +c m) Nn )
206 nncaddccl 4420 . . . . . . . . . . . . . . . . 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 4420 . . . . . . . . . . . . . . . . . . 19 ((q Nn q Nn ) → (q +c q) Nn )
209208anidms 626 . . . . . . . . . . . . . . . . . 18 (q Nn → (q +c q) Nn )
210 nncaddccl 4420 . . . . . . . . . . . . . . . . . 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 4404 . . . . . . . . . . . . . . . . 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 4409 . . . . . . . . . . . . . . . . . . 19 1c Nn
215 nncaddccl 4420 . . . . . . . . . . . . . . . . . . 19 ((1c Nn 1c Nn ) → (1c +c 1c) Nn )
216214, 214, 215mp2an 653 . . . . . . . . . . . . . . . . . 18 (1c +c 1c) Nn
217 nncaddccl 4420 . . . . . . . . . . . . . . . . . 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 4561 . . . . . . . . . . . . . . . . 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 4386 . . . . . . . . . . . . . . 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 4392 . . . . . . . . . . . . 13 (p = (q +c 1c) → ((p +c p) +c p) = (((q +c 1c) +c (q +c 1c)) +c (q +c 1c)))
231230addceq1d 4390 . . . . . . . . . . . 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 2739 . . . . . . . 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 2697 . . . . 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 4412 . . 3 (A Nnn Nn ¬ ((A +c A) +c A) = (((n +c n) +c n) +c 1c))
241 addceq12 4386 . . . . . . . . 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 4392 . . . . . . 7 (n = B → ((n +c n) +c n) = ((B +c B) +c B))
245244addceq1d 4390 . . . . . 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 2953 . . 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 2517  wral 2615  wrex 2616  Vcvv 2860  ccompl 3206  cin 3209  {csn 3738  1cc1c 4135   Nn cnnc 4374  0cc0c 4375   +c cplc 4376  cop 4562   class class class wbr 4640  1st c1st 4718   ccom 4722  cima 4723  ccnv 4772  ran crn 4774   cres 4775  2nd c2nd 4784  ctxp 5736   AddC caddcfn 5746   Ins3 cins3 5752   NC cncs 6089
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 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088
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 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-csb 3138  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-iun 3972  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-f1 4793  df-fo 4794  df-f1o 4795  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-cup 5743  df-disj 5745  df-addcfn 5747  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-fns 5763  df-trans 5900  df-sym 5909  df-er 5910  df-ec 5948  df-qs 5952  df-en 6030  df-ncs 6099  df-lec 6100  df-nc 6102
This theorem is referenced by:  nnc3n3p2  6280  nnc3p1n3p2  6281  nchoicelem1  6290
  Copyright terms: Public domain W3C validator