Metamath Proof Explorer

Theorem chtppilimlem1

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses chtppilim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
chtppilim.2 ⊢ ( 𝜑 → 𝐴 < 1 )
chtppilim.3 ⊢ ( 𝜑 → 𝑁 ∈ ( 2 [,) +∞ ) )
chtppilim.4 ⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) < ( 1 − 𝐴 ) )
Assertion chtppilimlem1 ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 chtppilim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 chtppilim.2 ⊢ ( 𝜑 → 𝐴 < 1 )
3 chtppilim.3 ⊢ ( 𝜑 → 𝑁 ∈ ( 2 [,) +∞ ) )
4 chtppilim.4 ⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) < ( 1 − 𝐴 ) )
5 1 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 5 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
7 6 sqvald ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
8 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 𝐴 · 𝐴 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
9 2re ⊢ 2 ∈ ℝ
10 elicopnf ⊢ ( 2 ∈ ℝ → ( 𝑁 ∈ ( 2 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) ) )
11 9 10 ax-mp ⊢ ( 𝑁 ∈ ( 2 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) )
12 3 11 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) )
13 12 simpld ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
14 ppicl ⊢ ( 𝑁 ∈ ℝ → ( π ‘ 𝑁 ) ∈ ℕ0 )
15 13 14 syl ⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℕ0 )
16 15 nn0red ⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℝ )
17 16 recnd ⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℂ )
18 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
19 9 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
20 2pos ⊢ 0 < 2
21 20 a1i ⊢ ( 𝜑 → 0 < 2 )
22 12 simprd ⊢ ( 𝜑 → 2 ≤ 𝑁 )
23 18 19 13 21 22 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
24 13 23 elrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
25 24 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
26 25 recnd ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
27 6 6 17 26 mul4d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐴 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
28 8 27 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
29 5 16 remulcld ⊢ ( 𝜑 → ( 𝐴 · ( π ‘ 𝑁 ) ) ∈ ℝ )
30 5 25 remulcld ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ )
31 29 30 remulcld ⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ∈ ℝ )
32 24 5 rpcxpcld ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ+ )
33 32 rpred ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ )
34 ppicl ⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
35 33 34 syl ⊢ ( 𝜑 → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
36 35 nn0red ⊢ ( 𝜑 → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ )
37 16 36 resubcld ⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ∈ ℝ )
38 37 30 remulcld ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ∈ ℝ )
39 chtcl ⊢ ( 𝑁 ∈ ℝ → ( θ ‘ 𝑁 ) ∈ ℝ )
40 13 39 syl ⊢ ( 𝜑 → ( θ ‘ 𝑁 ) ∈ ℝ )
41 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
42 1lt2 ⊢ 1 < 2
43 42 a1i ⊢ ( 𝜑 → 1 < 2 )
44 41 19 13 43 22 ltletrd ⊢ ( 𝜑 → 1 < 𝑁 )
45 13 44 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ+ )
46 1 45 rpmulcld ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ+ )
47 16 33 resubcld ⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ )
48 ppinncl ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( π ‘ 𝑁 ) ∈ ℕ )
49 12 48 syl ⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℕ )
50 33 49 nndivred ⊢ ( 𝜑 → ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ∈ ℝ )
51 50 41 5 4 ltsub13d ⊢ ( 𝜑 → 𝐴 < ( 1 − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
52 33 recnd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℂ )
53 49 nnrpd ⊢ ( 𝜑 → ( π ‘ 𝑁 ) ∈ ℝ+ )
54 53 rpcnne0d ⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑁 ) ≠ 0 ) )
55 divsubdir ⊢ ( ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( 𝑁 ↑𝑐 𝐴 ) ∈ ℂ ∧ ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑁 ) ≠ 0 ) ) → ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) = ( ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
56 17 52 54 55 syl3anc ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) = ( ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
57 divid ⊢ ( ( ( π ‘ 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑁 ) ≠ 0 ) → ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) = 1 )
58 54 57 syl ⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) = 1 )
59 58 oveq1d ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) / ( π ‘ 𝑁 ) ) − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) = ( 1 − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
60 56 59 eqtrd ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) = ( 1 − ( ( 𝑁 ↑𝑐 𝐴 ) / ( π ‘ 𝑁 ) ) ) )
61 51 60 breqtrrd ⊢ ( 𝜑 → 𝐴 < ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) )
62 5 47 53 ltmuldivd ⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) < ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) ↔ 𝐴 < ( ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) / ( π ‘ 𝑁 ) ) ) )
63 61 62 mpbird ⊢ ( 𝜑 → ( 𝐴 · ( π ‘ 𝑁 ) ) < ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) )
64 ppiltx ⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ+ → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) < ( 𝑁 ↑𝑐 𝐴 ) )
65 32 64 syl ⊢ ( 𝜑 → ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) < ( 𝑁 ↑𝑐 𝐴 ) )
66 36 33 16 65 ltsub2dd ⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( 𝑁 ↑𝑐 𝐴 ) ) < ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
67 29 47 37 63 66 lttrd ⊢ ( 𝜑 → ( 𝐴 · ( π ‘ 𝑁 ) ) < ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
68 29 37 46 67 ltmul1dd ⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) < ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
69 fzfid ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin )
70 inss1 ⊢ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) )
71 ssfi ⊢ ( ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ) → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
72 69 70 71 sylancl ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
74 73 elin2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
75 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
76 75 nnrpd ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ+ )
77 74 76 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
78 77 relogcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
79 72 78 fsumrecl ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ∈ ℝ )
80 30 recnd ⊢ ( 𝜑 → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℂ )
81 fsumconst ⊢ ( ( ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin ∧ ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℂ ) → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) = ( ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
82 72 80 81 syl2anc ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) = ( ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
83 ppifl ⊢ ( 𝑁 ∈ ℝ → ( π ‘ ( ⌊ ‘ 𝑁 ) ) = ( π ‘ 𝑁 ) )
84 13 83 syl ⊢ ( 𝜑 → ( π ‘ ( ⌊ ‘ 𝑁 ) ) = ( π ‘ 𝑁 ) )
85 ppifl ⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) = ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) )
86 33 85 syl ⊢ ( 𝜑 → ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) = ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) )
87 84 86 oveq12d ⊢ ( 𝜑 → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ) = ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
88 41 13 44 ltled ⊢ ( 𝜑 → 1 ≤ 𝑁 )
89 1re ⊢ 1 ∈ ℝ
90 ltle ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 < 1 → 𝐴 ≤ 1 ) )
91 5 89 90 sylancl ⊢ ( 𝜑 → ( 𝐴 < 1 → 𝐴 ≤ 1 ) )
92 2 91 mpd ⊢ ( 𝜑 → 𝐴 ≤ 1 )
93 13 88 5 41 92 cxplead ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( 𝑁 ↑𝑐 1 ) )
94 13 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
95 94 cxp1d ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 1 ) = 𝑁 )
96 93 95 breqtrd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ≤ 𝑁 )
97 flword2 ⊢ ( ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ↑𝑐 𝐴 ) ≤ 𝑁 ) → ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
98 33 13 96 97 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) )
99 ppidif ⊢ ( ( ⌊ ‘ 𝑁 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ) = ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
100 98 99 syl ⊢ ( 𝜑 → ( ( π ‘ ( ⌊ ‘ 𝑁 ) ) − ( π ‘ ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) ) = ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
101 87 100 eqtr3d ⊢ ( 𝜑 → ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) = ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) )
102 101 oveq1d ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) = ( ( ♯ ‘ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
103 82 102 eqtr4d ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) = ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
104 30 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ )
105 33 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ )
106 reflcl ⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ )
107 peano2re ⊢ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℝ )
108 33 106 107 3syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℝ )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℝ )
110 77 rpred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
111 fllep1 ⊢ ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) )
112 33 111 syl ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑁 ↑𝑐 𝐴 ) ≤ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) )
114 73 elin1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) )
115 elfzle1 ⊢ ( 𝑝 ∈ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ≤ 𝑝 )
116 114 115 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ≤ 𝑝 )
117 105 109 110 113 116 letrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑁 ↑𝑐 𝐴 ) ≤ 𝑝 )
118 24 rpne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
119 94 118 6 cxpefd ⊢ ( 𝜑 → ( 𝑁 ↑𝑐 𝐴 ) = ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) )
120 119 eqcomd ⊢ ( 𝜑 → ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) = ( 𝑁 ↑𝑐 𝐴 ) )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) = ( 𝑁 ↑𝑐 𝐴 ) )
122 77 reeflogd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ 𝑝 ) ) = 𝑝 )
123 117 121 122 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑝 ) ) )
124 efle ⊢ ( ( ( 𝐴 · ( log ‘ 𝑁 ) ) ∈ ℝ ∧ ( log ‘ 𝑝 ) ∈ ℝ ) → ( ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ ( log ‘ 𝑝 ) ↔ ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑝 ) ) ) )
125 104 78 124 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ ( log ‘ 𝑝 ) ↔ ( exp ‘ ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( exp ‘ ( log ‘ 𝑝 ) ) ) )
126 123 125 mpbird ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ ( log ‘ 𝑝 ) )
127 72 104 78 126 fsumle ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( 𝐴 · ( log ‘ 𝑁 ) ) ≤ Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
128 103 127 eqbrtrrd ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
129 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin )
130 inss1 ⊢ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) )
131 ssfi ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
132 129 130 131 sylancl ⊢ ( 𝜑 → ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ∈ Fin )
133 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
134 133 elin2d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
135 prmuz2 ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
136 134 135 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
137 eluz2b2 ⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
138 136 137 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( 𝑝 ∈ ℕ ∧ 1 < 𝑝 ) )
139 138 simpld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
140 139 nnred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
141 138 simprd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 1 < 𝑝 )
142 140 141 rplogcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
143 142 rpred ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
144 142 rpge0d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ) → 0 ≤ ( log ‘ 𝑝 ) )
145 32 rpge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑁 ↑𝑐 𝐴 ) )
146 flge0nn0 ⊢ ( ( ( 𝑁 ↑𝑐 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝑁 ↑𝑐 𝐴 ) ) → ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
147 33 145 146 syl2anc ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 )
148 nn0p1nn ⊢ ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℕ )
149 147 148 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ℕ )
150 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
151 149 150 eleqtrdi ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
152 fzss1 ⊢ ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) ) )
153 ssrin ⊢ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑁 ) ) → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
154 151 152 153 3syl ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
155 132 143 144 154 fsumless ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ≤ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
156 chtval ⊢ ( 𝑁 ∈ ℝ → ( θ ‘ 𝑁 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
157 13 156 syl ⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
158 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
159 ppisval2 ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
160 13 158 159 sylancl ⊢ ( 𝜑 → ( ( 0 [,] 𝑁 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) )
161 160 sumeq1d ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( 0 [,] 𝑁 ) ∩ ℙ ) ( log ‘ 𝑝 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
162 157 161 eqtrd ⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) )
163 155 162 breqtrrd ⊢ ( 𝜑 → Σ 𝑝 ∈ ( ( ( ( ⌊ ‘ ( 𝑁 ↑𝑐 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑁 ) ) ∩ ℙ ) ( log ‘ 𝑝 ) ≤ ( θ ‘ 𝑁 ) )
164 38 79 40 128 163 letrd ⊢ ( 𝜑 → ( ( ( π ‘ 𝑁 ) − ( π ‘ ( 𝑁 ↑𝑐 𝐴 ) ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) ≤ ( θ ‘ 𝑁 ) )
165 31 38 40 68 164 ltletrd ⊢ ( 𝜑 → ( ( 𝐴 · ( π ‘ 𝑁 ) ) · ( 𝐴 · ( log ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )
166 28 165 eqbrtrd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( ( π ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )