Step | Hyp | Ref
| Expression |
1 | | nncdiv3 6277 |
. 2
⊢ (A ∈ Nn → ∃n ∈ Nn (A = ((n +c n) +c n) ∨ A = (((n
+c n)
+c n)
+c 1c) ∨
A = (((n +c n) +c n) +c
2c))) |
2 | | id 19 |
. . . . . . 7
⊢ (n ∈ Nn → n ∈ Nn
) |
3 | | nntccl 6170 |
. . . . . . 7
⊢ (n ∈ Nn → Tc
n ∈ Nn ) |
4 | | nnc3n3p2 6279 |
. . . . . . 7
⊢ ((n ∈ Nn ∧ Tc n
∈ Nn ) →
¬ ((n +c n) +c n) = ((( Tc
n +c Tc n)
+c Tc n) +c
2c)) |
5 | 2, 3, 4 | syl2anc 642 |
. . . . . 6
⊢ (n ∈ Nn → ¬ ((n
+c n)
+c n) = ((( Tc n
+c Tc n) +c Tc n)
+c 2c)) |
6 | | nncaddccl 4419 |
. . . . . . . . . . . 12
⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n
+c n) ∈ Nn
) |
7 | 6 | anidms 626 |
. . . . . . . . . . 11
⊢ (n ∈ Nn → (n
+c n) ∈ Nn
) |
8 | | nnnc 6146 |
. . . . . . . . . . 11
⊢ ((n +c n) ∈ Nn → (n
+c n) ∈ NC
) |
9 | 7, 8 | syl 15 |
. . . . . . . . . 10
⊢ (n ∈ Nn → (n
+c n) ∈ NC
) |
10 | | nnnc 6146 |
. . . . . . . . . 10
⊢ (n ∈ Nn → n ∈ NC
) |
11 | | tcdi 6164 |
. . . . . . . . . 10
⊢ (((n +c n) ∈ NC ∧ n ∈ NC ) → Tc
((n +c n) +c n) = ( Tc
(n +c n) +c Tc n)) |
12 | 9, 10, 11 | syl2anc 642 |
. . . . . . . . 9
⊢ (n ∈ Nn → Tc
((n +c n) +c n) = ( Tc
(n +c n) +c Tc n)) |
13 | | tcdi 6164 |
. . . . . . . . . . 11
⊢ ((n ∈ NC ∧ n ∈ NC ) → Tc
(n +c n) = ( Tc
n +c Tc n)) |
14 | 10, 10, 13 | syl2anc 642 |
. . . . . . . . . 10
⊢ (n ∈ Nn → Tc
(n +c n) = ( Tc
n +c Tc n)) |
15 | 14 | addceq1d 4389 |
. . . . . . . . 9
⊢ (n ∈ Nn → ( Tc
(n +c n) +c Tc n) =
(( Tc n +c Tc n)
+c Tc n)) |
16 | 12, 15 | eqtrd 2385 |
. . . . . . . 8
⊢ (n ∈ Nn → Tc
((n +c n) +c n) = (( Tc
n +c Tc n)
+c Tc n)) |
17 | 16 | addceq1d 4389 |
. . . . . . 7
⊢ (n ∈ Nn → ( Tc
((n +c n) +c n) +c 2c) = (((
Tc n +c Tc n)
+c Tc n) +c
2c)) |
18 | 17 | eqeq2d 2364 |
. . . . . 6
⊢ (n ∈ Nn → (((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 2c) ↔ ((n +c n) +c n) = ((( Tc
n +c Tc n)
+c Tc n) +c
2c))) |
19 | 5, 18 | mtbird 292 |
. . . . 5
⊢ (n ∈ Nn → ¬ ((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 2c)) |
20 | | id 19 |
. . . . . . 7
⊢ (A = ((n
+c n)
+c n) → A = ((n
+c n)
+c n)) |
21 | | tceq 6158 |
. . . . . . . 8
⊢ (A = ((n
+c n)
+c n) → Tc A =
Tc ((n +c n) +c n)) |
22 | 21 | addceq1d 4389 |
. . . . . . 7
⊢ (A = ((n
+c n)
+c n) → ( Tc A
+c 2c) = ( Tc ((n
+c n)
+c n)
+c 2c)) |
23 | 20, 22 | eqeq12d 2367 |
. . . . . 6
⊢ (A = ((n
+c n)
+c n) → (A = ( Tc
A +c
2c) ↔ ((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 2c))) |
24 | 23 | notbid 285 |
. . . . 5
⊢ (A = ((n
+c n)
+c n) → (¬
A = ( Tc A
+c 2c) ↔ ¬ ((n +c n) +c n) = ( Tc
((n +c n) +c n) +c
2c))) |
25 | 19, 24 | syl5ibrcom 213 |
. . . 4
⊢ (n ∈ Nn → (A =
((n +c n) +c n) → ¬ A = ( Tc
A +c
2c))) |
26 | | nncaddccl 4419 |
. . . . . . . . . 10
⊢ (((n +c n) ∈ Nn ∧ n ∈ Nn ) → ((n
+c n)
+c n) ∈ Nn
) |
27 | 7, 2, 26 | syl2anc 642 |
. . . . . . . . 9
⊢ (n ∈ Nn → ((n
+c n)
+c n) ∈ Nn
) |
28 | | nntccl 6170 |
. . . . . . . . . . 11
⊢ (((n +c n) +c n) ∈ Nn → Tc
((n +c n) +c n) ∈ Nn ) |
29 | 27, 28 | syl 15 |
. . . . . . . . . 10
⊢ (n ∈ Nn → Tc
((n +c n) +c n) ∈ Nn ) |
30 | | 2nnc 6167 |
. . . . . . . . . 10
⊢
2c ∈ Nn |
31 | | nncaddccl 4419 |
. . . . . . . . . 10
⊢ (( Tc ((n
+c n)
+c n) ∈ Nn ∧ 2c ∈ Nn ) → ( Tc ((n
+c n)
+c n)
+c 2c) ∈
Nn ) |
32 | 29, 30, 31 | sylancl 643 |
. . . . . . . . 9
⊢ (n ∈ Nn → ( Tc
((n +c n) +c n) +c 2c) ∈ Nn
) |
33 | | suc11nnc 4558 |
. . . . . . . . 9
⊢ ((((n +c n) +c n) ∈ Nn ∧ ( Tc ((n
+c n)
+c n)
+c 2c) ∈
Nn ) → ((((n +c n) +c n) +c 1c) = ((
Tc ((n +c n) +c n) +c 2c)
+c 1c) ↔ ((n +c n) +c n) = ( Tc
((n +c n) +c n) +c
2c))) |
34 | 27, 32, 33 | syl2anc 642 |
. . . . . . . 8
⊢ (n ∈ Nn → ((((n
+c n)
+c n)
+c 1c) = (( Tc ((n
+c n)
+c n)
+c 2c) +c
1c) ↔ ((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 2c))) |
35 | 19, 34 | mtbird 292 |
. . . . . . 7
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 1c) = (( Tc ((n
+c n)
+c n)
+c 2c) +c
1c)) |
36 | | addc32 4416 |
. . . . . . . . 9
⊢ (( Tc ((n
+c n)
+c n)
+c Tc
1c) +c 2c) = (( Tc ((n
+c n)
+c n)
+c 2c) +c Tc 1c) |
37 | | tc1c 6165 |
. . . . . . . . . 10
⊢ Tc 1c =
1c |
38 | 37 | addceq2i 4387 |
. . . . . . . . 9
⊢ (( Tc ((n
+c n)
+c n)
+c 2c) +c Tc 1c) = (( Tc ((n
+c n)
+c n)
+c 2c) +c
1c) |
39 | 36, 38 | eqtri 2373 |
. . . . . . . 8
⊢ (( Tc ((n
+c n)
+c n)
+c Tc
1c) +c 2c) = (( Tc ((n
+c n)
+c n)
+c 2c) +c
1c) |
40 | 39 | eqeq2i 2363 |
. . . . . . 7
⊢ ((((n +c n) +c n) +c 1c) = ((
Tc ((n +c n) +c n) +c Tc 1c) +c
2c) ↔ (((n
+c n)
+c n)
+c 1c) = (( Tc ((n
+c n)
+c n)
+c 2c) +c
1c)) |
41 | 35, 40 | sylnibr 296 |
. . . . . 6
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 1c) = (( Tc ((n
+c n)
+c n)
+c Tc
1c) +c
2c)) |
42 | | nnnc 6146 |
. . . . . . . . . 10
⊢ (((n +c n) +c n) ∈ Nn → ((n
+c n)
+c n) ∈ NC
) |
43 | 27, 42 | syl 15 |
. . . . . . . . 9
⊢ (n ∈ Nn → ((n
+c n)
+c n) ∈ NC
) |
44 | | 1cnc 6139 |
. . . . . . . . 9
⊢
1c ∈ NC |
45 | | tcdi 6164 |
. . . . . . . . 9
⊢ ((((n +c n) +c n) ∈ NC ∧
1c ∈ NC ) → Tc
(((n +c n) +c n) +c 1c) = (
Tc ((n +c n) +c n) +c Tc 1c)) |
46 | 43, 44, 45 | sylancl 643 |
. . . . . . . 8
⊢ (n ∈ Nn → Tc
(((n +c n) +c n) +c 1c) = (
Tc ((n +c n) +c n) +c Tc 1c)) |
47 | 46 | addceq1d 4389 |
. . . . . . 7
⊢ (n ∈ Nn → ( Tc
(((n +c n) +c n) +c 1c)
+c 2c) = (( Tc ((n
+c n)
+c n)
+c Tc
1c) +c
2c)) |
48 | 47 | eqeq2d 2364 |
. . . . . 6
⊢ (n ∈ Nn → ((((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
2c) ↔ (((n
+c n)
+c n)
+c 1c) = (( Tc ((n
+c n)
+c n)
+c Tc
1c) +c
2c))) |
49 | 41, 48 | mtbird 292 |
. . . . 5
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
2c)) |
50 | | id 19 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 1c) → A = (((n
+c n)
+c n)
+c 1c)) |
51 | | tceq 6158 |
. . . . . . . 8
⊢ (A = (((n
+c n)
+c n)
+c 1c) → Tc A =
Tc (((n +c n) +c n) +c
1c)) |
52 | 51 | addceq1d 4389 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 1c) → ( Tc A
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
2c)) |
53 | 50, 52 | eqeq12d 2367 |
. . . . . 6
⊢ (A = (((n
+c n)
+c n)
+c 1c) → (A = ( Tc
A +c
2c) ↔ (((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
2c))) |
54 | 53 | notbid 285 |
. . . . 5
⊢ (A = (((n
+c n)
+c n)
+c 1c) → (¬ A = ( Tc
A +c
2c) ↔ ¬ (((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
2c))) |
55 | 49, 54 | syl5ibrcom 213 |
. . . 4
⊢ (n ∈ Nn → (A =
(((n +c n) +c n) +c 1c) →
¬ A = ( Tc A
+c 2c))) |
56 | | peano2 4403 |
. . . . . . . . 9
⊢ (n ∈ Nn → (n
+c 1c) ∈
Nn ) |
57 | | nntccl 6170 |
. . . . . . . . 9
⊢ ((n +c 1c) ∈ Nn → Tc (n
+c 1c) ∈
Nn ) |
58 | 56, 57 | syl 15 |
. . . . . . . 8
⊢ (n ∈ Nn → Tc
(n +c
1c) ∈ Nn ) |
59 | | nnc3p1n3p2 6280 |
. . . . . . . 8
⊢ (( Tc (n
+c 1c) ∈
Nn ∧ n ∈ Nn ) → ¬ ((( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c) = (((n
+c n)
+c n)
+c 2c)) |
60 | 58, 2, 59 | syl2anc 642 |
. . . . . . 7
⊢ (n ∈ Nn → ¬ ((( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c) = (((n
+c n)
+c n)
+c 2c)) |
61 | | eqcom 2355 |
. . . . . . 7
⊢ ((((n +c n) +c n) +c 2c) = (((
Tc (n +c 1c)
+c Tc (n +c 1c))
+c Tc (n +c 1c))
+c 1c) ↔ ((( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c) = (((n
+c n)
+c n)
+c 2c)) |
62 | 60, 61 | sylnibr 296 |
. . . . . 6
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 2c) = ((( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c)) |
63 | | addcass 4415 |
. . . . . . . . 9
⊢ ((((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c Tc n)
+c 1c) +c
1c) = (((( Tc
n +c
1c) +c ( Tc n
+c 1c)) +c Tc n)
+c (1c +c
1c)) |
64 | | addcass 4415 |
. . . . . . . . . 10
⊢ (((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c Tc n)
+c 1c) = ((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c ( Tc n
+c 1c)) |
65 | 64 | addceq1i 4386 |
. . . . . . . . 9
⊢ ((((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c Tc n)
+c 1c) +c
1c) = (((( Tc
n +c
1c) +c ( Tc n
+c 1c)) +c ( Tc n
+c 1c)) +c
1c) |
66 | | 1p1e2c 6155 |
. . . . . . . . . . . . . 14
⊢
(1c +c 1c) =
2c |
67 | 66 | addceq2i 4387 |
. . . . . . . . . . . . 13
⊢ (( Tc n
+c Tc n) +c (1c
+c 1c)) = (( Tc n
+c Tc n) +c
2c) |
68 | | addc4 4417 |
. . . . . . . . . . . . 13
⊢ (( Tc n
+c 1c) +c ( Tc n
+c 1c)) = (( Tc n
+c Tc n) +c (1c
+c 1c)) |
69 | | tc2c 6166 |
. . . . . . . . . . . . . 14
⊢ Tc 2c =
2c |
70 | 69 | addceq2i 4387 |
. . . . . . . . . . . . 13
⊢ (( Tc n
+c Tc n) +c Tc 2c) = (( Tc n
+c Tc n) +c
2c) |
71 | 67, 68, 70 | 3eqtr4i 2383 |
. . . . . . . . . . . 12
⊢ (( Tc n
+c 1c) +c ( Tc n
+c 1c)) = (( Tc n
+c Tc n) +c Tc 2c) |
72 | 71 | addceq1i 4386 |
. . . . . . . . . . 11
⊢ ((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c Tc n) =
((( Tc n +c Tc n)
+c Tc
2c) +c Tc n) |
73 | | addc32 4416 |
. . . . . . . . . . 11
⊢ ((( Tc n
+c Tc n) +c Tc 2c) +c
Tc n) = ((( Tc
n +c Tc n)
+c Tc n) +c Tc 2c) |
74 | 72, 73 | eqtri 2373 |
. . . . . . . . . 10
⊢ ((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c Tc n) =
((( Tc n +c Tc n)
+c Tc n) +c Tc 2c) |
75 | 74, 66 | addceq12i 4388 |
. . . . . . . . 9
⊢ (((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c Tc n)
+c (1c +c
1c)) = (((( Tc
n +c Tc n)
+c Tc n) +c Tc 2c) +c
2c) |
76 | 63, 65, 75 | 3eqtr3ri 2382 |
. . . . . . . 8
⊢ (((( Tc n
+c Tc n) +c Tc n)
+c Tc
2c) +c 2c) = (((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c ( Tc n
+c 1c)) +c
1c) |
77 | | 2nc 6168 |
. . . . . . . . . . 11
⊢
2c ∈ NC |
78 | | tcdi 6164 |
. . . . . . . . . . 11
⊢ ((((n +c n) +c n) ∈ NC ∧
2c ∈ NC ) → Tc
(((n +c n) +c n) +c 2c) = (
Tc ((n +c n) +c n) +c Tc 2c)) |
79 | 43, 77, 78 | sylancl 643 |
. . . . . . . . . 10
⊢ (n ∈ Nn → Tc
(((n +c n) +c n) +c 2c) = (
Tc ((n +c n) +c n) +c Tc 2c)) |
80 | 16 | addceq1d 4389 |
. . . . . . . . . 10
⊢ (n ∈ Nn → ( Tc
((n +c n) +c n) +c Tc 2c) = ((( Tc n
+c Tc n) +c Tc n)
+c Tc
2c)) |
81 | 79, 80 | eqtrd 2385 |
. . . . . . . . 9
⊢ (n ∈ Nn → Tc
(((n +c n) +c n) +c 2c) = (((
Tc n +c Tc n)
+c Tc n) +c Tc 2c)) |
82 | 81 | addceq1d 4389 |
. . . . . . . 8
⊢ (n ∈ Nn → ( Tc
(((n +c n) +c n) +c 2c)
+c 2c) = (((( Tc n
+c Tc n) +c Tc n)
+c Tc
2c) +c
2c)) |
83 | | tcdi 6164 |
. . . . . . . . . . . . 13
⊢ ((n ∈ NC ∧
1c ∈ NC ) → Tc
(n +c
1c) = ( Tc n +c Tc 1c)) |
84 | 10, 44, 83 | sylancl 643 |
. . . . . . . . . . . 12
⊢ (n ∈ Nn → Tc
(n +c
1c) = ( Tc n +c Tc 1c)) |
85 | 37 | addceq2i 4387 |
. . . . . . . . . . . 12
⊢ ( Tc n
+c Tc
1c) = ( Tc n +c
1c) |
86 | 84, 85 | syl6eq 2401 |
. . . . . . . . . . 11
⊢ (n ∈ Nn → Tc
(n +c
1c) = ( Tc n +c
1c)) |
87 | 86, 86 | addceq12d 4391 |
. . . . . . . . . 10
⊢ (n ∈ Nn → ( Tc
(n +c
1c) +c Tc (n
+c 1c)) = (( Tc n
+c 1c) +c ( Tc n
+c 1c))) |
88 | 87, 86 | addceq12d 4391 |
. . . . . . . . 9
⊢ (n ∈ Nn → (( Tc
(n +c
1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) = ((( Tc n
+c 1c) +c ( Tc n
+c 1c)) +c ( Tc n
+c 1c))) |
89 | 88 | addceq1d 4389 |
. . . . . . . 8
⊢ (n ∈ Nn → ((( Tc
(n +c
1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c) = (((( Tc
n +c
1c) +c ( Tc n
+c 1c)) +c ( Tc n
+c 1c)) +c
1c)) |
90 | 76, 82, 89 | 3eqtr4a 2411 |
. . . . . . 7
⊢ (n ∈ Nn → ( Tc
(((n +c n) +c n) +c 2c)
+c 2c) = ((( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c)) |
91 | 90 | eqeq2d 2364 |
. . . . . 6
⊢ (n ∈ Nn → ((((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
2c) ↔ (((n
+c n)
+c n)
+c 2c) = ((( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) +c
1c))) |
92 | 62, 91 | mtbird 292 |
. . . . 5
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
2c)) |
93 | | id 19 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 2c) → A = (((n
+c n)
+c n)
+c 2c)) |
94 | | tceq 6158 |
. . . . . . . 8
⊢ (A = (((n
+c n)
+c n)
+c 2c) → Tc A =
Tc (((n +c n) +c n) +c
2c)) |
95 | 94 | addceq1d 4389 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 2c) → ( Tc A
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
2c)) |
96 | 93, 95 | eqeq12d 2367 |
. . . . . 6
⊢ (A = (((n
+c n)
+c n)
+c 2c) → (A = ( Tc
A +c
2c) ↔ (((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
2c))) |
97 | 96 | notbid 285 |
. . . . 5
⊢ (A = (((n
+c n)
+c n)
+c 2c) → (¬ A = ( Tc
A +c
2c) ↔ ¬ (((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
2c))) |
98 | 92, 97 | syl5ibrcom 213 |
. . . 4
⊢ (n ∈ Nn → (A =
(((n +c n) +c n) +c 2c) →
¬ A = ( Tc A
+c 2c))) |
99 | 25, 55, 98 | 3jaod 1246 |
. . 3
⊢ (n ∈ Nn → ((A =
((n +c n) +c n) ∨ A = (((n
+c n)
+c n)
+c 1c) ∨
A = (((n +c n) +c n) +c 2c))
→ ¬ A = ( Tc A
+c 2c))) |
100 | 99 | rexlimiv 2732 |
. 2
⊢ (∃n ∈ Nn (A = ((n
+c n)
+c n) ∨ A =
(((n +c n) +c n) +c 1c) ∨ A =
(((n +c n) +c n) +c 2c))
→ ¬ A = ( Tc A
+c 2c)) |
101 | 1, 100 | syl 15 |
1
⊢ (A ∈ Nn → ¬ A =
( Tc A +c
2c)) |