Proof of Theorem 0dig2nn0o
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2nn 12340 | . . . 4
⊢ 2 ∈
ℕ | 
| 2 | 1 | a1i 11 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ∈ ℕ) | 
| 3 |  | 0nn0 12543 | . . . 4
⊢ 0 ∈
ℕ0 | 
| 4 | 3 | a1i 11 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 0 ∈ ℕ0) | 
| 5 |  | nn0rp0 13496 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(0[,)+∞)) | 
| 6 | 5 | adantr 480 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 𝑁 ∈ (0[,)+∞)) | 
| 7 |  | nn0digval 48526 | . . 3
⊢ ((2
∈ ℕ ∧ 0 ∈ ℕ0 ∧ 𝑁 ∈ (0[,)+∞)) →
(0(digit‘2)𝑁) =
((⌊‘(𝑁 /
(2↑0))) mod 2)) | 
| 8 | 2, 4, 6, 7 | syl3anc 1372 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (0(digit‘2)𝑁) = ((⌊‘(𝑁 / (2↑0))) mod 2)) | 
| 9 |  | 2cn 12342 | . . . . . . . 8
⊢ 2 ∈
ℂ | 
| 10 |  | exp0 14107 | . . . . . . . 8
⊢ (2 ∈
ℂ → (2↑0) = 1) | 
| 11 | 9, 10 | mp1i 13 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (2↑0) = 1) | 
| 12 | 11 | oveq2d 7448 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 / (2↑0)) = (𝑁 / 1)) | 
| 13 |  | nn0cn 12538 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) | 
| 14 | 13 | div1d 12036 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 / 1) = 𝑁) | 
| 15 | 14 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 / 1) = 𝑁) | 
| 16 | 12, 15 | eqtrd 2776 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 / (2↑0)) = 𝑁) | 
| 17 | 16 | fveq2d 6909 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (⌊‘(𝑁 / (2↑0))) = (⌊‘𝑁)) | 
| 18 | 17 | oveq1d 7447 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘(𝑁 / (2↑0))) mod 2) =
((⌊‘𝑁) mod
2)) | 
| 19 |  | nn0z 12640 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) | 
| 20 |  | flid 13849 | . . . . . . 7
⊢ (𝑁 ∈ ℤ →
(⌊‘𝑁) = 𝑁) | 
| 21 | 19, 20 | syl 17 | . . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (⌊‘𝑁) =
𝑁) | 
| 22 | 21 | oveq1d 7447 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((⌊‘𝑁)
mod 2) = (𝑁 mod
2)) | 
| 23 | 22 | adantr 480 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘𝑁) mod 2) = (𝑁 mod 2)) | 
| 24 |  | nn0z 12640 | . . . . . . . 8
⊢ (((𝑁 + 1) / 2) ∈
ℕ0 → ((𝑁 + 1) / 2) ∈ ℤ) | 
| 25 | 24 | adantl 481 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 + 1) / 2) ∈ ℤ) | 
| 26 |  | 2z 12651 | . . . . . . . . 9
⊢ 2 ∈
ℤ | 
| 27 | 26 | a1i 11 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ∈ ℤ) | 
| 28 |  | 2ne0 12371 | . . . . . . . . 9
⊢ 2 ≠
0 | 
| 29 | 28 | a1i 11 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ≠ 0) | 
| 30 |  | peano2nn0 12568 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 31 | 30 | nn0zd 12641 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) | 
| 32 | 31 | adantr 480 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 + 1) ∈ ℤ) | 
| 33 |  | dvdsval2 16294 | . . . . . . . 8
⊢ ((2
∈ ℤ ∧ 2 ≠ 0 ∧ (𝑁 + 1) ∈ ℤ) → (2 ∥
(𝑁 + 1) ↔ ((𝑁 + 1) / 2) ∈
ℤ)) | 
| 34 | 27, 29, 32, 33 | syl3anc 1372 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (2 ∥ (𝑁 + 1) ↔ ((𝑁 + 1) / 2) ∈ ℤ)) | 
| 35 | 25, 34 | mpbird 257 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 2 ∥ (𝑁 + 1)) | 
| 36 |  | oddp1even 16382 | . . . . . . . 8
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔ 2 ∥
(𝑁 + 1))) | 
| 37 | 19, 36 | syl 17 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (¬ 2 ∥ 𝑁
↔ 2 ∥ (𝑁 +
1))) | 
| 38 | 37 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) | 
| 39 | 35, 38 | mpbird 257 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ¬ 2 ∥ 𝑁) | 
| 40 | 19 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → 𝑁 ∈ ℤ) | 
| 41 |  | mod2eq1n2dvds 16385 | . . . . . 6
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2
∥ 𝑁)) | 
| 42 | 40, 41 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁)) | 
| 43 | 39, 42 | mpbird 257 | . . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (𝑁 mod 2) = 1) | 
| 44 | 23, 43 | eqtrd 2776 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘𝑁) mod 2) = 1) | 
| 45 | 18, 44 | eqtrd 2776 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → ((⌊‘(𝑁 / (2↑0))) mod 2) = 1) | 
| 46 | 8, 45 | eqtrd 2776 | 1
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑁 + 1) / 2) ∈
ℕ0) → (0(digit‘2)𝑁) = 1) |