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