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 | | nnc3n3p1 6278 |
. . . . . . 7
⊢ ((n ∈ Nn ∧ Tc n
∈ Nn ) →
¬ ((n +c n) +c n) = ((( Tc
n +c Tc n)
+c Tc n) +c
1c)) |
5 | 2, 3, 4 | syl2anc 642 |
. . . . . 6
⊢ (n ∈ Nn → ¬ ((n
+c n)
+c n) = ((( Tc n
+c Tc n) +c Tc n)
+c 1c)) |
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 1c) = (((
Tc n +c Tc n)
+c Tc n) +c
1c)) |
18 | 17 | eqeq2d 2364 |
. . . . . 6
⊢ (n ∈ Nn → (((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 1c) ↔ ((n +c n) +c n) = ((( Tc
n +c Tc n)
+c Tc n) +c
1c))) |
19 | 5, 18 | mtbird 292 |
. . . . 5
⊢ (n ∈ Nn → ¬ ((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 1c)) |
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 1c) = ( Tc ((n
+c n)
+c n)
+c 1c)) |
23 | 20, 22 | eqeq12d 2367 |
. . . . . 6
⊢ (A = ((n
+c n)
+c n) → (A = ( Tc
A +c
1c) ↔ ((n
+c n)
+c n) = ( Tc ((n
+c n)
+c n)
+c 1c))) |
24 | 23 | notbid 285 |
. . . . 5
⊢ (A = ((n
+c n)
+c n) → (¬
A = ( Tc A
+c 1c) ↔ ¬ ((n +c n) +c n) = ( Tc
((n +c n) +c n) +c
1c))) |
25 | 19, 24 | syl5ibrcom 213 |
. . . 4
⊢ (n ∈ Nn → (A =
((n +c n) +c n) → ¬ A = ( Tc
A +c
1c))) |
26 | | nncaddccl 4419 |
. . . . . . . . . . . 12
⊢ (((n +c n) ∈ Nn ∧ n ∈ Nn ) → ((n
+c n)
+c n) ∈ Nn
) |
27 | 7, 2, 26 | syl2anc 642 |
. . . . . . . . . . 11
⊢ (n ∈ Nn → ((n
+c n)
+c n) ∈ Nn
) |
28 | | nnnc 6146 |
. . . . . . . . . . 11
⊢ (((n +c n) +c n) ∈ Nn → ((n
+c n)
+c n) ∈ NC
) |
29 | 27, 28 | syl 15 |
. . . . . . . . . 10
⊢ (n ∈ Nn → ((n
+c n)
+c n) ∈ NC
) |
30 | | 1cnc 6139 |
. . . . . . . . . 10
⊢
1c ∈ NC |
31 | | tcdi 6164 |
. . . . . . . . . 10
⊢ ((((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)) |
32 | 29, 30, 31 | sylancl 643 |
. . . . . . . . 9
⊢ (n ∈ Nn → Tc
(((n +c n) +c n) +c 1c) = (
Tc ((n +c n) +c n) +c Tc 1c)) |
33 | | tc1c 6165 |
. . . . . . . . . . 11
⊢ Tc 1c =
1c |
34 | 33 | a1i 10 |
. . . . . . . . . 10
⊢ (n ∈ Nn → Tc
1c = 1c) |
35 | 16, 34 | addceq12d 4391 |
. . . . . . . . 9
⊢ (n ∈ Nn → ( Tc
((n +c n) +c n) +c Tc 1c) = ((( Tc n
+c Tc n) +c Tc n)
+c 1c)) |
36 | 32, 35 | eqtrd 2385 |
. . . . . . . 8
⊢ (n ∈ Nn → Tc
(((n +c n) +c n) +c 1c) = (((
Tc n +c Tc n)
+c Tc n) +c
1c)) |
37 | 36 | eqeq2d 2364 |
. . . . . . 7
⊢ (n ∈ Nn → (((n
+c n)
+c n) = Tc (((n
+c n)
+c n)
+c 1c) ↔ ((n +c n) +c n) = ((( Tc
n +c Tc n)
+c Tc n) +c
1c))) |
38 | 5, 37 | mtbird 292 |
. . . . . 6
⊢ (n ∈ Nn → ¬ ((n
+c n)
+c n) = Tc (((n
+c n)
+c n)
+c 1c)) |
39 | | peano2 4403 |
. . . . . . . . 9
⊢ (((n +c n) +c n) ∈ Nn → (((n
+c n)
+c n)
+c 1c) ∈
Nn ) |
40 | 27, 39 | syl 15 |
. . . . . . . 8
⊢ (n ∈ Nn → (((n
+c n)
+c n)
+c 1c) ∈
Nn ) |
41 | | nntccl 6170 |
. . . . . . . 8
⊢ ((((n +c n) +c n) +c 1c) ∈ Nn → Tc (((n
+c n)
+c n)
+c 1c) ∈
Nn ) |
42 | 40, 41 | syl 15 |
. . . . . . 7
⊢ (n ∈ Nn → Tc
(((n +c n) +c n) +c 1c) ∈ Nn
) |
43 | | suc11nnc 4558 |
. . . . . . 7
⊢ ((((n +c n) +c n) ∈ Nn ∧ Tc (((n
+c n)
+c n)
+c 1c) ∈
Nn ) → ((((n +c n) +c n) +c 1c) = (
Tc (((n +c n) +c n) +c 1c)
+c 1c) ↔ ((n +c n) +c n) = Tc
(((n +c n) +c n) +c
1c))) |
44 | 27, 42, 43 | syl2anc 642 |
. . . . . 6
⊢ (n ∈ Nn → ((((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
1c) ↔ ((n
+c n)
+c n) = Tc (((n
+c n)
+c n)
+c 1c))) |
45 | 38, 44 | mtbird 292 |
. . . . 5
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
1c)) |
46 | | id 19 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 1c) → A = (((n
+c n)
+c n)
+c 1c)) |
47 | | tceq 6158 |
. . . . . . . 8
⊢ (A = (((n
+c n)
+c n)
+c 1c) → Tc A =
Tc (((n +c n) +c n) +c
1c)) |
48 | 47 | addceq1d 4389 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 1c) → ( Tc A
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
1c)) |
49 | 46, 48 | eqeq12d 2367 |
. . . . . 6
⊢ (A = (((n
+c n)
+c n)
+c 1c) → (A = ( Tc
A +c
1c) ↔ (((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
1c))) |
50 | 49 | notbid 285 |
. . . . 5
⊢ (A = (((n
+c n)
+c n)
+c 1c) → (¬ A = ( Tc
A +c
1c) ↔ ¬ (((n
+c n)
+c n)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 1c) +c
1c))) |
51 | 45, 50 | syl5ibrcom 213 |
. . . 4
⊢ (n ∈ Nn → (A =
(((n +c n) +c n) +c 1c) →
¬ A = ( Tc A
+c 1c))) |
52 | | peano2 4403 |
. . . . . . . . 9
⊢ (n ∈ Nn → (n
+c 1c) ∈
Nn ) |
53 | | nntccl 6170 |
. . . . . . . . 9
⊢ ((n +c 1c) ∈ Nn → Tc (n
+c 1c) ∈
Nn ) |
54 | 52, 53 | syl 15 |
. . . . . . . 8
⊢ (n ∈ Nn → Tc
(n +c
1c) ∈ Nn ) |
55 | | nnc3n3p2 6279 |
. . . . . . . 8
⊢ (( Tc (n
+c 1c) ∈
Nn ∧ n ∈ Nn ) → ¬ (( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) = (((n +c n) +c n) +c
2c)) |
56 | 54, 2, 55 | syl2anc 642 |
. . . . . . 7
⊢ (n ∈ Nn → ¬ (( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c)) = (((n +c n) +c n) +c
2c)) |
57 | | 2nnc 6167 |
. . . . . . . . . . . . . 14
⊢
2c ∈ Nn |
58 | | nncaddccl 4419 |
. . . . . . . . . . . . . 14
⊢ ((((n +c n) +c n) ∈ Nn ∧
2c ∈ Nn ) → (((n
+c n)
+c n)
+c 2c) ∈
Nn ) |
59 | 27, 57, 58 | sylancl 643 |
. . . . . . . . . . . . 13
⊢ (n ∈ Nn → (((n
+c n)
+c n)
+c 2c) ∈
Nn ) |
60 | | nnnc 6146 |
. . . . . . . . . . . . 13
⊢ ((((n +c n) +c n) +c 2c) ∈ Nn →
(((n +c n) +c n) +c 2c) ∈ NC
) |
61 | 59, 60 | syl 15 |
. . . . . . . . . . . 12
⊢ (n ∈ Nn → (((n
+c n)
+c n)
+c 2c) ∈
NC ) |
62 | | tcdi 6164 |
. . . . . . . . . . . 12
⊢ (((((n +c n) +c n) +c 2c) ∈ NC ∧ 1c ∈ NC ) → Tc ((((n
+c n)
+c n)
+c 2c) +c
1c) = ( Tc
(((n +c n) +c n) +c 2c)
+c Tc
1c)) |
63 | 61, 30, 62 | sylancl 643 |
. . . . . . . . . . 11
⊢ (n ∈ Nn → Tc
((((n +c n) +c n) +c 2c)
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c Tc 1c)) |
64 | 63 | eqcomd 2358 |
. . . . . . . . . 10
⊢ (n ∈ Nn → ( Tc
(((n +c n) +c n) +c 2c)
+c Tc
1c) = Tc ((((n +c n) +c n) +c 2c)
+c 1c)) |
65 | 33 | addceq2i 4387 |
. . . . . . . . . 10
⊢ ( Tc (((n
+c n)
+c n)
+c 2c) +c Tc 1c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
1c) |
66 | | addccom 4406 |
. . . . . . . . . . . . . . . . 17
⊢
((1c +c 1c)
+c n) = (n +c (1c
+c 1c)) |
67 | | 1p1e2c 6155 |
. . . . . . . . . . . . . . . . . 18
⊢
(1c +c 1c) =
2c |
68 | 67 | addceq2i 4387 |
. . . . . . . . . . . . . . . . 17
⊢ (n +c (1c
+c 1c)) = (n +c
2c) |
69 | 66, 68 | eqtr2i 2374 |
. . . . . . . . . . . . . . . 16
⊢ (n +c 2c) =
((1c +c 1c)
+c n) |
70 | 69 | addceq1i 4386 |
. . . . . . . . . . . . . . 15
⊢ ((n +c 2c)
+c 1c) = (((1c
+c 1c) +c n) +c
1c) |
71 | | addcass 4415 |
. . . . . . . . . . . . . . 15
⊢ ((n +c 2c)
+c 1c) = (n +c (2c
+c 1c)) |
72 | | addcass 4415 |
. . . . . . . . . . . . . . 15
⊢
(((1c +c 1c)
+c n)
+c 1c) = ((1c
+c 1c) +c (n +c
1c)) |
73 | 70, 71, 72 | 3eqtr3i 2381 |
. . . . . . . . . . . . . 14
⊢ (n +c (2c
+c 1c)) = ((1c
+c 1c) +c (n +c
1c)) |
74 | 73 | addceq2i 4387 |
. . . . . . . . . . . . 13
⊢ ((n +c n) +c (n +c (2c
+c 1c))) = ((n +c n) +c ((1c
+c 1c) +c (n +c
1c))) |
75 | | addcass 4415 |
. . . . . . . . . . . . 13
⊢ (((n +c n) +c n) +c (2c
+c 1c)) = ((n +c n) +c (n +c (2c
+c 1c))) |
76 | | addcass 4415 |
. . . . . . . . . . . . 13
⊢ (((n +c n) +c (1c
+c 1c)) +c (n +c 1c)) =
((n +c n) +c ((1c
+c 1c) +c (n +c
1c))) |
77 | 74, 75, 76 | 3eqtr4i 2383 |
. . . . . . . . . . . 12
⊢ (((n +c n) +c n) +c (2c
+c 1c)) = (((n +c n) +c (1c
+c 1c)) +c (n +c
1c)) |
78 | | addcass 4415 |
. . . . . . . . . . . 12
⊢ ((((n +c n) +c n) +c 2c)
+c 1c) = (((n +c n) +c n) +c (2c
+c 1c)) |
79 | | addc4 4417 |
. . . . . . . . . . . . 13
⊢ ((n +c 1c)
+c (n
+c 1c)) = ((n +c n) +c (1c
+c 1c)) |
80 | 79 | addceq1i 4386 |
. . . . . . . . . . . 12
⊢ (((n +c 1c)
+c (n
+c 1c)) +c (n +c 1c)) =
(((n +c n) +c (1c
+c 1c)) +c (n +c
1c)) |
81 | 77, 78, 80 | 3eqtr4i 2383 |
. . . . . . . . . . 11
⊢ ((((n +c n) +c n) +c 2c)
+c 1c) = (((n +c 1c)
+c (n
+c 1c)) +c (n +c
1c)) |
82 | | tceq 6158 |
. . . . . . . . . . 11
⊢ (((((n +c n) +c n) +c 2c)
+c 1c) = (((n +c 1c)
+c (n
+c 1c)) +c (n +c 1c)) →
Tc ((((n +c n) +c n) +c 2c)
+c 1c) = Tc (((n
+c 1c) +c (n +c 1c))
+c (n
+c 1c))) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . . 10
⊢ Tc ((((n
+c n)
+c n)
+c 2c) +c
1c) = Tc (((n +c 1c)
+c (n
+c 1c)) +c (n +c
1c)) |
84 | 64, 65, 83 | 3eqtr3g 2408 |
. . . . . . . . 9
⊢ (n ∈ Nn → ( Tc
(((n +c n) +c n) +c 2c)
+c 1c) = Tc (((n
+c 1c) +c (n +c 1c))
+c (n
+c 1c))) |
85 | | nnnc 6146 |
. . . . . . . . . . . . 13
⊢ ((n +c 1c) ∈ Nn → (n +c 1c) ∈ NC
) |
86 | 52, 85 | syl 15 |
. . . . . . . . . . . 12
⊢ (n ∈ Nn → (n
+c 1c) ∈
NC ) |
87 | | ncaddccl 6144 |
. . . . . . . . . . . 12
⊢ (((n +c 1c) ∈ NC ∧ (n
+c 1c) ∈
NC ) → ((n +c 1c)
+c (n
+c 1c)) ∈
NC ) |
88 | 86, 86, 87 | syl2anc 642 |
. . . . . . . . . . 11
⊢ (n ∈ Nn → ((n
+c 1c) +c (n +c 1c)) ∈ NC
) |
89 | | tcdi 6164 |
. . . . . . . . . . 11
⊢ ((((n +c 1c)
+c (n
+c 1c)) ∈
NC ∧ (n +c 1c) ∈ NC ) → Tc (((n
+c 1c) +c (n +c 1c))
+c (n
+c 1c)) = ( Tc ((n
+c 1c) +c (n +c 1c))
+c Tc (n +c
1c))) |
90 | 88, 86, 89 | syl2anc 642 |
. . . . . . . . . 10
⊢ (n ∈ Nn → Tc
(((n +c
1c) +c (n +c 1c))
+c (n
+c 1c)) = ( Tc ((n
+c 1c) +c (n +c 1c))
+c Tc (n +c
1c))) |
91 | | tcdi 6164 |
. . . . . . . . . . . 12
⊢ (((n +c 1c) ∈ NC ∧ (n
+c 1c) ∈
NC ) → Tc ((n
+c 1c) +c (n +c 1c)) = (
Tc (n +c 1c)
+c Tc (n +c
1c))) |
92 | 86, 86, 91 | syl2anc 642 |
. . . . . . . . . . 11
⊢ (n ∈ Nn → Tc
((n +c
1c) +c (n +c 1c)) = (
Tc (n +c 1c)
+c Tc (n +c
1c))) |
93 | 92 | addceq1d 4389 |
. . . . . . . . . 10
⊢ (n ∈ Nn → ( Tc
((n +c
1c) +c (n +c 1c))
+c Tc (n +c 1c)) = ((
Tc (n +c 1c)
+c Tc (n +c 1c))
+c Tc (n +c
1c))) |
94 | 90, 93 | eqtrd 2385 |
. . . . . . . . 9
⊢ (n ∈ Nn → Tc
(((n +c
1c) +c (n +c 1c))
+c (n
+c 1c)) = (( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c))) |
95 | 84, 94 | eqtrd 2385 |
. . . . . . . 8
⊢ (n ∈ Nn → ( Tc
(((n +c n) +c n) +c 2c)
+c 1c) = (( Tc (n
+c 1c) +c Tc (n
+c 1c)) +c Tc (n
+c 1c))) |
96 | 95 | eqeq1d 2361 |
. . . . . . 7
⊢ (n ∈ Nn → (( Tc
(((n +c n) +c n) +c 2c)
+c 1c) = (((n +c n) +c n) +c 2c) ↔
(( Tc (n +c 1c)
+c Tc (n +c 1c))
+c Tc (n +c 1c)) =
(((n +c n) +c n) +c
2c))) |
97 | 56, 96 | mtbird 292 |
. . . . . 6
⊢ (n ∈ Nn → ¬ ( Tc (((n
+c n)
+c n)
+c 2c) +c
1c) = (((n
+c n)
+c n)
+c 2c)) |
98 | | eqcom 2355 |
. . . . . 6
⊢ (( Tc (((n
+c n)
+c n)
+c 2c) +c
1c) = (((n
+c n)
+c n)
+c 2c) ↔ (((n +c n) +c n) +c 2c) = (
Tc (((n +c n) +c n) +c 2c)
+c 1c)) |
99 | 97, 98 | sylnib 295 |
. . . . 5
⊢ (n ∈ Nn → ¬ (((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
1c)) |
100 | | id 19 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 2c) → A = (((n
+c n)
+c n)
+c 2c)) |
101 | | tceq 6158 |
. . . . . . . 8
⊢ (A = (((n
+c n)
+c n)
+c 2c) → Tc A =
Tc (((n +c n) +c n) +c
2c)) |
102 | 101 | addceq1d 4389 |
. . . . . . 7
⊢ (A = (((n
+c n)
+c n)
+c 2c) → ( Tc A
+c 1c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
1c)) |
103 | 100, 102 | eqeq12d 2367 |
. . . . . 6
⊢ (A = (((n
+c n)
+c n)
+c 2c) → (A = ( Tc
A +c
1c) ↔ (((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
1c))) |
104 | 103 | notbid 285 |
. . . . 5
⊢ (A = (((n
+c n)
+c n)
+c 2c) → (¬ A = ( Tc
A +c
1c) ↔ ¬ (((n
+c n)
+c n)
+c 2c) = ( Tc (((n
+c n)
+c n)
+c 2c) +c
1c))) |
105 | 99, 104 | syl5ibrcom 213 |
. . . 4
⊢ (n ∈ Nn → (A =
(((n +c n) +c n) +c 2c) →
¬ A = ( Tc A
+c 1c))) |
106 | 25, 51, 105 | 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 1c))) |
107 | 106 | 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 1c)) |
108 | 1, 107 | syl 15 |
1
⊢ (A ∈ Nn → ¬ A =
( Tc A +c
1c)) |