This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chpchtsum

Description: The second Chebyshev function is the sum of the theta function at arguments quickly approaching zero. (This is usually stated as an infinite sum, but after a certain point, the terms are all zero, and it is easier for us to use an explicit finite sum.) (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion chpchtsum ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
2 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
3 2 elin2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
4 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
5 3 4 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
6 5 nnrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
7 6 relogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
9 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin ∧ ( log ‘ 𝑝 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
10 1 8 9 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
11 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ )
12 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 ∈ ℝ )
13 5 nnred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
14 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
15 3 14 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
16 eluz2gt1 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
17 15 16 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 )
18 2 elin1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 0 [,] 𝐴 ) )
19 0re ⊢ 0 ∈ ℝ
20 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
21 19 11 20 sylancr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
22 18 21 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) )
23 22 simp3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ 𝐴 )
24 12 13 11 17 23 ltletrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝐴 )
25 11 24 rplogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
26 13 17 rplogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
27 25 26 rpdivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ+ )
28 27 rpred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
29 27 rpge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
30 flge0nn0 ⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
31 28 29 30 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
32 hashfz1 ⊢ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
33 31 32 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
34 33 oveq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) = ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) )
35 28 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
36 35 zcnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℂ )
37 36 8 mulcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
38 10 34 37 3eqtrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
39 38 sumeq2dv ⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
40 chpval2 ⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
41 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
42 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ∈ ℝ )
43 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 1 ∈ ℝ )
44 0lt1 ⊢ 0 < 1
45 44 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 < 1 )
46 elfzuz2 ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
47 eluzle ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ≤ ( ⌊ ‘ 𝐴 ) )
48 47 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → 1 ≤ ( ⌊ ‘ 𝐴 ) )
49 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → 𝐴 ∈ ℝ )
50 1z ⊢ 1 ∈ ℤ
51 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ 𝐴 ↔ 1 ≤ ( ⌊ ‘ 𝐴 ) ) )
52 49 50 51 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → ( 1 ≤ 𝐴 ↔ 1 ≤ ( ⌊ ‘ 𝐴 ) ) )
53 48 52 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) → 1 ≤ 𝐴 )
54 46 53 sylan2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 1 ≤ 𝐴 )
55 42 43 41 45 54 ltletrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 < 𝐴 )
56 42 41 55 ltled ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ≤ 𝐴 )
57 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ )
58 57 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑘 ∈ ℕ )
59 58 nnrecred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
60 41 56 59 recxpcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ )
61 chtval ⊢ ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ → ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
62 60 61 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
63 62 sumeq2dv ⊢ ( 𝐴 ∈ ℝ → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
64 ppifi ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
65 fzfid ⊢ ( 𝐴 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
66 elinel2 ⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ℙ )
67 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
68 66 67 anim12i ⊢ ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
69 68 a1i ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
70 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ∈ ℝ )
71 inss2 ⊢ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ℙ
72 71 a1i ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ℙ )
73 72 sselda ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
74 73 4 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
75 74 nnred ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
76 74 nngt0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝑝 )
77 70 75 11 76 23 ltletrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 < 𝐴 )
78 77 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 0 < 𝐴 ) )
79 78 adantrd ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → 0 < 𝐴 ) )
80 69 79 jcad ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) )
81 elinel2 ⊢ ( 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) → 𝑝 ∈ ℙ )
82 57 81 anim12ci ⊢ ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
83 82 a1i ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
84 55 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 0 < 𝐴 ) )
85 84 adantrd ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → 0 < 𝐴 ) )
86 83 85 jcad ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) → ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) )
87 elin ⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) )
88 simprll ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℙ )
89 88 biantrud ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) ) )
90 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ∈ ℝ )
91 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℝ )
92 88 4 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℕ )
93 92 nnred ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℝ )
94 92 nnnn0d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℕ0 )
95 94 nn0ge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ≤ 𝑝 )
96 df-3an ⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ 𝐴 ) )
97 20 96 bitrdi ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ 𝐴 ) ) )
98 97 baibd ⊢ ( ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
99 90 91 93 95 98 syl22anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
100 89 99 bitr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) ↔ 𝑝 ≤ 𝐴 ) )
101 87 100 bitrid ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ 𝑝 ≤ 𝐴 ) )
102 simprr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 < 𝐴 )
103 91 102 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℝ+ )
104 103 relogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
105 88 14 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
106 105 16 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 1 < 𝑝 )
107 93 106 rplogcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
108 104 107 rerpdivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
109 simprlr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℕ )
110 109 nnzd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℤ )
111 flge ⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
112 108 110 111 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
113 109 nnnn0d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℕ0 )
114 92 113 nnexpcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
115 114 nnrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ+ )
116 115 103 logled ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ) )
117 92 nnrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℝ+ )
118 relogexp ⊢ ( ( 𝑝 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
119 117 110 118 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
120 119 breq1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ↔ ( 𝑘 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ) )
121 109 nnred ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℝ )
122 121 104 107 lemuldivd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑘 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
123 116 120 122 3bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
124 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
125 109 124 eleqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
126 108 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
127 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
128 125 126 127 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
129 112 123 128 3bitr4rd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
130 101 129 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑝 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
131 91 flcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
132 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
133 125 131 132 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
134 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ≤ 𝐴 ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
135 91 110 134 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ≤ 𝐴 ↔ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
136 133 135 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ 𝑘 ≤ 𝐴 ) )
137 elin ⊢ ( 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) )
138 88 biantrud ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) ) )
139 103 rpge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ≤ 𝐴 )
140 109 nnrecred ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 1 / 𝑘 ) ∈ ℝ )
141 91 139 140 recxpcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ )
142 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ) )
143 df-3an ⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
144 142 143 bitrdi ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ) )
145 144 baibd ⊢ ( ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
146 90 141 93 95 145 syl22anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ↔ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
147 138 146 bitr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) ↔ 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )
148 91 139 140 cxpge0d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 0 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) )
149 109 nnrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℝ+ )
150 93 95 141 148 149 cxple2d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ≤ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↔ ( 𝑝 ↑𝑐 𝑘 ) ≤ ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) ) )
151 92 nncnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ∈ ℂ )
152 cxpexp ⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑝 ↑𝑐 𝑘 ) = ( 𝑝 ↑ 𝑘 ) )
153 151 113 152 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑𝑐 𝑘 ) = ( 𝑝 ↑ 𝑘 ) )
154 109 nncnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ∈ ℂ )
155 109 nnne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ≠ 0 )
156 154 155 recid2d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 1 / 𝑘 ) · 𝑘 ) = 1 )
157 156 oveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑘 ) · 𝑘 ) ) = ( 𝐴 ↑𝑐 1 ) )
158 103 140 154 cxpmuld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 ( ( 1 / 𝑘 ) · 𝑘 ) ) = ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) )
159 91 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝐴 ∈ ℂ )
160 159 cxp1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝐴 ↑𝑐 1 ) = 𝐴 )
161 157 158 160 3eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) = 𝐴 )
162 153 161 breq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑𝑐 𝑘 ) ≤ ( ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ↑𝑐 𝑘 ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
163 147 150 162 3bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∧ 𝑝 ∈ ℙ ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
164 137 163 bitrid ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
165 136 164 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ↔ ( 𝑘 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
166 114 nnred ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ )
167 bernneq3 ⊢ ( ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 < ( 𝑝 ↑ 𝑘 ) )
168 105 113 167 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 < ( 𝑝 ↑ 𝑘 ) )
169 121 166 168 ltled ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑘 ≤ ( 𝑝 ↑ 𝑘 ) )
170 letr ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑘 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑘 ≤ 𝐴 ) )
171 121 166 91 170 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑘 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑘 ≤ 𝐴 ) )
172 169 171 mpand ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 → 𝑘 ≤ 𝐴 ) )
173 172 pm4.71rd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑘 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
174 151 exp1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 1 ) = 𝑝 )
175 92 nnge1d ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 1 ≤ 𝑝 )
176 93 175 125 leexp2ad ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( 𝑝 ↑ 1 ) ≤ ( 𝑝 ↑ 𝑘 ) )
177 174 176 eqbrtrrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) )
178 letr ⊢ ( ( 𝑝 ∈ ℝ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑝 ≤ 𝐴 ) )
179 93 166 91 178 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑝 ≤ 𝐴 ) )
180 177 179 mpand ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 → 𝑝 ≤ 𝐴 ) )
181 180 pm4.71rd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑝 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
182 165 173 181 3bitr2rd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ≤ 𝐴 ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) )
183 130 182 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) )
184 183 ex ⊢ ( 𝐴 ∈ ℝ → ( ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 0 < 𝐴 ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) ) )
185 80 86 184 pm5.21ndd ⊢ ( 𝐴 ∈ ℝ → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ) ) )
186 8 adantrr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
187 64 65 1 185 186 fsumcom2 ⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑝 ∈ ( ( 0 [,] ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
188 63 187 eqtr4d ⊢ ( 𝐴 ∈ ℝ → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
189 39 40 188 3eqtr4d ⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( θ ‘ ( 𝐴 ↑𝑐 ( 1 / 𝑘 ) ) ) )