Step | Hyp | Ref
| Expression |
1 | | eqeq1 2738 |
. . . 4
⊢ (𝑚 = 0s → (𝑚 = (2s
·s 𝑥)
↔ 0s = (2s ·s 𝑥))) |
2 | 1 | rexbidv 3181 |
. . 3
⊢ (𝑚 = 0s →
(∃𝑥 ∈
ℕ0s 𝑚 =
(2s ·s 𝑥) ↔ ∃𝑥 ∈ ℕ0s 0s =
(2s ·s 𝑥))) |
3 | | eqeq1 2738 |
. . . 4
⊢ (𝑚 = 0s → (𝑚 = ((2s
·s 𝑥)
+s 1s ) ↔ 0s = ((2s
·s 𝑥)
+s 1s ))) |
4 | 3 | rexbidv 3181 |
. . 3
⊢ (𝑚 = 0s →
(∃𝑥 ∈
ℕ0s 𝑚 =
((2s ·s 𝑥) +s 1s ) ↔
∃𝑥 ∈
ℕ0s 0s = ((2s ·s 𝑥) +s 1s
))) |
5 | 2, 4 | orbi12d 917 |
. 2
⊢ (𝑚 = 0s →
((∃𝑥 ∈
ℕ0s 𝑚 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑚 = ((2s
·s 𝑥)
+s 1s )) ↔ (∃𝑥 ∈ ℕ0s 0s =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 0s =
((2s ·s 𝑥) +s 1s
)))) |
6 | | eqeq1 2738 |
. . . 4
⊢ (𝑚 = 𝑛 → (𝑚 = (2s ·s 𝑥) ↔ 𝑛 = (2s ·s 𝑥))) |
7 | 6 | rexbidv 3181 |
. . 3
⊢ (𝑚 = 𝑛 → (∃𝑥 ∈ ℕ0s 𝑚 = (2s
·s 𝑥)
↔ ∃𝑥 ∈
ℕ0s 𝑛 =
(2s ·s 𝑥))) |
8 | | eqeq1 2738 |
. . . 4
⊢ (𝑚 = 𝑛 → (𝑚 = ((2s ·s 𝑥) +s 1s )
↔ 𝑛 = ((2s
·s 𝑥)
+s 1s ))) |
9 | 8 | rexbidv 3181 |
. . 3
⊢ (𝑚 = 𝑛 → (∃𝑥 ∈ ℕ0s 𝑚 = ((2s
·s 𝑥)
+s 1s ) ↔ ∃𝑥 ∈ ℕ0s 𝑛 = ((2s
·s 𝑥)
+s 1s ))) |
10 | 7, 9 | orbi12d 917 |
. 2
⊢ (𝑚 = 𝑛 → ((∃𝑥 ∈ ℕ0s 𝑚 = (2s
·s 𝑥)
∨ ∃𝑥 ∈
ℕ0s 𝑚 =
((2s ·s 𝑥) +s 1s )) ↔
(∃𝑥 ∈
ℕ0s 𝑛 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑛 = ((2s
·s 𝑥)
+s 1s )))) |
11 | | eqeq1 2738 |
. . . . 5
⊢ (𝑚 = (𝑛 +s 1s ) → (𝑚 = (2s
·s 𝑥)
↔ (𝑛 +s
1s ) = (2s ·s 𝑥))) |
12 | 11 | rexbidv 3181 |
. . . 4
⊢ (𝑚 = (𝑛 +s 1s ) →
(∃𝑥 ∈
ℕ0s 𝑚 =
(2s ·s 𝑥) ↔ ∃𝑥 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑥))) |
13 | | oveq2 7453 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (2s ·s
𝑥) = (2s
·s 𝑦)) |
14 | 13 | eqeq2d 2745 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑛 +s 1s ) =
(2s ·s 𝑥) ↔ (𝑛 +s 1s ) =
(2s ·s 𝑦))) |
15 | 14 | cbvrexvw 3239 |
. . . 4
⊢
(∃𝑥 ∈
ℕ0s (𝑛
+s 1s ) = (2s ·s 𝑥) ↔ ∃𝑦 ∈ ℕ0s
(𝑛 +s
1s ) = (2s ·s 𝑦)) |
16 | 12, 15 | bitrdi 287 |
. . 3
⊢ (𝑚 = (𝑛 +s 1s ) →
(∃𝑥 ∈
ℕ0s 𝑚 =
(2s ·s 𝑥) ↔ ∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑦))) |
17 | | eqeq1 2738 |
. . . . 5
⊢ (𝑚 = (𝑛 +s 1s ) → (𝑚 = ((2s
·s 𝑥)
+s 1s ) ↔ (𝑛 +s 1s ) =
((2s ·s 𝑥) +s 1s
))) |
18 | 17 | rexbidv 3181 |
. . . 4
⊢ (𝑚 = (𝑛 +s 1s ) →
(∃𝑥 ∈
ℕ0s 𝑚 =
((2s ·s 𝑥) +s 1s ) ↔
∃𝑥 ∈
ℕ0s (𝑛
+s 1s ) = ((2s ·s 𝑥) +s 1s
))) |
19 | 13 | oveq1d 7460 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((2s ·s
𝑥) +s
1s ) = ((2s ·s 𝑦) +s 1s
)) |
20 | 19 | eqeq2d 2745 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑛 +s 1s ) =
((2s ·s 𝑥) +s 1s ) ↔ (𝑛 +s 1s ) =
((2s ·s 𝑦) +s 1s
))) |
21 | 20 | cbvrexvw 3239 |
. . . 4
⊢
(∃𝑥 ∈
ℕ0s (𝑛
+s 1s ) = ((2s ·s 𝑥) +s 1s )
↔ ∃𝑦 ∈
ℕ0s (𝑛
+s 1s ) = ((2s ·s 𝑦) +s 1s
)) |
22 | 18, 21 | bitrdi 287 |
. . 3
⊢ (𝑚 = (𝑛 +s 1s ) →
(∃𝑥 ∈
ℕ0s 𝑚 =
((2s ·s 𝑥) +s 1s ) ↔
∃𝑦 ∈
ℕ0s (𝑛
+s 1s ) = ((2s ·s 𝑦) +s 1s
))) |
23 | 16, 22 | orbi12d 917 |
. 2
⊢ (𝑚 = (𝑛 +s 1s ) →
((∃𝑥 ∈
ℕ0s 𝑚 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑚 = ((2s
·s 𝑥)
+s 1s )) ↔ (∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑦) ∨ ∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
((2s ·s 𝑦) +s 1s
)))) |
24 | | eqeq1 2738 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝑚 = (2s ·s 𝑥) ↔ 𝑁 = (2s ·s 𝑥))) |
25 | 24 | rexbidv 3181 |
. . 3
⊢ (𝑚 = 𝑁 → (∃𝑥 ∈ ℕ0s 𝑚 = (2s
·s 𝑥)
↔ ∃𝑥 ∈
ℕ0s 𝑁 =
(2s ·s 𝑥))) |
26 | | eqeq1 2738 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝑚 = ((2s ·s 𝑥) +s 1s )
↔ 𝑁 = ((2s
·s 𝑥)
+s 1s ))) |
27 | 26 | rexbidv 3181 |
. . 3
⊢ (𝑚 = 𝑁 → (∃𝑥 ∈ ℕ0s 𝑚 = ((2s
·s 𝑥)
+s 1s ) ↔ ∃𝑥 ∈ ℕ0s 𝑁 = ((2s
·s 𝑥)
+s 1s ))) |
28 | 25, 27 | orbi12d 917 |
. 2
⊢ (𝑚 = 𝑁 → ((∃𝑥 ∈ ℕ0s 𝑚 = (2s
·s 𝑥)
∨ ∃𝑥 ∈
ℕ0s 𝑚 =
((2s ·s 𝑥) +s 1s )) ↔
(∃𝑥 ∈
ℕ0s 𝑁 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑁 = ((2s
·s 𝑥)
+s 1s )))) |
29 | | 0n0s 28343 |
. . . 4
⊢
0s ∈ ℕ0s |
30 | | 2sno 28412 |
. . . . . 6
⊢
2s ∈ No |
31 | | muls01 28147 |
. . . . . 6
⊢
(2s ∈ No →
(2s ·s 0s ) = 0s
) |
32 | 30, 31 | ax-mp 5 |
. . . . 5
⊢
(2s ·s 0s ) =
0s |
33 | 32 | eqcomi 2743 |
. . . 4
⊢
0s = (2s ·s 0s
) |
34 | | oveq2 7453 |
. . . . 5
⊢ (𝑥 = 0s →
(2s ·s 𝑥) = (2s ·s
0s )) |
35 | 34 | rspceeqv 3653 |
. . . 4
⊢ ((
0s ∈ ℕ0s ∧ 0s = (2s
·s 0s )) → ∃𝑥 ∈ ℕ0s 0s =
(2s ·s 𝑥)) |
36 | 29, 33, 35 | mp2an 691 |
. . 3
⊢
∃𝑥 ∈
ℕ0s 0s = (2s ·s 𝑥) |
37 | 36 | orci 864 |
. 2
⊢
(∃𝑥 ∈
ℕ0s 0s = (2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 0s =
((2s ·s 𝑥) +s 1s
)) |
38 | | eqid 2734 |
. . . . . . . 8
⊢
((2s ·s 𝑥) +s 1s ) =
((2s ·s 𝑥) +s 1s
) |
39 | | oveq2 7453 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (2s ·s
𝑦) = (2s
·s 𝑥)) |
40 | 39 | oveq1d 7460 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((2s ·s
𝑦) +s
1s ) = ((2s ·s 𝑥) +s 1s
)) |
41 | 40 | rspceeqv 3653 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ0s
∧ ((2s ·s 𝑥) +s 1s ) =
((2s ·s 𝑥) +s 1s )) →
∃𝑦 ∈
ℕ0s ((2s ·s 𝑥) +s 1s ) =
((2s ·s 𝑦) +s 1s
)) |
42 | 38, 41 | mpan2 690 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0s
→ ∃𝑦 ∈
ℕ0s ((2s ·s 𝑥) +s 1s ) =
((2s ·s 𝑦) +s 1s
)) |
43 | | oveq1 7452 |
. . . . . . . . 9
⊢ (𝑛 = (2s
·s 𝑥)
→ (𝑛 +s
1s ) = ((2s ·s 𝑥) +s 1s
)) |
44 | 43 | eqeq1d 2736 |
. . . . . . . 8
⊢ (𝑛 = (2s
·s 𝑥)
→ ((𝑛 +s
1s ) = ((2s ·s 𝑦) +s 1s ) ↔
((2s ·s 𝑥) +s 1s ) =
((2s ·s 𝑦) +s 1s
))) |
45 | 44 | rexbidv 3181 |
. . . . . . 7
⊢ (𝑛 = (2s
·s 𝑥)
→ (∃𝑦 ∈
ℕ0s (𝑛
+s 1s ) = ((2s ·s 𝑦) +s 1s )
↔ ∃𝑦 ∈
ℕ0s ((2s ·s 𝑥) +s 1s ) =
((2s ·s 𝑦) +s 1s
))) |
46 | 42, 45 | syl5ibrcom 247 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0s
→ (𝑛 = (2s
·s 𝑥)
→ ∃𝑦 ∈
ℕ0s (𝑛
+s 1s ) = ((2s ·s 𝑦) +s 1s
))) |
47 | 46 | rexlimiv 3150 |
. . . . 5
⊢
(∃𝑥 ∈
ℕ0s 𝑛 =
(2s ·s 𝑥) → ∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
((2s ·s 𝑦) +s 1s
)) |
48 | | peano2n0s 28344 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0s
→ (𝑥 +s
1s ) ∈ ℕ0s) |
49 | | 1p1e2s 28409 |
. . . . . . . . . . 11
⊢ (
1s +s 1s ) = 2s |
50 | | mulsrid 28148 |
. . . . . . . . . . . 12
⊢
(2s ∈ No →
(2s ·s 1s ) =
2s) |
51 | 30, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(2s ·s 1s ) =
2s |
52 | 49, 51 | eqtr4i 2765 |
. . . . . . . . . 10
⊢ (
1s +s 1s ) = (2s
·s 1s ) |
53 | 52 | oveq2i 7456 |
. . . . . . . . 9
⊢
((2s ·s 𝑥) +s ( 1s +s
1s )) = ((2s ·s 𝑥) +s (2s
·s 1s )) |
54 | 30 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ0s
→ 2s ∈ No ) |
55 | | n0sno 28337 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℕ0s
→ 𝑥 ∈ No ) |
56 | 54, 55 | mulscld 28170 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0s
→ (2s ·s 𝑥) ∈ No
) |
57 | | 1sno 27881 |
. . . . . . . . . . 11
⊢
1s ∈ No |
58 | 57 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℕ0s
→ 1s ∈ No ) |
59 | 56, 58, 58 | addsassd 28048 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0s
→ (((2s ·s 𝑥) +s 1s ) +s
1s ) = ((2s ·s 𝑥) +s ( 1s +s
1s ))) |
60 | 54, 55, 58 | addsdid 28191 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ0s
→ (2s ·s (𝑥 +s 1s )) =
((2s ·s 𝑥) +s (2s
·s 1s ))) |
61 | 53, 59, 60 | 3eqtr4a 2800 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ0s
→ (((2s ·s 𝑥) +s 1s ) +s
1s ) = (2s ·s (𝑥 +s 1s
))) |
62 | | oveq2 7453 |
. . . . . . . . 9
⊢ (𝑦 = (𝑥 +s 1s ) →
(2s ·s 𝑦) = (2s ·s
(𝑥 +s
1s ))) |
63 | 62 | rspceeqv 3653 |
. . . . . . . 8
⊢ (((𝑥 +s 1s )
∈ ℕ0s ∧ (((2s ·s 𝑥) +s 1s )
+s 1s ) = (2s ·s (𝑥 +s 1s )))
→ ∃𝑦 ∈
ℕ0s (((2s ·s 𝑥) +s 1s ) +s
1s ) = (2s ·s 𝑦)) |
64 | 48, 61, 63 | syl2anc 583 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ0s
→ ∃𝑦 ∈
ℕ0s (((2s ·s 𝑥) +s 1s ) +s
1s ) = (2s ·s 𝑦)) |
65 | | oveq1 7452 |
. . . . . . . . 9
⊢ (𝑛 = ((2s
·s 𝑥)
+s 1s ) → (𝑛 +s 1s ) =
(((2s ·s 𝑥) +s 1s ) +s
1s )) |
66 | 65 | eqeq1d 2736 |
. . . . . . . 8
⊢ (𝑛 = ((2s
·s 𝑥)
+s 1s ) → ((𝑛 +s 1s ) =
(2s ·s 𝑦) ↔ (((2s
·s 𝑥)
+s 1s ) +s 1s ) = (2s
·s 𝑦))) |
67 | 66 | rexbidv 3181 |
. . . . . . 7
⊢ (𝑛 = ((2s
·s 𝑥)
+s 1s ) → (∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑦) ↔ ∃𝑦 ∈ ℕ0s (((2s
·s 𝑥)
+s 1s ) +s 1s ) = (2s
·s 𝑦))) |
68 | 64, 67 | syl5ibrcom 247 |
. . . . . 6
⊢ (𝑥 ∈ ℕ0s
→ (𝑛 = ((2s
·s 𝑥)
+s 1s ) → ∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑦))) |
69 | 68 | rexlimiv 3150 |
. . . . 5
⊢
(∃𝑥 ∈
ℕ0s 𝑛 =
((2s ·s 𝑥) +s 1s ) →
∃𝑦 ∈
ℕ0s (𝑛
+s 1s ) = (2s ·s 𝑦)) |
70 | 47, 69 | orim12i 907 |
. . . 4
⊢
((∃𝑥 ∈
ℕ0s 𝑛 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑛 = ((2s
·s 𝑥)
+s 1s )) → (∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
((2s ·s 𝑦) +s 1s ) ∨
∃𝑦 ∈
ℕ0s (𝑛
+s 1s ) = (2s ·s 𝑦))) |
71 | 70 | orcomd 870 |
. . 3
⊢
((∃𝑥 ∈
ℕ0s 𝑛 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑛 = ((2s
·s 𝑥)
+s 1s )) → (∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑦) ∨ ∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
((2s ·s 𝑦) +s 1s
))) |
72 | 71 | a1i 11 |
. 2
⊢ (𝑛 ∈ ℕ0s
→ ((∃𝑥 ∈
ℕ0s 𝑛 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑛 = ((2s
·s 𝑥)
+s 1s )) → (∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
(2s ·s 𝑦) ∨ ∃𝑦 ∈ ℕ0s (𝑛 +s 1s ) =
((2s ·s 𝑦) +s 1s
)))) |
73 | 5, 10, 23, 28, 37, 72 | n0sind 28346 |
1
⊢ (𝑁 ∈ ℕ0s
→ (∃𝑥 ∈
ℕ0s 𝑁 =
(2s ·s 𝑥) ∨ ∃𝑥 ∈ ℕ0s 𝑁 = ((2s
·s 𝑥)
+s 1s ))) |