| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
| 2 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
| 3 | 2 | elin2d 4205 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
| 4 | | prmnn 16711 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
| 6 | 5 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
| 7 | 6 | relogcld 26665 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
| 8 | 7 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
| 9 | | fsumconst 15826 |
. . . . 5
⊢
(((1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin ∧ (log‘𝑝) ∈ ℂ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) |
| 10 | 1, 8, 9 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) |
| 11 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ) |
| 12 | | 1red 11262 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈
ℝ) |
| 13 | 5 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
| 14 | | prmuz2 16733 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
| 15 | 3, 14 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
| 16 | | eluz2gt1 12962 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝) |
| 18 | 2 | elin1d 4204 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴)) |
| 19 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 20 | | elicc2 13452 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
| 21 | 19, 11, 20 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
| 22 | 18, 21 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)) |
| 23 | 22 | simp3d 1145 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴) |
| 24 | 12, 13, 11, 17, 23 | ltletrd 11421 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝐴) |
| 25 | 11, 24 | rplogcld 26671 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ+) |
| 26 | 13, 17 | rplogcld 26671 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) |
| 27 | 25, 26 | rpdivcld 13094 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ+) |
| 28 | 27 | rpred 13077 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) |
| 29 | 27 | rpge0d 13081 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤
((log‘𝐴) /
(log‘𝑝))) |
| 30 | | flge0nn0 13860 |
. . . . . . 7
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) |
| 31 | 28, 29, 30 | syl2anc 584 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) |
| 32 | | hashfz1 14385 |
. . . . . 6
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ0 →
(♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) |
| 33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) |
| 34 | 33 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝)) = ((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝))) |
| 35 | 28 | flcld 13838 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) |
| 36 | 35 | zcnd 12723 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℂ) |
| 37 | 36, 8 | mulcomd 11282 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝)) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 38 | 10, 34, 37 | 3eqtrrd 2782 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
| 39 | 38 | sumeq2dv 15738 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝)))) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
| 40 | | chpval2 27262 |
. 2
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 41 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
| 42 | | 0red 11264 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 ∈ ℝ) |
| 43 | | 1red 11262 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℝ) |
| 44 | | 0lt1 11785 |
. . . . . . . . 9
⊢ 0 <
1 |
| 45 | 44 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 < 1) |
| 46 | | elfzuz2 13569 |
. . . . . . . . 9
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘1)) |
| 47 | | eluzle 12891 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ (ℤ≥‘1) → 1 ≤ (⌊‘𝐴)) |
| 48 | 47 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → 1 ≤ (⌊‘𝐴)) |
| 49 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → 𝐴 ∈ ℝ) |
| 50 | | 1z 12647 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
| 51 | | flge 13845 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℤ) → (1 ≤ 𝐴
↔ 1 ≤ (⌊‘𝐴))) |
| 52 | 49, 50, 51 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → (1 ≤ 𝐴 ↔ 1 ≤ (⌊‘𝐴))) |
| 53 | 48, 52 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → 1 ≤ 𝐴) |
| 54 | 46, 53 | sylan2 593 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 1 ≤ 𝐴) |
| 55 | 42, 43, 41, 45, 54 | ltletrd 11421 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 < 𝐴) |
| 56 | 42, 41, 55 | ltled 11409 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 ≤ 𝐴) |
| 57 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ 𝑘 ∈
ℕ) |
| 58 | 57 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 𝑘 ∈
ℕ) |
| 59 | 58 | nnrecred 12317 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑘) ∈
ℝ) |
| 60 | 41, 56, 59 | recxpcld 26765 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ (𝐴↑𝑐(1 / 𝑘)) ∈
ℝ) |
| 61 | | chtval 27153 |
. . . . 5
⊢ ((𝐴↑𝑐(1 /
𝑘)) ∈ ℝ →
(θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
| 62 | 60, 61 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ (θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
| 63 | 62 | sumeq2dv 15738 |
. . 3
⊢ (𝐴 ∈ ℝ →
Σ𝑘 ∈
(1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑘 ∈ (1...(⌊‘𝐴))Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
| 64 | | ppifi 27149 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
| 65 | | fzfid 14014 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(1...(⌊‘𝐴))
∈ Fin) |
| 66 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
| 67 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
| 68 | 66, 67 | anim12i 613 |
. . . . . . 7
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
| 69 | 68 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
| 70 | | 0red 11264 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈
ℝ) |
| 71 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢
((0[,]𝐴) ∩
ℙ) ⊆ ℙ |
| 72 | 71 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
⊆ ℙ) |
| 73 | 72 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
| 74 | 73, 4 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
| 75 | 74 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
| 76 | 74 | nngt0d 12315 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝) |
| 77 | 70, 75, 11, 76, 23 | ltletrd 11421 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴) |
| 78 | 77 | ex 412 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 0 < 𝐴)) |
| 79 | 78 | adantrd 491 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 0 < 𝐴)) |
| 80 | 69, 79 | jcad 512 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴))) |
| 81 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) → 𝑝 ∈
ℙ) |
| 82 | 57, 81 | anim12ci 614 |
. . . . . . 7
⊢ ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
(𝑝 ∈ ℙ ∧
𝑘 ∈
ℕ)) |
| 83 | 82 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
(𝑝 ∈ ℙ ∧
𝑘 ∈
ℕ))) |
| 84 | 55 | ex 412 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝑘 ∈
(1...(⌊‘𝐴))
→ 0 < 𝐴)) |
| 85 | 84 | adantrd 491 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
0 < 𝐴)) |
| 86 | 83, 85 | jcad 512 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
((𝑝 ∈ ℙ ∧
𝑘 ∈ ℕ) ∧ 0
< 𝐴))) |
| 87 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ)) |
| 88 | | simprll 779 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℙ) |
| 89 | 88 | biantrud 531 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ))) |
| 90 | | 0red 11264 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ∈
ℝ) |
| 91 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝐴 ∈
ℝ) |
| 92 | 88, 4 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℕ) |
| 93 | 92 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℝ) |
| 94 | 92 | nnnn0d 12587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℕ0) |
| 95 | 94 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ≤ 𝑝) |
| 96 | | df-3an 1089 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ 𝐴) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ 𝐴)) |
| 97 | 20, 96 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
((𝑝 ∈ ℝ ∧ 0
≤ 𝑝) ∧ 𝑝 ≤ 𝐴))) |
| 98 | 97 | baibd 539 |
. . . . . . . . . . 11
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (𝑝
∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
| 99 | 90, 91, 93, 95, 98 | syl22anc 839 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
| 100 | 89, 99 | bitr3d 281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ) ↔ 𝑝 ≤ 𝐴)) |
| 101 | 87, 100 | bitrid 283 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ≤ 𝐴)) |
| 102 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 < 𝐴) |
| 103 | 91, 102 | elrpd 13074 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝐴 ∈
ℝ+) |
| 104 | 103 | relogcld 26665 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (log‘𝐴) ∈
ℝ) |
| 105 | 88, 14 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
(ℤ≥‘2)) |
| 106 | 105, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 1 < 𝑝) |
| 107 | 93, 106 | rplogcld 26671 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (log‘𝑝) ∈
ℝ+) |
| 108 | 104, 107 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
((log‘𝐴) /
(log‘𝑝)) ∈
ℝ) |
| 109 | | simprlr 780 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℕ) |
| 110 | 109 | nnzd 12640 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℤ) |
| 111 | | flge 13845 |
. . . . . . . . . 10
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 𝑘 ∈
ℤ) → (𝑘 ≤
((log‘𝐴) /
(log‘𝑝)) ↔ 𝑘 ≤
(⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 112 | 108, 110,
111 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ≤ ((log‘𝐴) / (log‘𝑝)) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 113 | 109 | nnnn0d 12587 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℕ0) |
| 114 | 92, 113 | nnexpcld 14284 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑘) ∈ ℕ) |
| 115 | 114 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑘) ∈
ℝ+) |
| 116 | 115, 103 | logled 26669 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (log‘(𝑝↑𝑘)) ≤ (log‘𝐴))) |
| 117 | 92 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℝ+) |
| 118 | | relogexp 26638 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
| 119 | 117, 110,
118 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
(log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
| 120 | 119 | breq1d 5153 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ (𝑘 · (log‘𝑝)) ≤ (log‘𝐴))) |
| 121 | 109 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℝ) |
| 122 | 121, 104,
107 | lemuldivd 13126 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑘 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
| 123 | 116, 120,
122 | 3bitrd 305 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
| 124 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 125 | 109, 124 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
(ℤ≥‘1)) |
| 126 | 108 | flcld 13838 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) |
| 127 | | elfz5 13556 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) →
(𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 128 | 125, 126,
127 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 129 | 112, 123,
128 | 3bitr4rd 312 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
| 130 | 101, 129 | anbi12d 632 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
| 131 | 91 | flcld 13838 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
(⌊‘𝐴) ∈
ℤ) |
| 132 | | elfz5 13556 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ ℤ) → (𝑘 ∈ (1...(⌊‘𝐴)) ↔ 𝑘 ≤ (⌊‘𝐴))) |
| 133 | 125, 131,
132 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ 𝑘 ≤
(⌊‘𝐴))) |
| 134 | | flge 13845 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℤ) → (𝑘 ≤ 𝐴 ↔ 𝑘 ≤ (⌊‘𝐴))) |
| 135 | 91, 110, 134 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ≤ 𝐴 ↔ 𝑘 ≤ (⌊‘𝐴))) |
| 136 | 133, 135 | bitr4d 282 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ 𝑘 ≤ 𝐴)) |
| 137 | | elin 3967 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) ↔ (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ)) |
| 138 | 88 | biantrud 531 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ))) |
| 139 | 103 | rpge0d 13081 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ≤ 𝐴) |
| 140 | 109 | nnrecred 12317 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (1 / 𝑘) ∈
ℝ) |
| 141 | 91, 139, 140 | recxpcld 26765 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐(1 /
𝑘)) ∈
ℝ) |
| 142 | | elicc2 13452 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (𝐴↑𝑐(1 / 𝑘)) ∈ ℝ) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘))))) |
| 143 | | df-3an 1089 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘))) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
| 144 | 142, 143 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝐴↑𝑐(1 / 𝑘)) ∈ ℝ) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘))))) |
| 145 | 144 | baibd 539 |
. . . . . . . . . . . . 13
⊢ (((0
∈ ℝ ∧ (𝐴↑𝑐(1 / 𝑘)) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤
𝑝)) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
| 146 | 90, 141, 93, 95, 145 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
| 147 | 138, 146 | bitr3d 281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ) ↔ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
| 148 | 91, 139, 140 | cxpge0d 26766 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ≤ (𝐴↑𝑐(1 /
𝑘))) |
| 149 | 109 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℝ+) |
| 150 | 93, 95, 141, 148, 149 | cxple2d 26769 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)) ↔ (𝑝↑𝑐𝑘) ≤ ((𝐴↑𝑐(1 / 𝑘))↑𝑐𝑘))) |
| 151 | 92 | nncnd 12282 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℂ) |
| 152 | | cxpexp 26710 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑐𝑘) = (𝑝↑𝑘)) |
| 153 | 151, 113,
152 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑐𝑘) = (𝑝↑𝑘)) |
| 154 | 109 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℂ) |
| 155 | 109 | nnne0d 12316 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ≠ 0) |
| 156 | 154, 155 | recid2d 12039 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((1 / 𝑘) · 𝑘) = 1) |
| 157 | 156 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐((1 /
𝑘) · 𝑘)) = (𝐴↑𝑐1)) |
| 158 | 103, 140,
154 | cxpmuld 26779 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐((1 /
𝑘) · 𝑘)) = ((𝐴↑𝑐(1 / 𝑘))↑𝑐𝑘)) |
| 159 | 91 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝐴 ∈
ℂ) |
| 160 | 159 | cxp1d 26748 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐1) =
𝐴) |
| 161 | 157, 158,
160 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝐴↑𝑐(1 /
𝑘))↑𝑐𝑘) = 𝐴) |
| 162 | 153, 161 | breq12d 5156 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑐𝑘) ≤ ((𝐴↑𝑐(1 / 𝑘))↑𝑐𝑘) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
| 163 | 147, 150,
162 | 3bitrd 305 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
| 164 | 137, 163 | bitrid 283 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
| 165 | 136, 164 | anbi12d 632 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) ↔
(𝑘 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
| 166 | 114 | nnred 12281 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑘) ∈ ℝ) |
| 167 | | bernneq3 14270 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ℕ0) → 𝑘 < (𝑝↑𝑘)) |
| 168 | 105, 113,
167 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 < (𝑝↑𝑘)) |
| 169 | 121, 166,
168 | ltled 11409 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ≤ (𝑝↑𝑘)) |
| 170 | | letr 11355 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑘 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑘 ≤ 𝐴)) |
| 171 | 121, 166,
91, 170 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑘 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑘 ≤ 𝐴)) |
| 172 | 169, 171 | mpand 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑘 ≤ 𝐴)) |
| 173 | 172 | pm4.71rd 562 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑘 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
| 174 | 151 | exp1d 14181 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑1) = 𝑝) |
| 175 | 92 | nnge1d 12314 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 1 ≤ 𝑝) |
| 176 | 93, 175, 125 | leexp2ad 14293 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑1) ≤ (𝑝↑𝑘)) |
| 177 | 174, 176 | eqbrtrrd 5167 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ≤ (𝑝↑𝑘)) |
| 178 | | letr 11355 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
| 179 | 93, 166, 91, 178 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
| 180 | 177, 179 | mpand 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ≤ 𝐴)) |
| 181 | 180 | pm4.71rd 562 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
| 182 | 165, 173,
181 | 3bitr2rd 308 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)))) |
| 183 | 130, 182 | bitrd 279 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)))) |
| 184 | 183 | ex 412 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ))))) |
| 185 | 80, 86, 184 | pm5.21ndd 379 |
. . . 4
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)))) |
| 186 | 8 | adantrr 717 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈
ℂ) |
| 187 | 64, 65, 1, 185, 186 | fsumcom2 15810 |
. . 3
⊢ (𝐴 ∈ ℝ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) = Σ𝑘 ∈ (1...(⌊‘𝐴))Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
| 188 | 63, 187 | eqtr4d 2780 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑘 ∈
(1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
| 189 | 39, 40, 188 | 3eqtr4d 2787 |
1
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑘 ∈
(1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘)))) |