Proof of Theorem digexp
Step | Hyp | Ref
| Expression |
1 | | eluzelcn 12450 |
. . . . . . . 8
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℂ) |
2 | | eluz2nn 12480 |
. . . . . . . . 9
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℕ) |
3 | 2 | nnne0d 11880 |
. . . . . . . 8
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ≠ 0) |
4 | 1, 3 | jca 515 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
5 | 4 | 3ad2ant1 1135 |
. . . . . 6
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐵 ∈ ℂ
∧ 𝐵 ≠
0)) |
6 | | nn0z 12200 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
7 | | nn0z 12200 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
8 | 6, 7 | anim12i 616 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
9 | 8 | ancomd 465 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
10 | 9 | 3adant1 1132 |
. . . . . 6
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑁 ∈ ℤ
∧ 𝐾 ∈
ℤ)) |
11 | | expsub 13683 |
. . . . . 6
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐵↑(𝑁 − 𝐾)) = ((𝐵↑𝑁) / (𝐵↑𝐾))) |
12 | 5, 10, 11 | syl2anc 587 |
. . . . 5
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑(𝑁 − 𝐾)) = ((𝐵↑𝑁) / (𝐵↑𝐾))) |
13 | 12 | eqcomd 2743 |
. . . 4
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝐵↑𝑁) / (𝐵↑𝐾)) = (𝐵↑(𝑁 − 𝐾))) |
14 | 13 | fveq2d 6721 |
. . 3
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (⌊‘((𝐵↑𝑁) / (𝐵↑𝐾))) = (⌊‘(𝐵↑(𝑁 − 𝐾)))) |
15 | 14 | oveq1d 7228 |
. 2
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((⌊‘((𝐵↑𝑁) / (𝐵↑𝐾))) mod 𝐵) = ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵)) |
16 | 2 | 3ad2ant1 1135 |
. . 3
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℕ) |
17 | | simp2 1139 |
. . 3
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐾 ∈
ℕ0) |
18 | | eluzelre 12449 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℝ) |
19 | | reexpcl 13652 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) ∈
ℝ) |
20 | 18, 19 | sylan 583 |
. . . . . 6
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐵↑𝑁) ∈ ℝ) |
21 | 18 | adantr 484 |
. . . . . . 7
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝐵 ∈
ℝ) |
22 | | simpr 488 |
. . . . . . 7
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
23 | | eluzge2nn0 12483 |
. . . . . . . . 9
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈
ℕ0) |
24 | 23 | nn0ge0d 12153 |
. . . . . . . 8
⊢ (𝐵 ∈
(ℤ≥‘2) → 0 ≤ 𝐵) |
25 | 24 | adantr 484 |
. . . . . . 7
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 0 ≤
𝐵) |
26 | 21, 22, 25 | expge0d 13734 |
. . . . . 6
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 0 ≤
(𝐵↑𝑁)) |
27 | 20, 26 | jca 515 |
. . . . 5
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → ((𝐵↑𝑁) ∈ ℝ ∧ 0 ≤ (𝐵↑𝑁))) |
28 | 27 | 3adant2 1133 |
. . . 4
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝐵↑𝑁) ∈ ℝ ∧ 0 ≤
(𝐵↑𝑁))) |
29 | | elrege0 13042 |
. . . 4
⊢ ((𝐵↑𝑁) ∈ (0[,)+∞) ↔ ((𝐵↑𝑁) ∈ ℝ ∧ 0 ≤ (𝐵↑𝑁))) |
30 | 28, 29 | sylibr 237 |
. . 3
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) ∈
(0[,)+∞)) |
31 | | nn0digval 45619 |
. . 3
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0
∧ (𝐵↑𝑁) ∈ (0[,)+∞)) →
(𝐾(digit‘𝐵)(𝐵↑𝑁)) = ((⌊‘((𝐵↑𝑁) / (𝐵↑𝐾))) mod 𝐵)) |
32 | 16, 17, 30, 31 | syl3anc 1373 |
. 2
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾(digit‘𝐵)(𝐵↑𝑁)) = ((⌊‘((𝐵↑𝑁) / (𝐵↑𝐾))) mod 𝐵)) |
33 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → 𝐾 = 𝑁) |
34 | 33 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → 𝑁 = 𝐾) |
35 | | nn0cn 12100 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
36 | 35 | 3ad2ant3 1137 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
37 | | nn0cn 12100 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
38 | 37 | 3ad2ant2 1136 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐾 ∈
ℂ) |
39 | 36, 38 | subeq0ad 11199 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 − 𝐾) = 0 ↔ 𝑁 = 𝐾)) |
40 | 39 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → ((𝑁 − 𝐾) = 0 ↔ 𝑁 = 𝐾)) |
41 | 34, 40 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (𝑁 − 𝐾) = 0) |
42 | 41 | oveq2d 7229 |
. . . . . . . 8
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (𝐵↑(𝑁 − 𝐾)) = (𝐵↑0)) |
43 | 1 | exp0d 13710 |
. . . . . . . . . 10
⊢ (𝐵 ∈
(ℤ≥‘2) → (𝐵↑0) = 1) |
44 | 43 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑0) =
1) |
45 | 44 | adantr 484 |
. . . . . . . 8
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (𝐵↑0) = 1) |
46 | 42, 45 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (𝐵↑(𝑁 − 𝐾)) = 1) |
47 | 46 | fveq2d 6721 |
. . . . . 6
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (⌊‘(𝐵↑(𝑁 − 𝐾))) = (⌊‘1)) |
48 | | 1zzd 12208 |
. . . . . . 7
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → 1 ∈ ℤ) |
49 | | flid 13383 |
. . . . . . 7
⊢ (1 ∈
ℤ → (⌊‘1) = 1) |
50 | 48, 49 | syl 17 |
. . . . . 6
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (⌊‘1) =
1) |
51 | 47, 50 | eqtrd 2777 |
. . . . 5
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (⌊‘(𝐵↑(𝑁 − 𝐾))) = 1) |
52 | 51 | oveq1d 7228 |
. . . 4
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵) = (1 mod 𝐵)) |
53 | | eluz2gt1 12516 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘2) → 1 < 𝐵) |
54 | | 1mod 13476 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 1 <
𝐵) → (1 mod 𝐵) = 1) |
55 | 18, 53, 54 | syl2anc 587 |
. . . . . 6
⊢ (𝐵 ∈
(ℤ≥‘2) → (1 mod 𝐵) = 1) |
56 | 55 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (1 mod 𝐵) =
1) |
57 | 56 | adantr 484 |
. . . 4
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → (1 mod 𝐵) = 1) |
58 | 52, 57 | eqtr2d 2778 |
. . 3
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ 𝐾 = 𝑁) → 1 = ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵)) |
59 | | simprl1 1220 |
. . . . . . . . 9
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → 𝐵 ∈
(ℤ≥‘2)) |
60 | 7 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈ ℤ) |
61 | 6 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝐾 ∈ ℤ) |
62 | 60, 61 | zsubcld 12287 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 − 𝐾) ∈ ℤ) |
63 | 62 | 3adant1 1132 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑁 − 𝐾) ∈
ℤ) |
64 | 63 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝑁 − 𝐾) ∈ ℤ) |
65 | | nn0re 12099 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
66 | 65 | 3ad2ant3 1137 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℝ) |
67 | | nn0re 12099 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
68 | 67 | 3ad2ant2 1136 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐾 ∈
ℝ) |
69 | 66, 68 | sublt0d 11458 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 − 𝐾) < 0 ↔ 𝑁 < 𝐾)) |
70 | 69 | biimprd 251 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝑁 < 𝐾 → (𝑁 − 𝐾) < 0)) |
71 | 70 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ ¬ 𝐾 = 𝑁) → (𝑁 < 𝐾 → (𝑁 − 𝐾) < 0)) |
72 | 71 | impcom 411 |
. . . . . . . . 9
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝑁 − 𝐾) < 0) |
73 | | expnegico01 45532 |
. . . . . . . . 9
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ (𝑁 − 𝐾) ∈ ℤ ∧ (𝑁 − 𝐾) < 0) → (𝐵↑(𝑁 − 𝐾)) ∈ (0[,)1)) |
74 | 59, 64, 72, 73 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐵↑(𝑁 − 𝐾)) ∈ (0[,)1)) |
75 | | ico01fl0 13394 |
. . . . . . . 8
⊢ ((𝐵↑(𝑁 − 𝐾)) ∈ (0[,)1) →
(⌊‘(𝐵↑(𝑁 − 𝐾))) = 0) |
76 | 74, 75 | syl 17 |
. . . . . . 7
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (⌊‘(𝐵↑(𝑁 − 𝐾))) = 0) |
77 | 76 | oveq1d 7228 |
. . . . . 6
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵) = (0 mod 𝐵)) |
78 | 2 | nnrpd 12626 |
. . . . . . . . 9
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈
ℝ+) |
79 | | 0mod 13475 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ+
→ (0 mod 𝐵) =
0) |
80 | 78, 79 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈
(ℤ≥‘2) → (0 mod 𝐵) = 0) |
81 | 80 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (0 mod 𝐵) =
0) |
82 | 81 | ad2antrl 728 |
. . . . . 6
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (0 mod 𝐵) = 0) |
83 | 77, 82 | eqtrd 2777 |
. . . . 5
⊢ ((𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵) = 0) |
84 | | eluzelz 12448 |
. . . . . . . . . . 11
⊢ (𝐵 ∈
(ℤ≥‘2) → 𝐵 ∈ ℤ) |
85 | 84 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℤ) |
86 | 85 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → 𝐵 ∈ ℤ) |
87 | 67, 65 | anim12i 616 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
88 | | lenlt 10911 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐾 ≤ 𝑁 ↔ ¬ 𝑁 < 𝐾)) |
89 | 88 | bicomd 226 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬
𝑁 < 𝐾 ↔ 𝐾 ≤ 𝑁)) |
90 | 87, 89 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 < 𝐾 ↔ 𝐾 ≤ 𝑁)) |
91 | 90 | biimpd 232 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (¬ 𝑁 < 𝐾 → 𝐾 ≤ 𝑁)) |
92 | 91 | 3adant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (¬ 𝑁 < 𝐾 → 𝐾 ≤ 𝑁)) |
93 | 92 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ ¬ 𝐾 = 𝑁) → (¬ 𝑁 < 𝐾 → 𝐾 ≤ 𝑁)) |
94 | 93 | impcom 411 |
. . . . . . . . . 10
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → 𝐾 ≤ 𝑁) |
95 | | 3simpc 1152 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0)) |
96 | 95 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐾 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
97 | | nn0sub 12140 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾 ≤ 𝑁 ↔ (𝑁 − 𝐾) ∈
ℕ0)) |
98 | 96, 97 | syl 17 |
. . . . . . . . . 10
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐾 ≤ 𝑁 ↔ (𝑁 − 𝐾) ∈
ℕ0)) |
99 | 94, 98 | mpbid 235 |
. . . . . . . . 9
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝑁 − 𝐾) ∈
ℕ0) |
100 | | zexpcl 13650 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℤ ∧ (𝑁 − 𝐾) ∈ ℕ0) → (𝐵↑(𝑁 − 𝐾)) ∈ ℤ) |
101 | 86, 99, 100 | syl2anc 587 |
. . . . . . . 8
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐵↑(𝑁 − 𝐾)) ∈ ℤ) |
102 | | flid 13383 |
. . . . . . . 8
⊢ ((𝐵↑(𝑁 − 𝐾)) ∈ ℤ →
(⌊‘(𝐵↑(𝑁 − 𝐾))) = (𝐵↑(𝑁 − 𝐾))) |
103 | 101, 102 | syl 17 |
. . . . . . 7
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (⌊‘(𝐵↑(𝑁 − 𝐾))) = (𝐵↑(𝑁 − 𝐾))) |
104 | 103 | oveq1d 7228 |
. . . . . 6
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵) = ((𝐵↑(𝑁 − 𝐾)) mod 𝐵)) |
105 | 1 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℂ) |
106 | 3 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ≠
0) |
107 | 105, 106,
63 | expm1d 13726 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑((𝑁 − 𝐾) − 1)) = ((𝐵↑(𝑁 − 𝐾)) / 𝐵)) |
108 | 107 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝐵↑(𝑁 − 𝐾)) / 𝐵) = (𝐵↑((𝑁 − 𝐾) − 1))) |
109 | 108 | ad2antrl 728 |
. . . . . . . 8
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((𝐵↑(𝑁 − 𝐾)) / 𝐵) = (𝐵↑((𝑁 − 𝐾) − 1))) |
110 | | pm4.56 989 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝐾 = 𝑁 ∧ ¬ 𝑁 < 𝐾) ↔ ¬ (𝐾 = 𝑁 ∨ 𝑁 < 𝐾)) |
111 | 87 | 3adant1 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾 ∈ ℝ
∧ 𝑁 ∈
ℝ)) |
112 | | axlttri 10904 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐾 < 𝑁 ↔ ¬ (𝐾 = 𝑁 ∨ 𝑁 < 𝐾))) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾 < 𝑁 ↔ ¬ (𝐾 = 𝑁 ∨ 𝑁 < 𝐾))) |
114 | 113 | biimprd 251 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (¬ (𝐾 = 𝑁 ∨ 𝑁 < 𝐾) → 𝐾 < 𝑁)) |
115 | 110, 114 | syl5bi 245 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((¬ 𝐾 = 𝑁 ∧ ¬ 𝑁 < 𝐾) → 𝐾 < 𝑁)) |
116 | 115 | expdimp 456 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ ¬ 𝐾 = 𝑁) → (¬ 𝑁 < 𝐾 → 𝐾 < 𝑁)) |
117 | 116 | impcom 411 |
. . . . . . . . . . 11
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → 𝐾 < 𝑁) |
118 | 8 | 3adant1 1132 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾 ∈ ℤ
∧ 𝑁 ∈
ℤ)) |
119 | 118 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
120 | | znnsub 12223 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . 11
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐾 < 𝑁 ↔ (𝑁 − 𝐾) ∈ ℕ)) |
122 | 117, 121 | mpbid 235 |
. . . . . . . . . 10
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝑁 − 𝐾) ∈ ℕ) |
123 | | nnm1nn0 12131 |
. . . . . . . . . 10
⊢ ((𝑁 − 𝐾) ∈ ℕ → ((𝑁 − 𝐾) − 1) ∈
ℕ0) |
124 | 122, 123 | syl 17 |
. . . . . . . . 9
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((𝑁 − 𝐾) − 1) ∈
ℕ0) |
125 | | zexpcl 13650 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℤ ∧ ((𝑁 − 𝐾) − 1) ∈ ℕ0)
→ (𝐵↑((𝑁 − 𝐾) − 1)) ∈
ℤ) |
126 | 86, 124, 125 | syl2anc 587 |
. . . . . . . 8
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (𝐵↑((𝑁 − 𝐾) − 1)) ∈
ℤ) |
127 | 109, 126 | eqeltrd 2838 |
. . . . . . 7
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((𝐵↑(𝑁 − 𝐾)) / 𝐵) ∈ ℤ) |
128 | 18 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℝ) |
129 | 128, 106,
63 | reexpclzd 13816 |
. . . . . . . . 9
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑(𝑁 − 𝐾)) ∈ ℝ) |
130 | 78 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ 𝐵 ∈
ℝ+) |
131 | | mod0 13449 |
. . . . . . . . 9
⊢ (((𝐵↑(𝑁 − 𝐾)) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (((𝐵↑(𝑁 − 𝐾)) mod 𝐵) = 0 ↔ ((𝐵↑(𝑁 − 𝐾)) / 𝐵) ∈ ℤ)) |
132 | 129, 130,
131 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (((𝐵↑(𝑁 − 𝐾)) mod 𝐵) = 0 ↔ ((𝐵↑(𝑁 − 𝐾)) / 𝐵) ∈ ℤ)) |
133 | 132 | ad2antrl 728 |
. . . . . . 7
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → (((𝐵↑(𝑁 − 𝐾)) mod 𝐵) = 0 ↔ ((𝐵↑(𝑁 − 𝐾)) / 𝐵) ∈ ℤ)) |
134 | 127, 133 | mpbird 260 |
. . . . . 6
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((𝐵↑(𝑁 − 𝐾)) mod 𝐵) = 0) |
135 | 104, 134 | eqtrd 2777 |
. . . . 5
⊢ ((¬
𝑁 < 𝐾 ∧ ((𝐵 ∈ (ℤ≥‘2)
∧ 𝐾 ∈
ℕ0 ∧ 𝑁
∈ ℕ0) ∧ ¬ 𝐾 = 𝑁)) → ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵) = 0) |
136 | 83, 135 | pm2.61ian 812 |
. . . 4
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ ¬ 𝐾 = 𝑁) → ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵) = 0) |
137 | 136 | eqcomd 2743 |
. . 3
⊢ (((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
∧ ¬ 𝐾 = 𝑁) → 0 =
((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵)) |
138 | 58, 137 | ifeqda 4475 |
. 2
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ if(𝐾 = 𝑁, 1, 0) = ((⌊‘(𝐵↑(𝑁 − 𝐾))) mod 𝐵)) |
139 | 15, 32, 138 | 3eqtr4d 2787 |
1
⊢ ((𝐵 ∈
(ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐾(digit‘𝐵)(𝐵↑𝑁)) = if(𝐾 = 𝑁, 1, 0)) |