Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hgt750lemd Structured version   Visualization version   GIF version

Theorem hgt750lemd 31328
Description: An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021.)
Hypotheses
Ref Expression
hgt750lemc.n (𝜑𝑁 ∈ ℕ)
hgt750lemd.0 (𝜑 → (10↑27) ≤ 𝑁)
Assertion
Ref Expression
hgt750lemd (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1.4263) · (√‘𝑁)))
Distinct variable groups:   𝑖,𝑁   𝜑,𝑖

Proof of Theorem hgt750lemd
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fzfid 13091 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
2 diffi 8480 . . . . 5 ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
31, 2syl 17 . . . 4 (𝜑 → ((1...𝑁) ∖ ℙ) ∈ Fin)
4 vmaf 25297 . . . . . 6 Λ:ℕ⟶ℝ
54a1i 11 . . . . 5 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → Λ:ℕ⟶ℝ)
6 fz1ssnn 12689 . . . . . . . 8 (1...𝑁) ⊆ ℕ
76a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) ⊆ ℕ)
87ssdifssd 3970 . . . . . 6 (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
98sselda 3820 . . . . 5 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → 𝑖 ∈ ℕ)
105, 9ffvelrnd 6624 . . . 4 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → (Λ‘𝑖) ∈ ℝ)
113, 10fsumrecl 14872 . . 3 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈ ℝ)
12 2rp 12142 . . . . 5 2 ∈ ℝ+
1312a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ+)
1413relogcld 24806 . . 3 (𝜑 → (log‘2) ∈ ℝ)
15 1nn0 11660 . . . . . 6 1 ∈ ℕ0
16 4re 11460 . . . . . . . 8 4 ∈ ℝ
17 2re 11449 . . . . . . . . . 10 2 ∈ ℝ
18 6re 11468 . . . . . . . . . . . 12 6 ∈ ℝ
1918, 17pm3.2i 464 . . . . . . . . . . 11 (6 ∈ ℝ ∧ 2 ∈ ℝ)
20 dp2cl 30150 . . . . . . . . . . 11 ((6 ∈ ℝ ∧ 2 ∈ ℝ) → 62 ∈ ℝ)
2119, 20ax-mp 5 . . . . . . . . . 10 62 ∈ ℝ
2217, 21pm3.2i 464 . . . . . . . . 9 (2 ∈ ℝ ∧ 62 ∈ ℝ)
23 dp2cl 30150 . . . . . . . . 9 ((2 ∈ ℝ ∧ 62 ∈ ℝ) → 262 ∈ ℝ)
2422, 23ax-mp 5 . . . . . . . 8 262 ∈ ℝ
2516, 24pm3.2i 464 . . . . . . 7 (4 ∈ ℝ ∧ 262 ∈ ℝ)
26 dp2cl 30150 . . . . . . 7 ((4 ∈ ℝ ∧ 262 ∈ ℝ) → 4262 ∈ ℝ)
2725, 26ax-mp 5 . . . . . 6 4262 ∈ ℝ
28 dpcl 30161 . . . . . 6 ((1 ∈ ℕ04262 ∈ ℝ) → (1.4262) ∈ ℝ)
2915, 27, 28mp2an 682 . . . . 5 (1.4262) ∈ ℝ
3029a1i 11 . . . 4 (𝜑 → (1.4262) ∈ ℝ)
31 hgt750lemc.n . . . . . 6 (𝜑𝑁 ∈ ℕ)
3231nnred 11391 . . . . 5 (𝜑𝑁 ∈ ℝ)
3331nnrpd 12179 . . . . . 6 (𝜑𝑁 ∈ ℝ+)
3433rpge0d 12185 . . . . 5 (𝜑 → 0 ≤ 𝑁)
3532, 34resqrtcld 14564 . . . 4 (𝜑 → (√‘𝑁) ∈ ℝ)
3630, 35remulcld 10407 . . 3 (𝜑 → ((1.4262) · (√‘𝑁)) ∈ ℝ)
37 0nn0 11659 . . . . . 6 0 ∈ ℕ0
38 0re 10378 . . . . . . . 8 0 ∈ ℝ
39 1re 10376 . . . . . . . . . . . 12 1 ∈ ℝ
4038, 39pm3.2i 464 . . . . . . . . . . 11 (0 ∈ ℝ ∧ 1 ∈ ℝ)
41 dp2cl 30150 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → 01 ∈ ℝ)
4240, 41ax-mp 5 . . . . . . . . . 10 01 ∈ ℝ
4338, 42pm3.2i 464 . . . . . . . . 9 (0 ∈ ℝ ∧ 01 ∈ ℝ)
44 dp2cl 30150 . . . . . . . . 9 ((0 ∈ ℝ ∧ 01 ∈ ℝ) → 001 ∈ ℝ)
4543, 44ax-mp 5 . . . . . . . 8 001 ∈ ℝ
4638, 45pm3.2i 464 . . . . . . 7 (0 ∈ ℝ ∧ 001 ∈ ℝ)
47 dp2cl 30150 . . . . . . 7 ((0 ∈ ℝ ∧ 001 ∈ ℝ) → 0001 ∈ ℝ)
4846, 47ax-mp 5 . . . . . 6 0001 ∈ ℝ
49 dpcl 30161 . . . . . 6 ((0 ∈ ℕ00001 ∈ ℝ) → (0.0001) ∈ ℝ)
5037, 48, 49mp2an 682 . . . . 5 (0.0001) ∈ ℝ
5150a1i 11 . . . 4 (𝜑 → (0.0001) ∈ ℝ)
5251, 35remulcld 10407 . . 3 (𝜑 → ((0.0001) · (√‘𝑁)) ∈ ℝ)
5331nnzd 11833 . . . . . . 7 (𝜑𝑁 ∈ ℤ)
54 chpvalz 31308 . . . . . . 7 (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖))
5553, 54syl 17 . . . . . 6 (𝜑 → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖))
56 chtvalz 31309 . . . . . . . 8 (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
5753, 56syl 17 . . . . . . 7 (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
58 inss2 4053 . . . . . . . . . . 11 ((1...𝑁) ∩ ℙ) ⊆ ℙ
5958a1i 11 . . . . . . . . . 10 (𝜑 → ((1...𝑁) ∩ ℙ) ⊆ ℙ)
6059sselda 3820 . . . . . . . . 9 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℙ)
61 vmaprm 25295 . . . . . . . . 9 (𝑖 ∈ ℙ → (Λ‘𝑖) = (log‘𝑖))
6260, 61syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) = (log‘𝑖))
6362sumeq2dv 14841 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
6457, 63eqtr4d 2816 . . . . . 6 (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖))
6555, 64oveq12d 6940 . . . . 5 (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) = (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)))
66 infi 8472 . . . . . . . 8 ((1...𝑁) ∈ Fin → ((1...𝑁) ∩ ℙ) ∈ Fin)
671, 66syl 17 . . . . . . 7 (𝜑 → ((1...𝑁) ∩ ℙ) ∈ Fin)
684a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → Λ:ℕ⟶ℝ)
69 inss1 4052 . . . . . . . . . . . 12 ((1...𝑁) ∩ ℙ) ⊆ (1...𝑁)
7069, 6sstri 3829 . . . . . . . . . . 11 ((1...𝑁) ∩ ℙ) ⊆ ℕ
7170a1i 11 . . . . . . . . . 10 (𝜑 → ((1...𝑁) ∩ ℙ) ⊆ ℕ)
7271sselda 3820 . . . . . . . . 9 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℕ)
7368, 72ffvelrnd 6624 . . . . . . . 8 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) ∈ ℝ)
7473recnd 10405 . . . . . . 7 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) ∈ ℂ)
7567, 74fsumcl 14871 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) ∈ ℂ)
7610recnd 10405 . . . . . . 7 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → (Λ‘𝑖) ∈ ℂ)
773, 76fsumcl 14871 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈ ℂ)
78 inindif 29915 . . . . . . . 8 (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) = ∅
7978a1i 11 . . . . . . 7 (𝜑 → (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) = ∅)
80 inundif 4269 . . . . . . . . 9 (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ)) = (1...𝑁)
8180eqcomi 2786 . . . . . . . 8 (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ))
8281a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ)))
834a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
847sselda 3820 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℕ)
8583, 84ffvelrnd 6624 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℝ)
8685recnd 10405 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℂ)
8779, 82, 1, 86fsumsplit 14878 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) + Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖)))
8875, 77, 87mvrladdd 10788 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)) = Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖))
8965, 88eqtr2d 2814 . . . 4 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) = ((ψ‘𝑁) − (θ‘𝑁)))
90 fveq2 6446 . . . . . . 7 (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁))
91 fveq2 6446 . . . . . . 7 (𝑥 = 𝑁 → (θ‘𝑥) = (θ‘𝑁))
9290, 91oveq12d 6940 . . . . . 6 (𝑥 = 𝑁 → ((ψ‘𝑥) − (θ‘𝑥)) = ((ψ‘𝑁) − (θ‘𝑁)))
93 fveq2 6446 . . . . . . 7 (𝑥 = 𝑁 → (√‘𝑥) = (√‘𝑁))
9493oveq2d 6938 . . . . . 6 (𝑥 = 𝑁 → ((1.4262) · (√‘𝑥)) = ((1.4262) · (√‘𝑁)))
9592, 94breq12d 4899 . . . . 5 (𝑥 = 𝑁 → (((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥)) ↔ ((ψ‘𝑁) − (θ‘𝑁)) < ((1.4262) · (√‘𝑁))))
96 ax-ros336 31326 . . . . . 6 𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))
9796a1i 11 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥)))
9895, 97, 33rspcdva 3516 . . . 4 (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) < ((1.4262) · (√‘𝑁)))
9989, 98eqbrtrd 4908 . . 3 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) < ((1.4262) · (√‘𝑁)))
10039a1i 11 . . . 4 (𝜑 → 1 ∈ ℝ)
101 log2le1 25129 . . . . 5 (log‘2) < 1
102101a1i 11 . . . 4 (𝜑 → (log‘2) < 1)
103 10nn0 11863 . . . . . . . . 9 10 ∈ ℕ0
104 7nn0 11666 . . . . . . . . 9 7 ∈ ℕ0
105103, 104nn0expcli 13204 . . . . . . . 8 (10↑7) ∈ ℕ0
106105nn0rei 11654 . . . . . . 7 (10↑7) ∈ ℝ
107106a1i 11 . . . . . 6 (𝜑 → (10↑7) ∈ ℝ)
10851, 107remulcld 10407 . . . . 5 (𝜑 → ((0.0001) · (10↑7)) ∈ ℝ)
109103nn0rei 11654 . . . . . . . . . . 11 10 ∈ ℝ
110 0z 11739 . . . . . . . . . . 11 0 ∈ ℤ
111 3z 11762 . . . . . . . . . . 11 3 ∈ ℤ
112109, 110, 1113pm3.2i 1395 . . . . . . . . . 10 (10 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ)
113 1lt10 11986 . . . . . . . . . . 11 1 < 10
114 3pos 11487 . . . . . . . . . . 11 0 < 3
115113, 114pm3.2i 464 . . . . . . . . . 10 (1 < 10 ∧ 0 < 3)
116 ltexp2a 13230 . . . . . . . . . 10 (((10 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (1 < 10 ∧ 0 < 3)) → (10↑0) < (10↑3))
117112, 115, 116mp2an 682 . . . . . . . . 9 (10↑0) < (10↑3)
118103numexp0 16184 . . . . . . . . . 10 (10↑0) = 1
119118eqcomi 2786 . . . . . . . . 9 1 = (10↑0)
120109recni 10391 . . . . . . . . . . 11 10 ∈ ℂ
121 10pos 11862 . . . . . . . . . . . 12 0 < 10
12238, 121gtneii 10488 . . . . . . . . . . 11 10 ≠ 0
123 4z 11763 . . . . . . . . . . 11 4 ∈ ℤ
124 expm1 13228 . . . . . . . . . . 11 ((10 ∈ ℂ ∧ 10 ≠ 0 ∧ 4 ∈ ℤ) → (10↑(4 − 1)) = ((10↑4) / 10))
125120, 122, 123, 124mp3an 1534 . . . . . . . . . 10 (10↑(4 − 1)) = ((10↑4) / 10)
126 4m1e3 11511 . . . . . . . . . . 11 (4 − 1) = 3
127126oveq2i 6933 . . . . . . . . . 10 (10↑(4 − 1)) = (10↑3)
128 4nn0 11663 . . . . . . . . . . . . 13 4 ∈ ℕ0
129103, 128nn0expcli 13204 . . . . . . . . . . . 12 (10↑4) ∈ ℕ0
130129nn0cni 11655 . . . . . . . . . . 11 (10↑4) ∈ ℂ
131 divrec2 11050 . . . . . . . . . . 11 (((10↑4) ∈ ℂ ∧ 10 ∈ ℂ ∧ 10 ≠ 0) → ((10↑4) / 10) = ((1 / 10) · (10↑4)))
132130, 120, 122, 131mp3an 1534 . . . . . . . . . 10 ((10↑4) / 10) = ((1 / 10) · (10↑4))
133125, 127, 1323eqtr3ri 2810 . . . . . . . . 9 ((1 / 10) · (10↑4)) = (10↑3)
134117, 119, 1333brtr4i 4916 . . . . . . . 8 1 < ((1 / 10) · (10↑4))
135 1rp 12141 . . . . . . . . . 10 1 ∈ ℝ+
136135dp0h 30172 . . . . . . . . 9 (0.1) = (1 / 10)
137136oveq1i 6932 . . . . . . . 8 ((0.1) · (10↑4)) = ((1 / 10) · (10↑4))
138134, 137breqtrri 4913 . . . . . . 7 1 < ((0.1) · (10↑4))
139138a1i 11 . . . . . 6 (𝜑 → 1 < ((0.1) · (10↑4)))
140 4p1e5 11528 . . . . . . . 8 (4 + 1) = 5
141 5nn0 11664 . . . . . . . . 9 5 ∈ ℕ0
142141nn0zi 11754 . . . . . . . 8 5 ∈ ℤ
14337, 135, 140, 123, 142dpexpp1 30178 . . . . . . 7 ((0.1) · (10↑4)) = ((0.01) · (10↑5))
14437, 135rpdp2cl 30152 . . . . . . . 8 01 ∈ ℝ+
145 5p1e6 11529 . . . . . . . 8 (5 + 1) = 6
146 6nn0 11665 . . . . . . . . 9 6 ∈ ℕ0
147146nn0zi 11754 . . . . . . . 8 6 ∈ ℤ
14837, 144, 145, 142, 147dpexpp1 30178 . . . . . . 7 ((0.01) · (10↑5)) = ((0.001) · (10↑6))
14937, 144rpdp2cl 30152 . . . . . . . 8 001 ∈ ℝ+
150 6p1e7 11530 . . . . . . . 8 (6 + 1) = 7
151104nn0zi 11754 . . . . . . . 8 7 ∈ ℤ
15237, 149, 150, 147, 151dpexpp1 30178 . . . . . . 7 ((0.001) · (10↑6)) = ((0.0001) · (10↑7))
153143, 148, 1523eqtrri 2806 . . . . . 6 ((0.0001) · (10↑7)) = ((0.1) · (10↑4))
154139, 153syl6breqr 4928 . . . . 5 (𝜑 → 1 < ((0.0001) · (10↑7)))
15537, 149rpdp2cl 30152 . . . . . . . 8 0001 ∈ ℝ+
15637, 155rpdpcl 30173 . . . . . . 7 (0.0001) ∈ ℝ+
157156a1i 11 . . . . . 6 (𝜑 → (0.0001) ∈ ℝ+)
158 2nn0 11661 . . . . . . . . . . . 12 2 ∈ ℕ0
159158, 104deccl 11860 . . . . . . . . . . 11 27 ∈ ℕ0
160103, 159nn0expcli 13204 . . . . . . . . . 10 (10↑27) ∈ ℕ0
161160nn0rei 11654 . . . . . . . . 9 (10↑27) ∈ ℝ
162161a1i 11 . . . . . . . 8 (𝜑 → (10↑27) ∈ ℝ)
163160nn0ge0i 11671 . . . . . . . . 9 0 ≤ (10↑27)
164163a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ (10↑27))
165162, 164resqrtcld 14564 . . . . . . 7 (𝜑 → (√‘(10↑27)) ∈ ℝ)
166 expmul 13223 . . . . . . . . . . . . 13 ((10 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (10↑(7 · 2)) = ((10↑7)↑2))
167120, 104, 158, 166mp3an 1534 . . . . . . . . . . . 12 (10↑(7 · 2)) = ((10↑7)↑2)
168 7t2e14 11956 . . . . . . . . . . . . 13 (7 · 2) = 14
169168oveq2i 6933 . . . . . . . . . . . 12 (10↑(7 · 2)) = (10↑14)
170167, 169eqtr3i 2803 . . . . . . . . . . 11 ((10↑7)↑2) = (10↑14)
171170fveq2i 6449 . . . . . . . . . 10 (√‘((10↑7)↑2)) = (√‘(10↑14))
172 expgt0 13211 . . . . . . . . . . . . 13 ((10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < 10) → 0 < (10↑7))
173109, 151, 121, 172mp3an 1534 . . . . . . . . . . . 12 0 < (10↑7)
17438, 106, 173ltleii 10499 . . . . . . . . . . 11 0 ≤ (10↑7)
175 sqrtsq 14417 . . . . . . . . . . 11 (((10↑7) ∈ ℝ ∧ 0 ≤ (10↑7)) → (√‘((10↑7)↑2)) = (10↑7))
176106, 174, 175mp2an 682 . . . . . . . . . 10 (√‘((10↑7)↑2)) = (10↑7)
177171, 176eqtr3i 2803 . . . . . . . . 9 (√‘(10↑14)) = (10↑7)
17815, 128deccl 11860 . . . . . . . . . . . . 13 14 ∈ ℕ0
179178nn0zi 11754 . . . . . . . . . . . 12 14 ∈ ℤ
180159nn0zi 11754 . . . . . . . . . . . 12 27 ∈ ℤ
181109, 179, 1803pm3.2i 1395 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 14 ∈ ℤ ∧ 27 ∈ ℤ)
182 4lt10 11983 . . . . . . . . . . . . 13 4 < 10
183 1lt2 11553 . . . . . . . . . . . . 13 1 < 2
18415, 158, 128, 104, 182, 183decltc 11875 . . . . . . . . . . . 12 14 < 27
185113, 184pm3.2i 464 . . . . . . . . . . 11 (1 < 10 ∧ 14 < 27)
186 ltexp2a 13230 . . . . . . . . . . 11 (((10 ∈ ℝ ∧ 14 ∈ ℤ ∧ 27 ∈ ℤ) ∧ (1 < 10 ∧ 14 < 27)) → (10↑14) < (10↑27))
187181, 185, 186mp2an 682 . . . . . . . . . 10 (10↑14) < (10↑27)
188103, 178nn0expcli 13204 . . . . . . . . . . . . 13 (10↑14) ∈ ℕ0
189188nn0rei 11654 . . . . . . . . . . . 12 (10↑14) ∈ ℝ
190 expgt0 13211 . . . . . . . . . . . . . 14 ((10 ∈ ℝ ∧ 14 ∈ ℤ ∧ 0 < 10) → 0 < (10↑14))
191109, 179, 121, 190mp3an 1534 . . . . . . . . . . . . 13 0 < (10↑14)
19238, 189, 191ltleii 10499 . . . . . . . . . . . 12 0 ≤ (10↑14)
193189, 192pm3.2i 464 . . . . . . . . . . 11 ((10↑14) ∈ ℝ ∧ 0 ≤ (10↑14))
194161, 163pm3.2i 464 . . . . . . . . . . 11 ((10↑27) ∈ ℝ ∧ 0 ≤ (10↑27))
195 sqrtlt 14409 . . . . . . . . . . 11 ((((10↑14) ∈ ℝ ∧ 0 ≤ (10↑14)) ∧ ((10↑27) ∈ ℝ ∧ 0 ≤ (10↑27))) → ((10↑14) < (10↑27) ↔ (√‘(10↑14)) < (√‘(10↑27))))
196193, 194, 195mp2an 682 . . . . . . . . . 10 ((10↑14) < (10↑27) ↔ (√‘(10↑14)) < (√‘(10↑27)))
197187, 196mpbi 222 . . . . . . . . 9 (√‘(10↑14)) < (√‘(10↑27))
198177, 197eqbrtrri 4909 . . . . . . . 8 (10↑7) < (√‘(10↑27))
199198a1i 11 . . . . . . 7 (𝜑 → (10↑7) < (√‘(10↑27)))
200 hgt750lemd.0 . . . . . . . 8 (𝜑 → (10↑27) ≤ 𝑁)
201162, 164, 32, 34sqrtled 14573 . . . . . . . 8 (𝜑 → ((10↑27) ≤ 𝑁 ↔ (√‘(10↑27)) ≤ (√‘𝑁)))
202200, 201mpbid 224 . . . . . . 7 (𝜑 → (√‘(10↑27)) ≤ (√‘𝑁))
203107, 165, 35, 199, 202ltletrd 10536 . . . . . 6 (𝜑 → (10↑7) < (√‘𝑁))
204107, 35, 157, 203ltmul2dd 12237 . . . . 5 (𝜑 → ((0.0001) · (10↑7)) < ((0.0001) · (√‘𝑁)))
205100, 108, 52, 154, 204lttrd 10537 . . . 4 (𝜑 → 1 < ((0.0001) · (√‘𝑁)))
20614, 100, 52, 102, 205lttrd 10537 . . 3 (𝜑 → (log‘2) < ((0.0001) · (√‘𝑁)))
20711, 14, 36, 52, 99, 206lt2addd 10998 . 2 (𝜑 → (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)) < (((1.4262) · (√‘𝑁)) + ((0.0001) · (√‘𝑁))))
208 nfv 1957 . . 3 𝑖𝜑
209 nfcv 2933 . . 3 𝑖(log‘2)
210 2prm 15810 . . . 4 2 ∈ ℙ
211210a1i 11 . . 3 (𝜑 → 2 ∈ ℙ)
212 elndif 3956 . . . 4 (2 ∈ ℙ → ¬ 2 ∈ ((1...𝑁) ∖ ℙ))
213211, 212syl 17 . . 3 (𝜑 → ¬ 2 ∈ ((1...𝑁) ∖ ℙ))
214 fveq2 6446 . . . 4 (𝑖 = 2 → (Λ‘𝑖) = (Λ‘2))
215 vmaprm 25295 . . . . 5 (2 ∈ ℙ → (Λ‘2) = (log‘2))
216210, 215ax-mp 5 . . . 4 (Λ‘2) = (log‘2)
217214, 216syl6eq 2829 . . 3 (𝑖 = 2 → (Λ‘𝑖) = (log‘2))
218 2cnd 11453 . . . 4 (𝜑 → 2 ∈ ℂ)
219 2ne0 11486 . . . . 5 2 ≠ 0
220219a1i 11 . . . 4 (𝜑 → 2 ≠ 0)
221218, 220logcld 24754 . . 3 (𝜑 → (log‘2) ∈ ℂ)
222208, 209, 3, 211, 213, 76, 217, 221fsumsplitsn 14881 . 2 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)))
223146, 12rpdp2cl 30152 . . . . . 6 62 ∈ ℝ+
224158, 223rpdp2cl 30152 . . . . 5 262 ∈ ℝ+
225 3rp 12143 . . . . . . 7 3 ∈ ℝ+
226146, 225rpdp2cl 30152 . . . . . 6 63 ∈ ℝ+
227158, 226rpdp2cl 30152 . . . . 5 263 ∈ ℝ+
228 1p0e1 11506 . . . . 5 (1 + 0) = 1
229 4cn 11461 . . . . . . 7 4 ∈ ℂ
230229addid1i 10563 . . . . . 6 (4 + 0) = 4
231 2cn 11450 . . . . . . . 8 2 ∈ ℂ
232231addid1i 10563 . . . . . . 7 (2 + 0) = 2
233 3nn0 11662 . . . . . . . 8 3 ∈ ℕ0
234 eqid 2777 . . . . . . . . 9 62 = 62
235 eqid 2777 . . . . . . . . 9 01 = 01
236 6cn 11469 . . . . . . . . . 10 6 ∈ ℂ
237236addid1i 10563 . . . . . . . . 9 (6 + 0) = 6
238 2p1e3 11524 . . . . . . . . 9 (2 + 1) = 3
239146, 158, 37, 15, 234, 235, 237, 238decadd 11900 . . . . . . . 8 (62 + 01) = 63
240146, 158, 37, 15, 146, 233, 239dpadd 30181 . . . . . . 7 ((6.2) + (0.1)) = (6.3)
241146, 12, 37, 135, 146, 225, 158, 37, 232, 240dpadd2 30180 . . . . . 6 ((2.62) + (0.01)) = (2.63)
242158, 223, 37, 144, 158, 226, 128, 37, 230, 241dpadd2 30180 . . . . 5 ((4.262) + (0.001)) = (4.263)
243128, 224, 37, 149, 128, 227, 15, 37, 228, 242dpadd2 30180 . . . 4 ((1.4262) + (0.0001)) = (1.4263)
244243oveq1i 6932 . . 3 (((1.4262) + (0.0001)) · (√‘𝑁)) = ((1.4263) · (√‘𝑁))
24530recnd 10405 . . . 4 (𝜑 → (1.4262) ∈ ℂ)
24651recnd 10405 . . . 4 (𝜑 → (0.0001) ∈ ℂ)
24735recnd 10405 . . . 4 (𝜑 → (√‘𝑁) ∈ ℂ)
248245, 246, 247adddird 10402 . . 3 (𝜑 → (((1.4262) + (0.0001)) · (√‘𝑁)) = (((1.4262) · (√‘𝑁)) + ((0.0001) · (√‘𝑁))))
249244, 248syl5eqr 2827 . 2 (𝜑 → ((1.4263) · (√‘𝑁)) = (((1.4262) · (√‘𝑁)) + ((0.0001) · (√‘𝑁))))
250207, 222, 2493brtr4d 4918 1 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1.4263) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2106  wne 2968  wral 3089  cdif 3788  cun 3789  cin 3790  wss 3791  c0 4140  {csn 4397   class class class wbr 4886  wf 6131  cfv 6135  (class class class)co 6922  Fincfn 8241  cc 10270  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277   < clt 10411  cle 10412  cmin 10606   / cdiv 11032  cn 11374  2c2 11430  3c3 11431  4c4 11432  5c5 11433  6c6 11434  7c7 11435  0cn0 11642  cz 11728  cdc 11845  +crp 12137  ...cfz 12643  cexp 13178  csqrt 14380  Σcsu 14824  cprime 15790  logclog 24738  θccht 25269  Λcvma 25270  ψcchp 25271  cdp2 30141  .cdp 30158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352  ax-ros336 31326
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-xnn0 11715  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ioc 12492  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-fac 13379  df-bc 13408  df-hash 13436  df-shft 14214  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-limsup 14610  df-clim 14627  df-rlim 14628  df-sum 14825  df-ef 15200  df-sin 15202  df-cos 15203  df-tan 15204  df-pi 15205  df-dvds 15388  df-gcd 15623  df-prm 15791  df-pc 15946  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-perf 21349  df-cn 21439  df-cnp 21440  df-haus 21527  df-cmp 21599  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cncf 23089  df-limc 24067  df-dv 24068  df-ulm 24568  df-log 24740  df-atan 25045  df-cht 25275  df-vma 25276  df-chp 25277  df-dp2 30142  df-dp 30159
This theorem is referenced by:  hgt750leme  31338
  Copyright terms: Public domain W3C validator