Proof of Theorem 0dig2nn0o
Step | Hyp | Ref
| Expression |
1 | | 2nn 12046 |
. . . 4
⊢ 2 ∈
ℕ |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ∈ ℕ) |
3 | | 0nn0 12248 |
. . . 4
⊢ 0 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 0 ∈ ℕ0) |
5 | | nn0rp0 13186 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(0[,)+∞)) |
6 | 5 | adantr 481 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 𝑁 ∈ (0[,)+∞)) |
7 | | nn0digval 45915 |
. . 3
⊢ ((2
∈ ℕ ∧ 0 ∈ ℕ0 ∧ 𝑁 ∈ (0[,)+∞)) →
(0(digit‘2)𝑁) =
((⌊‘(𝑁 /
(2↑0))) mod 2)) |
8 | 2, 4, 6, 7 | syl3anc 1370 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (0(digit‘2)𝑁) = ((⌊‘(𝑁 / (2↑0))) mod 2)) |
9 | | 2cn 12048 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
10 | | exp0 13784 |
. . . . . . . 8
⊢ (2 ∈
ℂ → (2↑0) = 1) |
11 | 9, 10 | mp1i 13 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (2↑0) = 1) |
12 | 11 | oveq2d 7287 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 / (2↑0)) = (𝑁 / 1)) |
13 | | nn0cn 12243 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
14 | 13 | div1d 11743 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 / 1) = 𝑁) |
15 | 14 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 / 1) = 𝑁) |
16 | 12, 15 | eqtrd 2780 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 / (2↑0)) = 𝑁) |
17 | 16 | fveq2d 6775 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (⌊‘(𝑁 / (2↑0))) = (⌊‘𝑁)) |
18 | 17 | oveq1d 7286 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘(𝑁 / (2↑0))) mod 2) =
((⌊‘𝑁) mod
2)) |
19 | | nn0z 12343 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
20 | | flid 13526 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ →
(⌊‘𝑁) = 𝑁) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (⌊‘𝑁) =
𝑁) |
22 | 21 | oveq1d 7286 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((⌊‘𝑁)
mod 2) = (𝑁 mod
2)) |
23 | 22 | adantr 481 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘𝑁) mod 2) = (𝑁 mod 2)) |
24 | | nn0z 12343 |
. . . . . . . 8
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → ((𝑁 + 1) / 2) ∈ ℤ) |
25 | 24 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 + 1) / 2) ∈ ℤ) |
26 | | 2z 12352 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ∈ ℤ) |
28 | | 2ne0 12077 |
. . . . . . . . 9
⊢ 2 ≠
0 |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ≠ 0) |
30 | | peano2nn0 12273 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
31 | 30 | nn0zd 12423 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 + 1) ∈ ℤ) |
33 | | dvdsval2 15964 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 + 1) ∈ ℤ) → (2 ∥
(𝑁 + 1) ↔ ((𝑁 + 1) / 2) ∈
ℤ)) |
34 | 27, 29, 32, 33 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (2 ∥ (𝑁 + 1) ↔ ((𝑁 + 1) / 2) ∈ ℤ)) |
35 | 25, 34 | mpbird 256 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ∥ (𝑁 + 1)) |
36 | | oddp1even 16051 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔ 2 ∥
(𝑁 + 1))) |
37 | 19, 36 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (¬ 2 ∥ 𝑁
↔ 2 ∥ (𝑁 +
1))) |
38 | 37 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) |
39 | 35, 38 | mpbird 256 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ¬ 2 ∥ 𝑁) |
40 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 𝑁 ∈ ℤ) |
41 | | mod2eq1n2dvds 16054 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2
∥ 𝑁)) |
42 | 40, 41 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁)) |
43 | 39, 42 | mpbird 256 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 mod 2) = 1) |
44 | 23, 43 | eqtrd 2780 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘𝑁) mod 2) = 1) |
45 | 18, 44 | eqtrd 2780 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘(𝑁 / (2↑0))) mod 2) = 1) |
46 | 8, 45 | eqtrd 2780 |
1
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (0(digit‘2)𝑁) = 1) |