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 33729
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 13940 . . . . 5 (πœ‘ β†’ (1...𝑁) ∈ Fin)
2 diffi 9181 . . . . 5 ((1...𝑁) ∈ Fin β†’ ((1...𝑁) βˆ– β„™) ∈ Fin)
31, 2syl 17 . . . 4 (πœ‘ β†’ ((1...𝑁) βˆ– β„™) ∈ Fin)
4 vmaf 26630 . . . . . 6 Ξ›:β„•βŸΆβ„
54a1i 11 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) βˆ– β„™)) β†’ Ξ›:β„•βŸΆβ„)
6 fz1ssnn 13534 . . . . . . . 8 (1...𝑁) βŠ† β„•
76a1i 11 . . . . . . 7 (πœ‘ β†’ (1...𝑁) βŠ† β„•)
87ssdifssd 4142 . . . . . 6 (πœ‘ β†’ ((1...𝑁) βˆ– β„™) βŠ† β„•)
98sselda 3982 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) βˆ– β„™)) β†’ 𝑖 ∈ β„•)
105, 9ffvelcdmd 7087 . . . 4 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) βˆ– β„™)) β†’ (Ξ›β€˜π‘–) ∈ ℝ)
113, 10fsumrecl 15682 . . 3 (πœ‘ β†’ Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–) ∈ ℝ)
12 2rp 12981 . . . . 5 2 ∈ ℝ+
1312a1i 11 . . . 4 (πœ‘ β†’ 2 ∈ ℝ+)
1413relogcld 26138 . . 3 (πœ‘ β†’ (logβ€˜2) ∈ ℝ)
15 1nn0 12490 . . . . . 6 1 ∈ β„•0
16 4re 12298 . . . . . . . 8 4 ∈ ℝ
17 2re 12288 . . . . . . . . . 10 2 ∈ ℝ
18 6re 12304 . . . . . . . . . . . 12 6 ∈ ℝ
1918, 17pm3.2i 471 . . . . . . . . . . 11 (6 ∈ ℝ ∧ 2 ∈ ℝ)
20 dp2cl 32084 . . . . . . . . . . 11 ((6 ∈ ℝ ∧ 2 ∈ ℝ) β†’ 62 ∈ ℝ)
2119, 20ax-mp 5 . . . . . . . . . 10 62 ∈ ℝ
2217, 21pm3.2i 471 . . . . . . . . 9 (2 ∈ ℝ ∧ 62 ∈ ℝ)
23 dp2cl 32084 . . . . . . . . 9 ((2 ∈ ℝ ∧ 62 ∈ ℝ) β†’ 262 ∈ ℝ)
2422, 23ax-mp 5 . . . . . . . 8 262 ∈ ℝ
2516, 24pm3.2i 471 . . . . . . 7 (4 ∈ ℝ ∧ 262 ∈ ℝ)
26 dp2cl 32084 . . . . . . 7 ((4 ∈ ℝ ∧ 262 ∈ ℝ) β†’ 4262 ∈ ℝ)
2725, 26ax-mp 5 . . . . . 6 4262 ∈ ℝ
28 dpcl 32095 . . . . . 6 ((1 ∈ β„•0 ∧ 4262 ∈ ℝ) β†’ (1.4262) ∈ ℝ)
2915, 27, 28mp2an 690 . . . . 5 (1.4262) ∈ ℝ
3029a1i 11 . . . 4 (πœ‘ β†’ (1.4262) ∈ ℝ)
31 hgt750lemc.n . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
3231nnred 12229 . . . . 5 (πœ‘ β†’ 𝑁 ∈ ℝ)
3331nnrpd 13016 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ ℝ+)
3433rpge0d 13022 . . . . 5 (πœ‘ β†’ 0 ≀ 𝑁)
3532, 34resqrtcld 15366 . . . 4 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ ℝ)
3630, 35remulcld 11246 . . 3 (πœ‘ β†’ ((1.4262) Β· (βˆšβ€˜π‘)) ∈ ℝ)
37 0nn0 12489 . . . . . 6 0 ∈ β„•0
38 0re 11218 . . . . . . . 8 0 ∈ ℝ
39 1re 11216 . . . . . . . . . . . 12 1 ∈ ℝ
4038, 39pm3.2i 471 . . . . . . . . . . 11 (0 ∈ ℝ ∧ 1 ∈ ℝ)
41 dp2cl 32084 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ 1 ∈ ℝ) β†’ 01 ∈ ℝ)
4240, 41ax-mp 5 . . . . . . . . . 10 01 ∈ ℝ
4338, 42pm3.2i 471 . . . . . . . . 9 (0 ∈ ℝ ∧ 01 ∈ ℝ)
44 dp2cl 32084 . . . . . . . . 9 ((0 ∈ ℝ ∧ 01 ∈ ℝ) β†’ 001 ∈ ℝ)
4543, 44ax-mp 5 . . . . . . . 8 001 ∈ ℝ
4638, 45pm3.2i 471 . . . . . . 7 (0 ∈ ℝ ∧ 001 ∈ ℝ)
47 dp2cl 32084 . . . . . . 7 ((0 ∈ ℝ ∧ 001 ∈ ℝ) β†’ 0001 ∈ ℝ)
4846, 47ax-mp 5 . . . . . 6 0001 ∈ ℝ
49 dpcl 32095 . . . . . 6 ((0 ∈ β„•0 ∧ 0001 ∈ ℝ) β†’ (0.0001) ∈ ℝ)
5037, 48, 49mp2an 690 . . . . 5 (0.0001) ∈ ℝ
5150a1i 11 . . . 4 (πœ‘ β†’ (0.0001) ∈ ℝ)
5251, 35remulcld 11246 . . 3 (πœ‘ β†’ ((0.0001) Β· (βˆšβ€˜π‘)) ∈ ℝ)
5331nnzd 12587 . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ β„€)
54 chpvalz 33709 . . . . . . 7 (𝑁 ∈ β„€ β†’ (Οˆβ€˜π‘) = Σ𝑖 ∈ (1...𝑁)(Ξ›β€˜π‘–))
5553, 54syl 17 . . . . . 6 (πœ‘ β†’ (Οˆβ€˜π‘) = Σ𝑖 ∈ (1...𝑁)(Ξ›β€˜π‘–))
56 chtvalz 33710 . . . . . . . 8 (𝑁 ∈ β„€ β†’ (ΞΈβ€˜π‘) = Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(logβ€˜π‘–))
5753, 56syl 17 . . . . . . 7 (πœ‘ β†’ (ΞΈβ€˜π‘) = Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(logβ€˜π‘–))
58 inss2 4229 . . . . . . . . . . 11 ((1...𝑁) ∩ β„™) βŠ† β„™
5958a1i 11 . . . . . . . . . 10 (πœ‘ β†’ ((1...𝑁) ∩ β„™) βŠ† β„™)
6059sselda 3982 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) ∩ β„™)) β†’ 𝑖 ∈ β„™)
61 vmaprm 26628 . . . . . . . . 9 (𝑖 ∈ β„™ β†’ (Ξ›β€˜π‘–) = (logβ€˜π‘–))
6260, 61syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) ∩ β„™)) β†’ (Ξ›β€˜π‘–) = (logβ€˜π‘–))
6362sumeq2dv 15651 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(Ξ›β€˜π‘–) = Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(logβ€˜π‘–))
6457, 63eqtr4d 2775 . . . . . 6 (πœ‘ β†’ (ΞΈβ€˜π‘) = Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(Ξ›β€˜π‘–))
6555, 64oveq12d 7429 . . . . 5 (πœ‘ β†’ ((Οˆβ€˜π‘) βˆ’ (ΞΈβ€˜π‘)) = (Σ𝑖 ∈ (1...𝑁)(Ξ›β€˜π‘–) βˆ’ Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(Ξ›β€˜π‘–)))
66 infi 9270 . . . . . . . 8 ((1...𝑁) ∈ Fin β†’ ((1...𝑁) ∩ β„™) ∈ Fin)
671, 66syl 17 . . . . . . 7 (πœ‘ β†’ ((1...𝑁) ∩ β„™) ∈ Fin)
684a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) ∩ β„™)) β†’ Ξ›:β„•βŸΆβ„)
69 inss1 4228 . . . . . . . . . . . 12 ((1...𝑁) ∩ β„™) βŠ† (1...𝑁)
7069, 6sstri 3991 . . . . . . . . . . 11 ((1...𝑁) ∩ β„™) βŠ† β„•
7170a1i 11 . . . . . . . . . 10 (πœ‘ β†’ ((1...𝑁) ∩ β„™) βŠ† β„•)
7271sselda 3982 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) ∩ β„™)) β†’ 𝑖 ∈ β„•)
7368, 72ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) ∩ β„™)) β†’ (Ξ›β€˜π‘–) ∈ ℝ)
7473recnd 11244 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) ∩ β„™)) β†’ (Ξ›β€˜π‘–) ∈ β„‚)
7567, 74fsumcl 15681 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(Ξ›β€˜π‘–) ∈ β„‚)
7610recnd 11244 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ ((1...𝑁) βˆ– β„™)) β†’ (Ξ›β€˜π‘–) ∈ β„‚)
773, 76fsumcl 15681 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–) ∈ β„‚)
78 inindif 31792 . . . . . . . 8 (((1...𝑁) ∩ β„™) ∩ ((1...𝑁) βˆ– β„™)) = βˆ…
7978a1i 11 . . . . . . 7 (πœ‘ β†’ (((1...𝑁) ∩ β„™) ∩ ((1...𝑁) βˆ– β„™)) = βˆ…)
80 inundif 4478 . . . . . . . . 9 (((1...𝑁) ∩ β„™) βˆͺ ((1...𝑁) βˆ– β„™)) = (1...𝑁)
8180eqcomi 2741 . . . . . . . 8 (1...𝑁) = (((1...𝑁) ∩ β„™) βˆͺ ((1...𝑁) βˆ– β„™))
8281a1i 11 . . . . . . 7 (πœ‘ β†’ (1...𝑁) = (((1...𝑁) ∩ β„™) βˆͺ ((1...𝑁) βˆ– β„™)))
834a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (1...𝑁)) β†’ Ξ›:β„•βŸΆβ„)
847sselda 3982 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (1...𝑁)) β†’ 𝑖 ∈ β„•)
8583, 84ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (1...𝑁)) β†’ (Ξ›β€˜π‘–) ∈ ℝ)
8685recnd 11244 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (1...𝑁)) β†’ (Ξ›β€˜π‘–) ∈ β„‚)
8779, 82, 1, 86fsumsplit 15689 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (1...𝑁)(Ξ›β€˜π‘–) = (Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(Ξ›β€˜π‘–) + Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–)))
8875, 77, 87mvrladdd 11629 . . . . 5 (πœ‘ β†’ (Σ𝑖 ∈ (1...𝑁)(Ξ›β€˜π‘–) βˆ’ Σ𝑖 ∈ ((1...𝑁) ∩ β„™)(Ξ›β€˜π‘–)) = Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–))
8965, 88eqtr2d 2773 . . . 4 (πœ‘ β†’ Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–) = ((Οˆβ€˜π‘) βˆ’ (ΞΈβ€˜π‘)))
90 fveq2 6891 . . . . . . 7 (π‘₯ = 𝑁 β†’ (Οˆβ€˜π‘₯) = (Οˆβ€˜π‘))
91 fveq2 6891 . . . . . . 7 (π‘₯ = 𝑁 β†’ (ΞΈβ€˜π‘₯) = (ΞΈβ€˜π‘))
9290, 91oveq12d 7429 . . . . . 6 (π‘₯ = 𝑁 β†’ ((Οˆβ€˜π‘₯) βˆ’ (ΞΈβ€˜π‘₯)) = ((Οˆβ€˜π‘) βˆ’ (ΞΈβ€˜π‘)))
93 fveq2 6891 . . . . . . 7 (π‘₯ = 𝑁 β†’ (βˆšβ€˜π‘₯) = (βˆšβ€˜π‘))
9493oveq2d 7427 . . . . . 6 (π‘₯ = 𝑁 β†’ ((1.4262) Β· (βˆšβ€˜π‘₯)) = ((1.4262) Β· (βˆšβ€˜π‘)))
9592, 94breq12d 5161 . . . . 5 (π‘₯ = 𝑁 β†’ (((Οˆβ€˜π‘₯) βˆ’ (ΞΈβ€˜π‘₯)) < ((1.4262) Β· (βˆšβ€˜π‘₯)) ↔ ((Οˆβ€˜π‘) βˆ’ (ΞΈβ€˜π‘)) < ((1.4262) Β· (βˆšβ€˜π‘))))
96 ax-ros336 33727 . . . . . 6 βˆ€π‘₯ ∈ ℝ+ ((Οˆβ€˜π‘₯) βˆ’ (ΞΈβ€˜π‘₯)) < ((1.4262) Β· (βˆšβ€˜π‘₯))
9796a1i 11 . . . . 5 (πœ‘ β†’ βˆ€π‘₯ ∈ ℝ+ ((Οˆβ€˜π‘₯) βˆ’ (ΞΈβ€˜π‘₯)) < ((1.4262) Β· (βˆšβ€˜π‘₯)))
9895, 97, 33rspcdva 3613 . . . 4 (πœ‘ β†’ ((Οˆβ€˜π‘) βˆ’ (ΞΈβ€˜π‘)) < ((1.4262) Β· (βˆšβ€˜π‘)))
9989, 98eqbrtrd 5170 . . 3 (πœ‘ β†’ Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–) < ((1.4262) Β· (βˆšβ€˜π‘)))
10039a1i 11 . . . 4 (πœ‘ β†’ 1 ∈ ℝ)
101 log2le1 26462 . . . . 5 (logβ€˜2) < 1
102101a1i 11 . . . 4 (πœ‘ β†’ (logβ€˜2) < 1)
103 10nn0 12697 . . . . . . . . 9 10 ∈ β„•0
104 7nn0 12496 . . . . . . . . 9 7 ∈ β„•0
105103, 104nn0expcli 14056 . . . . . . . 8 (10↑7) ∈ β„•0
106105nn0rei 12485 . . . . . . 7 (10↑7) ∈ ℝ
107106a1i 11 . . . . . 6 (πœ‘ β†’ (10↑7) ∈ ℝ)
10851, 107remulcld 11246 . . . . 5 (πœ‘ β†’ ((0.0001) Β· (10↑7)) ∈ ℝ)
109103nn0rei 12485 . . . . . . . . . . 11 10 ∈ ℝ
110 0z 12571 . . . . . . . . . . 11 0 ∈ β„€
111 3z 12597 . . . . . . . . . . 11 3 ∈ β„€
112109, 110, 1113pm3.2i 1339 . . . . . . . . . 10 (10 ∈ ℝ ∧ 0 ∈ β„€ ∧ 3 ∈ β„€)
113 1lt10 12818 . . . . . . . . . . 11 1 < 10
114 3pos 12319 . . . . . . . . . . 11 0 < 3
115113, 114pm3.2i 471 . . . . . . . . . 10 (1 < 10 ∧ 0 < 3)
116 ltexp2a 14133 . . . . . . . . . 10 (((10 ∈ ℝ ∧ 0 ∈ β„€ ∧ 3 ∈ β„€) ∧ (1 < 10 ∧ 0 < 3)) β†’ (10↑0) < (10↑3))
117112, 115, 116mp2an 690 . . . . . . . . 9 (10↑0) < (10↑3)
118103numexp0 17011 . . . . . . . . . 10 (10↑0) = 1
119118eqcomi 2741 . . . . . . . . 9 1 = (10↑0)
120109recni 11230 . . . . . . . . . . 11 10 ∈ β„‚
121 10pos 12696 . . . . . . . . . . . 12 0 < 10
12238, 121gtneii 11328 . . . . . . . . . . 11 10 β‰  0
123 4z 12598 . . . . . . . . . . 11 4 ∈ β„€
124 expm1 14080 . . . . . . . . . . 11 ((10 ∈ β„‚ ∧ 10 β‰  0 ∧ 4 ∈ β„€) β†’ (10↑(4 βˆ’ 1)) = ((10↑4) / 10))
125120, 122, 123, 124mp3an 1461 . . . . . . . . . 10 (10↑(4 βˆ’ 1)) = ((10↑4) / 10)
126 4m1e3 12343 . . . . . . . . . . 11 (4 βˆ’ 1) = 3
127126oveq2i 7422 . . . . . . . . . 10 (10↑(4 βˆ’ 1)) = (10↑3)
128 4nn0 12493 . . . . . . . . . . . . 13 4 ∈ β„•0
129103, 128nn0expcli 14056 . . . . . . . . . . . 12 (10↑4) ∈ β„•0
130129nn0cni 12486 . . . . . . . . . . 11 (10↑4) ∈ β„‚
131 divrec2 11891 . . . . . . . . . . 11 (((10↑4) ∈ β„‚ ∧ 10 ∈ β„‚ ∧ 10 β‰  0) β†’ ((10↑4) / 10) = ((1 / 10) Β· (10↑4)))
132130, 120, 122, 131mp3an 1461 . . . . . . . . . 10 ((10↑4) / 10) = ((1 / 10) Β· (10↑4))
133125, 127, 1323eqtr3ri 2769 . . . . . . . . 9 ((1 / 10) Β· (10↑4)) = (10↑3)
134117, 119, 1333brtr4i 5178 . . . . . . . 8 1 < ((1 / 10) Β· (10↑4))
135 1rp 12980 . . . . . . . . . 10 1 ∈ ℝ+
136135dp0h 32106 . . . . . . . . 9 (0.1) = (1 / 10)
137136oveq1i 7421 . . . . . . . 8 ((0.1) Β· (10↑4)) = ((1 / 10) Β· (10↑4))
138134, 137breqtrri 5175 . . . . . . 7 1 < ((0.1) Β· (10↑4))
139138a1i 11 . . . . . 6 (πœ‘ β†’ 1 < ((0.1) Β· (10↑4)))
140 4p1e5 12360 . . . . . . . 8 (4 + 1) = 5
141 5nn0 12494 . . . . . . . . 9 5 ∈ β„•0
142141nn0zi 12589 . . . . . . . 8 5 ∈ β„€
14337, 135, 140, 123, 142dpexpp1 32112 . . . . . . 7 ((0.1) Β· (10↑4)) = ((0.01) Β· (10↑5))
14437, 135rpdp2cl 32086 . . . . . . . 8 01 ∈ ℝ+
145 5p1e6 12361 . . . . . . . 8 (5 + 1) = 6
146 6nn0 12495 . . . . . . . . 9 6 ∈ β„•0
147146nn0zi 12589 . . . . . . . 8 6 ∈ β„€
14837, 144, 145, 142, 147dpexpp1 32112 . . . . . . 7 ((0.01) Β· (10↑5)) = ((0.001) Β· (10↑6))
14937, 144rpdp2cl 32086 . . . . . . . 8 001 ∈ ℝ+
150 6p1e7 12362 . . . . . . . 8 (6 + 1) = 7
151104nn0zi 12589 . . . . . . . 8 7 ∈ β„€
15237, 149, 150, 147, 151dpexpp1 32112 . . . . . . 7 ((0.001) Β· (10↑6)) = ((0.0001) Β· (10↑7))
153143, 148, 1523eqtrri 2765 . . . . . 6 ((0.0001) Β· (10↑7)) = ((0.1) Β· (10↑4))
154139, 153breqtrrdi 5190 . . . . 5 (πœ‘ β†’ 1 < ((0.0001) Β· (10↑7)))
15537, 149rpdp2cl 32086 . . . . . . . 8 0001 ∈ ℝ+
15637, 155rpdpcl 32107 . . . . . . 7 (0.0001) ∈ ℝ+
157156a1i 11 . . . . . 6 (πœ‘ β†’ (0.0001) ∈ ℝ+)
158 2nn0 12491 . . . . . . . . . . . 12 2 ∈ β„•0
159158, 104deccl 12694 . . . . . . . . . . 11 27 ∈ β„•0
160103, 159nn0expcli 14056 . . . . . . . . . 10 (10↑27) ∈ β„•0
161160nn0rei 12485 . . . . . . . . 9 (10↑27) ∈ ℝ
162161a1i 11 . . . . . . . 8 (πœ‘ β†’ (10↑27) ∈ ℝ)
163160nn0ge0i 12501 . . . . . . . . 9 0 ≀ (10↑27)
164163a1i 11 . . . . . . . 8 (πœ‘ β†’ 0 ≀ (10↑27))
165162, 164resqrtcld 15366 . . . . . . 7 (πœ‘ β†’ (βˆšβ€˜(10↑27)) ∈ ℝ)
166 expmul 14075 . . . . . . . . . . . . 13 ((10 ∈ β„‚ ∧ 7 ∈ β„•0 ∧ 2 ∈ β„•0) β†’ (10↑(7 Β· 2)) = ((10↑7)↑2))
167120, 104, 158, 166mp3an 1461 . . . . . . . . . . . 12 (10↑(7 Β· 2)) = ((10↑7)↑2)
168 7t2e14 12788 . . . . . . . . . . . . 13 (7 Β· 2) = 14
169168oveq2i 7422 . . . . . . . . . . . 12 (10↑(7 Β· 2)) = (10↑14)
170167, 169eqtr3i 2762 . . . . . . . . . . 11 ((10↑7)↑2) = (10↑14)
171170fveq2i 6894 . . . . . . . . . 10 (βˆšβ€˜((10↑7)↑2)) = (βˆšβ€˜(10↑14))
172 expgt0 14063 . . . . . . . . . . . . 13 ((10 ∈ ℝ ∧ 7 ∈ β„€ ∧ 0 < 10) β†’ 0 < (10↑7))
173109, 151, 121, 172mp3an 1461 . . . . . . . . . . . 12 0 < (10↑7)
17438, 106, 173ltleii 11339 . . . . . . . . . . 11 0 ≀ (10↑7)
175 sqrtsq 15218 . . . . . . . . . . 11 (((10↑7) ∈ ℝ ∧ 0 ≀ (10↑7)) β†’ (βˆšβ€˜((10↑7)↑2)) = (10↑7))
176106, 174, 175mp2an 690 . . . . . . . . . 10 (βˆšβ€˜((10↑7)↑2)) = (10↑7)
177171, 176eqtr3i 2762 . . . . . . . . 9 (βˆšβ€˜(10↑14)) = (10↑7)
17815, 128deccl 12694 . . . . . . . . . . . . 13 14 ∈ β„•0
179178nn0zi 12589 . . . . . . . . . . . 12 14 ∈ β„€
180159nn0zi 12589 . . . . . . . . . . . 12 27 ∈ β„€
181109, 179, 1803pm3.2i 1339 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 14 ∈ β„€ ∧ 27 ∈ β„€)
182 4lt10 12815 . . . . . . . . . . . . 13 4 < 10
183 1lt2 12385 . . . . . . . . . . . . 13 1 < 2
18415, 158, 128, 104, 182, 183decltc 12708 . . . . . . . . . . . 12 14 < 27
185113, 184pm3.2i 471 . . . . . . . . . . 11 (1 < 10 ∧ 14 < 27)
186 ltexp2a 14133 . . . . . . . . . . 11 (((10 ∈ ℝ ∧ 14 ∈ β„€ ∧ 27 ∈ β„€) ∧ (1 < 10 ∧ 14 < 27)) β†’ (10↑14) < (10↑27))
187181, 185, 186mp2an 690 . . . . . . . . . 10 (10↑14) < (10↑27)
188103, 178nn0expcli 14056 . . . . . . . . . . . . 13 (10↑14) ∈ β„•0
189188nn0rei 12485 . . . . . . . . . . . 12 (10↑14) ∈ ℝ
190 expgt0 14063 . . . . . . . . . . . . . 14 ((10 ∈ ℝ ∧ 14 ∈ β„€ ∧ 0 < 10) β†’ 0 < (10↑14))
191109, 179, 121, 190mp3an 1461 . . . . . . . . . . . . 13 0 < (10↑14)
19238, 189, 191ltleii 11339 . . . . . . . . . . . 12 0 ≀ (10↑14)
193189, 192pm3.2i 471 . . . . . . . . . . 11 ((10↑14) ∈ ℝ ∧ 0 ≀ (10↑14))
194161, 163pm3.2i 471 . . . . . . . . . . 11 ((10↑27) ∈ ℝ ∧ 0 ≀ (10↑27))
195 sqrtlt 15210 . . . . . . . . . . 11 ((((10↑14) ∈ ℝ ∧ 0 ≀ (10↑14)) ∧ ((10↑27) ∈ ℝ ∧ 0 ≀ (10↑27))) β†’ ((10↑14) < (10↑27) ↔ (βˆšβ€˜(10↑14)) < (βˆšβ€˜(10↑27))))
196193, 194, 195mp2an 690 . . . . . . . . . 10 ((10↑14) < (10↑27) ↔ (βˆšβ€˜(10↑14)) < (βˆšβ€˜(10↑27)))
197187, 196mpbi 229 . . . . . . . . 9 (βˆšβ€˜(10↑14)) < (βˆšβ€˜(10↑27))
198177, 197eqbrtrri 5171 . . . . . . . 8 (10↑7) < (βˆšβ€˜(10↑27))
199198a1i 11 . . . . . . 7 (πœ‘ β†’ (10↑7) < (βˆšβ€˜(10↑27)))
200 hgt750lemd.0 . . . . . . . 8 (πœ‘ β†’ (10↑27) ≀ 𝑁)
201162, 164, 32, 34sqrtled 15375 . . . . . . . 8 (πœ‘ β†’ ((10↑27) ≀ 𝑁 ↔ (βˆšβ€˜(10↑27)) ≀ (βˆšβ€˜π‘)))
202200, 201mpbid 231 . . . . . . 7 (πœ‘ β†’ (βˆšβ€˜(10↑27)) ≀ (βˆšβ€˜π‘))
203107, 165, 35, 199, 202ltletrd 11376 . . . . . 6 (πœ‘ β†’ (10↑7) < (βˆšβ€˜π‘))
204107, 35, 157, 203ltmul2dd 13074 . . . . 5 (πœ‘ β†’ ((0.0001) Β· (10↑7)) < ((0.0001) Β· (βˆšβ€˜π‘)))
205100, 108, 52, 154, 204lttrd 11377 . . . 4 (πœ‘ β†’ 1 < ((0.0001) Β· (βˆšβ€˜π‘)))
20614, 100, 52, 102, 205lttrd 11377 . . 3 (πœ‘ β†’ (logβ€˜2) < ((0.0001) Β· (βˆšβ€˜π‘)))
20711, 14, 36, 52, 99, 206lt2addd 11839 . 2 (πœ‘ β†’ (Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–) + (logβ€˜2)) < (((1.4262) Β· (βˆšβ€˜π‘)) + ((0.0001) Β· (βˆšβ€˜π‘))))
208 nfv 1917 . . 3 β„²π‘–πœ‘
209 nfcv 2903 . . 3 Ⅎ𝑖(logβ€˜2)
210 2prm 16631 . . . 4 2 ∈ β„™
211210a1i 11 . . 3 (πœ‘ β†’ 2 ∈ β„™)
212 elndif 4128 . . . 4 (2 ∈ β„™ β†’ Β¬ 2 ∈ ((1...𝑁) βˆ– β„™))
213211, 212syl 17 . . 3 (πœ‘ β†’ Β¬ 2 ∈ ((1...𝑁) βˆ– β„™))
214 fveq2 6891 . . . 4 (𝑖 = 2 β†’ (Ξ›β€˜π‘–) = (Ξ›β€˜2))
215 vmaprm 26628 . . . . 5 (2 ∈ β„™ β†’ (Ξ›β€˜2) = (logβ€˜2))
216210, 215ax-mp 5 . . . 4 (Ξ›β€˜2) = (logβ€˜2)
217214, 216eqtrdi 2788 . . 3 (𝑖 = 2 β†’ (Ξ›β€˜π‘–) = (logβ€˜2))
218 2cnd 12292 . . . 4 (πœ‘ β†’ 2 ∈ β„‚)
219 2ne0 12318 . . . . 5 2 β‰  0
220219a1i 11 . . . 4 (πœ‘ β†’ 2 β‰  0)
221218, 220logcld 26086 . . 3 (πœ‘ β†’ (logβ€˜2) ∈ β„‚)
222208, 209, 3, 211, 213, 76, 217, 221fsumsplitsn 15692 . 2 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) = (Σ𝑖 ∈ ((1...𝑁) βˆ– β„™)(Ξ›β€˜π‘–) + (logβ€˜2)))
223146, 12rpdp2cl 32086 . . . . . 6 62 ∈ ℝ+
224158, 223rpdp2cl 32086 . . . . 5 262 ∈ ℝ+
225 3rp 12982 . . . . . . 7 3 ∈ ℝ+
226146, 225rpdp2cl 32086 . . . . . 6 63 ∈ ℝ+
227158, 226rpdp2cl 32086 . . . . 5 263 ∈ ℝ+
228 1p0e1 12338 . . . . 5 (1 + 0) = 1
229 4cn 12299 . . . . . . 7 4 ∈ β„‚
230229addridi 11403 . . . . . 6 (4 + 0) = 4
231 2cn 12289 . . . . . . . 8 2 ∈ β„‚
232231addridi 11403 . . . . . . 7 (2 + 0) = 2
233 3nn0 12492 . . . . . . . 8 3 ∈ β„•0
234 eqid 2732 . . . . . . . . 9 62 = 62
235 eqid 2732 . . . . . . . . 9 01 = 01
236 6cn 12305 . . . . . . . . . 10 6 ∈ β„‚
237236addridi 11403 . . . . . . . . 9 (6 + 0) = 6
238 2p1e3 12356 . . . . . . . . 9 (2 + 1) = 3
239146, 158, 37, 15, 234, 235, 237, 238decadd 12733 . . . . . . . 8 (62 + 01) = 63
240146, 158, 37, 15, 146, 233, 239dpadd 32115 . . . . . . 7 ((6.2) + (0.1)) = (6.3)
241146, 12, 37, 135, 146, 225, 158, 37, 232, 240dpadd2 32114 . . . . . 6 ((2.62) + (0.01)) = (2.63)
242158, 223, 37, 144, 158, 226, 128, 37, 230, 241dpadd2 32114 . . . . 5 ((4.262) + (0.001)) = (4.263)
243128, 224, 37, 149, 128, 227, 15, 37, 228, 242dpadd2 32114 . . . 4 ((1.4262) + (0.0001)) = (1.4263)
244243oveq1i 7421 . . 3 (((1.4262) + (0.0001)) Β· (βˆšβ€˜π‘)) = ((1.4263) Β· (βˆšβ€˜π‘))
24530recnd 11244 . . . 4 (πœ‘ β†’ (1.4262) ∈ β„‚)
24651recnd 11244 . . . 4 (πœ‘ β†’ (0.0001) ∈ β„‚)
24735recnd 11244 . . . 4 (πœ‘ β†’ (βˆšβ€˜π‘) ∈ β„‚)
248245, 246, 247adddird 11241 . . 3 (πœ‘ β†’ (((1.4262) + (0.0001)) Β· (βˆšβ€˜π‘)) = (((1.4262) Β· (βˆšβ€˜π‘)) + ((0.0001) Β· (βˆšβ€˜π‘))))
249244, 248eqtr3id 2786 . 2 (πœ‘ β†’ ((1.4263) Β· (βˆšβ€˜π‘)) = (((1.4262) Β· (βˆšβ€˜π‘)) + ((0.0001) Β· (βˆšβ€˜π‘))))
250207, 222, 2493brtr4d 5180 1 (πœ‘ β†’ Σ𝑖 ∈ (((1...𝑁) βˆ– β„™) βˆͺ {2})(Ξ›β€˜π‘–) < ((1.4263) Β· (βˆšβ€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628   class class class wbr 5148  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7411  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446   / cdiv 11873  β„•cn 12214  2c2 12269  3c3 12270  4c4 12271  5c5 12272  6c6 12273  7c7 12274  β„•0cn0 12474  β„€cz 12560  cdc 12679  β„+crp 12976  ...cfz 13486  β†‘cexp 14029  βˆšcsqrt 15182  Ξ£csu 15634  β„™cprime 16610  logclog 26070  ΞΈccht 26602  Ξ›cvma 26603  Οˆcchp 26604  cdp2 32075  .cdp 32092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192  ax-ros336 33727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-xnn0 12547  df-z 12561  df-dec 12680  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-ioo 13330  df-ioc 13331  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-fac 14236  df-bc 14265  df-hash 14293  df-shft 15016  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-limsup 15417  df-clim 15434  df-rlim 15435  df-sum 15635  df-ef 16013  df-sin 16015  df-cos 16016  df-tan 16017  df-pi 16018  df-dvds 16200  df-gcd 16438  df-prm 16611  df-pc 16772  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-starv 17214  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ds 17221  df-unif 17222  df-hom 17223  df-cco 17224  df-rest 17370  df-topn 17371  df-0g 17389  df-gsum 17390  df-topgen 17391  df-pt 17392  df-prds 17395  df-xrs 17450  df-qtop 17455  df-imas 17456  df-xps 17458  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-submnd 18674  df-mulg 18953  df-cntz 19183  df-cmn 19652  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-fbas 20947  df-fg 20948  df-cnfld 20951  df-top 22403  df-topon 22420  df-topsp 22442  df-bases 22456  df-cld 22530  df-ntr 22531  df-cls 22532  df-nei 22609  df-lp 22647  df-perf 22648  df-cn 22738  df-cnp 22739  df-haus 22826  df-cmp 22898  df-tx 23073  df-hmeo 23266  df-fil 23357  df-fm 23449  df-flim 23450  df-flf 23451  df-xms 23833  df-ms 23834  df-tms 23835  df-cncf 24401  df-limc 25390  df-dv 25391  df-ulm 25896  df-log 26072  df-atan 26379  df-cht 26608  df-vma 26609  df-chp 26610  df-dp2 32076  df-dp 32093
This theorem is referenced by:  hgt750leme  33739
  Copyright terms: Public domain W3C validator