nnc3n3p1 - New Foundations Explorer

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

Proof of Theorem nnc3n3p1 Dummy variables a m n p q x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2863	. . . . . . . 8 ⊢ a ∈ V
2	1	elcompl 3226	. . . . . . 7 ⊢ (a ∈ ∼ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) ↔ ¬ a ∈ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ))
3		elima 4755	. . . . . . . . 9 ⊢ (a ∈ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) ↔ ∃n ∈ Nn nran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))a)
4		df-br 4641	. . . . . . . . . . 11 ⊢ (nran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))a ↔ ⟨n, a⟩ ∈ ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))))
5		elrn 4897	. . . . . . . . . . . 12 ⊢ (⟨n, a⟩ ∈ ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ ∃p p(ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))⟨n, a⟩)
6		df-br 4641	. . . . . . . . . . . . . . 15 ⊢ (p(ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))⟨n, a⟩ ↔ ⟨p, ⟨n, a⟩⟩ ∈ (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))))
7		oteltxp 5783	. . . . . . . . . . . . . . 15 ⊢ (⟨p, ⟨n, a⟩⟩ ∈ (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ (⟨p, n⟩ ∈ ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∧ ⟨p, a⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))))
8	6, 7	bitri 240	. . . . . . . . . . . . . 14 ⊢ (p(ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))⟨n, a⟩ ↔ (⟨p, n⟩ ∈ ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∧ ⟨p, a⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))))
9		elrn2 4898	. . . . . . . . . . . . . . . 16 ⊢ (⟨p, n⟩ ∈ ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ ∃q⟨q, ⟨p, n⟩⟩ ∈ (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))))
10		oteltxp 5783	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨q, ⟨p, n⟩⟩ ∈ (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ (⟨q, p⟩ ∈ ( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ∧ ⟨q, n⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))))
11		opelco 4885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨q, p⟩ ∈ ( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ↔ ∃x(q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ∧ x AddC p))
12		brcnv 4893	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ↔ x(1^st ↾ (^◡2^nd “ {1_c}))q)
13		brres 4950	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x(1^st ↾ (^◡2^nd “ {1_c}))q ↔ (x1^st q ∧ x ∈ (^◡2^nd “ {1_c})))
14	12, 13	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ↔ (x1^st q ∧ x ∈ (^◡2^nd “ {1_c})))
15		eliniseg 5021	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (x ∈ (^◡2^nd “ {1_c}) ↔ x2^nd 1_c)
16	15	anbi2i 675	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((x1^st q ∧ x ∈ (^◡2^nd “ {1_c})) ↔ (x1^st q ∧ x2^nd 1_c))
17		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ q ∈ V
18		1cex 4143	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1_c ∈ V
19	17, 18	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((x1^st q ∧ x2^nd 1_c) ↔ x = ⟨q, 1_c⟩)
20	14, 16, 19	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ↔ x = ⟨q, 1_c⟩)
21	20	anbi1i 676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ∧ x AddC p) ↔ (x = ⟨q, 1_c⟩ ∧ x AddC p))
22	21	exbii 1582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃x(q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ∧ x AddC p) ↔ ∃x(x = ⟨q, 1_c⟩ ∧ x AddC p))
23	17, 18	opex 4589	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨q, 1_c⟩ ∈ V
24		breq1 4643	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (x = ⟨q, 1_c⟩ → (x AddC p ↔ ⟨q, 1_c⟩ AddC p))
25	23, 24	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃x(x = ⟨q, 1_c⟩ ∧ x AddC p) ↔ ⟨q, 1_c⟩ AddC p)
26	22, 25	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃x(q^◡(1^st ↾ (^◡2^nd “ {1_c}))x ∧ x AddC p) ↔ ⟨q, 1_c⟩ AddC p)
27	17, 18	braddcfn 5827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨q, 1_c⟩ AddC p ↔ (q +_c 1_c) = p)
28		eqcom 2355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((q +_c 1_c) = p ↔ p = (q +_c 1_c))
29	27, 28	bitri 240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨q, 1_c⟩ AddC p ↔ p = (q +_c 1_c))
30	11, 26, 29	3bitri 262	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨q, p⟩ ∈ ( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ↔ p = (q +_c 1_c))
31		opelcnv 4894	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨q, n⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ↔ ⟨n, q⟩ ∈ ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))
32		nncdiv3lem1 6276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨n, q⟩ ∈ ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ↔ q = ((n +_c n) +_c n))
33	31, 32	bitri 240	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨q, n⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ↔ q = ((n +_c n) +_c n))
34	30, 33	anbi12i 678	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨q, p⟩ ∈ ( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ∧ ⟨q, n⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ (p = (q +_c 1_c) ∧ q = ((n +_c n) +_c n)))
35		ancom 437	. . . . . . . . . . . . . . . . . 18 ⊢ ((p = (q +_c 1_c) ∧ q = ((n +_c n) +_c n)) ↔ (q = ((n +_c n) +_c n) ∧ p = (q +_c 1_c)))
36	10, 34, 35	3bitri 262	. . . . . . . . . . . . . . . . 17 ⊢ (⟨q, ⟨p, n⟩⟩ ∈ (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ (q = ((n +_c n) +_c n) ∧ p = (q +_c 1_c)))
37	36	exbii 1582	. . . . . . . . . . . . . . . 16 ⊢ (∃q⟨q, ⟨p, n⟩⟩ ∈ (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ ∃q(q = ((n +_c n) +_c n) ∧ p = (q +_c 1_c)))
38		vex 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ n ∈ V
39	38, 38	addcex 4395	. . . . . . . . . . . . . . . . . 18 ⊢ (n +_c n) ∈ V
40	39, 38	addcex 4395	. . . . . . . . . . . . . . . . 17 ⊢ ((n +_c n) +_c n) ∈ V
41		addceq1 4384	. . . . . . . . . . . . . . . . . 18 ⊢ (q = ((n +_c n) +_c n) → (q +_c 1_c) = (((n +_c n) +_c n) +_c 1_c))
42	41	eqeq2d 2364	. . . . . . . . . . . . . . . . 17 ⊢ (q = ((n +_c n) +_c n) → (p = (q +_c 1_c) ↔ p = (((n +_c n) +_c n) +_c 1_c)))
43	40, 42	ceqsexv 2895	. . . . . . . . . . . . . . . 16 ⊢ (∃q(q = ((n +_c n) +_c n) ∧ p = (q +_c 1_c)) ↔ p = (((n +_c n) +_c n) +_c 1_c))
44	9, 37, 43	3bitri 262	. . . . . . . . . . . . . . 15 ⊢ (⟨p, n⟩ ∈ ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ p = (((n +_c n) +_c n) +_c 1_c))
45		opelcnv 4894	. . . . . . . . . . . . . . . 16 ⊢ (⟨p, a⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ↔ ⟨a, p⟩ ∈ ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))
46		nncdiv3lem1 6276	. . . . . . . . . . . . . . . 16 ⊢ (⟨a, p⟩ ∈ ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ↔ p = ((a +_c a) +_c a))
47	45, 46	bitri 240	. . . . . . . . . . . . . . 15 ⊢ (⟨p, a⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ↔ p = ((a +_c a) +_c a))
48	44, 47	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ ((⟨p, n⟩ ∈ ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∧ ⟨p, a⟩ ∈ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ (p = (((n +_c n) +_c n) +_c 1_c) ∧ p = ((a +_c a) +_c a)))
49		ancom 437	. . . . . . . . . . . . . 14 ⊢ ((p = (((n +_c n) +_c n) +_c 1_c) ∧ p = ((a +_c a) +_c a)) ↔ (p = ((a +_c a) +_c a) ∧ p = (((n +_c n) +_c n) +_c 1_c)))
50	8, 48, 49	3bitri 262	. . . . . . . . . . . . 13 ⊢ (p(ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))⟨n, a⟩ ↔ (p = ((a +_c a) +_c a) ∧ p = (((n +_c n) +_c n) +_c 1_c)))
51	50	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃p p(ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))⟨n, a⟩ ↔ ∃p(p = ((a +_c a) +_c a) ∧ p = (((n +_c n) +_c n) +_c 1_c)))
52	1, 1	addcex 4395	. . . . . . . . . . . . . 14 ⊢ (a +_c a) ∈ V
53	52, 1	addcex 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 1_c) ↔ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c)))
55	53, 54	ceqsexv 2895	. . . . . . . . . . . 12 ⊢ (∃p(p = ((a +_c a) +_c a) ∧ p = (((n +_c n) +_c n) +_c 1_c)) ↔ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
56	5, 51, 55	3bitri 262	. . . . . . . . . . 11 ⊢ (⟨n, a⟩ ∈ ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ↔ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
57	4, 56	bitri 240	. . . . . . . . . 10 ⊢ (nran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))a ↔ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
58	57	rexbii 2640	. . . . . . . . 9 ⊢ (∃n ∈ Nn nran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )))a ↔ ∃n ∈ Nn ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
59		dfrex2 2628	. . . . . . . . 9 ⊢ (∃n ∈ Nn ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ ∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
60	3, 58, 59	3bitrri 263	. . . . . . . 8 ⊢ (¬ ∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ a ∈ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ))
61	60	con1bii 321	. . . . . . 7 ⊢ (¬ a ∈ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) ↔ ∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
62	2, 61	bitri 240	. . . . . 6 ⊢ (a ∈ ∼ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) ↔ ∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c))
63	62	abbi2i 2465	. . . . 5 ⊢ ∼ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) = {a ∣ ∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c)}
64		addcfnex 5825	. . . . . . . . . . . 12 ⊢ AddC ∈ V
65		1stex 4740	. . . . . . . . . . . . . 14 ⊢ 1^st ∈ V
66		2ndex 5113	. . . . . . . . . . . . . . . 16 ⊢ 2^nd ∈ V
67	66	cnvex 5103	. . . . . . . . . . . . . . 15 ⊢ ^◡2^nd ∈ V
68		snex 4112	. . . . . . . . . . . . . . 15 ⊢ {1_c} ∈ V
69	67, 68	imaex 4748	. . . . . . . . . . . . . 14 ⊢ (^◡2^nd “ {1_c}) ∈ V
70	65, 69	resex 5118	. . . . . . . . . . . . 13 ⊢ (1^st ↾ (^◡2^nd “ {1_c})) ∈ V
71	70	cnvex 5103	. . . . . . . . . . . 12 ⊢ ^◡(1^st ↾ (^◡2^nd “ {1_c})) ∈ V
72	64, 71	coex 4751	. . . . . . . . . . 11 ⊢ ( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ∈ V
73	65	cnvex 5103	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡1^st ∈ V
74	65, 66	inex 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1^st ∩ 2^nd ) ∈ V
75	73, 74	txpex 5786	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡1^st ⊗ (1^st ∩ 2^nd )) ∈ V
76	75	rnex 5108	. . . . . . . . . . . . . . . . . 18 ⊢ ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ∈ V
77	76, 66	txpex 5786	. . . . . . . . . . . . . . . . 17 ⊢ (ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) ∈ V
78	77, 64	imaex 4748	. . . . . . . . . . . . . . . 16 ⊢ ((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∈ V
79	78	cnvex 5103	. . . . . . . . . . . . . . 15 ⊢ ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∈ V
80	79	ins3ex 5799	. . . . . . . . . . . . . 14 ⊢ Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∈ V
81	65, 65	coex 4751	. . . . . . . . . . . . . . . 16 ⊢ (1^st ∘ 1^st ) ∈ V
82	66, 65	coex 4751	. . . . . . . . . . . . . . . . 17 ⊢ (2^nd ∘ 1^st ) ∈ V
83	82, 66	txpex 5786	. . . . . . . . . . . . . . . 16 ⊢ ((2^nd ∘ 1^st ) ⊗ 2^nd ) ∈ V
84	81, 83	txpex 5786	. . . . . . . . . . . . . . 15 ⊢ ((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) ∈ V
85	84, 64	imaex 4748	. . . . . . . . . . . . . 14 ⊢ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ) ∈ V
86	80, 85	inex 4106	. . . . . . . . . . . . 13 ⊢ ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ∈ V
87	86	rnex 5108	. . . . . . . . . . . 12 ⊢ ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ∈ V
88	87	cnvex 5103	. . . . . . . . . . 11 ⊢ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC )) ∈ V
89	72, 88	txpex 5786	. . . . . . . . . 10 ⊢ (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∈ V
90	89	rnex 5108	. . . . . . . . 9 ⊢ ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∈ V
91	90, 88	txpex 5786	. . . . . . . 8 ⊢ (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∈ V
92	91	rnex 5108	. . . . . . 7 ⊢ ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ∈ V
93		nncex 4397	. . . . . . 7 ⊢ Nn ∈ V
94	92, 93	imaex 4748	. . . . . 6 ⊢ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) ∈ V
95	94	complex 4105	. . . . 5 ⊢ ∼ (ran (ran (( AddC ∘ ^◡(1^st ↾ (^◡2^nd “ {1_c}))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) ⊗ ^◡ran ( Ins3 ^◡((ran (^◡1^st ⊗ (1^st ∩ 2^nd )) ⊗ 2^nd ) “ AddC ) ∩ (((1^st ∘ 1^st ) ⊗ ((2^nd ∘ 1^st ) ⊗ 2^nd )) “ AddC ))) “ Nn ) ∈ V
96	63, 95	eqeltrri 2424	. . . 4 ⊢ {a ∣ ∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c)} ∈ V
97		addceq12 4386	. . . . . . . . . 10 ⊢ ((a = 0_c ∧ a = 0_c) → (a +_c a) = (0_c +_c 0_c))
98	97	anidms 626	. . . . . . . . 9 ⊢ (a = 0_c → (a +_c a) = (0_c +_c 0_c))
99		id 19	. . . . . . . . 9 ⊢ (a = 0_c → a = 0_c)
100	98, 99	addceq12d 4392	. . . . . . . 8 ⊢ (a = 0_c → ((a +_c a) +_c a) = ((0_c +_c 0_c) +_c 0_c))
101		addcid1 4406	. . . . . . . . 9 ⊢ ((0_c +_c 0_c) +_c 0_c) = (0_c +_c 0_c)
102		addcid2 4408	. . . . . . . . 9 ⊢ (0_c +_c 0_c) = 0_c
103	101, 102	eqtri 2373	. . . . . . . 8 ⊢ ((0_c +_c 0_c) +_c 0_c) = 0_c
104	100, 103	syl6eq 2401	. . . . . . 7 ⊢ (a = 0_c → ((a +_c a) +_c a) = 0_c)
105	104	eqeq1d 2361	. . . . . 6 ⊢ (a = 0_c → (((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ 0_c = (((n +_c n) +_c n) +_c 1_c)))
106	105	notbid 285	. . . . 5 ⊢ (a = 0_c → (¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ 0_c = (((n +_c n) +_c n) +_c 1_c)))
107	106	ralbidv 2635	. . . 4 ⊢ (a = 0_c → (∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ∀n ∈ Nn ¬ 0_c = (((n +_c n) +_c n) +_c 1_c)))
108		addceq12 4386	. . . . . . . . 9 ⊢ ((a = m ∧ a = m) → (a +_c a) = (m +_c m))
109	108	anidms 626	. . . . . . . 8 ⊢ (a = m → (a +_c a) = (m +_c m))
110		id 19	. . . . . . . 8 ⊢ (a = m → a = m)
111	109, 110	addceq12d 4392	. . . . . . 7 ⊢ (a = m → ((a +_c a) +_c a) = ((m +_c m) +_c m))
112	111	eqeq1d 2361	. . . . . 6 ⊢ (a = m → (((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)))
113	112	notbid 285	. . . . 5 ⊢ (a = m → (¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)))
114	113	ralbidv 2635	. . . 4 ⊢ (a = m → (∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)))
115		addceq12 4386	. . . . . . . . . 10 ⊢ ((a = (m +_c 1_c) ∧ a = (m +_c 1_c)) → (a +_c a) = ((m +_c 1_c) +_c (m +_c 1_c)))
116	115	anidms 626	. . . . . . . . 9 ⊢ (a = (m +_c 1_c) → (a +_c a) = ((m +_c 1_c) +_c (m +_c 1_c)))
117		id 19	. . . . . . . . 9 ⊢ (a = (m +_c 1_c) → a = (m +_c 1_c))
118	116, 117	addceq12d 4392	. . . . . . . 8 ⊢ (a = (m +_c 1_c) → ((a +_c a) +_c a) = (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)))
119	118	eqeq1d 2361	. . . . . . 7 ⊢ (a = (m +_c 1_c) → (((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((n +_c n) +_c n) +_c 1_c)))
120	119	notbid 285	. . . . . 6 ⊢ (a = (m +_c 1_c) → (¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((n +_c n) +_c n) +_c 1_c)))
121	120	ralbidv 2635	. . . . 5 ⊢ (a = (m +_c 1_c) → (∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ∀n ∈ Nn ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((n +_c n) +_c n) +_c 1_c)))
122		addceq12 4386	. . . . . . . . . . 11 ⊢ ((n = p ∧ n = p) → (n +_c n) = (p +_c p))
123	122	anidms 626	. . . . . . . . . 10 ⊢ (n = p → (n +_c n) = (p +_c p))
124		id 19	. . . . . . . . . 10 ⊢ (n = p → n = p)
125	123, 124	addceq12d 4392	. . . . . . . . 9 ⊢ (n = p → ((n +_c n) +_c n) = ((p +_c p) +_c p))
126	125	addceq1d 4390	. . . . . . . 8 ⊢ (n = p → (((n +_c n) +_c n) +_c 1_c) = (((p +_c p) +_c p) +_c 1_c))
127	126	eqeq2d 2364	. . . . . . 7 ⊢ (n = p → ((((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((n +_c n) +_c n) +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
128	127	notbid 285	. . . . . 6 ⊢ (n = p → (¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
129	128	cbvralv 2836	. . . . 5 ⊢ (∀n ∈ Nn ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((n +_c n) +_c n) +_c 1_c) ↔ ∀p ∈ Nn ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c))
130	121, 129	syl6bb 252	. . . 4 ⊢ (a = (m +_c 1_c) → (∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ∀p ∈ Nn ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
131		addceq12 4386	. . . . . . . . 9 ⊢ ((a = A ∧ a = A) → (a +_c a) = (A +_c A))
132	131	anidms 626	. . . . . . . 8 ⊢ (a = A → (a +_c a) = (A +_c A))
133		id 19	. . . . . . . 8 ⊢ (a = A → a = A)
134	132, 133	addceq12d 4392	. . . . . . 7 ⊢ (a = A → ((a +_c a) +_c a) = ((A +_c A) +_c A))
135	134	eqeq1d 2361	. . . . . 6 ⊢ (a = A → (((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c)))
136	135	notbid 285	. . . . 5 ⊢ (a = A → (¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ ((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c)))
137	136	ralbidv 2635	. . . 4 ⊢ (a = A → (∀n ∈ Nn ¬ ((a +_c a) +_c a) = (((n +_c n) +_c n) +_c 1_c) ↔ ∀n ∈ Nn ¬ ((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c)))
138		1ne0c 6242	. . . . . . . 8 ⊢ 1_c ≠ 0_c
139		df-ne 2519	. . . . . . . 8 ⊢ (1_c ≠ 0_c ↔ ¬ 1_c = 0_c)
140	138, 139	mpbi 199	. . . . . . 7 ⊢ ¬ 1_c = 0_c
141	140	intnan 880	. . . . . 6 ⊢ ¬ (((n +_c n) +_c n) = 0_c ∧ 1_c = 0_c)
142		eqcom 2355	. . . . . . 7 ⊢ (0_c = (((n +_c n) +_c n) +_c 1_c) ↔ (((n +_c n) +_c n) +_c 1_c) = 0_c)
143		nncaddccl 4420	. . . . . . . . . . 11 ⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n +_c n) ∈ Nn )
144	143	anidms 626	. . . . . . . . . 10 ⊢ (n ∈ Nn → (n +_c n) ∈ Nn )
145		nncaddccl 4420	. . . . . . . . . 10 ⊢ (((n +_c n) ∈ Nn ∧ n ∈ Nn ) → ((n +_c n) +_c n) ∈ Nn )
146	144, 145	mpancom 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 )
148	146, 147	syl 15	. . . . . . . 8 ⊢ (n ∈ Nn → ((n +_c n) +_c n) ∈ NC )
149		1cnc 6140	. . . . . . . 8 ⊢ 1_c ∈ NC
150		addceq0 6220	. . . . . . . 8 ⊢ ((((n +_c n) +_c n) ∈ NC ∧ 1_c ∈ NC ) → ((((n +_c n) +_c n) +_c 1_c) = 0_c ↔ (((n +_c n) +_c n) = 0_c ∧ 1_c = 0_c)))
151	148, 149, 150	sylancl 643	. . . . . . 7 ⊢ (n ∈ Nn → ((((n +_c n) +_c n) +_c 1_c) = 0_c ↔ (((n +_c n) +_c n) = 0_c ∧ 1_c = 0_c)))
152	142, 151	syl5bb 248	. . . . . 6 ⊢ (n ∈ Nn → (0_c = (((n +_c n) +_c n) +_c 1_c) ↔ (((n +_c n) +_c n) = 0_c ∧ 1_c = 0_c)))
153	141, 152	mtbiri 294	. . . . 5 ⊢ (n ∈ Nn → ¬ 0_c = (((n +_c n) +_c n) +_c 1_c))
154	153	rgen 2680	. . . 4 ⊢ ∀n ∈ Nn ¬ 0_c = (((n +_c n) +_c n) +_c 1_c)
155		nnc0suc 4413	. . . . . . 7 ⊢ (p ∈ Nn ↔ (p = 0_c ∨ ∃q ∈ Nn p = (q +_c 1_c)))
156		0cnsuc 4402	. . . . . . . . . . . . . . 15 ⊢ ((((m +_c 1_c) +_c m) +_c m) +_c 1_c) ≠ 0_c
157		df-ne 2519	. . . . . . . . . . . . . . 15 ⊢ (((((m +_c 1_c) +_c m) +_c m) +_c 1_c) ≠ 0_c ↔ ¬ ((((m +_c 1_c) +_c m) +_c m) +_c 1_c) = 0_c)
158	156, 157	mpbi 199	. . . . . . . . . . . . . 14 ⊢ ¬ ((((m +_c 1_c) +_c m) +_c m) +_c 1_c) = 0_c
159	158	a1i 10	. . . . . . . . . . . . 13 ⊢ (m ∈ Nn → ¬ ((((m +_c 1_c) +_c m) +_c m) +_c 1_c) = 0_c)
160		addcass 4416	. . . . . . . . . . . . . . . 16 ⊢ (((m +_c 1_c) +_c m) +_c 1_c) = ((m +_c 1_c) +_c (m +_c 1_c))
161	160	addceq1i 4387	. . . . . . . . . . . . . . 15 ⊢ ((((m +_c 1_c) +_c m) +_c 1_c) +_c m) = (((m +_c 1_c) +_c (m +_c 1_c)) +_c m)
162		addc32 4417	. . . . . . . . . . . . . . 15 ⊢ ((((m +_c 1_c) +_c m) +_c 1_c) +_c m) = ((((m +_c 1_c) +_c m) +_c m) +_c 1_c)
163	161, 162	eqtr3i 2375	. . . . . . . . . . . . . 14 ⊢ (((m +_c 1_c) +_c (m +_c 1_c)) +_c m) = ((((m +_c 1_c) +_c m) +_c m) +_c 1_c)
164	163	eqeq1i 2360	. . . . . . . . . . . . 13 ⊢ ((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) = 0_c ↔ ((((m +_c 1_c) +_c m) +_c m) +_c 1_c) = 0_c)
165	159, 164	sylnibr 296	. . . . . . . . . . . 12 ⊢ (m ∈ Nn → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c m) = 0_c)
166		peano2 4404	. . . . . . . . . . . . . . 15 ⊢ (m ∈ Nn → (m +_c 1_c) ∈ Nn )
167		nncaddccl 4420	. . . . . . . . . . . . . . . 16 ⊢ (((m +_c 1_c) ∈ Nn ∧ (m +_c 1_c) ∈ Nn ) → ((m +_c 1_c) +_c (m +_c 1_c)) ∈ Nn )
168	167	anidms 626	. . . . . . . . . . . . . . 15 ⊢ ((m +_c 1_c) ∈ Nn → ((m +_c 1_c) +_c (m +_c 1_c)) ∈ Nn )
169	166, 168	syl 15	. . . . . . . . . . . . . 14 ⊢ (m ∈ Nn → ((m +_c 1_c) +_c (m +_c 1_c)) ∈ Nn )
170		nncaddccl 4420	. . . . . . . . . . . . . 14 ⊢ ((((m +_c 1_c) +_c (m +_c 1_c)) ∈ Nn ∧ m ∈ Nn ) → (((m +_c 1_c) +_c (m +_c 1_c)) +_c m) ∈ Nn )
171	169, 170	mpancom 650	. . . . . . . . . . . . 13 ⊢ (m ∈ Nn → (((m +_c 1_c) +_c (m +_c 1_c)) +_c m) ∈ Nn )
172		peano1 4403	. . . . . . . . . . . . 13 ⊢ 0_c ∈ Nn
173		suc11nnc 4559	. . . . . . . . . . . . 13 ⊢ (((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) ∈ Nn ∧ 0_c ∈ Nn ) → (((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) +_c 1_c) = (0_c +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c m) = 0_c))
174	171, 172, 173	sylancl 643	. . . . . . . . . . . 12 ⊢ (m ∈ Nn → (((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) +_c 1_c) = (0_c +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c m) = 0_c))
175	165, 174	mtbird 292	. . . . . . . . . . 11 ⊢ (m ∈ Nn → ¬ ((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) +_c 1_c) = (0_c +_c 1_c))
176		addcass 4416	. . . . . . . . . . . 12 ⊢ ((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) +_c 1_c) = (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c))
177	176	eqeq1i 2360	. . . . . . . . . . 11 ⊢ (((((m +_c 1_c) +_c (m +_c 1_c)) +_c m) +_c 1_c) = (0_c +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (0_c +_c 1_c))
178	175, 177	sylnib 295	. . . . . . . . . 10 ⊢ (m ∈ Nn → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (0_c +_c 1_c))
179		addceq12 4386	. . . . . . . . . . . . . . . 16 ⊢ ((p = 0_c ∧ p = 0_c) → (p +_c p) = (0_c +_c 0_c))
180	179	anidms 626	. . . . . . . . . . . . . . 15 ⊢ (p = 0_c → (p +_c p) = (0_c +_c 0_c))
181		id 19	. . . . . . . . . . . . . . 15 ⊢ (p = 0_c → p = 0_c)
182	180, 181	addceq12d 4392	. . . . . . . . . . . . . 14 ⊢ (p = 0_c → ((p +_c p) +_c p) = ((0_c +_c 0_c) +_c 0_c))
183	182, 103	syl6eq 2401	. . . . . . . . . . . . 13 ⊢ (p = 0_c → ((p +_c p) +_c p) = 0_c)
184	183	addceq1d 4390	. . . . . . . . . . . 12 ⊢ (p = 0_c → (((p +_c p) +_c p) +_c 1_c) = (0_c +_c 1_c))
185	184	eqeq2d 2364	. . . . . . . . . . 11 ⊢ (p = 0_c → ((((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (0_c +_c 1_c)))
186	185	notbid 285	. . . . . . . . . 10 ⊢ (p = 0_c → (¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c) ↔ ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (0_c +_c 1_c)))
187	178, 186	syl5ibrcom 213	. . . . . . . . 9 ⊢ (m ∈ Nn → (p = 0_c → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
188	187	adantr 451	. . . . . . . 8 ⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) → (p = 0_c → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
189		addceq12 4386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((n = q ∧ n = q) → (n +_c n) = (q +_c q))
190	189	anidms 626	. . . . . . . . . . . . . . . . . . 19 ⊢ (n = q → (n +_c n) = (q +_c q))
191		id 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (n = q → n = q)
192	190, 191	addceq12d 4392	. . . . . . . . . . . . . . . . . 18 ⊢ (n = q → ((n +_c n) +_c n) = ((q +_c q) +_c q))
193	192	addceq1d 4390	. . . . . . . . . . . . . . . . 17 ⊢ (n = q → (((n +_c n) +_c n) +_c 1_c) = (((q +_c q) +_c q) +_c 1_c))
194	193	eqeq2d 2364	. . . . . . . . . . . . . . . 16 ⊢ (n = q → (((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c) ↔ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
195	194	notbid 285	. . . . . . . . . . . . . . 15 ⊢ (n = q → (¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
196	195	rspcv 2952	. . . . . . . . . . . . . 14 ⊢ (q ∈ Nn → (∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c) → ¬ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
197	196	adantl 452	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ q ∈ Nn ) → (∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c) → ¬ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
198		addc6 4419	. . . . . . . . . . . . . . . 16 ⊢ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((m +_c m) +_c m) +_c ((1_c +_c 1_c) +_c 1_c))
199		addc6 4419	. . . . . . . . . . . . . . . . . 18 ⊢ (((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) = (((q +_c q) +_c q) +_c ((1_c +_c 1_c) +_c 1_c))
200	199	addceq1i 4387	. . . . . . . . . . . . . . . . 17 ⊢ ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c) = ((((q +_c q) +_c q) +_c ((1_c +_c 1_c) +_c 1_c)) +_c 1_c)
201		addc32 4417	. . . . . . . . . . . . . . . . 17 ⊢ ((((q +_c q) +_c q) +_c ((1_c +_c 1_c) +_c 1_c)) +_c 1_c) = ((((q +_c q) +_c q) +_c 1_c) +_c ((1_c +_c 1_c) +_c 1_c))
202	200, 201	eqtri 2373	. . . . . . . . . . . . . . . 16 ⊢ ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c) = ((((q +_c q) +_c q) +_c 1_c) +_c ((1_c +_c 1_c) +_c 1_c))
203	198, 202	eqeq12i 2366	. . . . . . . . . . . . . . 15 ⊢ ((((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c) ↔ (((m +_c m) +_c m) +_c ((1_c +_c 1_c) +_c 1_c)) = ((((q +_c q) +_c q) +_c 1_c) +_c ((1_c +_c 1_c) +_c 1_c)))
204		nncaddccl 4420	. . . . . . . . . . . . . . . . . 18 ⊢ ((m ∈ Nn ∧ m ∈ Nn ) → (m +_c m) ∈ Nn )
205	204	anidms 626	. . . . . . . . . . . . . . . . 17 ⊢ (m ∈ Nn → (m +_c m) ∈ Nn )
206		nncaddccl 4420	. . . . . . . . . . . . . . . . 17 ⊢ (((m +_c m) ∈ Nn ∧ m ∈ Nn ) → ((m +_c m) +_c m) ∈ Nn )
207	205, 206	mpancom 650	. . . . . . . . . . . . . . . 16 ⊢ (m ∈ Nn → ((m +_c m) +_c m) ∈ Nn )
208		nncaddccl 4420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((q ∈ Nn ∧ q ∈ Nn ) → (q +_c q) ∈ Nn )
209	208	anidms 626	. . . . . . . . . . . . . . . . . 18 ⊢ (q ∈ Nn → (q +_c q) ∈ Nn )
210		nncaddccl 4420	. . . . . . . . . . . . . . . . . 18 ⊢ (((q +_c q) ∈ Nn ∧ q ∈ Nn ) → ((q +_c q) +_c q) ∈ Nn )
211	209, 210	mpancom 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 1_c) ∈ Nn )
213	211, 212	syl 15	. . . . . . . . . . . . . . . 16 ⊢ (q ∈ Nn → (((q +_c q) +_c q) +_c 1_c) ∈ Nn )
214		1cnnc 4409	. . . . . . . . . . . . . . . . . . 19 ⊢ 1_c ∈ Nn
215		nncaddccl 4420	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1_c ∈ Nn ∧ 1_c ∈ Nn ) → (1_c +_c 1_c) ∈ Nn )
216	214, 214, 215	mp2an 653	. . . . . . . . . . . . . . . . . 18 ⊢ (1_c +_c 1_c) ∈ Nn
217		nncaddccl 4420	. . . . . . . . . . . . . . . . . 18 ⊢ (((1_c +_c 1_c) ∈ Nn ∧ 1_c ∈ Nn ) → ((1_c +_c 1_c) +_c 1_c) ∈ Nn )
218	216, 214, 217	mp2an 653	. . . . . . . . . . . . . . . . 17 ⊢ ((1_c +_c 1_c) +_c 1_c) ∈ Nn
219		addccan1 4561	. . . . . . . . . . . . . . . . 17 ⊢ ((((m +_c m) +_c m) ∈ Nn ∧ (((q +_c q) +_c q) +_c 1_c) ∈ Nn ∧ ((1_c +_c 1_c) +_c 1_c) ∈ Nn ) → ((((m +_c m) +_c m) +_c ((1_c +_c 1_c) +_c 1_c)) = ((((q +_c q) +_c q) +_c 1_c) +_c ((1_c +_c 1_c) +_c 1_c)) ↔ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
220	218, 219	mp3an3 1266	. . . . . . . . . . . . . . . 16 ⊢ ((((m +_c m) +_c m) ∈ Nn ∧ (((q +_c q) +_c q) +_c 1_c) ∈ Nn ) → ((((m +_c m) +_c m) +_c ((1_c +_c 1_c) +_c 1_c)) = ((((q +_c q) +_c q) +_c 1_c) +_c ((1_c +_c 1_c) +_c 1_c)) ↔ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
221	207, 213, 220	syl2an 463	. . . . . . . . . . . . . . 15 ⊢ ((m ∈ Nn ∧ q ∈ Nn ) → ((((m +_c m) +_c m) +_c ((1_c +_c 1_c) +_c 1_c)) = ((((q +_c q) +_c q) +_c 1_c) +_c ((1_c +_c 1_c) +_c 1_c)) ↔ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
222	203, 221	syl5bb 248	. . . . . . . . . . . . . 14 ⊢ ((m ∈ Nn ∧ q ∈ Nn ) → ((((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c) ↔ ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
223	222	biimpd 198	. . . . . . . . . . . . 13 ⊢ ((m ∈ Nn ∧ q ∈ Nn ) → ((((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c) → ((m +_c m) +_c m) = (((q +_c q) +_c q) +_c 1_c)))
224	197, 223	nsyld 132	. . . . . . . . . . . 12 ⊢ ((m ∈ Nn ∧ q ∈ Nn ) → (∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c) → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c)))
225	224	imp 418	. . . . . . . . . . 11 ⊢ (((m ∈ Nn ∧ q ∈ Nn ) ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c))
226	225	an32s 779	. . . . . . . . . 10 ⊢ (((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) ∧ q ∈ Nn ) → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c))
227		addceq12 4386	. . . . . . . . . . . . . . 15 ⊢ ((p = (q +_c 1_c) ∧ p = (q +_c 1_c)) → (p +_c p) = ((q +_c 1_c) +_c (q +_c 1_c)))
228	227	anidms 626	. . . . . . . . . . . . . 14 ⊢ (p = (q +_c 1_c) → (p +_c p) = ((q +_c 1_c) +_c (q +_c 1_c)))
229		id 19	. . . . . . . . . . . . . 14 ⊢ (p = (q +_c 1_c) → p = (q +_c 1_c))
230	228, 229	addceq12d 4392	. . . . . . . . . . . . 13 ⊢ (p = (q +_c 1_c) → ((p +_c p) +_c p) = (((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)))
231	230	addceq1d 4390	. . . . . . . . . . . 12 ⊢ (p = (q +_c 1_c) → (((p +_c p) +_c p) +_c 1_c) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c))
232	231	eqeq2d 2364	. . . . . . . . . . 11 ⊢ (p = (q +_c 1_c) → ((((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c) ↔ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c)))
233	232	notbid 285	. . . . . . . . . 10 ⊢ (p = (q +_c 1_c) → (¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c) ↔ ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = ((((q +_c 1_c) +_c (q +_c 1_c)) +_c (q +_c 1_c)) +_c 1_c)))
234	226, 233	syl5ibrcom 213	. . . . . . . . 9 ⊢ (((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) ∧ q ∈ Nn ) → (p = (q +_c 1_c) → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
235	234	rexlimdva 2739	. . . . . . . 8 ⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) → (∃q ∈ Nn p = (q +_c 1_c) → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
236	188, 235	jaod 369	. . . . . . 7 ⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) → ((p = 0_c ∨ ∃q ∈ Nn p = (q +_c 1_c)) → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
237	155, 236	syl5bi 208	. . . . . 6 ⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) → (p ∈ Nn → ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
238	237	ralrimiv 2697	. . . . 5 ⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c)) → ∀p ∈ Nn ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c))
239	238	ex 423	. . . 4 ⊢ (m ∈ Nn → (∀n ∈ Nn ¬ ((m +_c m) +_c m) = (((n +_c n) +_c n) +_c 1_c) → ∀p ∈ Nn ¬ (((m +_c 1_c) +_c (m +_c 1_c)) +_c (m +_c 1_c)) = (((p +_c p) +_c p) +_c 1_c)))
240	96, 107, 114, 130, 137, 154, 239	finds 4412	. . 3 ⊢ (A ∈ Nn → ∀n ∈ Nn ¬ ((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c))
241		addceq12 4386	. . . . . . . . 9 ⊢ ((n = B ∧ n = B) → (n +_c n) = (B +_c B))
242	241	anidms 626	. . . . . . . 8 ⊢ (n = B → (n +_c n) = (B +_c B))
243		id 19	. . . . . . . 8 ⊢ (n = B → n = B)
244	242, 243	addceq12d 4392	. . . . . . 7 ⊢ (n = B → ((n +_c n) +_c n) = ((B +_c B) +_c B))
245	244	addceq1d 4390	. . . . . 6 ⊢ (n = B → (((n +_c n) +_c n) +_c 1_c) = (((B +_c B) +_c B) +_c 1_c))
246	245	eqeq2d 2364	. . . . 5 ⊢ (n = B → (((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c) ↔ ((A +_c A) +_c A) = (((B +_c B) +_c B) +_c 1_c)))
247	246	notbid 285	. . . 4 ⊢ (n = B → (¬ ((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c) ↔ ¬ ((A +_c A) +_c A) = (((B +_c B) +_c B) +_c 1_c)))
248	247	rspccv 2953	. . 3 ⊢ (∀n ∈ Nn ¬ ((A +_c A) +_c A) = (((n +_c n) +_c n) +_c 1_c) → (B ∈ Nn → ¬ ((A +_c A) +_c A) = (((B +_c B) +_c B) +_c 1_c)))
249	240, 248	syl 15	. 2 ⊢ (A ∈ Nn → (B ∈ Nn → ¬ ((A +_c A) +_c A) = (((B +_c B) +_c B) +_c 1_c)))
250	249	imp 418	1 ⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ ((A +_c A) +_c A) = (((B +_c B) +_c B) +_c 1_c))

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 1_cc1c 4135 Nn cnnc 4374 0_cc0c 4375 +_c cplc 4376 ⟨cop 4562 class class class wbr 4640 1^st c1st 4718 ∘ ccom 4722 “ cima 4723 ^◡ccnv 4772 ran crn 4774 ↾ cres 4775 2^nd 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

W3C validator