Proof of Theorem digit1
| Step | Hyp | Ref
| Expression |
| 1 | | digit2 14275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = ((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))))) |
| 2 | 1 | 3coml 1128 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = ((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))))) |
| 3 | 2 | 3expa 1119 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = ((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))))) |
| 4 | 3 | oveq1d 7446 |
. . . 4
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
(((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) mod (𝐵↑𝐾)) = (((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)))) mod (𝐵↑𝐾))) |
| 5 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 6 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → 𝐾 ∈
ℕ0) |
| 7 | | reexpcl 14119 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐾 ∈ ℕ0)
→ (𝐵↑𝐾) ∈
ℝ) |
| 8 | 5, 6, 7 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑𝐾) ∈ ℝ) |
| 9 | | remulcl 11240 |
. . . . . . . 8
⊢ (((𝐵↑𝐾) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵↑𝐾) · 𝐴) ∈ ℝ) |
| 10 | 8, 9 | sylan 580 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵↑𝐾) · 𝐴) ∈ ℝ) |
| 11 | | reflcl 13836 |
. . . . . . 7
⊢ (((𝐵↑𝐾) · 𝐴) ∈ ℝ →
(⌊‘((𝐵↑𝐾) · 𝐴)) ∈ ℝ) |
| 12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
(⌊‘((𝐵↑𝐾) · 𝐴)) ∈ ℝ) |
| 13 | | nnrp 13046 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ+) |
| 14 | 13 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℝ+) |
| 15 | 12, 14 | modcld 13915 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) ∈ ℝ) |
| 16 | | nnexpcl 14115 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0)
→ (𝐵↑𝐾) ∈
ℕ) |
| 17 | 6, 16 | sylan2 593 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑𝐾) ∈ ℕ) |
| 18 | 17 | nnrpd 13075 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑𝐾) ∈
ℝ+) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (𝐵↑𝐾) ∈
ℝ+) |
| 20 | | modge0 13919 |
. . . . . 6
⊢
(((⌊‘((𝐵↑𝐾) · 𝐴)) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 0 ≤
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵)) |
| 21 | 12, 14, 20 | syl2anc 584 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 0 ≤
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵)) |
| 22 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℝ) |
| 23 | 8 | adantr 480 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (𝐵↑𝐾) ∈ ℝ) |
| 24 | | modlt 13920 |
. . . . . . 7
⊢
(((⌊‘((𝐵↑𝐾) · 𝐴)) ∈ ℝ ∧ 𝐵 ∈ ℝ+) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) < 𝐵) |
| 25 | 12, 14, 24 | syl2anc 584 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) < 𝐵) |
| 26 | | nncn 12274 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
| 27 | | exp1 14108 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → (𝐵↑1) = 𝐵) |
| 29 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑1) = 𝐵) |
| 30 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → 𝐵 ∈
ℝ) |
| 31 | | nnge1 12294 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → 1 ≤
𝐵) |
| 32 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → 1 ≤
𝐵) |
| 33 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
ℕ) |
| 34 | | nnuz 12921 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
| 35 | 33, 34 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → 𝐾 ∈
(ℤ≥‘1)) |
| 36 | | leexp2a 14212 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 1 ≤
𝐵 ∧ 𝐾 ∈ (ℤ≥‘1))
→ (𝐵↑1) ≤
(𝐵↑𝐾)) |
| 37 | 30, 32, 35, 36 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑1) ≤ (𝐵↑𝐾)) |
| 38 | 29, 37 | eqbrtrrd 5167 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → 𝐵 ≤ (𝐵↑𝐾)) |
| 39 | 38 | adantr 480 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 𝐵 ≤ (𝐵↑𝐾)) |
| 40 | 15, 22, 23, 25, 39 | ltletrd 11421 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) < (𝐵↑𝐾)) |
| 41 | | modid 13936 |
. . . . 5
⊢
(((((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) ∈ ℝ ∧ (𝐵↑𝐾) ∈ ℝ+) ∧ (0 ≤
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) ∧ ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) < (𝐵↑𝐾))) → (((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) mod (𝐵↑𝐾)) = ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵)) |
| 42 | 15, 19, 21, 40, 41 | syl22anc 839 |
. . . 4
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
(((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) mod (𝐵↑𝐾)) = ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵)) |
| 43 | | simpll 767 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℕ) |
| 44 | | nnm1nn0 12567 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
| 45 | | reexpcl 14119 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐵↑(𝐾 − 1)) ∈
ℝ) |
| 46 | 5, 44, 45 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑(𝐾 − 1)) ∈
ℝ) |
| 47 | | remulcl 11240 |
. . . . . . . 8
⊢ (((𝐵↑(𝐾 − 1)) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝐵↑(𝐾 − 1)) · 𝐴) ∈ ℝ) |
| 48 | 46, 47 | sylan 580 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵↑(𝐾 − 1)) · 𝐴) ∈ ℝ) |
| 49 | | nnexpcl 14115 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐵↑(𝐾 − 1)) ∈
ℕ) |
| 50 | 44, 49 | sylan2 593 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑(𝐾 − 1)) ∈
ℕ) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (𝐵↑(𝐾 − 1)) ∈
ℕ) |
| 52 | | modmulnn 13929 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ ((𝐵↑(𝐾 − 1)) · 𝐴) ∈ ℝ ∧ (𝐵↑(𝐾 − 1)) ∈ ℕ) → ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵 · (𝐵↑(𝐾 − 1)))) ≤ ((⌊‘(𝐵 · ((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵 · (𝐵↑(𝐾 − 1))))) |
| 53 | 43, 48, 51, 52 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵 · (𝐵↑(𝐾 − 1)))) ≤ ((⌊‘(𝐵 · ((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵 · (𝐵↑(𝐾 − 1))))) |
| 54 | | expm1t 14131 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝐵↑𝐾) = ((𝐵↑(𝐾 − 1)) · 𝐵)) |
| 55 | | expcl 14120 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℂ ∧ (𝐾 − 1) ∈
ℕ0) → (𝐵↑(𝐾 − 1)) ∈
ℂ) |
| 56 | 44, 55 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝐵↑(𝐾 − 1)) ∈
ℂ) |
| 57 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ) → 𝐵 ∈
ℂ) |
| 58 | 56, 57 | mulcomd 11282 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ) → ((𝐵↑(𝐾 − 1)) · 𝐵) = (𝐵 · (𝐵↑(𝐾 − 1)))) |
| 59 | 54, 58 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℂ ∧ 𝐾 ∈ ℕ) → (𝐵↑𝐾) = (𝐵 · (𝐵↑(𝐾 − 1)))) |
| 60 | 26, 59 | sylan 580 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑𝐾) = (𝐵 · (𝐵↑(𝐾 − 1)))) |
| 61 | 60 | adantr 480 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (𝐵↑𝐾) = (𝐵 · (𝐵↑(𝐾 − 1)))) |
| 62 | 61 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)) = ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵 · (𝐵↑(𝐾 − 1))))) |
| 63 | 61 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵↑𝐾) · 𝐴) = ((𝐵 · (𝐵↑(𝐾 − 1))) · 𝐴)) |
| 64 | 26 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 𝐵 ∈
ℂ) |
| 65 | 26, 44, 55 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝐵↑(𝐾 − 1)) ∈
ℂ) |
| 66 | 65 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (𝐵↑(𝐾 − 1)) ∈
ℂ) |
| 67 | | recn 11245 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 68 | 67 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → 𝐴 ∈
ℂ) |
| 69 | 64, 66, 68 | mulassd 11284 |
. . . . . . . . 9
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵 · (𝐵↑(𝐾 − 1))) · 𝐴) = (𝐵 · ((𝐵↑(𝐾 − 1)) · 𝐴))) |
| 70 | 63, 69 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵↑𝐾) · 𝐴) = (𝐵 · ((𝐵↑(𝐾 − 1)) · 𝐴))) |
| 71 | 70 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
(⌊‘((𝐵↑𝐾) · 𝐴)) = (⌊‘(𝐵 · ((𝐵↑(𝐾 − 1)) · 𝐴)))) |
| 72 | 71, 61 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) = ((⌊‘(𝐵 · ((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵 · (𝐵↑(𝐾 − 1))))) |
| 73 | 53, 62, 72 | 3brtr4d 5175 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)) ≤ ((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾))) |
| 74 | | reflcl 13836 |
. . . . . . . 8
⊢ (((𝐵↑(𝐾 − 1)) · 𝐴) ∈ ℝ →
(⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)) ∈ ℝ) |
| 75 | 48, 74 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
(⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)) ∈ ℝ) |
| 76 | | remulcl 11240 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧
(⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)) ∈ ℝ) → (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) ∈ ℝ) |
| 77 | 22, 75, 76 | syl2anc 584 |
. . . . . 6
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) ∈ ℝ) |
| 78 | | modsubdir 13981 |
. . . . . 6
⊢
(((⌊‘((𝐵↑𝐾) · 𝐴)) ∈ ℝ ∧ (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) ∈ ℝ ∧ (𝐵↑𝐾) ∈ ℝ+) →
(((𝐵 ·
(⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)) ≤ ((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) ↔ (((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)))) mod (𝐵↑𝐾)) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾))))) |
| 79 | 12, 77, 19, 78 | syl3anc 1373 |
. . . . 5
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) → (((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)) ≤ ((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) ↔ (((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)))) mod (𝐵↑𝐾)) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾))))) |
| 80 | 73, 79 | mpbid 232 |
. . . 4
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
(((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴)))) mod (𝐵↑𝐾)) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) |
| 81 | 4, 42, 80 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) |
| 82 | 81 | 3impa 1110 |
. 2
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℝ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) |
| 83 | 82 | 3comr 1126 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) →
((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) |