Metamath Proof Explorer

Theorem fsumvma2

Description: Apply fsumvma for the common case of all numbers less than a real number A . (Contributed by Mario Carneiro, 30-Apr-2016)

Ref Expression
Hypotheses fsumvma2.1 ⊢ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) → 𝐵 = 𝐶 )
fsumvma2.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fsumvma2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐵 ∈ ℂ )
fsumvma2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑥 ) = 0 ) ) → 𝐵 = 0 )
Assertion fsumvma2 ( 𝜑 → Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐵 = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) 𝐶 )

Proof

Step Hyp Ref Expression
1 fsumvma2.1 ⊢ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) → 𝐵 = 𝐶 )
2 fsumvma2.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 fsumvma2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐵 ∈ ℂ )
4 fsumvma2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑥 ) = 0 ) ) → 𝐵 = 0 )
5 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
6 fz1ssnn ⊢ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ℕ
7 6 a1i ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ℕ )
8 ppifi ⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
9 2 8 syl ⊢ ( 𝜑 → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
10 elinel2 ⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) → 𝑝 ∈ ℙ )
11 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
12 10 11 anim12i ⊢ ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
13 12 pm4.71ri ⊢ ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) )
14 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝐴 ∈ ℝ )
15 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
16 15 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑝 ∈ ℕ )
17 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
18 17 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑘 ∈ ℕ0 )
19 16 18 nnexpcld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
20 19 nnzd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℤ )
21 flge ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℤ ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑝 ↑ 𝑘 ) ≤ ( ⌊ ‘ 𝐴 ) ) )
22 14 20 21 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑝 ↑ 𝑘 ) ≤ ( ⌊ ‘ 𝐴 ) ) )
23 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑝 ∈ ℙ )
24 23 15 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑝 ∈ ℕ )
25 24 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑝 ∈ ℝ+ )
26 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑘 ∈ ℕ )
27 26 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑘 ∈ ℤ )
28 relogexp ⊢ ( ( 𝑝 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
29 25 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( log ‘ ( 𝑝 ↑ 𝑘 ) ) = ( 𝑘 · ( log ‘ 𝑝 ) ) )
30 29 breq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ↔ ( 𝑘 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ) )
31 26 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑘 ∈ ℝ )
32 14 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝐴 ∈ ℝ )
33 0red ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 0 ∈ ℝ )
34 16 nnred ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑝 ∈ ℝ )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑝 ∈ ℝ )
36 24 nngt0d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 0 < 𝑝 )
37 0red ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 0 ∈ ℝ )
38 16 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑝 ∈ ℕ0 )
39 38 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 0 ≤ 𝑝 )
40 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
41 df-3an ⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ 𝐴 ) )
42 40 41 bitrdi ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ 𝐴 ) ) )
43 42 baibd ⊢ ( ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
44 37 14 34 39 43 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ 𝑝 ≤ 𝐴 ) )
45 44 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑝 ≤ 𝐴 )
46 33 35 32 36 45 ltletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 0 < 𝐴 )
47 32 46 elrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝐴 ∈ ℝ+ )
48 47 relogcld ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
49 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
50 eluzelre ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 𝑝 ∈ ℝ )
51 eluz2gt1 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
52 50 51 rplogcld ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
53 23 49 52 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
54 31 48 53 lemuldivd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ( 𝑘 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
55 48 53 rerpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
56 flge ⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
57 55 27 56 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑘 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
58 30 54 57 3bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
59 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℕ )
60 59 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ+ )
61 60 47 logled ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( log ‘ ( 𝑝 ↑ 𝑘 ) ) ≤ ( log ‘ 𝐴 ) ) )
62 simprr ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑘 ∈ ℕ )
63 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
64 62 63 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
66 55 flcld ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ )
67 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℤ ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
68 65 66 67 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ↔ 𝑘 ≤ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
69 58 61 68 3bitr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ∧ 𝑝 ∈ ( 0 [,] 𝐴 ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) )
70 69 pm5.32da ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) )
71 16 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑝 ∈ ℂ )
72 71 exp1d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ↑ 1 ) = 𝑝 )
73 16 nnge1d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 1 ≤ 𝑝 )
74 34 73 64 leexp2ad ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ↑ 1 ) ≤ ( 𝑝 ↑ 𝑘 ) )
75 72 74 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) )
76 19 nnred ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ℝ )
77 letr ⊢ ( ( 𝑝 ∈ ℝ ∧ ( 𝑝 ↑ 𝑘 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑝 ≤ 𝐴 ) )
78 34 76 14 77 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ≤ ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) → 𝑝 ≤ 𝐴 ) )
79 75 78 mpand ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 → 𝑝 ≤ 𝐴 ) )
80 79 44 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 → 𝑝 ∈ ( 0 [,] 𝐴 ) ) )
81 80 pm4.71rd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) ) )
82 elin ⊢ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑝 ∈ ℙ ) )
83 82 rbaib ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ 𝑝 ∈ ( 0 [,] 𝐴 ) ) )
84 83 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ↔ 𝑝 ∈ ( 0 [,] 𝐴 ) ) )
85 84 anbi1d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑝 ∈ ( 0 [,] 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) )
86 70 81 85 3bitr4rd ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ 𝐴 ) )
87 19 63 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( 𝑝 ↑ 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) )
88 14 flcld ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
89 elfz5 ⊢ ( ( ( 𝑝 ↑ 𝑘 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( ( 𝑝 ↑ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ ( ⌊ ‘ 𝐴 ) ) )
90 87 88 89 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑝 ↑ 𝑘 ) ≤ ( ⌊ ‘ 𝐴 ) ) )
91 22 86 90 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( 𝑝 ↑ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) )
92 91 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ) )
93 13 92 syl5bb ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ) )
94 1 5 7 9 93 3 4 fsumvma ⊢ ( 𝜑 → Σ 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐵 = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) 𝐶 )