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

Theorem hgt750leme 31037
Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of [Helfgott] p. 69. (Contributed by Thierry Arnoux, 29-Dec-2021.)
Hypotheses
Ref Expression
hgt750leme.o 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
hgt750leme.n (𝜑𝑁 ∈ ℕ)
hgt750leme.0 (𝜑 → (10↑27) ≤ 𝑁)
hgt750leme.h (𝜑𝐻:ℕ⟶(0[,)+∞))
hgt750leme.k (𝜑𝐾:ℕ⟶(0[,)+∞))
hgt750leme.1 ((𝜑𝑚 ∈ ℕ) → (𝐾𝑚) ≤ (1.079955))
hgt750leme.2 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ≤ (1.414))
Assertion
Ref Expression
hgt750leme (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
Distinct variable groups:   𝑧,𝑂   𝑚,𝐻   𝑚,𝐾   𝑚,𝑁,𝑛   𝑚,𝑂,𝑛,𝑧   𝜑,𝑚,𝑛
Allowed substitution hints:   𝜑(𝑧)   𝐻(𝑧,𝑛)   𝐾(𝑧,𝑛)   𝑁(𝑧)

Proof of Theorem hgt750leme
Dummy variables 𝑎 𝑐 𝑑 𝑒 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hgt750leme.n . . . . . 6 (𝜑𝑁 ∈ ℕ)
21nnnn0d 11535 . . . . 5 (𝜑𝑁 ∈ ℕ0)
3 3nn0 11494 . . . . . 6 3 ∈ ℕ0
43a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ0)
5 ssid 3757 . . . . . 6 ℕ ⊆ ℕ
65a1i 11 . . . . 5 (𝜑 → ℕ ⊆ ℕ)
72, 4, 6reprfi2 31002 . . . 4 (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
8 diffi 8349 . . . 4 ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
97, 8syl 17 . . 3 (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
10 vmaf 25036 . . . . . . 7 Λ:ℕ⟶ℝ
1110a1i 11 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
125a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
131nnzd 11665 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
1413adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ)
153a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈ ℕ0)
16 simpr 479 . . . . . . . . 9 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))
1716eldifad 3719 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
1812, 14, 15, 17reprf 30991 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
19 c0ex 10218 . . . . . . . . . 10 0 ∈ V
2019tpid1 4439 . . . . . . . . 9 0 ∈ {0, 1, 2}
21 fzo0to3tp 12740 . . . . . . . . 9 (0..^3) = {0, 1, 2}
2220, 21eleqtrri 2830 . . . . . . . 8 0 ∈ (0..^3)
2322a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
2418, 23ffvelrnd 6515 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
2511, 24ffvelrnd 6515 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
26 rge0ssre 12465 . . . . . 6 (0[,)+∞) ⊆ ℝ
27 hgt750leme.h . . . . . . . 8 (𝜑𝐻:ℕ⟶(0[,)+∞))
2827adantr 472 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
2928, 24ffvelrnd 6515 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
3026, 29sseldi 3734 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
3125, 30remulcld 10254 . . . 4 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
32 1ex 10219 . . . . . . . . . . 11 1 ∈ V
3332tpid2 4440 . . . . . . . . . 10 1 ∈ {0, 1, 2}
3433, 21eleqtrri 2830 . . . . . . . . 9 1 ∈ (0..^3)
3534a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
3618, 35ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
3711, 36ffvelrnd 6515 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘1)) ∈ ℝ)
38 hgt750leme.k . . . . . . . . 9 (𝜑𝐾:ℕ⟶(0[,)+∞))
3938adantr 472 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞))
4039, 36ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
4126, 40sseldi 3734 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
4237, 41remulcld 10254 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
43 2ex 11276 . . . . . . . . . . 11 2 ∈ V
4443tpid3 4442 . . . . . . . . . 10 2 ∈ {0, 1, 2}
4544, 21eleqtrri 2830 . . . . . . . . 9 2 ∈ (0..^3)
4645a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
4718, 46ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
4811, 47ffvelrnd 6515 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
4939, 47ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
5026, 49sseldi 3734 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
5148, 50remulcld 10254 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
5242, 51remulcld 10254 . . . 4 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
5331, 52remulcld 10254 . . 3 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
549, 53fsumrecl 14656 . 2 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
55 3re 11278 . . . 4 3 ∈ ℝ
5655a1i 11 . . 3 (𝜑 → 3 ∈ ℝ)
57 1nn0 11492 . . . . . . . . 9 1 ∈ ℕ0
58 0nn0 11491 . . . . . . . . . 10 0 ∈ ℕ0
59 7nn0 11498 . . . . . . . . . . 11 7 ∈ ℕ0
60 9nn0 11500 . . . . . . . . . . . 12 9 ∈ ℕ0
61 5nn0 11496 . . . . . . . . . . . . . 14 5 ∈ ℕ0
62 5nn 11372 . . . . . . . . . . . . . . 15 5 ∈ ℕ
63 nnrp 12027 . . . . . . . . . . . . . . 15 (5 ∈ ℕ → 5 ∈ ℝ+)
6462, 63ax-mp 5 . . . . . . . . . . . . . 14 5 ∈ ℝ+
6561, 64rpdp2cl 29890 . . . . . . . . . . . . 13 55 ∈ ℝ+
6660, 65rpdp2cl 29890 . . . . . . . . . . . 12 955 ∈ ℝ+
6760, 66rpdp2cl 29890 . . . . . . . . . . 11 9955 ∈ ℝ+
6859, 67rpdp2cl 29890 . . . . . . . . . 10 79955 ∈ ℝ+
6958, 68rpdp2cl 29890 . . . . . . . . 9 079955 ∈ ℝ+
7057, 69rpdpcl 29912 . . . . . . . 8 (1.079955) ∈ ℝ+
7170a1i 11 . . . . . . 7 (𝜑 → (1.079955) ∈ ℝ+)
7271rpred 12057 . . . . . 6 (𝜑 → (1.079955) ∈ ℝ)
7372resqcld 13221 . . . . 5 (𝜑 → ((1.079955)↑2) ∈ ℝ)
74 4nn0 11495 . . . . . . . . 9 4 ∈ ℕ0
75 4nn 11371 . . . . . . . . . . 11 4 ∈ ℕ
76 nnrp 12027 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
7775, 76ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
7857, 77rpdp2cl 29890 . . . . . . . . 9 14 ∈ ℝ+
7974, 78rpdp2cl 29890 . . . . . . . 8 414 ∈ ℝ+
8057, 79rpdpcl 29912 . . . . . . 7 (1.414) ∈ ℝ+
8180a1i 11 . . . . . 6 (𝜑 → (1.414) ∈ ℝ+)
8281rpred 12057 . . . . 5 (𝜑 → (1.414) ∈ ℝ)
8373, 82remulcld 10254 . . . 4 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℝ)
84 fveq1 6343 . . . . . . . . . 10 (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
8584eleq1d 2816 . . . . . . . . 9 (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
8685notbid 307 . . . . . . . 8 (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
8786cbvrabv 3331 . . . . . . 7 {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
8887ssrab3 3821 . . . . . 6 {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
89 ssfi 8337 . . . . . 6 (((ℕ(repr‘3)𝑁) ∈ Fin ∧ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)) → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
907, 88, 89sylancl 697 . . . . 5 (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
9110a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
925a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
9313adantr 472 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ)
943a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 3 ∈ ℕ0)
9588a1i 11 . . . . . . . . . 10 (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁))
9695sselda 3736 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
9792, 93, 94, 96reprf 30991 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
9822a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
9997, 98ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
10091, 99ffvelrnd 6515 . . . . . 6 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
10134a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
10297, 101ffvelrnd 6515 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
10391, 102ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
10445a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
10597, 104ffvelrnd 6515 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
10691, 105ffvelrnd 6515 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
107103, 106remulcld 10254 . . . . . 6 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
108100, 107remulcld 10254 . . . . 5 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
10990, 108fsumrecl 14656 . . . 4 (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
11083, 109remulcld 10254 . . 3 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
11156, 110remulcld 10254 . 2 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
112 4re 11281 . . . . . . . . . 10 4 ∈ ℝ
113 8re 11289 . . . . . . . . . 10 8 ∈ ℝ
114112, 113pm3.2i 470 . . . . . . . . 9 (4 ∈ ℝ ∧ 8 ∈ ℝ)
115 dp2cl 29888 . . . . . . . . 9 ((4 ∈ ℝ ∧ 8 ∈ ℝ) → 48 ∈ ℝ)
116114, 115ax-mp 5 . . . . . . . 8 48 ∈ ℝ
11755, 116pm3.2i 470 . . . . . . 7 (3 ∈ ℝ ∧ 48 ∈ ℝ)
118 dp2cl 29888 . . . . . . 7 ((3 ∈ ℝ ∧ 48 ∈ ℝ) → 348 ∈ ℝ)
119117, 118ax-mp 5 . . . . . 6 348 ∈ ℝ
120 dpcl 29899 . . . . . 6 ((7 ∈ ℕ0348 ∈ ℝ) → (7.348) ∈ ℝ)
12159, 119, 120mp2an 710 . . . . 5 (7.348) ∈ ℝ
122121a1i 11 . . . 4 (𝜑 → (7.348) ∈ ℝ)
1231nnrpd 12055 . . . . . 6 (𝜑𝑁 ∈ ℝ+)
124123relogcld 24560 . . . . 5 (𝜑 → (log‘𝑁) ∈ ℝ)
1251nnred 11219 . . . . . 6 (𝜑𝑁 ∈ ℝ)
126123rpge0d 12061 . . . . . 6 (𝜑 → 0 ≤ 𝑁)
127125, 126resqrtcld 14347 . . . . 5 (𝜑 → (√‘𝑁) ∈ ℝ)
128123rpsqrtcld 14341 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
129128rpne0d 12062 . . . . 5 (𝜑 → (√‘𝑁) ≠ 0)
130124, 127, 129redivcld 11037 . . . 4 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
131122, 130remulcld 10254 . . 3 (𝜑 → ((7.348) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
132125resqcld 13221 . . 3 (𝜑 → (𝑁↑2) ∈ ℝ)
133131, 132remulcld 10254 . 2 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
134 0re 10224 . . . . . . . . . . 11 0 ∈ ℝ
135 7re 11287 . . . . . . . . . . . . 13 7 ∈ ℝ
136 9re 11291 . . . . . . . . . . . . . . 15 9 ∈ ℝ
137 5re 11283 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℝ
138137, 137pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℝ ∧ 5 ∈ ℝ)
139 dp2cl 29888 . . . . . . . . . . . . . . . . . 18 ((5 ∈ ℝ ∧ 5 ∈ ℝ) → 55 ∈ ℝ)
140138, 139ax-mp 5 . . . . . . . . . . . . . . . . 17 55 ∈ ℝ
141136, 140pm3.2i 470 . . . . . . . . . . . . . . . 16 (9 ∈ ℝ ∧ 55 ∈ ℝ)
142 dp2cl 29888 . . . . . . . . . . . . . . . 16 ((9 ∈ ℝ ∧ 55 ∈ ℝ) → 955 ∈ ℝ)
143141, 142ax-mp 5 . . . . . . . . . . . . . . 15 955 ∈ ℝ
144136, 143pm3.2i 470 . . . . . . . . . . . . . 14 (9 ∈ ℝ ∧ 955 ∈ ℝ)
145 dp2cl 29888 . . . . . . . . . . . . . 14 ((9 ∈ ℝ ∧ 955 ∈ ℝ) → 9955 ∈ ℝ)
146144, 145ax-mp 5 . . . . . . . . . . . . 13 9955 ∈ ℝ
147135, 146pm3.2i 470 . . . . . . . . . . . 12 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
148 dp2cl 29888 . . . . . . . . . . . 12 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) → 79955 ∈ ℝ)
149147, 148ax-mp 5 . . . . . . . . . . 11 79955 ∈ ℝ
150134, 149pm3.2i 470 . . . . . . . . . 10 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
151 dp2cl 29888 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) → 079955 ∈ ℝ)
152150, 151ax-mp 5 . . . . . . . . 9 079955 ∈ ℝ
153 dpcl 29899 . . . . . . . . 9 ((1 ∈ ℕ0079955 ∈ ℝ) → (1.079955) ∈ ℝ)
15457, 152, 153mp2an 710 . . . . . . . 8 (1.079955) ∈ ℝ
155154a1i 11 . . . . . . 7 (𝜑 → (1.079955) ∈ ℝ)
156155resqcld 13221 . . . . . 6 (𝜑 → ((1.079955)↑2) ∈ ℝ)
157 1re 10223 . . . . . . . . . . . 12 1 ∈ ℝ
158157, 112pm3.2i 470 . . . . . . . . . . 11 (1 ∈ ℝ ∧ 4 ∈ ℝ)
159 dp2cl 29888 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 4 ∈ ℝ) → 14 ∈ ℝ)
160158, 159ax-mp 5 . . . . . . . . . 10 14 ∈ ℝ
161112, 160pm3.2i 470 . . . . . . . . 9 (4 ∈ ℝ ∧ 14 ∈ ℝ)
162 dp2cl 29888 . . . . . . . . 9 ((4 ∈ ℝ ∧ 14 ∈ ℝ) → 414 ∈ ℝ)
163161, 162ax-mp 5 . . . . . . . 8 414 ∈ ℝ
164 dpcl 29899 . . . . . . . 8 ((1 ∈ ℕ0414 ∈ ℝ) → (1.414) ∈ ℝ)
16557, 163, 164mp2an 710 . . . . . . 7 (1.414) ∈ ℝ
166165a1i 11 . . . . . 6 (𝜑 → (1.414) ∈ ℝ)
167156, 166remulcld 10254 . . . . 5 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℝ)
16837, 48remulcld 10254 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
16925, 168remulcld 10254 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
1709, 169fsumrecl 14656 . . . . 5 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
171167, 170remulcld 10254 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
17256, 109remulcld 10254 . . . . 5 (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
173167, 172remulcld 10254 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
174 hgt750leme.1 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐾𝑚) ≤ (1.079955))
175 hgt750leme.2 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ≤ (1.414))
1769, 155, 166, 27, 38, 24, 36, 47, 174, 175hgt750lemf 31032 . . . 4 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
177 hgt750leme.o . . . . . 6 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
178 2re 11274 . . . . . . . 8 2 ∈ ℝ
179178a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℝ)
180 10nn0 11700 . . . . . . . . . 10 10 ∈ ℕ0
181 2nn0 11493 . . . . . . . . . . 11 2 ∈ ℕ0
182181, 59deccl 11696 . . . . . . . . . 10 27 ∈ ℕ0
183180, 182nn0expcli 13072 . . . . . . . . 9 (10↑27) ∈ ℕ0
184183nn0rei 11487 . . . . . . . 8 (10↑27) ∈ ℝ
185184a1i 11 . . . . . . 7 (𝜑 → (10↑27) ∈ ℝ)
186180numexp1 15975 . . . . . . . . . 10 (10↑1) = 10
187180nn0rei 11487 . . . . . . . . . 10 10 ∈ ℝ
188186, 187eqeltri 2827 . . . . . . . . 9 (10↑1) ∈ ℝ
189188a1i 11 . . . . . . . 8 (𝜑 → (10↑1) ∈ ℝ)
190 1nn 11215 . . . . . . . . . . 11 1 ∈ ℕ
191 2lt9 11412 . . . . . . . . . . . 12 2 < 9
192178, 136, 191ltleii 10344 . . . . . . . . . . 11 2 ≤ 9
193190, 58, 181, 192declei 11726 . . . . . . . . . 10 2 ≤ 10
194193, 186breqtrri 4823 . . . . . . . . 9 2 ≤ (10↑1)
195194a1i 11 . . . . . . . 8 (𝜑 → 2 ≤ (10↑1))
196 1z 11591 . . . . . . . . . . . 12 1 ∈ ℤ
197182nn0zi 11586 . . . . . . . . . . . 12 27 ∈ ℤ
198187, 196, 1973pm3.2i 1421 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ)
199 1lt10 11865 . . . . . . . . . . 11 1 < 10
200198, 199pm3.2i 470 . . . . . . . . . 10 ((10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ) ∧ 1 < 10)
201 2nn 11369 . . . . . . . . . . 11 2 ∈ ℕ
202 1lt9 11413 . . . . . . . . . . . 12 1 < 9
203157, 136, 202ltleii 10344 . . . . . . . . . . 11 1 ≤ 9
204201, 59, 57, 203declei 11726 . . . . . . . . . 10 1 ≤ 27
205 leexp2 13101 . . . . . . . . . . 11 (((10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ) ∧ 1 < 10) → (1 ≤ 27 ↔ (10↑1) ≤ (10↑27)))
206205biimpa 502 . . . . . . . . . 10 ((((10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ) ∧ 1 < 10) ∧ 1 ≤ 27) → (10↑1) ≤ (10↑27))
207200, 204, 206mp2an 710 . . . . . . . . 9 (10↑1) ≤ (10↑27)
208207a1i 11 . . . . . . . 8 (𝜑 → (10↑1) ≤ (10↑27))
209179, 189, 185, 195, 208letrd 10378 . . . . . . 7 (𝜑 → 2 ≤ (10↑27))
210 hgt750leme.0 . . . . . . 7 (𝜑 → (10↑27) ≤ 𝑁)
211179, 185, 125, 209, 210letrd 10378 . . . . . 6 (𝜑 → 2 ≤ 𝑁)
212 eqid 2752 . . . . . 6 (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0})))) = (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))
213177, 1, 211, 87, 212hgt750lema 31036 . . . . 5 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
214 2z 11593 . . . . . . . . 9 2 ∈ ℤ
215214a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
21671, 215rpexpcld 13218 . . . . . . 7 (𝜑 → ((1.079955)↑2) ∈ ℝ+)
217216, 81rpmulcld 12073 . . . . . 6 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℝ+)
218170, 172, 217lemul2d 12101 . . . . 5 (𝜑 → (Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ↔ ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))))
219213, 218mpbid 222 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
22054, 171, 173, 176, 219letrd 10378 . . 3 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
221155recnd 10252 . . . . . 6 (𝜑 → (1.079955) ∈ ℂ)
222221sqcld 13192 . . . . 5 (𝜑 → ((1.079955)↑2) ∈ ℂ)
223166recnd 10252 . . . . 5 (𝜑 → (1.414) ∈ ℂ)
224222, 223mulcld 10244 . . . 4 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℂ)
225 3cn 11279 . . . . 5 3 ∈ ℂ
226225a1i 11 . . . 4 (𝜑 → 3 ∈ ℂ)
227109recnd 10252 . . . 4 (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
228224, 226, 227mul12d 10429 . . 3 (𝜑 → ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) = (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
229220, 228breqtrd 4822 . 2 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
230 fzfi 12957 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
231 diffi 8349 . . . . . . . . . . 11 ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
232230, 231ax-mp 5 . . . . . . . . . 10 ((1...𝑁) ∖ ℙ) ∈ Fin
233 snfi 8195 . . . . . . . . . 10 {2} ∈ Fin
234 unfi 8384 . . . . . . . . . 10 ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
235232, 233, 234mp2an 710 . . . . . . . . 9 (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
236235a1i 11 . . . . . . . 8 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
23710a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
238 fz1ssnn 12557 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℕ
239238a1i 11 . . . . . . . . . . . 12 (𝜑 → (1...𝑁) ⊆ ℕ)
240239ssdifssd 3883 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
241201a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℕ)
242241snssd 4477 . . . . . . . . . . 11 (𝜑 → {2} ⊆ ℕ)
243240, 242unssd 3924 . . . . . . . . . 10 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
244243sselda 3736 . . . . . . . . 9 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
245237, 244ffvelrnd 6515 . . . . . . . 8 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
246236, 245fsumrecl 14656 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
247 chpvalz 31007 . . . . . . . . 9 (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
24813, 247syl 17 . . . . . . . 8 (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
249 chpf 25040 . . . . . . . . . 10 ψ:ℝ⟶ℝ
250249a1i 11 . . . . . . . . 9 (𝜑 → ψ:ℝ⟶ℝ)
251250, 125ffvelrnd 6515 . . . . . . . 8 (𝜑 → (ψ‘𝑁) ∈ ℝ)
252248, 251eqeltrrd 2832 . . . . . . 7 (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
253246, 252remulcld 10254 . . . . . 6 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
254124, 253remulcld 10254 . . . . 5 (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
25583, 254remulcld 10254 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
25656, 255remulcld 10254 . . 3 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
257177, 1, 211, 87hgt750lemb 31035 . . . . 5 (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
258109, 254, 217lemul2d 12101 . . . . 5 (𝜑 → (Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ↔ ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))))
259257, 258mpbid 222 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))
260 3rp 12023 . . . . . 6 3 ∈ ℝ+
261260a1i 11 . . . . 5 (𝜑 → 3 ∈ ℝ+)
262110, 255, 261lemul2d 12101 . . . 4 (𝜑 → (((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ↔ (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))))
263259, 262mpbid 222 . . 3 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))))
264 6re 11285 . . . . . . . . . . . . . . . . 17 6 ∈ ℝ
265264, 55pm3.2i 470 . . . . . . . . . . . . . . . 16 (6 ∈ ℝ ∧ 3 ∈ ℝ)
266 dp2cl 29888 . . . . . . . . . . . . . . . 16 ((6 ∈ ℝ ∧ 3 ∈ ℝ) → 63 ∈ ℝ)
267265, 266ax-mp 5 . . . . . . . . . . . . . . 15 63 ∈ ℝ
268178, 267pm3.2i 470 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 63 ∈ ℝ)
269 dp2cl 29888 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 63 ∈ ℝ) → 263 ∈ ℝ)
270268, 269ax-mp 5 . . . . . . . . . . . . 13 263 ∈ ℝ
271112, 270pm3.2i 470 . . . . . . . . . . . 12 (4 ∈ ℝ ∧ 263 ∈ ℝ)
272 dp2cl 29888 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 263 ∈ ℝ) → 4263 ∈ ℝ)
273271, 272ax-mp 5 . . . . . . . . . . 11 4263 ∈ ℝ
274 dpcl 29899 . . . . . . . . . . 11 ((1 ∈ ℕ04263 ∈ ℝ) → (1.4263) ∈ ℝ)
27557, 273, 274mp2an 710 . . . . . . . . . 10 (1.4263) ∈ ℝ
276275a1i 11 . . . . . . . . 9 (𝜑 → (1.4263) ∈ ℝ)
277276, 127remulcld 10254 . . . . . . . 8 (𝜑 → ((1.4263) · (√‘𝑁)) ∈ ℝ)
278113, 55pm3.2i 470 . . . . . . . . . . . . . . . . . 18 (8 ∈ ℝ ∧ 3 ∈ ℝ)
279 dp2cl 29888 . . . . . . . . . . . . . . . . . 18 ((8 ∈ ℝ ∧ 3 ∈ ℝ) → 83 ∈ ℝ)
280278, 279ax-mp 5 . . . . . . . . . . . . . . . . 17 83 ∈ ℝ
281113, 280pm3.2i 470 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 83 ∈ ℝ)
282 dp2cl 29888 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 83 ∈ ℝ) → 883 ∈ ℝ)
283281, 282ax-mp 5 . . . . . . . . . . . . . . 15 883 ∈ ℝ
28455, 283pm3.2i 470 . . . . . . . . . . . . . 14 (3 ∈ ℝ ∧ 883 ∈ ℝ)
285 dp2cl 29888 . . . . . . . . . . . . . 14 ((3 ∈ ℝ ∧ 883 ∈ ℝ) → 3883 ∈ ℝ)
286284, 285ax-mp 5 . . . . . . . . . . . . 13 3883 ∈ ℝ
287134, 286pm3.2i 470 . . . . . . . . . . . 12 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
288 dp2cl 29888 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) → 03883 ∈ ℝ)
289287, 288ax-mp 5 . . . . . . . . . . 11 03883 ∈ ℝ
290 dpcl 29899 . . . . . . . . . . 11 ((1 ∈ ℕ003883 ∈ ℝ) → (1.03883) ∈ ℝ)
29157, 289, 290mp2an 710 . . . . . . . . . 10 (1.03883) ∈ ℝ
292291a1i 11 . . . . . . . . 9 (𝜑 → (1.03883) ∈ ℝ)
293292, 125remulcld 10254 . . . . . . . 8 (𝜑 → ((1.03883) · 𝑁) ∈ ℝ)
294277, 293remulcld 10254 . . . . . . 7 (𝜑 → (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)) ∈ ℝ)
295124, 294remulcld 10254 . . . . . 6 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) ∈ ℝ)
29683, 295remulcld 10254 . . . . 5 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) ∈ ℝ)
29756, 296remulcld 10254 . . . 4 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) ∈ ℝ)
298 vmage0 25038 . . . . . . . . . . 11 (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
299244, 298syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
300236, 245, 299fsumge0 14718 . . . . . . . . 9 (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
3011, 210hgt750lemd 31027 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1.4263) · (√‘𝑁)))
302 fzfid 12958 . . . . . . . . . 10 (𝜑 → (1...𝑁) ∈ Fin)
30310a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
304239sselda 3736 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
305303, 304ffvelrnd 6515 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
306 vmage0 25038 . . . . . . . . . . 11 (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
307304, 306syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
308302, 305, 307fsumge0 14718 . . . . . . . . 9 (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
3091hgt750lemc 31026 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1.03883) · 𝑁))
310246, 277, 252, 293, 300, 301, 308, 309ltmul12ad 11149 . . . . . . . 8 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))
311253, 294, 310ltled 10369 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))
312157a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
313 1lt2 11378 . . . . . . . . . . 11 1 < 2
314313a1i 11 . . . . . . . . . 10 (𝜑 → 1 < 2)
315312, 179, 125, 314, 211ltletrd 10381 . . . . . . . . 9 (𝜑 → 1 < 𝑁)
316125, 315rplogcld 24566 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ+)
317253, 294, 316lemul2d 12101 . . . . . . 7 (𝜑 → ((Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)) ↔ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))))
318311, 317mpbid 222 . . . . . 6 (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))
319254, 295, 217lemul2d 12101 . . . . . 6 (𝜑 → (((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) ↔ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))))
320318, 319mpbid 222 . . . . 5 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))))
321255, 296, 261lemul2d 12101 . . . . 5 (𝜑 → (((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) ↔ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))))))
322320, 321mpbid 222 . . . 4 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))))
323154resqcli 13135 . . . . . . . . . 10 ((1.079955)↑2) ∈ ℝ
324323, 165remulcli 10238 . . . . . . . . 9 (((1.079955)↑2) · (1.414)) ∈ ℝ
325275, 291remulcli 10238 . . . . . . . . 9 ((1.4263) · (1.03883)) ∈ ℝ
326324, 325remulcli 10238 . . . . . . . 8 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) ∈ ℝ
32755, 326remulcli 10238 . . . . . . 7 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ∈ ℝ
328 hgt750lem2 31031 . . . . . . 7 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (7.348)
329327, 121, 328ltleii 10344 . . . . . 6 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ≤ (7.348)
330327a1i 11 . . . . . . 7 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ∈ ℝ)
331316, 128rpdivcld 12074 . . . . . . . 8 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ+)
332123, 215rpexpcld 13218 . . . . . . . 8 (𝜑 → (𝑁↑2) ∈ ℝ+)
333331, 332rpmulcld 12073 . . . . . . 7 (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ+)
334330, 122, 333lemul1d 12100 . . . . . 6 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ≤ (7.348) ↔ ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7.348) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))))
335329, 334mpbii 223 . . . . 5 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7.348) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
336276recnd 10252 . . . . . . . . . . . . . 14 (𝜑 → (1.4263) ∈ ℂ)
337127recnd 10252 . . . . . . . . . . . . . 14 (𝜑 → (√‘𝑁) ∈ ℂ)
338292recnd 10252 . . . . . . . . . . . . . 14 (𝜑 → (1.03883) ∈ ℂ)
339125recnd 10252 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
340336, 337, 338, 339mul4d 10432 . . . . . . . . . . . . 13 (𝜑 → (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)) = (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)))
341340oveq2d 6821 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) = ((log‘𝑁) · (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁))))
342124recnd 10252 . . . . . . . . . . . . 13 (𝜑 → (log‘𝑁) ∈ ℂ)
343336, 338mulcld 10244 . . . . . . . . . . . . . 14 (𝜑 → ((1.4263) · (1.03883)) ∈ ℂ)
344337, 339mulcld 10244 . . . . . . . . . . . . . 14 (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
345343, 344mulcld 10244 . . . . . . . . . . . . 13 (𝜑 → (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
346342, 345mulcomd 10245 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑁) · (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁))) = ((((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
347341, 346eqtrd 2786 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) = ((((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
348343, 344, 342mulassd 10247 . . . . . . . . . . 11 (𝜑 → ((((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)) = (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
349347, 348eqtrd 2786 . . . . . . . . . 10 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) = (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
350349oveq2d 6821 . . . . . . . . 9 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) = ((((1.079955)↑2) · (1.414)) · (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
35183recnd 10252 . . . . . . . . . 10 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℂ)
352344, 342mulcld 10244 . . . . . . . . . 10 (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
353351, 343, 352mulassd 10247 . . . . . . . . 9 (𝜑 → (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((((1.079955)↑2) · (1.414)) · (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
354350, 353eqtr4d 2789 . . . . . . . 8 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) = (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
355354oveq2d 6821 . . . . . . 7 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) = (3 · (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
35656recnd 10252 . . . . . . . 8 (𝜑 → 3 ∈ ℂ)
357351, 343mulcld 10244 . . . . . . . 8 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) ∈ ℂ)
358356, 357, 352mulassd 10247 . . . . . . 7 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = (3 · (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
359355, 358eqtr4d 2789 . . . . . 6 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) = ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
360132recnd 10252 . . . . . . . . 9 (𝜑 → (𝑁↑2) ∈ ℂ)
361342, 337, 360, 129div32d 11008 . . . . . . . 8 (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
362360, 337, 129divcld 10985 . . . . . . . . 9 (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
363342, 362mulcomd 10245 . . . . . . . 8 (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
364339sqvald 13191 . . . . . . . . . . . 12 (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
365364oveq1d 6820 . . . . . . . . . . 11 (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
366339, 339, 337, 129divassd 11020 . . . . . . . . . . 11 (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
367 divsqrtid 30973 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ+ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
368123, 367syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
369368oveq2d 6821 . . . . . . . . . . 11 (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
370365, 366, 3693eqtrd 2790 . . . . . . . . . 10 (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
371339, 337mulcomd 10245 . . . . . . . . . 10 (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
372370, 371eqtrd 2786 . . . . . . . . 9 (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
373372oveq1d 6820 . . . . . . . 8 (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
374361, 363, 3733eqtrrd 2791 . . . . . . 7 (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
375374oveq2d 6821 . . . . . 6 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
376359, 375eqtrd 2786 . . . . 5 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) = ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
377122recnd 10252 . . . . . 6 (𝜑 → (7.348) ∈ ℂ)
378130recnd 10252 . . . . . 6 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
379377, 378, 360mulassd 10247 . . . . 5 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7.348) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
380335, 376, 3793brtr4d 4828 . . . 4 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
381256, 297, 133, 322, 380letrd 10378 . . 3 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
382111, 256, 133, 263, 381letrd 10378 . 2 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
38354, 111, 133, 229, 382letrd 10378 1 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1072   = wceq 1624  wcel 2131  {crab 3046  cdif 3704  cun 3705  cin 3706  wss 3707  ifcif 4222  {csn 4313  {cpr 4315  {ctp 4317   class class class wbr 4796  cmpt 4873   I cid 5165  cres 5260  ccom 5262  wf 6037  cfv 6041  (class class class)co 6805  Fincfn 8113  cc 10118  cr 10119  0cc0 10120  1c1 10121   · cmul 10125  +∞cpnf 10255   < clt 10258  cle 10259   / cdiv 10868  cn 11204  2c2 11254  3c3 11255  4c4 11256  5c5 11257  6c6 11258  7c7 11259  8c8 11260  9c9 11261  0cn0 11476  cz 11561  cdc 11677  +crp 12017  [,)cico 12362  ...cfz 12511  ..^cfzo 12651  cexp 13046  csqrt 14164  Σcsu 14607  cdvds 15174  cprime 15579  pmTrspcpmtr 18053  logclog 24492  Λcvma 25009  ψcchp 25010  cdp2 29878  .cdp 29896  reprcrepr 30987
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-reg 8654  ax-inf2 8703  ax-ac2 9469  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-ros335 31024  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-r1 8792  df-rank 8793  df-card 8947  df-ac 9121  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-prod 14827  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-pmtr 18054  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  df-repr 30988
This theorem is referenced by:  tgoldbachgtde  31039
  Copyright terms: Public domain W3C validator