Step | Hyp | Ref
| Expression |
1 | | fzfid 13074 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
2 | | inss2 4060 |
. . . . . . . . . 10
⊢
((0[,]𝐴) ∩
ℙ) ⊆ ℙ |
3 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
4 | 2, 3 | sseldi 3825 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
5 | | prmnn 15767 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
6 | 4, 5 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
7 | 6 | nnrpd 12161 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
8 | 7 | relogcld 24775 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
9 | 8 | recnd 10392 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
10 | | fsumconst 14903 |
. . . . 5
⊢
(((1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin ∧ (log‘𝑝) ∈ ℂ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) |
11 | 1, 9, 10 | syl2anc 579 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) |
12 | | simpl 476 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ) |
13 | | 1red 10364 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈
ℝ) |
14 | 6 | nnred 11374 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
15 | | prmuz2 15787 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
16 | 4, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
17 | | eluz2b2 12051 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
18 | 17 | simprbi 492 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝) |
20 | | inss1 4059 |
. . . . . . . . . . . . . 14
⊢
((0[,]𝐴) ∩
ℙ) ⊆ (0[,]𝐴) |
21 | 20, 3 | sseldi 3825 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴)) |
22 | | 0re 10365 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
23 | | elicc2 12533 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
24 | 22, 12, 23 | sylancr 581 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
25 | 21, 24 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)) |
26 | 25 | simp3d 1178 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴) |
27 | 13, 14, 12, 19, 26 | ltletrd 10523 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝐴) |
28 | 12, 27 | rplogcld 24781 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ+) |
29 | 14, 19 | rplogcld 24781 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) |
30 | 28, 29 | rpdivcld 12180 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ+) |
31 | 30 | rpred 12163 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) |
32 | 30 | rpge0d 12167 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤
((log‘𝐴) /
(log‘𝑝))) |
33 | | flge0nn0 12923 |
. . . . . . 7
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) |
34 | 31, 32, 33 | syl2anc 579 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) |
35 | | hashfz1 13433 |
. . . . . 6
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ0 →
(♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) |
37 | 36 | oveq1d 6925 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝)) = ((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝))) |
38 | 31 | flcld 12901 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) |
39 | 38 | zcnd 11818 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℂ) |
40 | 39, 9 | mulcomd 10385 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝)) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) |
41 | 11, 37, 40 | 3eqtrrd 2866 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
42 | 41 | sumeq2dv 14817 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝)))) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
43 | | chpval2 25363 |
. 2
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) |
44 | | simpl 476 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 𝐴 ∈
ℝ) |
45 | | 0red 10367 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 ∈ ℝ) |
46 | | 1red 10364 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 1 ∈ ℝ) |
47 | | 0lt1 10881 |
. . . . . . . . 9
⊢ 0 <
1 |
48 | 47 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 < 1) |
49 | | elfzuz2 12646 |
. . . . . . . . 9
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘1)) |
50 | | eluzle 11988 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ (ℤ≥‘1) → 1 ≤ (⌊‘𝐴)) |
51 | 50 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → 1 ≤ (⌊‘𝐴)) |
52 | | simpl 476 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → 𝐴 ∈ ℝ) |
53 | | 1z 11742 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
54 | | flge 12908 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℤ) → (1 ≤ 𝐴
↔ 1 ≤ (⌊‘𝐴))) |
55 | 52, 53, 54 | sylancl 580 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → (1 ≤ 𝐴 ↔ 1 ≤ (⌊‘𝐴))) |
56 | 51, 55 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘1)) → 1 ≤ 𝐴) |
57 | 49, 56 | sylan2 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 1 ≤ 𝐴) |
58 | 45, 46, 44, 48, 57 | ltletrd 10523 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 < 𝐴) |
59 | 45, 44, 58 | ltled 10511 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 0 ≤ 𝐴) |
60 | | elfznn 12670 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝐴))
→ 𝑘 ∈
ℕ) |
61 | 60 | adantl 475 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ 𝑘 ∈
ℕ) |
62 | 61 | nnrecred 11409 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ (1 / 𝑘) ∈
ℝ) |
63 | 44, 59, 62 | recxpcld 24875 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ (𝐴↑𝑐(1 / 𝑘)) ∈
ℝ) |
64 | | chtval 25256 |
. . . . 5
⊢ ((𝐴↑𝑐(1 /
𝑘)) ∈ ℝ →
(θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
65 | 63, 64 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈
(1...(⌊‘𝐴)))
→ (θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
66 | 65 | sumeq2dv 14817 |
. . 3
⊢ (𝐴 ∈ ℝ →
Σ𝑘 ∈
(1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑘 ∈ (1...(⌊‘𝐴))Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
67 | | ppifi 25252 |
. . . 4
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
68 | | fzfid 13074 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(1...(⌊‘𝐴))
∈ Fin) |
69 | 2 | sseli 3823 |
. . . . . . . 8
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
70 | | elfznn 12670 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
71 | 69, 70 | anim12i 606 |
. . . . . . 7
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
72 | 71 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ))) |
73 | | 0red 10367 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈
ℝ) |
74 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
⊆ ℙ) |
75 | 74 | sselda 3827 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
76 | 75, 5 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
77 | 76 | nnred 11374 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
78 | 76 | nngt0d 11407 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝) |
79 | 73, 77, 12, 78, 26 | ltletrd 10523 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴) |
80 | 79 | ex 403 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 0 < 𝐴)) |
81 | 80 | adantrd 487 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 0 < 𝐴)) |
82 | 72, 81 | jcad 508 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴))) |
83 | | inss2 4060 |
. . . . . . . . 9
⊢
((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) ⊆
ℙ |
84 | 83 | sseli 3823 |
. . . . . . . 8
⊢ (𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) → 𝑝 ∈
ℙ) |
85 | 60, 84 | anim12ci 607 |
. . . . . . 7
⊢ ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
(𝑝 ∈ ℙ ∧
𝑘 ∈
ℕ)) |
86 | 85 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
(𝑝 ∈ ℙ ∧
𝑘 ∈
ℕ))) |
87 | 58 | ex 403 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝑘 ∈
(1...(⌊‘𝐴))
→ 0 < 𝐴)) |
88 | 87 | adantrd 487 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
0 < 𝐴)) |
89 | 86, 88 | jcad 508 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) →
((𝑝 ∈ ℙ ∧
𝑘 ∈ ℕ) ∧ 0
< 𝐴))) |
90 | | elin 4025 |
. . . . . . . . 9
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ)) |
91 | | simprll 797 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℙ) |
92 | 91 | biantrud 527 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ))) |
93 | | 0red 10367 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ∈
ℝ) |
94 | | simpl 476 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝐴 ∈
ℝ) |
95 | 91, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℕ) |
96 | 95 | nnred 11374 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℝ) |
97 | 95 | nnnn0d 11685 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℕ0) |
98 | 97 | nn0ge0d 11688 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ≤ 𝑝) |
99 | | df-3an 1113 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ 𝐴) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ 𝐴)) |
100 | 23, 99 | syl6bb 279 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
((𝑝 ∈ ℝ ∧ 0
≤ 𝑝) ∧ 𝑝 ≤ 𝐴))) |
101 | 100 | baibd 535 |
. . . . . . . . . . 11
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (𝑝
∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
102 | 93, 94, 96, 98, 101 | syl22anc 872 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
103 | 92, 102 | bitr3d 273 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ) ↔ 𝑝 ≤ 𝐴)) |
104 | 90, 103 | syl5bb 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ≤ 𝐴)) |
105 | | simprr 789 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 < 𝐴) |
106 | 94, 105 | elrpd 12160 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝐴 ∈
ℝ+) |
107 | 106 | relogcld 24775 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (log‘𝐴) ∈
ℝ) |
108 | 91, 15 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
(ℤ≥‘2)) |
109 | 108, 18 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 1 < 𝑝) |
110 | 96, 109 | rplogcld 24781 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (log‘𝑝) ∈
ℝ+) |
111 | 107, 110 | rerpdivcld 12194 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
((log‘𝐴) /
(log‘𝑝)) ∈
ℝ) |
112 | | simprlr 798 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℕ) |
113 | 112 | nnzd 11816 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℤ) |
114 | | flge 12908 |
. . . . . . . . . 10
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 𝑘 ∈
ℤ) → (𝑘 ≤
((log‘𝐴) /
(log‘𝑝)) ↔ 𝑘 ≤
(⌊‘((log‘𝐴) / (log‘𝑝))))) |
115 | 111, 113,
114 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ≤ ((log‘𝐴) / (log‘𝑝)) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
116 | 112 | nnnn0d 11685 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℕ0) |
117 | 95, 116 | nnexpcld 13333 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑘) ∈ ℕ) |
118 | 117 | nnrpd 12161 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑘) ∈
ℝ+) |
119 | 118, 106 | logled 24779 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (log‘(𝑝↑𝑘)) ≤ (log‘𝐴))) |
120 | 95 | nnrpd 12161 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℝ+) |
121 | | relogexp 24748 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
122 | 120, 113,
121 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
(log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
123 | 122 | breq1d 4885 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ (𝑘 · (log‘𝑝)) ≤ (log‘𝐴))) |
124 | 112 | nnred 11374 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℝ) |
125 | 124, 107,
110 | lemuldivd 12212 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑘 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
126 | 119, 123,
125 | 3bitrd 297 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
127 | | nnuz 12012 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
128 | 112, 127 | syl6eleq 2916 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
(ℤ≥‘1)) |
129 | 111 | flcld 12901 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) |
130 | | elfz5 12634 |
. . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) →
(𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
131 | 128, 129,
130 | syl2anc 579 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
132 | 115, 126,
131 | 3bitr4rd 304 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
133 | 104, 132 | anbi12d 624 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
134 | 94 | flcld 12901 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) →
(⌊‘𝐴) ∈
ℤ) |
135 | | elfz5 12634 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈ ℤ) → (𝑘 ∈ (1...(⌊‘𝐴)) ↔ 𝑘 ≤ (⌊‘𝐴))) |
136 | 128, 134,
135 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ 𝑘 ≤
(⌊‘𝐴))) |
137 | | flge 12908 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑘 ∈ ℤ) → (𝑘 ≤ 𝐴 ↔ 𝑘 ≤ (⌊‘𝐴))) |
138 | 94, 113, 137 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ≤ 𝐴 ↔ 𝑘 ≤ (⌊‘𝐴))) |
139 | 136, 138 | bitr4d 274 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑘 ∈
(1...(⌊‘𝐴))
↔ 𝑘 ≤ 𝐴)) |
140 | | elin 4025 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) ↔ (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ)) |
141 | 91 | biantrud 527 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ))) |
142 | 106 | rpge0d 12167 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ≤ 𝐴) |
143 | 112 | nnrecred 11409 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (1 / 𝑘) ∈
ℝ) |
144 | 94, 142, 143 | recxpcld 24875 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐(1 /
𝑘)) ∈
ℝ) |
145 | | elicc2 12533 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ (𝐴↑𝑐(1 / 𝑘)) ∈ ℝ) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘))))) |
146 | | df-3an 1113 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘))) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
147 | 145, 146 | syl6bb 279 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝐴↑𝑐(1 / 𝑘)) ∈ ℝ) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘))))) |
148 | 147 | baibd 535 |
. . . . . . . . . . . . 13
⊢ (((0
∈ ℝ ∧ (𝐴↑𝑐(1 / 𝑘)) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤
𝑝)) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
149 | 93, 144, 96, 98, 148 | syl22anc 872 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ↔ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
150 | 141, 149 | bitr3d 273 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ) ↔ 𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)))) |
151 | 94, 142, 143 | cxpge0d 24876 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 0 ≤ (𝐴↑𝑐(1 /
𝑘))) |
152 | 112 | nnrpd 12161 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℝ+) |
153 | 96, 98, 144, 151, 152 | cxple2d 24879 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ≤ (𝐴↑𝑐(1 / 𝑘)) ↔ (𝑝↑𝑐𝑘) ≤ ((𝐴↑𝑐(1 / 𝑘))↑𝑐𝑘))) |
154 | 95 | nncnd 11375 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ∈
ℂ) |
155 | | cxpexp 24820 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑐𝑘) = (𝑝↑𝑘)) |
156 | 154, 116,
155 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑐𝑘) = (𝑝↑𝑘)) |
157 | 112 | nncnd 11375 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ∈
ℂ) |
158 | 112 | nnne0d 11408 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ≠ 0) |
159 | 157, 158 | recid2d 11130 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((1 / 𝑘) · 𝑘) = 1) |
160 | 159 | oveq2d 6926 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐((1 /
𝑘) · 𝑘)) = (𝐴↑𝑐1)) |
161 | 106, 143,
157 | cxpmuld 24888 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐((1 /
𝑘) · 𝑘)) = ((𝐴↑𝑐(1 / 𝑘))↑𝑐𝑘)) |
162 | 94 | recnd 10392 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝐴 ∈
ℂ) |
163 | 162 | cxp1d 24858 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝐴↑𝑐1) =
𝐴) |
164 | 160, 161,
163 | 3eqtr3d 2869 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝐴↑𝑐(1 /
𝑘))↑𝑐𝑘) = 𝐴) |
165 | 156, 164 | breq12d 4888 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑐𝑘) ≤ ((𝐴↑𝑐(1 / 𝑘))↑𝑐𝑘) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
166 | 150, 153,
165 | 3bitrd 297 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ (0[,](𝐴↑𝑐(1 / 𝑘))) ∧ 𝑝 ∈ ℙ) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
167 | 140, 166 | syl5bb 275 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩ ℙ) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
168 | 139, 167 | anbi12d 624 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑘 ∈
(1...(⌊‘𝐴))
∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 /
𝑘))) ∩ ℙ)) ↔
(𝑘 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
169 | 117 | nnred 11374 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑𝑘) ∈ ℝ) |
170 | | bernneq3 13293 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
(ℤ≥‘2) ∧ 𝑘 ∈ ℕ0) → 𝑘 < (𝑝↑𝑘)) |
171 | 108, 116,
170 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 < (𝑝↑𝑘)) |
172 | 124, 169,
171 | ltled 10511 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑘 ≤ (𝑝↑𝑘)) |
173 | | letr 10457 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑘 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑘 ≤ 𝐴)) |
174 | 124, 169,
94, 173 | syl3anc 1494 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑘 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑘 ≤ 𝐴)) |
175 | 172, 174 | mpand 686 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑘 ≤ 𝐴)) |
176 | 175 | pm4.71rd 558 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑘 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
177 | 154 | exp1d 13304 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑1) = 𝑝) |
178 | 95 | nnge1d 11406 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 1 ≤ 𝑝) |
179 | 96, 178, 128 | leexp2ad 13344 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → (𝑝↑1) ≤ (𝑝↑𝑘)) |
180 | 177, 179 | eqbrtrrd 4899 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → 𝑝 ≤ (𝑝↑𝑘)) |
181 | | letr 10457 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
182 | 96, 169, 94, 181 | syl3anc 1494 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
183 | 180, 182 | mpand 686 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ≤ 𝐴)) |
184 | 183 | pm4.71rd 558 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴))) |
185 | 168, 176,
184 | 3bitr2rd 300 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ≤ 𝐴 ∧ (𝑝↑𝑘) ≤ 𝐴) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)))) |
186 | 133, 185 | bitrd 271 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)))) |
187 | 186 | ex 403 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ 0 <
𝐴) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ))))) |
188 | 82, 89, 187 | pm5.21ndd 371 |
. . . 4
⊢ (𝐴 ∈ ℝ → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑘 ∈ (1...(⌊‘𝐴)) ∧ 𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)))) |
189 | 9 | adantrr 708 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈
ℂ) |
190 | 67, 68, 1, 188, 189 | fsumcom2 14887 |
. . 3
⊢ (𝐴 ∈ ℝ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) = Σ𝑘 ∈ (1...(⌊‘𝐴))Σ𝑝 ∈ ((0[,](𝐴↑𝑐(1 / 𝑘))) ∩
ℙ)(log‘𝑝)) |
191 | 66, 190 | eqtr4d 2864 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑘 ∈
(1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘))) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
192 | 42, 43, 191 | 3eqtr4d 2871 |
1
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑘 ∈
(1...(⌊‘𝐴))(θ‘(𝐴↑𝑐(1 / 𝑘)))) |