Proof of Theorem dignn0fr
| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . 3
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ) |
| 2 | | eldifi 4131 |
. . 3
⊢ (𝐾 ∈ (ℤ ∖
ℕ0) → 𝐾 ∈ ℤ) |
| 3 | | nn0re 12535 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 4 | | nn0ge0 12551 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
| 5 | | elrege0 13494 |
. . . 4
⊢ (𝑁 ∈ (0[,)+∞) ↔
(𝑁 ∈ ℝ ∧ 0
≤ 𝑁)) |
| 6 | 3, 4, 5 | sylanbrc 583 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
(0[,)+∞)) |
| 7 | | digval 48519 |
. . 3
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ (0[,)+∞)) →
(𝐾(digit‘𝐵)𝑁) = ((⌊‘((𝐵↑-𝐾) · 𝑁)) mod 𝐵)) |
| 8 | 1, 2, 6, 7 | syl3an 1161 |
. 2
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = ((⌊‘((𝐵↑-𝐾) · 𝑁)) mod 𝐵)) |
| 9 | | nnz 12634 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
| 10 | | eldif 3961 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (ℤ ∖
ℕ0) ↔ (𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈
ℕ0)) |
| 11 | | znnn0nn 12729 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℤ ∧ ¬
𝐾 ∈
ℕ0) → -𝐾 ∈ ℕ) |
| 12 | 10, 11 | sylbi 217 |
. . . . . . . . 9
⊢ (𝐾 ∈ (ℤ ∖
ℕ0) → -𝐾 ∈ ℕ) |
| 13 | 12 | nnnn0d 12587 |
. . . . . . . 8
⊢ (𝐾 ∈ (ℤ ∖
ℕ0) → -𝐾 ∈
ℕ0) |
| 14 | | zexpcl 14117 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ -𝐾 ∈ ℕ0)
→ (𝐵↑-𝐾) ∈
ℤ) |
| 15 | 9, 13, 14 | syl2an 596 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0)) → (𝐵↑-𝐾) ∈ ℤ) |
| 16 | 15 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐵↑-𝐾) ∈ ℤ) |
| 17 | | nn0z 12638 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 18 | 17 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℤ) |
| 19 | 16, 18 | zmulcld 12728 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝐵↑-𝐾) · 𝑁) ∈ ℤ) |
| 20 | | flid 13848 |
. . . . 5
⊢ (((𝐵↑-𝐾) · 𝑁) ∈ ℤ →
(⌊‘((𝐵↑-𝐾) · 𝑁)) = ((𝐵↑-𝐾) · 𝑁)) |
| 21 | 19, 20 | syl 17 |
. . . 4
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) →
(⌊‘((𝐵↑-𝐾) · 𝑁)) = ((𝐵↑-𝐾) · 𝑁)) |
| 22 | 21 | oveq1d 7446 |
. . 3
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) →
((⌊‘((𝐵↑-𝐾) · 𝑁)) mod 𝐵) = (((𝐵↑-𝐾) · 𝑁) mod 𝐵)) |
| 23 | | nnre 12273 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 24 | | reexpcl 14119 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ -𝐾 ∈ ℕ0)
→ (𝐵↑-𝐾) ∈
ℝ) |
| 25 | 23, 13, 24 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0)) → (𝐵↑-𝐾) ∈ ℝ) |
| 26 | 25 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0)) → (𝐵↑-𝐾) ∈ ℂ) |
| 27 | 26 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐵↑-𝐾) ∈ ℂ) |
| 28 | | nn0cn 12536 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 29 | 28 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℂ) |
| 30 | | nncn 12274 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
| 31 | | nnne0 12300 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
| 32 | 30, 31 | jca 511 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
| 33 | 32 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
| 34 | | div23 11941 |
. . . . . . 7
⊢ (((𝐵↑-𝐾) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → (((𝐵↑-𝐾) · 𝑁) / 𝐵) = (((𝐵↑-𝐾) / 𝐵) · 𝑁)) |
| 35 | 27, 29, 33, 34 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝐵↑-𝐾) · 𝑁) / 𝐵) = (((𝐵↑-𝐾) / 𝐵) · 𝑁)) |
| 36 | 30 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐵 ∈
ℂ) |
| 37 | 31 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐵 ≠ 0) |
| 38 | 12 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (ℤ ∖
ℕ0) → -𝐾 ∈ ℤ) |
| 39 | 38 | 3ad2ant2 1135 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → -𝐾 ∈
ℤ) |
| 40 | 36, 37, 39 | expm1d 14196 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐵↑(-𝐾 − 1)) = ((𝐵↑-𝐾) / 𝐵)) |
| 41 | 40 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝐵↑-𝐾) / 𝐵) = (𝐵↑(-𝐾 − 1))) |
| 42 | 41 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝐵↑-𝐾) / 𝐵) · 𝑁) = ((𝐵↑(-𝐾 − 1)) · 𝑁)) |
| 43 | 35, 42 | eqtrd 2777 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝐵↑-𝐾) · 𝑁) / 𝐵) = ((𝐵↑(-𝐾 − 1)) · 𝑁)) |
| 44 | | nnm1nn0 12567 |
. . . . . . . . 9
⊢ (-𝐾 ∈ ℕ → (-𝐾 − 1) ∈
ℕ0) |
| 45 | 12, 44 | syl 17 |
. . . . . . . 8
⊢ (𝐾 ∈ (ℤ ∖
ℕ0) → (-𝐾 − 1) ∈
ℕ0) |
| 46 | | zexpcl 14117 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ (-𝐾 − 1) ∈
ℕ0) → (𝐵↑(-𝐾 − 1)) ∈
ℤ) |
| 47 | 9, 45, 46 | syl2an 596 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0)) → (𝐵↑(-𝐾 − 1)) ∈
ℤ) |
| 48 | 47 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐵↑(-𝐾 − 1)) ∈
ℤ) |
| 49 | 48, 18 | zmulcld 12728 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝐵↑(-𝐾 − 1)) · 𝑁) ∈ ℤ) |
| 50 | 43, 49 | eqeltrd 2841 |
. . . 4
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝐵↑-𝐾) · 𝑁) / 𝐵) ∈ ℤ) |
| 51 | 25 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐵↑-𝐾) ∈ ℝ) |
| 52 | 3 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℝ) |
| 53 | 51, 52 | remulcld 11291 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝐵↑-𝐾) · 𝑁) ∈ ℝ) |
| 54 | | nnrp 13046 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ+) |
| 55 | 54 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → 𝐵 ∈
ℝ+) |
| 56 | | mod0 13916 |
. . . . 5
⊢ ((((𝐵↑-𝐾) · 𝑁) ∈ ℝ ∧ 𝐵 ∈ ℝ+) →
((((𝐵↑-𝐾) · 𝑁) mod 𝐵) = 0 ↔ (((𝐵↑-𝐾) · 𝑁) / 𝐵) ∈ ℤ)) |
| 57 | 53, 55, 56 | syl2anc 584 |
. . . 4
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) →
((((𝐵↑-𝐾) · 𝑁) mod 𝐵) = 0 ↔ (((𝐵↑-𝐾) · 𝑁) / 𝐵) ∈ ℤ)) |
| 58 | 50, 57 | mpbird 257 |
. . 3
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝐵↑-𝐾) · 𝑁) mod 𝐵) = 0) |
| 59 | 22, 58 | eqtrd 2777 |
. 2
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) →
((⌊‘((𝐵↑-𝐾) · 𝑁)) mod 𝐵) = 0) |
| 60 | 8, 59 | eqtrd 2777 |
1
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖
ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = 0) |