Proof of Theorem dignn0ehalf
Step | Hyp | Ref
| Expression |
1 | | nn0cn 12243 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
2 | 1 | 3ad2ant2 1133 |
. . . . . 6
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → 𝐴 ∈ ℂ) |
3 | | 2cnne0 12183 |
. . . . . . 7
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (2 ∈ ℂ ∧ 2 ≠
0)) |
5 | | 2nn0 12250 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
6 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℕ0
→ 2 ∈ ℕ0) |
7 | | id 22 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℕ0) |
8 | 6, 7 | nn0expcld 13961 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ (2↑𝐼) ∈
ℕ0) |
9 | 8 | nn0cnd 12295 |
. . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ (2↑𝐼) ∈
ℂ) |
10 | | 2cnd 12051 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 2 ∈ ℂ) |
11 | | 2ne0 12077 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 2 ≠ 0) |
13 | | nn0z 12343 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℕ0
→ 𝐼 ∈
ℤ) |
14 | 10, 12, 13 | expne0d 13870 |
. . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ (2↑𝐼) ≠
0) |
15 | 9, 14 | jca 512 |
. . . . . . 7
⊢ (𝐼 ∈ ℕ0
→ ((2↑𝐼) ∈
ℂ ∧ (2↑𝐼)
≠ 0)) |
16 | 15 | 3ad2ant3 1134 |
. . . . . 6
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → ((2↑𝐼) ∈ ℂ ∧ (2↑𝐼) ≠ 0)) |
17 | | divdiv1 11686 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (2 ∈
ℂ ∧ 2 ≠ 0) ∧ ((2↑𝐼) ∈ ℂ ∧ (2↑𝐼) ≠ 0)) → ((𝐴 / 2) / (2↑𝐼)) = (𝐴 / (2 · (2↑𝐼)))) |
18 | 2, 4, 16, 17 | syl3anc 1370 |
. . . . 5
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → ((𝐴 / 2) / (2↑𝐼)) = (𝐴 / (2 · (2↑𝐼)))) |
19 | 10, 9 | mulcomd 10996 |
. . . . . . . 8
⊢ (𝐼 ∈ ℕ0
→ (2 · (2↑𝐼)) = ((2↑𝐼) · 2)) |
20 | 19 | 3ad2ant3 1134 |
. . . . . . 7
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (2 · (2↑𝐼)) = ((2↑𝐼) · 2)) |
21 | | 2cnd 12051 |
. . . . . . . 8
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → 2 ∈ ℂ) |
22 | | simp3 1137 |
. . . . . . . 8
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → 𝐼 ∈
ℕ0) |
23 | 21, 22 | expp1d 13865 |
. . . . . . 7
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (2↑(𝐼 + 1)) = ((2↑𝐼) · 2)) |
24 | 20, 23 | eqtr4d 2781 |
. . . . . 6
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (2 · (2↑𝐼)) = (2↑(𝐼 + 1))) |
25 | 24 | oveq2d 7291 |
. . . . 5
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (𝐴 / (2 · (2↑𝐼))) = (𝐴 / (2↑(𝐼 + 1)))) |
26 | 18, 25 | eqtr2d 2779 |
. . . 4
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (𝐴 / (2↑(𝐼 + 1))) = ((𝐴 / 2) / (2↑𝐼))) |
27 | 26 | fveq2d 6778 |
. . 3
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (⌊‘(𝐴 / (2↑(𝐼 + 1)))) = (⌊‘((𝐴 / 2) / (2↑𝐼)))) |
28 | 27 | oveq1d 7290 |
. 2
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → ((⌊‘(𝐴 / (2↑(𝐼 + 1)))) mod 2) = ((⌊‘((𝐴 / 2) / (2↑𝐼))) mod 2)) |
29 | | 2nn 12046 |
. . . 4
⊢ 2 ∈
ℕ |
30 | 29 | a1i 11 |
. . 3
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → 2 ∈ ℕ) |
31 | | peano2nn0 12273 |
. . . 4
⊢ (𝐼 ∈ ℕ0
→ (𝐼 + 1) ∈
ℕ0) |
32 | 31 | 3ad2ant3 1134 |
. . 3
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (𝐼 + 1) ∈
ℕ0) |
33 | | nn0rp0 13187 |
. . . 4
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
(0[,)+∞)) |
34 | 33 | 3ad2ant2 1133 |
. . 3
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → 𝐴 ∈ (0[,)+∞)) |
35 | | nn0digval 45946 |
. . 3
⊢ ((2
∈ ℕ ∧ (𝐼 +
1) ∈ ℕ0 ∧ 𝐴 ∈ (0[,)+∞)) → ((𝐼 + 1)(digit‘2)𝐴) = ((⌊‘(𝐴 / (2↑(𝐼 + 1)))) mod 2)) |
36 | 30, 32, 34, 35 | syl3anc 1370 |
. 2
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → ((𝐼 + 1)(digit‘2)𝐴) = ((⌊‘(𝐴 / (2↑(𝐼 + 1)))) mod 2)) |
37 | | nn0rp0 13187 |
. . . 4
⊢ ((𝐴 / 2) ∈ ℕ0
→ (𝐴 / 2) ∈
(0[,)+∞)) |
38 | 37 | 3ad2ant1 1132 |
. . 3
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (𝐴 / 2) ∈
(0[,)+∞)) |
39 | | nn0digval 45946 |
. . 3
⊢ ((2
∈ ℕ ∧ 𝐼
∈ ℕ0 ∧ (𝐴 / 2) ∈ (0[,)+∞)) → (𝐼(digit‘2)(𝐴 / 2)) = ((⌊‘((𝐴 / 2) / (2↑𝐼))) mod 2)) |
40 | 30, 22, 38, 39 | syl3anc 1370 |
. 2
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → (𝐼(digit‘2)(𝐴 / 2)) = ((⌊‘((𝐴 / 2) / (2↑𝐼))) mod 2)) |
41 | 28, 36, 40 | 3eqtr4d 2788 |
1
⊢ (((𝐴 / 2) ∈ ℕ0
∧ 𝐴 ∈
ℕ0 ∧ 𝐼
∈ ℕ0) → ((𝐼 + 1)(digit‘2)𝐴) = (𝐼(digit‘2)(𝐴 / 2))) |