Metamath Proof Explorer


Theorem hgt750lemd

Description: An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021)

Ref Expression
Hypotheses hgt750lemc.n ( 𝜑𝑁 ∈ ℕ )
hgt750lemd.0 ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
Assertion hgt750lemd ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemc.n ( 𝜑𝑁 ∈ ℕ )
2 hgt750lemd.0 ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
3 fzfid ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
4 diffi ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
5 3 4 syl ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
6 vmaf Λ : ℕ ⟶ ℝ
7 6 a1i ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → Λ : ℕ ⟶ ℝ )
8 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
9 8 a1i ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
10 9 ssdifssd ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ℕ )
11 10 sselda ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → 𝑖 ∈ ℕ )
12 7 11 ffvelrnd ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
13 5 12 fsumrecl ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℝ )
14 2rp 2 ∈ ℝ+
15 14 a1i ( 𝜑 → 2 ∈ ℝ+ )
16 15 relogcld ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
17 1nn0 1 ∈ ℕ0
18 4re 4 ∈ ℝ
19 2re 2 ∈ ℝ
20 6re 6 ∈ ℝ
21 20 19 pm3.2i ( 6 ∈ ℝ ∧ 2 ∈ ℝ )
22 dp2cl ( ( 6 ∈ ℝ ∧ 2 ∈ ℝ ) → 6 2 ∈ ℝ )
23 21 22 ax-mp 6 2 ∈ ℝ
24 19 23 pm3.2i ( 2 ∈ ℝ ∧ 6 2 ∈ ℝ )
25 dp2cl ( ( 2 ∈ ℝ ∧ 6 2 ∈ ℝ ) → 2 6 2 ∈ ℝ )
26 24 25 ax-mp 2 6 2 ∈ ℝ
27 18 26 pm3.2i ( 4 ∈ ℝ ∧ 2 6 2 ∈ ℝ )
28 dp2cl ( ( 4 ∈ ℝ ∧ 2 6 2 ∈ ℝ ) → 4 2 6 2 ∈ ℝ )
29 27 28 ax-mp 4 2 6 2 ∈ ℝ
30 dpcl ( ( 1 ∈ ℕ0 4 2 6 2 ∈ ℝ ) → ( 1 . 4 2 6 2 ) ∈ ℝ )
31 17 29 30 mp2an ( 1 . 4 2 6 2 ) ∈ ℝ
32 31 a1i ( 𝜑 → ( 1 . 4 2 6 2 ) ∈ ℝ )
33 1 nnred ( 𝜑𝑁 ∈ ℝ )
34 1 nnrpd ( 𝜑𝑁 ∈ ℝ+ )
35 34 rpge0d ( 𝜑 → 0 ≤ 𝑁 )
36 33 35 resqrtcld ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
37 32 36 remulcld ( 𝜑 → ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
38 0nn0 0 ∈ ℕ0
39 0re 0 ∈ ℝ
40 1re 1 ∈ ℝ
41 39 40 pm3.2i ( 0 ∈ ℝ ∧ 1 ∈ ℝ )
42 dp2cl ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → 0 1 ∈ ℝ )
43 41 42 ax-mp 0 1 ∈ ℝ
44 39 43 pm3.2i ( 0 ∈ ℝ ∧ 0 1 ∈ ℝ )
45 dp2cl ( ( 0 ∈ ℝ ∧ 0 1 ∈ ℝ ) → 0 0 1 ∈ ℝ )
46 44 45 ax-mp 0 0 1 ∈ ℝ
47 39 46 pm3.2i ( 0 ∈ ℝ ∧ 0 0 1 ∈ ℝ )
48 dp2cl ( ( 0 ∈ ℝ ∧ 0 0 1 ∈ ℝ ) → 0 0 0 1 ∈ ℝ )
49 47 48 ax-mp 0 0 0 1 ∈ ℝ
50 dpcl ( ( 0 ∈ ℕ0 0 0 0 1 ∈ ℝ ) → ( 0 . 0 0 0 1 ) ∈ ℝ )
51 38 49 50 mp2an ( 0 . 0 0 0 1 ) ∈ ℝ
52 51 a1i ( 𝜑 → ( 0 . 0 0 0 1 ) ∈ ℝ )
53 52 36 remulcld ( 𝜑 → ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
54 1 nnzd ( 𝜑𝑁 ∈ ℤ )
55 chpvalz ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) )
56 54 55 syl ( 𝜑 → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) )
57 chtvalz ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
58 54 57 syl ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
59 inss2 ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ
60 59 a1i ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ )
61 60 sselda ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℙ )
62 vmaprm ( 𝑖 ∈ ℙ → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) )
63 61 62 syl ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) )
64 63 sumeq2dv ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
65 58 64 eqtr4d ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) )
66 56 65 oveq12d ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) )
67 infi ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin )
68 3 67 syl ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin )
69 6 a1i ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → Λ : ℕ ⟶ ℝ )
70 inss1 ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ( 1 ... 𝑁 )
71 70 8 sstri ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ
72 71 a1i ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ )
73 72 sselda ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℕ )
74 69 73 ffvelrnd ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
75 74 recnd ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
76 68 75 fsumcl ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ )
77 12 recnd ( ( 𝜑𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
78 5 77 fsumcl ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ )
79 inindif ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅
80 79 a1i ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅ )
81 inundif ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ( 1 ... 𝑁 )
82 81 eqcomi ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
83 82 a1i ( 𝜑 → ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) )
84 6 a1i ( ( 𝜑𝑖 ∈ ( 1 ... 𝑁 ) ) → Λ : ℕ ⟶ ℝ )
85 9 sselda ( ( 𝜑𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ℕ )
86 84 85 ffvelrnd ( ( 𝜑𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
87 86 recnd ( ( 𝜑𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
88 80 83 3 87 fsumsplit ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ) )
89 76 78 88 mvrladdd ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) )
90 66 89 eqtr2d ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) )
91 fveq2 ( 𝑥 = 𝑁 → ( ψ ‘ 𝑥 ) = ( ψ ‘ 𝑁 ) )
92 fveq2 ( 𝑥 = 𝑁 → ( θ ‘ 𝑥 ) = ( θ ‘ 𝑁 ) )
93 91 92 oveq12d ( 𝑥 = 𝑁 → ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) )
94 fveq2 ( 𝑥 = 𝑁 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝑁 ) )
95 94 oveq2d ( 𝑥 = 𝑁 → ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) ) = ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) )
96 93 95 breq12d ( 𝑥 = 𝑁 → ( ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) ) ↔ ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) ) )
97 ax-ros336 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) )
98 97 a1i ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) ) )
99 96 98 34 rspcdva ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) )
100 90 99 eqbrtrd ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) )
101 40 a1i ( 𝜑 → 1 ∈ ℝ )
102 log2le1 ( log ‘ 2 ) < 1
103 102 a1i ( 𝜑 → ( log ‘ 2 ) < 1 )
104 10nn0 1 0 ∈ ℕ0
105 7nn0 7 ∈ ℕ0
106 104 105 nn0expcli ( 1 0 ↑ 7 ) ∈ ℕ0
107 106 nn0rei ( 1 0 ↑ 7 ) ∈ ℝ
108 107 a1i ( 𝜑 → ( 1 0 ↑ 7 ) ∈ ℝ )
109 52 108 remulcld ( 𝜑 → ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) ∈ ℝ )
110 104 nn0rei 1 0 ∈ ℝ
111 0z 0 ∈ ℤ
112 3z 3 ∈ ℤ
113 110 111 112 3pm3.2i ( 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ )
114 1lt10 1 < 1 0
115 3pos 0 < 3
116 114 115 pm3.2i ( 1 < 1 0 ∧ 0 < 3 )
117 ltexp2a ( ( ( 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 0 < 3 ) ) → ( 1 0 ↑ 0 ) < ( 1 0 ↑ 3 ) )
118 113 116 117 mp2an ( 1 0 ↑ 0 ) < ( 1 0 ↑ 3 )
119 104 numexp0 ( 1 0 ↑ 0 ) = 1
120 119 eqcomi 1 = ( 1 0 ↑ 0 )
121 110 recni 1 0 ∈ ℂ
122 10pos 0 < 1 0
123 39 122 gtneii 1 0 ≠ 0
124 4z 4 ∈ ℤ
125 expm1 ( ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ∧ 4 ∈ ℤ ) → ( 1 0 ↑ ( 4 − 1 ) ) = ( ( 1 0 ↑ 4 ) / 1 0 ) )
126 121 123 124 125 mp3an ( 1 0 ↑ ( 4 − 1 ) ) = ( ( 1 0 ↑ 4 ) / 1 0 )
127 4m1e3 ( 4 − 1 ) = 3
128 127 oveq2i ( 1 0 ↑ ( 4 − 1 ) ) = ( 1 0 ↑ 3 )
129 4nn0 4 ∈ ℕ0
130 104 129 nn0expcli ( 1 0 ↑ 4 ) ∈ ℕ0
131 130 nn0cni ( 1 0 ↑ 4 ) ∈ ℂ
132 divrec2 ( ( ( 1 0 ↑ 4 ) ∈ ℂ ∧ 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) → ( ( 1 0 ↑ 4 ) / 1 0 ) = ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) ) )
133 131 121 123 132 mp3an ( ( 1 0 ↑ 4 ) / 1 0 ) = ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) )
134 126 128 133 3eqtr3ri ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) ) = ( 1 0 ↑ 3 )
135 118 120 134 3brtr4i 1 < ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) )
136 1rp 1 ∈ ℝ+
137 136 dp0h ( 0 . 1 ) = ( 1 / 1 0 )
138 137 oveq1i ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) ) = ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) )
139 135 138 breqtrri 1 < ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) )
140 139 a1i ( 𝜑 → 1 < ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) ) )
141 4p1e5 ( 4 + 1 ) = 5
142 5nn0 5 ∈ ℕ0
143 142 nn0zi 5 ∈ ℤ
144 38 136 141 124 143 dpexpp1 ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) ) = ( ( 0 . 0 1 ) · ( 1 0 ↑ 5 ) )
145 38 136 rpdp2cl 0 1 ∈ ℝ+
146 5p1e6 ( 5 + 1 ) = 6
147 6nn0 6 ∈ ℕ0
148 147 nn0zi 6 ∈ ℤ
149 38 145 146 143 148 dpexpp1 ( ( 0 . 0 1 ) · ( 1 0 ↑ 5 ) ) = ( ( 0 . 0 0 1 ) · ( 1 0 ↑ 6 ) )
150 38 145 rpdp2cl 0 0 1 ∈ ℝ+
151 6p1e7 ( 6 + 1 ) = 7
152 105 nn0zi 7 ∈ ℤ
153 38 150 151 148 152 dpexpp1 ( ( 0 . 0 0 1 ) · ( 1 0 ↑ 6 ) ) = ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) )
154 144 149 153 3eqtrri ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) = ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) )
155 140 154 breqtrrdi ( 𝜑 → 1 < ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) )
156 38 150 rpdp2cl 0 0 0 1 ∈ ℝ+
157 38 156 rpdpcl ( 0 . 0 0 0 1 ) ∈ ℝ+
158 157 a1i ( 𝜑 → ( 0 . 0 0 0 1 ) ∈ ℝ+ )
159 2nn0 2 ∈ ℕ0
160 159 105 deccl 2 7 ∈ ℕ0
161 104 160 nn0expcli ( 1 0 ↑ 2 7 ) ∈ ℕ0
162 161 nn0rei ( 1 0 ↑ 2 7 ) ∈ ℝ
163 162 a1i ( 𝜑 → ( 1 0 ↑ 2 7 ) ∈ ℝ )
164 161 nn0ge0i 0 ≤ ( 1 0 ↑ 2 7 )
165 164 a1i ( 𝜑 → 0 ≤ ( 1 0 ↑ 2 7 ) )
166 163 165 resqrtcld ( 𝜑 → ( √ ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ )
167 expmul ( ( 1 0 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 1 0 ↑ ( 7 · 2 ) ) = ( ( 1 0 ↑ 7 ) ↑ 2 ) )
168 121 105 159 167 mp3an ( 1 0 ↑ ( 7 · 2 ) ) = ( ( 1 0 ↑ 7 ) ↑ 2 )
169 7t2e14 ( 7 · 2 ) = 1 4
170 169 oveq2i ( 1 0 ↑ ( 7 · 2 ) ) = ( 1 0 ↑ 1 4 )
171 168 170 eqtr3i ( ( 1 0 ↑ 7 ) ↑ 2 ) = ( 1 0 ↑ 1 4 )
172 171 fveq2i ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( √ ‘ ( 1 0 ↑ 1 4 ) )
173 expgt0 ( ( 1 0 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < 1 0 ) → 0 < ( 1 0 ↑ 7 ) )
174 110 152 122 173 mp3an 0 < ( 1 0 ↑ 7 )
175 39 107 174 ltleii 0 ≤ ( 1 0 ↑ 7 )
176 sqrtsq ( ( ( 1 0 ↑ 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 7 ) ) → ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( 1 0 ↑ 7 ) )
177 107 175 176 mp2an ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( 1 0 ↑ 7 )
178 172 177 eqtr3i ( √ ‘ ( 1 0 ↑ 1 4 ) ) = ( 1 0 ↑ 7 )
179 17 129 deccl 1 4 ∈ ℕ0
180 179 nn0zi 1 4 ∈ ℤ
181 160 nn0zi 2 7 ∈ ℤ
182 110 180 181 3pm3.2i ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 2 7 ∈ ℤ )
183 4lt10 4 < 1 0
184 1lt2 1 < 2
185 17 159 129 105 183 184 decltc 1 4 < 2 7
186 114 185 pm3.2i ( 1 < 1 0 ∧ 1 4 < 2 7 )
187 ltexp2a ( ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 1 4 < 2 7 ) ) → ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) )
188 182 186 187 mp2an ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 )
189 104 179 nn0expcli ( 1 0 ↑ 1 4 ) ∈ ℕ0
190 189 nn0rei ( 1 0 ↑ 1 4 ) ∈ ℝ
191 expgt0 ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 0 < 1 0 ) → 0 < ( 1 0 ↑ 1 4 ) )
192 110 180 122 191 mp3an 0 < ( 1 0 ↑ 1 4 )
193 39 190 192 ltleii 0 ≤ ( 1 0 ↑ 1 4 )
194 190 193 pm3.2i ( ( 1 0 ↑ 1 4 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 1 4 ) )
195 162 164 pm3.2i ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 2 7 ) )
196 sqrtlt ( ( ( ( 1 0 ↑ 1 4 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 1 4 ) ) ∧ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 2 7 ) ) ) → ( ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) ↔ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) )
197 194 195 196 mp2an ( ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) ↔ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
198 188 197 mpbi ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) )
199 178 198 eqbrtrri ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) )
200 199 a1i ( 𝜑 → ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
201 163 165 33 35 sqrtled ( 𝜑 → ( ( 1 0 ↑ 2 7 ) ≤ 𝑁 ↔ ( √ ‘ ( 1 0 ↑ 2 7 ) ) ≤ ( √ ‘ 𝑁 ) ) )
202 2 201 mpbid ( 𝜑 → ( √ ‘ ( 1 0 ↑ 2 7 ) ) ≤ ( √ ‘ 𝑁 ) )
203 108 166 36 200 202 ltletrd ( 𝜑 → ( 1 0 ↑ 7 ) < ( √ ‘ 𝑁 ) )
204 108 36 158 203 ltmul2dd ( 𝜑 → ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) )
205 101 109 53 155 204 lttrd ( 𝜑 → 1 < ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) )
206 16 101 53 103 205 lttrd ( 𝜑 → ( log ‘ 2 ) < ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) )
207 13 16 37 53 100 206 lt2addd ( 𝜑 → ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) < ( ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
208 nfv 𝑖 𝜑
209 nfcv 𝑖 ( log ‘ 2 )
210 2prm 2 ∈ ℙ
211 210 a1i ( 𝜑 → 2 ∈ ℙ )
212 elndif ( 2 ∈ ℙ → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
213 211 212 syl ( 𝜑 → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
214 fveq2 ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( Λ ‘ 2 ) )
215 vmaprm ( 2 ∈ ℙ → ( Λ ‘ 2 ) = ( log ‘ 2 ) )
216 210 215 ax-mp ( Λ ‘ 2 ) = ( log ‘ 2 )
217 214 216 eqtrdi ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( log ‘ 2 ) )
218 2cnd ( 𝜑 → 2 ∈ ℂ )
219 2ne0 2 ≠ 0
220 219 a1i ( 𝜑 → 2 ≠ 0 )
221 218 220 logcld ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
222 208 209 5 211 213 77 217 221 fsumsplitsn ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) )
223 147 14 rpdp2cl 6 2 ∈ ℝ+
224 159 223 rpdp2cl 2 6 2 ∈ ℝ+
225 3rp 3 ∈ ℝ+
226 147 225 rpdp2cl 6 3 ∈ ℝ+
227 159 226 rpdp2cl 2 6 3 ∈ ℝ+
228 1p0e1 ( 1 + 0 ) = 1
229 4cn 4 ∈ ℂ
230 229 addid1i ( 4 + 0 ) = 4
231 2cn 2 ∈ ℂ
232 231 addid1i ( 2 + 0 ) = 2
233 3nn0 3 ∈ ℕ0
234 eqid 6 2 = 6 2
235 eqid 0 1 = 0 1
236 6cn 6 ∈ ℂ
237 236 addid1i ( 6 + 0 ) = 6
238 2p1e3 ( 2 + 1 ) = 3
239 147 159 38 17 234 235 237 238 decadd ( 6 2 + 0 1 ) = 6 3
240 147 159 38 17 147 233 239 dpadd ( ( 6 . 2 ) + ( 0 . 1 ) ) = ( 6 . 3 )
241 147 14 38 136 147 225 159 38 232 240 dpadd2 ( ( 2 . 6 2 ) + ( 0 . 0 1 ) ) = ( 2 . 6 3 )
242 159 223 38 145 159 226 129 38 230 241 dpadd2 ( ( 4 . 2 6 2 ) + ( 0 . 0 0 1 ) ) = ( 4 . 2 6 3 )
243 129 224 38 150 129 227 17 38 228 242 dpadd2 ( ( 1 . 4 2 6 2 ) + ( 0 . 0 0 0 1 ) ) = ( 1 . 4 2 6 3 )
244 243 oveq1i ( ( ( 1 . 4 2 6 2 ) + ( 0 . 0 0 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) )
245 32 recnd ( 𝜑 → ( 1 . 4 2 6 2 ) ∈ ℂ )
246 52 recnd ( 𝜑 → ( 0 . 0 0 0 1 ) ∈ ℂ )
247 36 recnd ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℂ )
248 245 246 247 adddird ( 𝜑 → ( ( ( 1 . 4 2 6 2 ) + ( 0 . 0 0 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
249 244 248 eqtr3id ( 𝜑 → ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
250 207 222 249 3brtr4d ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) )