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 ‘ 𝑁 ) ) ) < ( θ ‘ 𝑁 ) )