Step | Hyp | Ref
| Expression |
1 | | nncdiv3lem2 6276 |
. 2
⊢ {a ∣ ∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))}
∈ V |
2 | | eqeq1 2359 |
. . . 4
⊢ (a = 0c → (a = ((n
+c n)
+c n) ↔
0c = ((n
+c n)
+c n))) |
3 | | eqeq1 2359 |
. . . 4
⊢ (a = 0c → (a = (((n
+c n)
+c n)
+c 1c) ↔ 0c =
(((n +c n) +c n) +c
1c))) |
4 | | eqeq1 2359 |
. . . 4
⊢ (a = 0c → (a = (((n
+c n)
+c n)
+c 2c) ↔ 0c =
(((n +c n) +c n) +c
2c))) |
5 | 2, 3, 4 | 3orbi123d 1251 |
. . 3
⊢ (a = 0c → ((a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ (0c = ((n
+c n)
+c n) ∨ 0c = (((n +c n) +c n) +c 1c) ∨ 0c = (((n +c n) +c n) +c
2c)))) |
6 | 5 | rexbidv 2635 |
. 2
⊢ (a = 0c → (∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ ∃n ∈ Nn (0c = ((n +c n) +c n) ∨
0c = (((n
+c n)
+c n)
+c 1c) ∨
0c = (((n
+c n)
+c n)
+c 2c)))) |
7 | | eqeq1 2359 |
. . . 4
⊢ (a = m →
(a = ((n +c n) +c n) ↔ m =
((n +c n) +c n))) |
8 | | eqeq1 2359 |
. . . 4
⊢ (a = m →
(a = (((n +c n) +c n) +c 1c) ↔
m = (((n +c n) +c n) +c
1c))) |
9 | | eqeq1 2359 |
. . . 4
⊢ (a = m →
(a = (((n +c n) +c n) +c 2c) ↔
m = (((n +c n) +c n) +c
2c))) |
10 | 7, 8, 9 | 3orbi123d 1251 |
. . 3
⊢ (a = m →
((a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c) ∨
a = (((n +c n) +c n) +c 2c))
↔ (m = ((n +c n) +c n) ∨ m = (((n
+c n)
+c n)
+c 1c) ∨
m = (((n +c n) +c n) +c
2c)))) |
11 | 10 | rexbidv 2635 |
. 2
⊢ (a = m →
(∃n
∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ ∃n ∈ Nn (m = ((n +c n) +c n) ∨ m = (((n
+c n)
+c n)
+c 1c) ∨
m = (((n +c n) +c n) +c
2c)))) |
12 | | eqeq1 2359 |
. . . 4
⊢ (a = (m
+c 1c) → (a = ((n
+c n)
+c n) ↔ (m +c 1c) =
((n +c n) +c n))) |
13 | | eqeq1 2359 |
. . . 4
⊢ (a = (m
+c 1c) → (a = (((n
+c n)
+c n)
+c 1c) ↔ (m +c 1c) =
(((n +c n) +c n) +c
1c))) |
14 | | eqeq1 2359 |
. . . 4
⊢ (a = (m
+c 1c) → (a = (((n
+c n)
+c n)
+c 2c) ↔ (m +c 1c) =
(((n +c n) +c n) +c
2c))) |
15 | 12, 13, 14 | 3orbi123d 1251 |
. . 3
⊢ (a = (m
+c 1c) → ((a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ ((m +c
1c) = ((n
+c n)
+c n) ∨ (m
+c 1c) = (((n +c n) +c n) +c 1c) ∨ (m
+c 1c) = (((n +c n) +c n) +c
2c)))) |
16 | 15 | rexbidv 2635 |
. 2
⊢ (a = (m
+c 1c) → (∃n ∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ ∃n ∈ Nn ((m
+c 1c) = ((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ (m
+c 1c) = (((n +c n) +c n) +c
2c)))) |
17 | | eqeq1 2359 |
. . . 4
⊢ (a = A →
(a = ((n +c n) +c n) ↔ A =
((n +c n) +c n))) |
18 | | eqeq1 2359 |
. . . 4
⊢ (a = A →
(a = (((n +c n) +c n) +c 1c) ↔
A = (((n +c n) +c n) +c
1c))) |
19 | | eqeq1 2359 |
. . . 4
⊢ (a = A →
(a = (((n +c n) +c n) +c 2c) ↔
A = (((n +c n) +c n) +c
2c))) |
20 | 17, 18, 19 | 3orbi123d 1251 |
. . 3
⊢ (a = A →
((a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c) ∨
a = (((n +c n) +c n) +c 2c))
↔ (A = ((n +c n) +c n) ∨ A = (((n
+c n)
+c n)
+c 1c) ∨
A = (((n +c n) +c n) +c
2c)))) |
21 | 20 | rexbidv 2635 |
. 2
⊢ (a = A →
(∃n
∈ Nn (a = ((n
+c n)
+c n) ∨ a =
(((n +c n) +c n) +c 1c) ∨ a =
(((n +c n) +c n) +c 2c))
↔ ∃n ∈ Nn (A = ((n +c n) +c n) ∨ A = (((n
+c n)
+c n)
+c 1c) ∨
A = (((n +c n) +c n) +c
2c)))) |
22 | | peano1 4402 |
. . 3
⊢
0c ∈ Nn |
23 | | addcid1 4405 |
. . . . 5
⊢
((0c +c 0c)
+c 0c) = (0c
+c 0c) |
24 | | addcid2 4407 |
. . . . 5
⊢
(0c +c 0c) =
0c |
25 | 23, 24 | eqtr2i 2374 |
. . . 4
⊢
0c = ((0c +c
0c) +c
0c) |
26 | | 3mix1 1124 |
. . . 4
⊢
(0c = ((0c +c
0c) +c 0c) →
(0c = ((0c +c
0c) +c 0c) ∨ 0c = (((0c
+c 0c) +c
0c) +c 1c) ∨ 0c = (((0c
+c 0c) +c
0c) +c
2c))) |
27 | 25, 26 | ax-mp 5 |
. . 3
⊢
(0c = ((0c +c
0c) +c 0c) ∨ 0c = (((0c
+c 0c) +c
0c) +c 1c) ∨ 0c = (((0c
+c 0c) +c
0c) +c
2c)) |
28 | | addceq12 4385 |
. . . . . . . 8
⊢ ((n = 0c ∧ n =
0c) → (n
+c n) =
(0c +c
0c)) |
29 | 28 | anidms 626 |
. . . . . . 7
⊢ (n = 0c → (n +c n) = (0c +c
0c)) |
30 | | id 19 |
. . . . . . 7
⊢ (n = 0c → n = 0c) |
31 | 29, 30 | addceq12d 4391 |
. . . . . 6
⊢ (n = 0c → ((n +c n) +c n) = ((0c +c
0c) +c
0c)) |
32 | 31 | eqeq2d 2364 |
. . . . 5
⊢ (n = 0c →
(0c = ((n
+c n)
+c n) ↔
0c = ((0c +c
0c) +c
0c))) |
33 | 31 | addceq1d 4389 |
. . . . . 6
⊢ (n = 0c → (((n +c n) +c n) +c 1c) =
(((0c +c 0c)
+c 0c) +c
1c)) |
34 | 33 | eqeq2d 2364 |
. . . . 5
⊢ (n = 0c →
(0c = (((n
+c n)
+c n)
+c 1c) ↔ 0c =
(((0c +c 0c)
+c 0c) +c
1c))) |
35 | 31 | addceq1d 4389 |
. . . . . 6
⊢ (n = 0c → (((n +c n) +c n) +c 2c) =
(((0c +c 0c)
+c 0c) +c
2c)) |
36 | 35 | eqeq2d 2364 |
. . . . 5
⊢ (n = 0c →
(0c = (((n
+c n)
+c n)
+c 2c) ↔ 0c =
(((0c +c 0c)
+c 0c) +c
2c))) |
37 | 32, 34, 36 | 3orbi123d 1251 |
. . . 4
⊢ (n = 0c →
((0c = ((n
+c n)
+c n) ∨ 0c = (((n +c n) +c n) +c 1c) ∨ 0c = (((n +c n) +c n) +c 2c))
↔ (0c = ((0c +c
0c) +c 0c) ∨ 0c = (((0c
+c 0c) +c
0c) +c 1c) ∨ 0c = (((0c
+c 0c) +c
0c) +c
2c)))) |
38 | 37 | rspcev 2955 |
. . 3
⊢
((0c ∈ Nn ∧
(0c = ((0c +c
0c) +c 0c) ∨ 0c = (((0c
+c 0c) +c
0c) +c 1c) ∨ 0c = (((0c
+c 0c) +c
0c) +c 2c))) → ∃n ∈ Nn
(0c = ((n
+c n)
+c n) ∨ 0c = (((n +c n) +c n) +c 1c) ∨ 0c = (((n +c n) +c n) +c
2c))) |
39 | 22, 27, 38 | mp2an 653 |
. 2
⊢ ∃n ∈ Nn
(0c = ((n
+c n)
+c n) ∨ 0c = (((n +c n) +c n) +c 1c) ∨ 0c = (((n +c n) +c n) +c
2c)) |
40 | | addceq1 4383 |
. . . . . 6
⊢ (m = ((n
+c n)
+c n) → (m +c 1c) =
(((n +c n) +c n) +c
1c)) |
41 | 40 | reximi 2721 |
. . . . 5
⊢ (∃n ∈ Nn m = ((n
+c n)
+c n) → ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c
1c)) |
42 | 41 | a1i 10 |
. . . 4
⊢ (m ∈ Nn → (∃n ∈ Nn m = ((n +c n) +c n) → ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c
1c))) |
43 | | addceq1 4383 |
. . . . . . 7
⊢ (m = (((n
+c n)
+c n)
+c 1c) → (m +c 1c) =
((((n +c n) +c n) +c 1c)
+c 1c)) |
44 | | addcass 4415 |
. . . . . . . 8
⊢ ((((n +c n) +c n) +c 1c)
+c 1c) = (((n +c n) +c n) +c (1c
+c 1c)) |
45 | | 1p1e2c 6155 |
. . . . . . . . 9
⊢
(1c +c 1c) =
2c |
46 | 45 | addceq2i 4387 |
. . . . . . . 8
⊢ (((n +c n) +c n) +c (1c
+c 1c)) = (((n +c n) +c n) +c
2c) |
47 | 44, 46 | eqtri 2373 |
. . . . . . 7
⊢ ((((n +c n) +c n) +c 1c)
+c 1c) = (((n +c n) +c n) +c
2c) |
48 | 43, 47 | syl6eq 2401 |
. . . . . 6
⊢ (m = (((n
+c n)
+c n)
+c 1c) → (m +c 1c) =
(((n +c n) +c n) +c
2c)) |
49 | 48 | reximi 2721 |
. . . . 5
⊢ (∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c) → ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c
2c)) |
50 | 49 | a1i 10 |
. . . 4
⊢ (m ∈ Nn → (∃n ∈ Nn m = (((n +c n) +c n) +c 1c) →
∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c
2c))) |
51 | | peano2 4403 |
. . . . . . . . 9
⊢ (n ∈ Nn → (n
+c 1c) ∈
Nn ) |
52 | | addc32 4416 |
. . . . . . . . . . . 12
⊢ (((n +c n) +c n) +c 2c) =
(((n +c n) +c 2c)
+c n) |
53 | 45 | addceq2i 4387 |
. . . . . . . . . . . . . 14
⊢ ((n +c n) +c (1c
+c 1c)) = ((n +c n) +c
2c) |
54 | | addc4 4417 |
. . . . . . . . . . . . . 14
⊢ ((n +c n) +c (1c
+c 1c)) = ((n +c 1c)
+c (n
+c 1c)) |
55 | 53, 54 | eqtr3i 2375 |
. . . . . . . . . . . . 13
⊢ ((n +c n) +c 2c) =
((n +c
1c) +c (n +c
1c)) |
56 | 55 | addceq1i 4386 |
. . . . . . . . . . . 12
⊢ (((n +c n) +c 2c)
+c n) = (((n +c 1c)
+c (n
+c 1c)) +c n) |
57 | 52, 56 | eqtri 2373 |
. . . . . . . . . . 11
⊢ (((n +c n) +c n) +c 2c) =
(((n +c
1c) +c (n +c 1c))
+c n) |
58 | 57 | addceq1i 4386 |
. . . . . . . . . 10
⊢ ((((n +c n) +c n) +c 2c)
+c 1c) = ((((n +c 1c)
+c (n
+c 1c)) +c n) +c
1c) |
59 | | addcass 4415 |
. . . . . . . . . 10
⊢ ((((n +c 1c)
+c (n
+c 1c)) +c n) +c 1c) =
(((n +c
1c) +c (n +c 1c))
+c (n
+c 1c)) |
60 | 58, 59 | eqtri 2373 |
. . . . . . . . 9
⊢ ((((n +c n) +c n) +c 2c)
+c 1c) = (((n +c 1c)
+c (n
+c 1c)) +c (n +c
1c)) |
61 | | addceq12 4385 |
. . . . . . . . . . . . 13
⊢ ((a = (n
+c 1c) ∧
a = (n
+c 1c)) → (a +c a) = ((n
+c 1c) +c (n +c
1c))) |
62 | 61 | anidms 626 |
. . . . . . . . . . . 12
⊢ (a = (n
+c 1c) → (a +c a) = ((n
+c 1c) +c (n +c
1c))) |
63 | | id 19 |
. . . . . . . . . . . 12
⊢ (a = (n
+c 1c) → a = (n
+c 1c)) |
64 | 62, 63 | addceq12d 4391 |
. . . . . . . . . . 11
⊢ (a = (n
+c 1c) → ((a +c a) +c a) = (((n
+c 1c) +c (n +c 1c))
+c (n
+c 1c))) |
65 | 64 | eqeq2d 2364 |
. . . . . . . . . 10
⊢ (a = (n
+c 1c) → (((((n +c n) +c n) +c 2c)
+c 1c) = ((a +c a) +c a) ↔ ((((n
+c n)
+c n)
+c 2c) +c
1c) = (((n
+c 1c) +c (n +c 1c))
+c (n
+c 1c)))) |
66 | 65 | rspcev 2955 |
. . . . . . . . 9
⊢ (((n +c 1c) ∈ Nn ∧ ((((n
+c n)
+c n)
+c 2c) +c
1c) = (((n
+c 1c) +c (n +c 1c))
+c (n
+c 1c))) → ∃a ∈ Nn ((((n +c n) +c n) +c 2c)
+c 1c) = ((a +c a) +c a)) |
67 | 51, 60, 66 | sylancl 643 |
. . . . . . . 8
⊢ (n ∈ Nn → ∃a ∈ Nn ((((n
+c n)
+c n)
+c 2c) +c
1c) = ((a
+c a)
+c a)) |
68 | | addceq1 4383 |
. . . . . . . . . 10
⊢ (m = (((n
+c n)
+c n)
+c 2c) → (m +c 1c) =
((((n +c n) +c n) +c 2c)
+c 1c)) |
69 | 68 | eqeq1d 2361 |
. . . . . . . . 9
⊢ (m = (((n
+c n)
+c n)
+c 2c) → ((m +c 1c) =
((a +c a) +c a) ↔ ((((n
+c n)
+c n)
+c 2c) +c
1c) = ((a
+c a)
+c a))) |
70 | 69 | rexbidv 2635 |
. . . . . . . 8
⊢ (m = (((n
+c n)
+c n)
+c 2c) → (∃a ∈ Nn (m +c 1c) =
((a +c a) +c a) ↔ ∃a ∈ Nn ((((n +c n) +c n) +c 2c)
+c 1c) = ((a +c a) +c a))) |
71 | 67, 70 | syl5ibrcom 213 |
. . . . . . 7
⊢ (n ∈ Nn → (m =
(((n +c n) +c n) +c 2c) →
∃a ∈ Nn (m +c 1c) =
((a +c a) +c a))) |
72 | 71 | rexlimiv 2732 |
. . . . . 6
⊢ (∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c) → ∃a ∈ Nn (m +c 1c) =
((a +c a) +c a)) |
73 | | addceq12 4385 |
. . . . . . . . . 10
⊢ ((a = n ∧ a = n) → (a
+c a) = (n +c n)) |
74 | 73 | anidms 626 |
. . . . . . . . 9
⊢ (a = n →
(a +c a) = (n
+c n)) |
75 | | id 19 |
. . . . . . . . 9
⊢ (a = n →
a = n) |
76 | 74, 75 | addceq12d 4391 |
. . . . . . . 8
⊢ (a = n →
((a +c a) +c a) = ((n
+c n)
+c n)) |
77 | 76 | eqeq2d 2364 |
. . . . . . 7
⊢ (a = n →
((m +c
1c) = ((a
+c a)
+c a) ↔ (m +c 1c) =
((n +c n) +c n))) |
78 | 77 | cbvrexv 2836 |
. . . . . 6
⊢ (∃a ∈ Nn (m +c 1c) =
((a +c a) +c a) ↔ ∃n ∈ Nn (m +c 1c) =
((n +c n) +c n)) |
79 | 72, 78 | sylib 188 |
. . . . 5
⊢ (∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c) → ∃n ∈ Nn (m +c 1c) =
((n +c n) +c n)) |
80 | 79 | a1i 10 |
. . . 4
⊢ (m ∈ Nn → (∃n ∈ Nn m = (((n +c n) +c n) +c 2c) →
∃n ∈ Nn (m +c 1c) =
((n +c n) +c n))) |
81 | 42, 50, 80 | 3orim123d 1260 |
. . 3
⊢ (m ∈ Nn → ((∃n ∈ Nn m = ((n +c n) +c n) ∨ ∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c) ∨
∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c)) → (∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c) ∨ ∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n)))) |
82 | | df-3or 935 |
. . . . 5
⊢ ((m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c) ∨ m =
(((n +c n) +c n) +c 2c))
↔ ((m = ((n +c n) +c n) ∨ m = (((n
+c n)
+c n)
+c 1c)) ∨
m = (((n +c n) +c n) +c
2c))) |
83 | 82 | rexbii 2639 |
. . . 4
⊢ (∃n ∈ Nn (m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c) ∨ m =
(((n +c n) +c n) +c 2c))
↔ ∃n ∈ Nn ((m = ((n +c n) +c n) ∨ m = (((n
+c n)
+c n)
+c 1c)) ∨
m = (((n +c n) +c n) +c
2c))) |
84 | | r19.43 2766 |
. . . . . 6
⊢ (∃n ∈ Nn (m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c))
↔ (∃n ∈ Nn m = ((n +c n) +c n) ∨ ∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c))) |
85 | 84 | orbi1i 506 |
. . . . 5
⊢ ((∃n ∈ Nn (m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c)) ∨ ∃n ∈ Nn m = (((n +c n) +c n) +c 2c))
↔ ((∃n ∈ Nn m = ((n +c n) +c n) ∨ ∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c)) ∨
∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c))) |
86 | | r19.43 2766 |
. . . . 5
⊢ (∃n ∈ Nn ((m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c)) ∨ m =
(((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn (m = ((n +c n) +c n) ∨ m = (((n
+c n)
+c n)
+c 1c)) ∨
∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c))) |
87 | | df-3or 935 |
. . . . 5
⊢ ((∃n ∈ Nn m = ((n
+c n)
+c n) ∨ ∃n ∈ Nn m = (((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn m = (((n +c n) +c n) +c 2c))
↔ ((∃n ∈ Nn m = ((n +c n) +c n) ∨ ∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c)) ∨
∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c))) |
88 | 85, 86, 87 | 3bitr4i 268 |
. . . 4
⊢ (∃n ∈ Nn ((m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c)) ∨ m =
(((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn m = ((n +c n) +c n) ∨ ∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c) ∨
∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c))) |
89 | 83, 88 | bitri 240 |
. . 3
⊢ (∃n ∈ Nn (m = ((n
+c n)
+c n) ∨ m =
(((n +c n) +c n) +c 1c) ∨ m =
(((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn m = ((n +c n) +c n) ∨ ∃n ∈ Nn m = (((n
+c n)
+c n)
+c 1c) ∨
∃n ∈ Nn m = (((n
+c n)
+c n)
+c 2c))) |
90 | | df-3or 935 |
. . . . 5
⊢ (((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ (((m +c
1c) = ((n
+c n)
+c n) ∨ (m
+c 1c) = (((n +c n) +c n) +c 1c)) ∨ (m
+c 1c) = (((n +c n) +c n) +c
2c))) |
91 | 90 | rexbii 2639 |
. . . 4
⊢ (∃n ∈ Nn ((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ ∃n ∈ Nn (((m
+c 1c) = ((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ (m
+c 1c) = (((n +c n) +c n) +c
2c))) |
92 | | r19.43 2766 |
. . . . 5
⊢ (∃n ∈ Nn (((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn ((m
+c 1c) = ((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c
2c))) |
93 | | r19.43 2766 |
. . . . . . 7
⊢ (∃n ∈ Nn ((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c))
↔ (∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n) ∨ ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c
1c))) |
94 | 93 | orbi1i 506 |
. . . . . 6
⊢ ((∃n ∈ Nn ((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ ((∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n) ∨ ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c
2c))) |
95 | | df-3or 935 |
. . . . . 6
⊢ ((∃n ∈ Nn (m +c 1c) =
((n +c n) +c n) ∨ ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ ((∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n) ∨ ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c
2c))) |
96 | | 3orrot 940 |
. . . . . 6
⊢ ((∃n ∈ Nn (m +c 1c) =
((n +c n) +c n) ∨ ∃n ∈ Nn (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c) ∨ ∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n))) |
97 | 94, 95, 96 | 3bitr2i 264 |
. . . . 5
⊢ ((∃n ∈ Nn ((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c) ∨ ∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n))) |
98 | 92, 97 | bitri 240 |
. . . 4
⊢ (∃n ∈ Nn (((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c)) ∨ (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c) ∨ ∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n))) |
99 | 91, 98 | bitri 240 |
. . 3
⊢ (∃n ∈ Nn ((m +c 1c) =
((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ (m
+c 1c) = (((n +c n) +c n) +c 2c))
↔ (∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 1c) ∨ ∃n ∈ Nn (m
+c 1c) = (((n +c n) +c n) +c 2c) ∨ ∃n ∈ Nn (m
+c 1c) = ((n +c n) +c n))) |
100 | 81, 89, 99 | 3imtr4g 261 |
. 2
⊢ (m ∈ Nn → (∃n ∈ Nn (m = ((n +c n) +c n) ∨ m = (((n
+c n)
+c n)
+c 1c) ∨
m = (((n +c n) +c n) +c 2c))
→ ∃n ∈ Nn ((m
+c 1c) = ((n +c n) +c n) ∨ (m +c 1c) =
(((n +c n) +c n) +c 1c) ∨ (m
+c 1c) = (((n +c n) +c n) +c
2c)))) |
101 | 1, 6, 11, 16, 21, 39, 100 | finds 4411 |
1
⊢ (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))) |