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 31027
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 12958 . . . . 5 (𝜑 → (1...𝑁) ∈ Fin)
2 diffi 8349 . . . . 5 ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
31, 2syl 17 . . . 4 (𝜑 → ((1...𝑁) ∖ ℙ) ∈ Fin)
4 vmaf 25036 . . . . . 6 Λ:ℕ⟶ℝ
54a1i 11 . . . . 5 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → Λ:ℕ⟶ℝ)
6 fz1ssnn 12557 . . . . . . . 8 (1...𝑁) ⊆ ℕ
76a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) ⊆ ℕ)
87ssdifssd 3883 . . . . . 6 (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
98sselda 3736 . . . . 5 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → 𝑖 ∈ ℕ)
105, 9ffvelrnd 6515 . . . 4 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → (Λ‘𝑖) ∈ ℝ)
113, 10fsumrecl 14656 . . 3 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈ ℝ)
12 2rp 12022 . . . . 5 2 ∈ ℝ+
1312a1i 11 . . . 4 (𝜑 → 2 ∈ ℝ+)
1413relogcld 24560 . . 3 (𝜑 → (log‘2) ∈ ℝ)
15 1nn0 11492 . . . . . 6 1 ∈ ℕ0
16 4re 11281 . . . . . . . 8 4 ∈ ℝ
17 2re 11274 . . . . . . . . . 10 2 ∈ ℝ
18 6re 11285 . . . . . . . . . . . 12 6 ∈ ℝ
1918, 17pm3.2i 470 . . . . . . . . . . 11 (6 ∈ ℝ ∧ 2 ∈ ℝ)
20 dp2cl 29888 . . . . . . . . . . 11 ((6 ∈ ℝ ∧ 2 ∈ ℝ) → 62 ∈ ℝ)
2119, 20ax-mp 5 . . . . . . . . . 10 62 ∈ ℝ
2217, 21pm3.2i 470 . . . . . . . . 9 (2 ∈ ℝ ∧ 62 ∈ ℝ)
23 dp2cl 29888 . . . . . . . . 9 ((2 ∈ ℝ ∧ 62 ∈ ℝ) → 262 ∈ ℝ)
2422, 23ax-mp 5 . . . . . . . 8 262 ∈ ℝ
2516, 24pm3.2i 470 . . . . . . 7 (4 ∈ ℝ ∧ 262 ∈ ℝ)
26 dp2cl 29888 . . . . . . 7 ((4 ∈ ℝ ∧ 262 ∈ ℝ) → 4262 ∈ ℝ)
2725, 26ax-mp 5 . . . . . 6 4262 ∈ ℝ
28 dpcl 29899 . . . . . 6 ((1 ∈ ℕ04262 ∈ ℝ) → (1.4262) ∈ ℝ)
2915, 27, 28mp2an 710 . . . . 5 (1.4262) ∈ ℝ
3029a1i 11 . . . 4 (𝜑 → (1.4262) ∈ ℝ)
31 hgt750lemc.n . . . . . 6 (𝜑𝑁 ∈ ℕ)
3231nnred 11219 . . . . 5 (𝜑𝑁 ∈ ℝ)
3331nnrpd 12055 . . . . . 6 (𝜑𝑁 ∈ ℝ+)
3433rpge0d 12061 . . . . 5 (𝜑 → 0 ≤ 𝑁)
3532, 34resqrtcld 14347 . . . 4 (𝜑 → (√‘𝑁) ∈ ℝ)
3630, 35remulcld 10254 . . 3 (𝜑 → ((1.4262) · (√‘𝑁)) ∈ ℝ)
37 0nn0 11491 . . . . . 6 0 ∈ ℕ0
38 0re 10224 . . . . . . . 8 0 ∈ ℝ
39 1re 10223 . . . . . . . . . . . 12 1 ∈ ℝ
4038, 39pm3.2i 470 . . . . . . . . . . 11 (0 ∈ ℝ ∧ 1 ∈ ℝ)
41 dp2cl 29888 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → 01 ∈ ℝ)
4240, 41ax-mp 5 . . . . . . . . . 10 01 ∈ ℝ
4338, 42pm3.2i 470 . . . . . . . . 9 (0 ∈ ℝ ∧ 01 ∈ ℝ)
44 dp2cl 29888 . . . . . . . . 9 ((0 ∈ ℝ ∧ 01 ∈ ℝ) → 001 ∈ ℝ)
4543, 44ax-mp 5 . . . . . . . 8 001 ∈ ℝ
4638, 45pm3.2i 470 . . . . . . 7 (0 ∈ ℝ ∧ 001 ∈ ℝ)
47 dp2cl 29888 . . . . . . 7 ((0 ∈ ℝ ∧ 001 ∈ ℝ) → 0001 ∈ ℝ)
4846, 47ax-mp 5 . . . . . 6 0001 ∈ ℝ
49 dpcl 29899 . . . . . 6 ((0 ∈ ℕ00001 ∈ ℝ) → (0.0001) ∈ ℝ)
5037, 48, 49mp2an 710 . . . . 5 (0.0001) ∈ ℝ
5150a1i 11 . . . 4 (𝜑 → (0.0001) ∈ ℝ)
5251, 35remulcld 10254 . . 3 (𝜑 → ((0.0001) · (√‘𝑁)) ∈ ℝ)
5331nnzd 11665 . . . . . . 7 (𝜑𝑁 ∈ ℤ)
54 chpvalz 31007 . . . . . . 7 (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖))
5553, 54syl 17 . . . . . 6 (𝜑 → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖))
56 chtvalz 31008 . . . . . . . 8 (𝑁 ∈ ℤ → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
5753, 56syl 17 . . . . . . 7 (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
58 inss2 3969 . . . . . . . . . . 11 ((1...𝑁) ∩ ℙ) ⊆ ℙ
5958a1i 11 . . . . . . . . . 10 (𝜑 → ((1...𝑁) ∩ ℙ) ⊆ ℙ)
6059sselda 3736 . . . . . . . . 9 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℙ)
61 vmaprm 25034 . . . . . . . . 9 (𝑖 ∈ ℙ → (Λ‘𝑖) = (log‘𝑖))
6260, 61syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) = (log‘𝑖))
6362sumeq2dv 14624 . . . . . . 7 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖))
6457, 63eqtr4d 2789 . . . . . 6 (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖))
6555, 64oveq12d 6823 . . . . 5 (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) = (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)))
6610recnd 10252 . . . . . . 7 ((𝜑𝑖 ∈ ((1...𝑁) ∖ ℙ)) → (Λ‘𝑖) ∈ ℂ)
673, 66fsumcl 14655 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈ ℂ)
68 infi 8341 . . . . . . . 8 ((1...𝑁) ∈ Fin → ((1...𝑁) ∩ ℙ) ∈ Fin)
691, 68syl 17 . . . . . . 7 (𝜑 → ((1...𝑁) ∩ ℙ) ∈ Fin)
704a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → Λ:ℕ⟶ℝ)
71 inss1 3968 . . . . . . . . . . . 12 ((1...𝑁) ∩ ℙ) ⊆ (1...𝑁)
7271, 6sstri 3745 . . . . . . . . . . 11 ((1...𝑁) ∩ ℙ) ⊆ ℕ
7372a1i 11 . . . . . . . . . 10 (𝜑 → ((1...𝑁) ∩ ℙ) ⊆ ℕ)
7473sselda 3736 . . . . . . . . 9 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℕ)
7570, 74ffvelrnd 6515 . . . . . . . 8 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) ∈ ℝ)
7675recnd 10252 . . . . . . 7 ((𝜑𝑖 ∈ ((1...𝑁) ∩ ℙ)) → (Λ‘𝑖) ∈ ℂ)
7769, 76fsumcl 14655 . . . . . 6 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) ∈ ℂ)
78 inindif 29652 . . . . . . . . 9 (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) = ∅
7978a1i 11 . . . . . . . 8 (𝜑 → (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) = ∅)
80 inundif 4182 . . . . . . . . . 10 (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ)) = (1...𝑁)
8180eqcomi 2761 . . . . . . . . 9 (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ))
8281a1i 11 . . . . . . . 8 (𝜑 → (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖ ℙ)))
834a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
847sselda 3736 . . . . . . . . . 10 ((𝜑𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℕ)
8583, 84ffvelrnd 6515 . . . . . . . . 9 ((𝜑𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℝ)
8685recnd 10252 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℂ)
8779, 82, 1, 86fsumsplit 14662 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) + Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖)))
8877, 67, 87comraddd 10434 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)))
8967, 77, 88mvrraddd 10629 . . . . 5 (𝜑 → (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)) = Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖))
9065, 89eqtr2d 2787 . . . 4 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) = ((ψ‘𝑁) − (θ‘𝑁)))
91 fveq2 6344 . . . . . . 7 (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁))
92 fveq2 6344 . . . . . . 7 (𝑥 = 𝑁 → (θ‘𝑥) = (θ‘𝑁))
9391, 92oveq12d 6823 . . . . . 6 (𝑥 = 𝑁 → ((ψ‘𝑥) − (θ‘𝑥)) = ((ψ‘𝑁) − (θ‘𝑁)))
94 fveq2 6344 . . . . . . 7 (𝑥 = 𝑁 → (√‘𝑥) = (√‘𝑁))
9594oveq2d 6821 . . . . . 6 (𝑥 = 𝑁 → ((1.4262) · (√‘𝑥)) = ((1.4262) · (√‘𝑁)))
9693, 95breq12d 4809 . . . . 5 (𝑥 = 𝑁 → (((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥)) ↔ ((ψ‘𝑁) − (θ‘𝑁)) < ((1.4262) · (√‘𝑁))))
97 ax-ros336 31025 . . . . . 6 𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))
9897a1i 11 . . . . 5 (𝜑 → ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥)))
9996, 98, 33rspcdva 3447 . . . 4 (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) < ((1.4262) · (√‘𝑁)))
10090, 99eqbrtrd 4818 . . 3 (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) < ((1.4262) · (√‘𝑁)))
10139a1i 11 . . . 4 (𝜑 → 1 ∈ ℝ)
102 log2le1 24868 . . . . 5 (log‘2) < 1
103102a1i 11 . . . 4 (𝜑 → (log‘2) < 1)
104 10nn0 11700 . . . . . . . . 9 10 ∈ ℕ0
105 7nn0 11498 . . . . . . . . 9 7 ∈ ℕ0
106104, 105nn0expcli 13072 . . . . . . . 8 (10↑7) ∈ ℕ0
107106nn0rei 11487 . . . . . . 7 (10↑7) ∈ ℝ
108107a1i 11 . . . . . 6 (𝜑 → (10↑7) ∈ ℝ)
10951, 108remulcld 10254 . . . . 5 (𝜑 → ((0.0001) · (10↑7)) ∈ ℝ)
110104nn0rei 11487 . . . . . . . . . . 11 10 ∈ ℝ
111 0z 11572 . . . . . . . . . . 11 0 ∈ ℤ
112 3z 11594 . . . . . . . . . . 11 3 ∈ ℤ
113110, 111, 1123pm3.2i 1421 . . . . . . . . . 10 (10 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ)
114 1lt10 11865 . . . . . . . . . . 11 1 < 10
115 3pos 11298 . . . . . . . . . . 11 0 < 3
116114, 115pm3.2i 470 . . . . . . . . . 10 (1 < 10 ∧ 0 < 3)
117 ltexp2a 13098 . . . . . . . . . 10 (((10 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ) ∧ (1 < 10 ∧ 0 < 3)) → (10↑0) < (10↑3))
118113, 116, 117mp2an 710 . . . . . . . . 9 (10↑0) < (10↑3)
119104numexp0 15974 . . . . . . . . . 10 (10↑0) = 1
120119eqcomi 2761 . . . . . . . . 9 1 = (10↑0)
121110recni 10236 . . . . . . . . . . 11 10 ∈ ℂ
122 10pos 11699 . . . . . . . . . . . 12 0 < 10
12338, 122gtneii 10333 . . . . . . . . . . 11 10 ≠ 0
124 4z 11595 . . . . . . . . . . 11 4 ∈ ℤ
125 expm1 13096 . . . . . . . . . . 11 ((10 ∈ ℂ ∧ 10 ≠ 0 ∧ 4 ∈ ℤ) → (10↑(4 − 1)) = ((10↑4) / 10))
126121, 123, 124, 125mp3an 1565 . . . . . . . . . 10 (10↑(4 − 1)) = ((10↑4) / 10)
127 4m1e3 11322 . . . . . . . . . . 11 (4 − 1) = 3
128127oveq2i 6816 . . . . . . . . . 10 (10↑(4 − 1)) = (10↑3)
129 4nn0 11495 . . . . . . . . . . . . 13 4 ∈ ℕ0
130104, 129nn0expcli 13072 . . . . . . . . . . . 12 (10↑4) ∈ ℕ0
131130nn0cni 11488 . . . . . . . . . . 11 (10↑4) ∈ ℂ
132 divrec2 10886 . . . . . . . . . . 11 (((10↑4) ∈ ℂ ∧ 10 ∈ ℂ ∧ 10 ≠ 0) → ((10↑4) / 10) = ((1 / 10) · (10↑4)))
133131, 121, 123, 132mp3an 1565 . . . . . . . . . 10 ((10↑4) / 10) = ((1 / 10) · (10↑4))
134126, 128, 1333eqtr3ri 2783 . . . . . . . . 9 ((1 / 10) · (10↑4)) = (10↑3)
135118, 120, 1343brtr4i 4826 . . . . . . . 8 1 < ((1 / 10) · (10↑4))
136 1rp 12021 . . . . . . . . . 10 1 ∈ ℝ+
137136dp0h 29911 . . . . . . . . 9 (0.1) = (1 / 10)
138137oveq1i 6815 . . . . . . . 8 ((0.1) · (10↑4)) = ((1 / 10) · (10↑4))
139135, 138breqtrri 4823 . . . . . . 7 1 < ((0.1) · (10↑4))
140139a1i 11 . . . . . 6 (𝜑 → 1 < ((0.1) · (10↑4)))
141 4p1e5 11338 . . . . . . . 8 (4 + 1) = 5
142 5nn0 11496 . . . . . . . . 9 5 ∈ ℕ0
143142nn0zi 11586 . . . . . . . 8 5 ∈ ℤ
14437, 136, 141, 124, 143dpexpp1 29917 . . . . . . 7 ((0.1) · (10↑4)) = ((0.01) · (10↑5))
14537, 136rpdp2cl 29890 . . . . . . . 8 01 ∈ ℝ+
146 5p1e6 11339 . . . . . . . 8 (5 + 1) = 6
147 6nn0 11497 . . . . . . . . 9 6 ∈ ℕ0
148147nn0zi 11586 . . . . . . . 8 6 ∈ ℤ
14937, 145, 146, 143, 148dpexpp1 29917 . . . . . . 7 ((0.01) · (10↑5)) = ((0.001) · (10↑6))
15037, 145rpdp2cl 29890 . . . . . . . 8 001 ∈ ℝ+
151 6p1e7 11340 . . . . . . . 8 (6 + 1) = 7
152105nn0zi 11586 . . . . . . . 8 7 ∈ ℤ
15337, 150, 151, 148, 152dpexpp1 29917 . . . . . . 7 ((0.001) · (10↑6)) = ((0.0001) · (10↑7))
154144, 149, 1533eqtrri 2779 . . . . . 6 ((0.0001) · (10↑7)) = ((0.1) · (10↑4))
155140, 154syl6breqr 4838 . . . . 5 (𝜑 → 1 < ((0.0001) · (10↑7)))
15637, 150rpdp2cl 29890 . . . . . . . 8 0001 ∈ ℝ+
15737, 156rpdpcl 29912 . . . . . . 7 (0.0001) ∈ ℝ+
158157a1i 11 . . . . . 6 (𝜑 → (0.0001) ∈ ℝ+)
159 2nn0 11493 . . . . . . . . . . . 12 2 ∈ ℕ0
160159, 105deccl 11696 . . . . . . . . . . 11 27 ∈ ℕ0
161104, 160nn0expcli 13072 . . . . . . . . . 10 (10↑27) ∈ ℕ0
162161nn0rei 11487 . . . . . . . . 9 (10↑27) ∈ ℝ
163162a1i 11 . . . . . . . 8 (𝜑 → (10↑27) ∈ ℝ)
164161nn0ge0i 11504 . . . . . . . . 9 0 ≤ (10↑27)
165164a1i 11 . . . . . . . 8 (𝜑 → 0 ≤ (10↑27))
166163, 165resqrtcld 14347 . . . . . . 7 (𝜑 → (√‘(10↑27)) ∈ ℝ)
167 expmul 13091 . . . . . . . . . . . . 13 ((10 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (10↑(7 · 2)) = ((10↑7)↑2))
168121, 105, 159, 167mp3an 1565 . . . . . . . . . . . 12 (10↑(7 · 2)) = ((10↑7)↑2)
169 7t2e14 11832 . . . . . . . . . . . . 13 (7 · 2) = 14
170169oveq2i 6816 . . . . . . . . . . . 12 (10↑(7 · 2)) = (10↑14)
171168, 170eqtr3i 2776 . . . . . . . . . . 11 ((10↑7)↑2) = (10↑14)
172171fveq2i 6347 . . . . . . . . . 10 (√‘((10↑7)↑2)) = (√‘(10↑14))
173 expgt0 13079 . . . . . . . . . . . . 13 ((10 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < 10) → 0 < (10↑7))
174110, 152, 122, 173mp3an 1565 . . . . . . . . . . . 12 0 < (10↑7)
17538, 107, 174ltleii 10344 . . . . . . . . . . 11 0 ≤ (10↑7)
176 sqrtsq 14201 . . . . . . . . . . 11 (((10↑7) ∈ ℝ ∧ 0 ≤ (10↑7)) → (√‘((10↑7)↑2)) = (10↑7))
177107, 175, 176mp2an 710 . . . . . . . . . 10 (√‘((10↑7)↑2)) = (10↑7)
178172, 177eqtr3i 2776 . . . . . . . . 9 (√‘(10↑14)) = (10↑7)
17915, 129deccl 11696 . . . . . . . . . . . . 13 14 ∈ ℕ0
180179nn0zi 11586 . . . . . . . . . . . 12 14 ∈ ℤ
181160nn0zi 11586 . . . . . . . . . . . 12 27 ∈ ℤ
182110, 180, 1813pm3.2i 1421 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 14 ∈ ℤ ∧ 27 ∈ ℤ)
183 4lt10 11862 . . . . . . . . . . . . 13 4 < 10
184 1lt2 11378 . . . . . . . . . . . . 13 1 < 2
18515, 159, 129, 105, 183, 184decltc 11716 . . . . . . . . . . . 12 14 < 27
186114, 185pm3.2i 470 . . . . . . . . . . 11 (1 < 10 ∧ 14 < 27)
187 ltexp2a 13098 . . . . . . . . . . 11 (((10 ∈ ℝ ∧ 14 ∈ ℤ ∧ 27 ∈ ℤ) ∧ (1 < 10 ∧ 14 < 27)) → (10↑14) < (10↑27))
188182, 186, 187mp2an 710 . . . . . . . . . 10 (10↑14) < (10↑27)
189104, 179nn0expcli 13072 . . . . . . . . . . . . 13 (10↑14) ∈ ℕ0
190189nn0rei 11487 . . . . . . . . . . . 12 (10↑14) ∈ ℝ
191 expgt0 13079 . . . . . . . . . . . . . 14 ((10 ∈ ℝ ∧ 14 ∈ ℤ ∧ 0 < 10) → 0 < (10↑14))
192110, 180, 122, 191mp3an 1565 . . . . . . . . . . . . 13 0 < (10↑14)
19338, 190, 192ltleii 10344 . . . . . . . . . . . 12 0 ≤ (10↑14)
194190, 193pm3.2i 470 . . . . . . . . . . 11 ((10↑14) ∈ ℝ ∧ 0 ≤ (10↑14))
195162, 164pm3.2i 470 . . . . . . . . . . 11 ((10↑27) ∈ ℝ ∧ 0 ≤ (10↑27))
196 sqrtlt 14193 . . . . . . . . . . 11 ((((10↑14) ∈ ℝ ∧ 0 ≤ (10↑14)) ∧ ((10↑27) ∈ ℝ ∧ 0 ≤ (10↑27))) → ((10↑14) < (10↑27) ↔ (√‘(10↑14)) < (√‘(10↑27))))
197194, 195, 196mp2an 710 . . . . . . . . . 10 ((10↑14) < (10↑27) ↔ (√‘(10↑14)) < (√‘(10↑27)))
198188, 197mpbi 220 . . . . . . . . 9 (√‘(10↑14)) < (√‘(10↑27))
199178, 198eqbrtrri 4819 . . . . . . . 8 (10↑7) < (√‘(10↑27))
200199a1i 11 . . . . . . 7 (𝜑 → (10↑7) < (√‘(10↑27)))
201 hgt750lemd.0 . . . . . . . 8 (𝜑 → (10↑27) ≤ 𝑁)
202163, 165, 32, 34sqrtled 14356 . . . . . . . 8 (𝜑 → ((10↑27) ≤ 𝑁 ↔ (√‘(10↑27)) ≤ (√‘𝑁)))
203201, 202mpbid 222 . . . . . . 7 (𝜑 → (√‘(10↑27)) ≤ (√‘𝑁))
204108, 166, 35, 200, 203ltletrd 10381 . . . . . 6 (𝜑 → (10↑7) < (√‘𝑁))
205108, 35, 158, 204ltmul2dd 12113 . . . . 5 (𝜑 → ((0.0001) · (10↑7)) < ((0.0001) · (√‘𝑁)))
206101, 109, 52, 155, 205lttrd 10382 . . . 4 (𝜑 → 1 < ((0.0001) · (√‘𝑁)))
20714, 101, 52, 103, 206lttrd 10382 . . 3 (𝜑 → (log‘2) < ((0.0001) · (√‘𝑁)))
20811, 14, 36, 52, 100, 207lt2addd 10834 . 2 (𝜑 → (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)) < (((1.4262) · (√‘𝑁)) + ((0.0001) · (√‘𝑁))))
209 nfv 1984 . . 3 𝑖𝜑
210 nfcv 2894 . . 3 𝑖(log‘2)
211 2prm 15599 . . . 4 2 ∈ ℙ
212211a1i 11 . . 3 (𝜑 → 2 ∈ ℙ)
213 elndif 3869 . . . 4 (2 ∈ ℙ → ¬ 2 ∈ ((1...𝑁) ∖ ℙ))
214212, 213syl 17 . . 3 (𝜑 → ¬ 2 ∈ ((1...𝑁) ∖ ℙ))
215 fveq2 6344 . . . 4 (𝑖 = 2 → (Λ‘𝑖) = (Λ‘2))
216 vmaprm 25034 . . . . 5 (2 ∈ ℙ → (Λ‘2) = (log‘2))
217211, 216ax-mp 5 . . . 4 (Λ‘2) = (log‘2)
218215, 217syl6eq 2802 . . 3 (𝑖 = 2 → (Λ‘𝑖) = (log‘2))
219 2cnd 11277 . . . 4 (𝜑 → 2 ∈ ℂ)
220 2ne0 11297 . . . . 5 2 ≠ 0
221220a1i 11 . . . 4 (𝜑 → 2 ≠ 0)
222219, 221logcld 24508 . . 3 (𝜑 → (log‘2) ∈ ℂ)
223209, 210, 3, 212, 214, 66, 218, 222fsumsplitsn 14665 . 2 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)))
224147, 12rpdp2cl 29890 . . . . . 6 62 ∈ ℝ+
225159, 224rpdp2cl 29890 . . . . 5 262 ∈ ℝ+
226 3rp 12023 . . . . . . 7 3 ∈ ℝ+
227147, 226rpdp2cl 29890 . . . . . 6 63 ∈ ℝ+
228159, 227rpdp2cl 29890 . . . . 5 263 ∈ ℝ+
229 1p0e1 11317 . . . . 5 (1 + 0) = 1
230 4cn 11282 . . . . . . 7 4 ∈ ℂ
231230addid1i 10407 . . . . . 6 (4 + 0) = 4
232 2cn 11275 . . . . . . . 8 2 ∈ ℂ
233232addid1i 10407 . . . . . . 7 (2 + 0) = 2
234 3nn0 11494 . . . . . . . 8 3 ∈ ℕ0
235 eqid 2752 . . . . . . . . 9 62 = 62
236 eqid 2752 . . . . . . . . 9 01 = 01
237 6cn 11286 . . . . . . . . . 10 6 ∈ ℂ
238237addid1i 10407 . . . . . . . . 9 (6 + 0) = 6
239 2p1e3 11335 . . . . . . . . 9 (2 + 1) = 3
240147, 159, 37, 15, 235, 236, 238, 239decadd 11754 . . . . . . . 8 (62 + 01) = 63
241147, 159, 37, 15, 147, 234, 240dpadd 29920 . . . . . . 7 ((6.2) + (0.1)) = (6.3)
242147, 12, 37, 136, 147, 226, 159, 37, 233, 241dpadd2 29919 . . . . . 6 ((2.62) + (0.01)) = (2.63)
243159, 224, 37, 145, 159, 227, 129, 37, 231, 242dpadd2 29919 . . . . 5 ((4.262) + (0.001)) = (4.263)
244129, 225, 37, 150, 129, 228, 15, 37, 229, 243dpadd2 29919 . . . 4 ((1.4262) + (0.0001)) = (1.4263)
245244oveq1i 6815 . . 3 (((1.4262) + (0.0001)) · (√‘𝑁)) = ((1.4263) · (√‘𝑁))
24630recnd 10252 . . . 4 (𝜑 → (1.4262) ∈ ℂ)
24751recnd 10252 . . . 4 (𝜑 → (0.0001) ∈ ℂ)
24835recnd 10252 . . . 4 (𝜑 → (√‘𝑁) ∈ ℂ)
249246, 247, 248adddird 10249 . . 3 (𝜑 → (((1.4262) + (0.0001)) · (√‘𝑁)) = (((1.4262) · (√‘𝑁)) + ((0.0001) · (√‘𝑁))))
250245, 249syl5eqr 2800 . 2 (𝜑 → ((1.4263) · (√‘𝑁)) = (((1.4262) · (√‘𝑁)) + ((0.0001) · (√‘𝑁))))
251208, 223, 2503brtr4d 4828 1 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1.4263) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1624  wcel 2131  wne 2924  wral 3042  cdif 3704  cun 3705  cin 3706  wss 3707  c0 4050  {csn 4313   class class class wbr 4796  wf 6037  cfv 6041  (class class class)co 6805  Fincfn 8113  cc 10118  cr 10119  0cc0 10120  1c1 10121   + caddc 10123   · cmul 10125   < clt 10258  cle 10259  cmin 10450   / cdiv 10868  cn 11204  2c2 11254  3c3 11255  4c4 11256  5c5 11257  6c6 11258  7c7 11259  0cn0 11476  cz 11561  cdc 11677  +crp 12017  ...cfz 12511  cexp 13046  csqrt 14164  Σcsu 14607  cprime 15579  logclog 24492  θccht 25008  Λcvma 25009  ψcchp 25010  cdp2 29878  .cdp 29896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200  ax-ros336 31025
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-1st 7325  df-2nd 7326  df-supp 7456  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-xnn0 11548  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ioc 12365  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-mod 12855  df-seq 12988  df-exp 13047  df-fac 13247  df-bc 13276  df-hash 13304  df-shft 13998  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-limsup 14393  df-clim 14410  df-rlim 14411  df-sum 14608  df-ef 14989  df-sin 14991  df-cos 14992  df-tan 14993  df-pi 14994  df-dvds 15175  df-gcd 15411  df-prm 15580  df-pc 15736  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-sets 16058  df-ress 16059  df-plusg 16148  df-mulr 16149  df-starv 16150  df-sca 16151  df-vsca 16152  df-ip 16153  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-hom 16160  df-cco 16161  df-rest 16277  df-topn 16278  df-0g 16296  df-gsum 16297  df-topgen 16298  df-pt 16299  df-prds 16302  df-xrs 16356  df-qtop 16361  df-imas 16362  df-xps 16364  df-mre 16440  df-mrc 16441  df-acs 16443  df-mgm 17435  df-sgrp 17477  df-mnd 17488  df-submnd 17529  df-mulg 17734  df-cntz 17942  df-cmn 18387  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-fbas 19937  df-fg 19938  df-cnfld 19941  df-top 20893  df-topon 20910  df-topsp 20931  df-bases 20944  df-cld 21017  df-ntr 21018  df-cls 21019  df-nei 21096  df-lp 21134  df-perf 21135  df-cn 21225  df-cnp 21226  df-haus 21313  df-cmp 21384  df-tx 21559  df-hmeo 21752  df-fil 21843  df-fm 21935  df-flim 21936  df-flf 21937  df-xms 22318  df-ms 22319  df-tms 22320  df-cncf 22874  df-limc 23821  df-dv 23822  df-ulm 24322  df-log 24494  df-atan 24785  df-cht 25014  df-vma 25015  df-chp 25016  df-dp2 29879  df-dp 29897
This theorem is referenced by:  hgt750leme  31037
  Copyright terms: Public domain W3C validator