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 32350
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 12150 . . . . 5 (𝜑𝑁 ∈ ℕ0)
3 3nn0 12108 . . . . . 6 3 ∈ ℕ0
43a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ0)
5 ssidd 3924 . . . . 5 (𝜑 → ℕ ⊆ ℕ)
62, 4, 5reprfi2 32315 . . . 4 (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
7 diffi 8906 . . . 4 ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
86, 7syl 17 . . 3 (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
9 vmaf 26001 . . . . . . 7 Λ:ℕ⟶ℝ
109a1i 11 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → Λ:ℕ⟶ℝ)
11 ssidd 3924 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆ ℕ)
121nnzd 12281 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
1312adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ)
143a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈ ℕ0)
15 simpr 488 . . . . . . . . 9 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))
1615eldifad 3878 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
1711, 13, 14, 16reprf 32304 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ)
18 c0ex 10827 . . . . . . . . . 10 0 ∈ V
1918tpid1 4684 . . . . . . . . 9 0 ∈ {0, 1, 2}
20 fzo0to3tp 13328 . . . . . . . . 9 (0..^3) = {0, 1, 2}
2119, 20eleqtrri 2837 . . . . . . . 8 0 ∈ (0..^3)
2221a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈ (0..^3))
2317, 22ffvelrnd 6905 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ)
2410, 23ffvelrnd 6905 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘0)) ∈ ℝ)
25 rge0ssre 13044 . . . . . 6 (0[,)+∞) ⊆ ℝ
26 hgt750leme.h . . . . . . . 8 (𝜑𝐻:ℕ⟶(0[,)+∞))
2726adantr 484 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞))
2827, 23ffvelrnd 6905 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ (0[,)+∞))
2925, 28sseldi 3899 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ)
3024, 29remulcld 10863 . . . 4 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
31 1ex 10829 . . . . . . . . . . 11 1 ∈ V
3231tpid2 4686 . . . . . . . . . 10 1 ∈ {0, 1, 2}
3332, 20eleqtrri 2837 . . . . . . . . 9 1 ∈ (0..^3)
3433a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈ (0..^3))
3517, 34ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ)
3610, 35ffvelrnd 6905 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘1)) ∈ ℝ)
37 hgt750leme.k . . . . . . . . 9 (𝜑𝐾:ℕ⟶(0[,)+∞))
3837adantr 484 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞))
3938, 35ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ (0[,)+∞))
4025, 39sseldi 3899 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ)
4136, 40remulcld 10863 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
42 2ex 11907 . . . . . . . . . . 11 2 ∈ V
4342tpid3 4689 . . . . . . . . . 10 2 ∈ {0, 1, 2}
4443, 20eleqtrri 2837 . . . . . . . . 9 2 ∈ (0..^3)
4544a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈ (0..^3))
4617, 45ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ)
4710, 46ffvelrnd 6905 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (Λ‘(𝑛‘2)) ∈ ℝ)
4838, 46ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ (0[,)+∞))
4925, 48sseldi 3899 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ)
5047, 49remulcld 10863 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
5141, 50remulcld 10863 . . . 4 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
5230, 51remulcld 10863 . . 3 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
538, 52fsumrecl 15298 . 2 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
54 3re 11910 . . . 4 3 ∈ ℝ
5554a1i 11 . . 3 (𝜑 → 3 ∈ ℝ)
56 1nn0 12106 . . . . . . . . 9 1 ∈ ℕ0
57 0nn0 12105 . . . . . . . . . 10 0 ∈ ℕ0
58 7nn0 12112 . . . . . . . . . . 11 7 ∈ ℕ0
59 9nn0 12114 . . . . . . . . . . . 12 9 ∈ ℕ0
60 5nn0 12110 . . . . . . . . . . . . . 14 5 ∈ ℕ0
61 5nn 11916 . . . . . . . . . . . . . . 15 5 ∈ ℕ
62 nnrp 12597 . . . . . . . . . . . . . . 15 (5 ∈ ℕ → 5 ∈ ℝ+)
6361, 62ax-mp 5 . . . . . . . . . . . . . 14 5 ∈ ℝ+
6460, 63rpdp2cl 30876 . . . . . . . . . . . . 13 55 ∈ ℝ+
6559, 64rpdp2cl 30876 . . . . . . . . . . . 12 955 ∈ ℝ+
6659, 65rpdp2cl 30876 . . . . . . . . . . 11 9955 ∈ ℝ+
6758, 66rpdp2cl 30876 . . . . . . . . . 10 79955 ∈ ℝ+
6857, 67rpdp2cl 30876 . . . . . . . . 9 079955 ∈ ℝ+
6956, 68rpdpcl 30897 . . . . . . . 8 (1.079955) ∈ ℝ+
7069a1i 11 . . . . . . 7 (𝜑 → (1.079955) ∈ ℝ+)
7170rpred 12628 . . . . . 6 (𝜑 → (1.079955) ∈ ℝ)
7271resqcld 13817 . . . . 5 (𝜑 → ((1.079955)↑2) ∈ ℝ)
73 4nn0 12109 . . . . . . . . 9 4 ∈ ℕ0
74 4nn 11913 . . . . . . . . . . 11 4 ∈ ℕ
75 nnrp 12597 . . . . . . . . . . 11 (4 ∈ ℕ → 4 ∈ ℝ+)
7674, 75ax-mp 5 . . . . . . . . . 10 4 ∈ ℝ+
7756, 76rpdp2cl 30876 . . . . . . . . 9 14 ∈ ℝ+
7873, 77rpdp2cl 30876 . . . . . . . 8 414 ∈ ℝ+
7956, 78rpdpcl 30897 . . . . . . 7 (1.414) ∈ ℝ+
8079a1i 11 . . . . . 6 (𝜑 → (1.414) ∈ ℝ+)
8180rpred 12628 . . . . 5 (𝜑 → (1.414) ∈ ℝ)
8272, 81remulcld 10863 . . . 4 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℝ)
83 fveq1 6716 . . . . . . . . . 10 (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0))
8483eleq1d 2822 . . . . . . . . 9 (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
8584notbid 321 . . . . . . . 8 (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)))
8685cbvrabv 3402 . . . . . . 7 {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} = {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘0) ∈ (𝑂 ∩ ℙ)}
8786ssrab3 3995 . . . . . 6 {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)
88 ssfi 8851 . . . . . 6 (((ℕ(repr‘3)𝑁) ∈ Fin ∧ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁)) → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
896, 87, 88sylancl 589 . . . . 5 (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈ Fin)
909a1i 11 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → Λ:ℕ⟶ℝ)
91 ssidd 3924 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ ⊆ ℕ)
9212adantr 484 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈ ℤ)
933a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 3 ∈ ℕ0)
9487a1i 11 . . . . . . . . . 10 (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆ (ℕ(repr‘3)𝑁))
9594sselda 3901 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
9691, 92, 93, 95reprf 32304 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ)
9721a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0 ∈ (0..^3))
9896, 97ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈ ℕ)
9990, 98ffvelrnd 6905 . . . . . 6 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘0)) ∈ ℝ)
10033a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1 ∈ (0..^3))
10196, 100ffvelrnd 6905 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈ ℕ)
10290, 101ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘1)) ∈ ℝ)
10344a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2 ∈ (0..^3))
10496, 103ffvelrnd 6905 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈ ℕ)
10590, 104ffvelrnd 6905 . . . . . . 7 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (Λ‘(𝑛‘2)) ∈ ℝ)
106102, 105remulcld 10863 . . . . . 6 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
10799, 106remulcld 10863 . . . . 5 ((𝜑𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
10889, 107fsumrecl 15298 . . . 4 (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
10982, 108remulcld 10863 . . 3 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
11055, 109remulcld 10863 . 2 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
111 4re 11914 . . . . . . . . . 10 4 ∈ ℝ
112 8re 11926 . . . . . . . . . 10 8 ∈ ℝ
113111, 112pm3.2i 474 . . . . . . . . 9 (4 ∈ ℝ ∧ 8 ∈ ℝ)
114 dp2cl 30874 . . . . . . . . 9 ((4 ∈ ℝ ∧ 8 ∈ ℝ) → 48 ∈ ℝ)
115113, 114ax-mp 5 . . . . . . . 8 48 ∈ ℝ
11654, 115pm3.2i 474 . . . . . . 7 (3 ∈ ℝ ∧ 48 ∈ ℝ)
117 dp2cl 30874 . . . . . . 7 ((3 ∈ ℝ ∧ 48 ∈ ℝ) → 348 ∈ ℝ)
118116, 117ax-mp 5 . . . . . 6 348 ∈ ℝ
119 dpcl 30885 . . . . . 6 ((7 ∈ ℕ0348 ∈ ℝ) → (7.348) ∈ ℝ)
12058, 118, 119mp2an 692 . . . . 5 (7.348) ∈ ℝ
121120a1i 11 . . . 4 (𝜑 → (7.348) ∈ ℝ)
1221nnrpd 12626 . . . . . 6 (𝜑𝑁 ∈ ℝ+)
123122relogcld 25511 . . . . 5 (𝜑 → (log‘𝑁) ∈ ℝ)
1241nnred 11845 . . . . . 6 (𝜑𝑁 ∈ ℝ)
125122rpge0d 12632 . . . . . 6 (𝜑 → 0 ≤ 𝑁)
126124, 125resqrtcld 14981 . . . . 5 (𝜑 → (√‘𝑁) ∈ ℝ)
127122rpsqrtcld 14975 . . . . . 6 (𝜑 → (√‘𝑁) ∈ ℝ+)
128127rpne0d 12633 . . . . 5 (𝜑 → (√‘𝑁) ≠ 0)
129123, 126, 128redivcld 11660 . . . 4 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
130121, 129remulcld 10863 . . 3 (𝜑 → ((7.348) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
131124resqcld 13817 . . 3 (𝜑 → (𝑁↑2) ∈ ℝ)
132130, 131remulcld 10863 . 2 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
133 0re 10835 . . . . . . . . . . 11 0 ∈ ℝ
134 7re 11923 . . . . . . . . . . . . 13 7 ∈ ℝ
135 9re 11929 . . . . . . . . . . . . . . 15 9 ∈ ℝ
136 5re 11917 . . . . . . . . . . . . . . . . . . 19 5 ∈ ℝ
137136, 136pm3.2i 474 . . . . . . . . . . . . . . . . . 18 (5 ∈ ℝ ∧ 5 ∈ ℝ)
138 dp2cl 30874 . . . . . . . . . . . . . . . . . 18 ((5 ∈ ℝ ∧ 5 ∈ ℝ) → 55 ∈ ℝ)
139137, 138ax-mp 5 . . . . . . . . . . . . . . . . 17 55 ∈ ℝ
140135, 139pm3.2i 474 . . . . . . . . . . . . . . . 16 (9 ∈ ℝ ∧ 55 ∈ ℝ)
141 dp2cl 30874 . . . . . . . . . . . . . . . 16 ((9 ∈ ℝ ∧ 55 ∈ ℝ) → 955 ∈ ℝ)
142140, 141ax-mp 5 . . . . . . . . . . . . . . 15 955 ∈ ℝ
143135, 142pm3.2i 474 . . . . . . . . . . . . . 14 (9 ∈ ℝ ∧ 955 ∈ ℝ)
144 dp2cl 30874 . . . . . . . . . . . . . 14 ((9 ∈ ℝ ∧ 955 ∈ ℝ) → 9955 ∈ ℝ)
145143, 144ax-mp 5 . . . . . . . . . . . . 13 9955 ∈ ℝ
146134, 145pm3.2i 474 . . . . . . . . . . . 12 (7 ∈ ℝ ∧ 9955 ∈ ℝ)
147 dp2cl 30874 . . . . . . . . . . . 12 ((7 ∈ ℝ ∧ 9955 ∈ ℝ) → 79955 ∈ ℝ)
148146, 147ax-mp 5 . . . . . . . . . . 11 79955 ∈ ℝ
149133, 148pm3.2i 474 . . . . . . . . . 10 (0 ∈ ℝ ∧ 79955 ∈ ℝ)
150 dp2cl 30874 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 79955 ∈ ℝ) → 079955 ∈ ℝ)
151149, 150ax-mp 5 . . . . . . . . 9 079955 ∈ ℝ
152 dpcl 30885 . . . . . . . . 9 ((1 ∈ ℕ0079955 ∈ ℝ) → (1.079955) ∈ ℝ)
15356, 151, 152mp2an 692 . . . . . . . 8 (1.079955) ∈ ℝ
154153a1i 11 . . . . . . 7 (𝜑 → (1.079955) ∈ ℝ)
155154resqcld 13817 . . . . . 6 (𝜑 → ((1.079955)↑2) ∈ ℝ)
156 1re 10833 . . . . . . . . . . . 12 1 ∈ ℝ
157156, 111pm3.2i 474 . . . . . . . . . . 11 (1 ∈ ℝ ∧ 4 ∈ ℝ)
158 dp2cl 30874 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ 4 ∈ ℝ) → 14 ∈ ℝ)
159157, 158ax-mp 5 . . . . . . . . . 10 14 ∈ ℝ
160111, 159pm3.2i 474 . . . . . . . . 9 (4 ∈ ℝ ∧ 14 ∈ ℝ)
161 dp2cl 30874 . . . . . . . . 9 ((4 ∈ ℝ ∧ 14 ∈ ℝ) → 414 ∈ ℝ)
162160, 161ax-mp 5 . . . . . . . 8 414 ∈ ℝ
163 dpcl 30885 . . . . . . . 8 ((1 ∈ ℕ0414 ∈ ℝ) → (1.414) ∈ ℝ)
16456, 162, 163mp2an 692 . . . . . . 7 (1.414) ∈ ℝ
165164a1i 11 . . . . . 6 (𝜑 → (1.414) ∈ ℝ)
166155, 165remulcld 10863 . . . . 5 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℝ)
16736, 47remulcld 10863 . . . . . . 7 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈ ℝ)
16824, 167remulcld 10863 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
1698, 168fsumrecl 15298 . . . . 5 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℝ)
170166, 169remulcld 10863 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
17155, 108remulcld 10863 . . . . 5 (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ∈ ℝ)
172166, 171remulcld 10863 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ∈ ℝ)
173 hgt750leme.1 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐾𝑚) ≤ (1.079955))
174 hgt750leme.2 . . . . 5 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ≤ (1.414))
1758, 154, 165, 26, 37, 23, 35, 46, 173, 174hgt750lemf 32345 . . . 4 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
176 hgt750leme.o . . . . . 6 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
177 2re 11904 . . . . . . . 8 2 ∈ ℝ
178177a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℝ)
179 10nn0 12311 . . . . . . . . . 10 10 ∈ ℕ0
180 2nn0 12107 . . . . . . . . . . 11 2 ∈ ℕ0
181180, 58deccl 12308 . . . . . . . . . 10 27 ∈ ℕ0
182179, 181nn0expcli 13661 . . . . . . . . 9 (10↑27) ∈ ℕ0
183182nn0rei 12101 . . . . . . . 8 (10↑27) ∈ ℝ
184183a1i 11 . . . . . . 7 (𝜑 → (10↑27) ∈ ℝ)
185179numexp1 16630 . . . . . . . . . 10 (10↑1) = 10
186179nn0rei 12101 . . . . . . . . . 10 10 ∈ ℝ
187185, 186eqeltri 2834 . . . . . . . . 9 (10↑1) ∈ ℝ
188187a1i 11 . . . . . . . 8 (𝜑 → (10↑1) ∈ ℝ)
189 1nn 11841 . . . . . . . . . . 11 1 ∈ ℕ
190 2lt9 12035 . . . . . . . . . . . 12 2 < 9
191177, 135, 190ltleii 10955 . . . . . . . . . . 11 2 ≤ 9
192189, 57, 180, 191declei 12329 . . . . . . . . . 10 2 ≤ 10
193192, 185breqtrri 5080 . . . . . . . . 9 2 ≤ (10↑1)
194193a1i 11 . . . . . . . 8 (𝜑 → 2 ≤ (10↑1))
195 1z 12207 . . . . . . . . . . . 12 1 ∈ ℤ
196181nn0zi 12202 . . . . . . . . . . . 12 27 ∈ ℤ
197186, 195, 1963pm3.2i 1341 . . . . . . . . . . 11 (10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ)
198 1lt10 12432 . . . . . . . . . . 11 1 < 10
199197, 198pm3.2i 474 . . . . . . . . . 10 ((10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ) ∧ 1 < 10)
200 2nn 11903 . . . . . . . . . . 11 2 ∈ ℕ
201 1lt9 12036 . . . . . . . . . . . 12 1 < 9
202156, 135, 201ltleii 10955 . . . . . . . . . . 11 1 ≤ 9
203200, 58, 56, 202declei 12329 . . . . . . . . . 10 1 ≤ 27
204 leexp2 13741 . . . . . . . . . . 11 (((10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ) ∧ 1 < 10) → (1 ≤ 27 ↔ (10↑1) ≤ (10↑27)))
205204biimpa 480 . . . . . . . . . 10 ((((10 ∈ ℝ ∧ 1 ∈ ℤ ∧ 27 ∈ ℤ) ∧ 1 < 10) ∧ 1 ≤ 27) → (10↑1) ≤ (10↑27))
206199, 203, 205mp2an 692 . . . . . . . . 9 (10↑1) ≤ (10↑27)
207206a1i 11 . . . . . . . 8 (𝜑 → (10↑1) ≤ (10↑27))
208178, 188, 184, 194, 207letrd 10989 . . . . . . 7 (𝜑 → 2 ≤ (10↑27))
209 hgt750leme.0 . . . . . . 7 (𝜑 → (10↑27) ≤ 𝑁)
210178, 184, 124, 208, 209letrd 10989 . . . . . 6 (𝜑 → 2 ≤ 𝑁)
211 eqid 2737 . . . . . 6 (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0})))) = (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)), ((pmTrsp‘(0..^3))‘{𝑎, 0}))))
212176, 1, 210, 86, 211hgt750lema 32349 . . . . 5 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))))
213 2z 12209 . . . . . . . . 9 2 ∈ ℤ
214213a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℤ)
21570, 214rpexpcld 13814 . . . . . . 7 (𝜑 → ((1.079955)↑2) ∈ ℝ+)
216215, 80rpmulcld 12644 . . . . . 6 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℝ+)
217169, 171, 216lemul2d 12672 . . . . 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))))))))
218212, 217mpbid 235 . . . 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)))))))
21953, 170, 172, 175, 218letrd 10989 . . 3 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
220154recnd 10861 . . . . . 6 (𝜑 → (1.079955) ∈ ℂ)
221220sqcld 13714 . . . . 5 (𝜑 → ((1.079955)↑2) ∈ ℂ)
222165recnd 10861 . . . . 5 (𝜑 → (1.414) ∈ ℂ)
223221, 222mulcld 10853 . . . 4 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℂ)
224 3cn 11911 . . . . 5 3 ∈ ℂ
225224a1i 11 . . . 4 (𝜑 → 3 ∈ ℂ)
226108recnd 10861 . . . 4 (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈ ℂ)
227223, 225, 226mul12d 11041 . . 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)))))))
228219, 227breqtrd 5079 . 2 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))))
229 fzfi 13545 . . . . . . . . . . 11 (1...𝑁) ∈ Fin
230 diffi 8906 . . . . . . . . . . 11 ((1...𝑁) ∈ Fin → ((1...𝑁) ∖ ℙ) ∈ Fin)
231229, 230ax-mp 5 . . . . . . . . . 10 ((1...𝑁) ∖ ℙ) ∈ Fin
232 snfi 8721 . . . . . . . . . 10 {2} ∈ Fin
233 unfi 8850 . . . . . . . . . 10 ((((1...𝑁) ∖ ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
234231, 232, 233mp2an 692 . . . . . . . . 9 (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin
235234a1i 11 . . . . . . . 8 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈ Fin)
2369a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → Λ:ℕ⟶ℝ)
237 fz1ssnn 13143 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℕ
238237a1i 11 . . . . . . . . . . . 12 (𝜑 → (1...𝑁) ⊆ ℕ)
239238ssdifssd 4057 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ ℙ) ⊆ ℕ)
240200a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℕ)
241240snssd 4722 . . . . . . . . . . 11 (𝜑 → {2} ⊆ ℕ)
242239, 241unssd 4100 . . . . . . . . . 10 (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆ ℕ)
243242sselda 3901 . . . . . . . . 9 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈ ℕ)
244236, 243ffvelrnd 6905 . . . . . . . 8 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → (Λ‘𝑖) ∈ ℝ)
245235, 244fsumrecl 15298 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) ∈ ℝ)
246 chpvalz 32320 . . . . . . . . 9 (𝑁 ∈ ℤ → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
24712, 246syl 17 . . . . . . . 8 (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
248 chpf 26005 . . . . . . . . . 10 ψ:ℝ⟶ℝ
249248a1i 11 . . . . . . . . 9 (𝜑 → ψ:ℝ⟶ℝ)
250249, 124ffvelrnd 6905 . . . . . . . 8 (𝜑 → (ψ‘𝑁) ∈ ℝ)
251247, 250eqeltrrd 2839 . . . . . . 7 (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ)
252245, 251remulcld 10863 . . . . . 6 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ∈ ℝ)
253123, 252remulcld 10863 . . . . 5 (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ∈ ℝ)
25482, 253remulcld 10863 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ)
25555, 254remulcld 10863 . . 3 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ)
256176, 1, 210, 86hgt750lemb 32348 . . . . 5 (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))
257108, 253, 216lemul2d 12672 . . . . 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...𝑁)(Λ‘𝑗))))))
258256, 257mpbid 235 . . . 4 (𝜑 → ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))
259 3rp 12592 . . . . . 6 3 ∈ ℝ+
260259a1i 11 . . . . 5 (𝜑 → 3 ∈ ℝ+)
261109, 254, 260lemul2d 12672 . . . 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...𝑁)(Λ‘𝑗)))))))
262258, 261mpbid 235 . . 3 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))))
263 6re 11920 . . . . . . . . . . . . . . . . 17 6 ∈ ℝ
264263, 54pm3.2i 474 . . . . . . . . . . . . . . . 16 (6 ∈ ℝ ∧ 3 ∈ ℝ)
265 dp2cl 30874 . . . . . . . . . . . . . . . 16 ((6 ∈ ℝ ∧ 3 ∈ ℝ) → 63 ∈ ℝ)
266264, 265ax-mp 5 . . . . . . . . . . . . . . 15 63 ∈ ℝ
267177, 266pm3.2i 474 . . . . . . . . . . . . . 14 (2 ∈ ℝ ∧ 63 ∈ ℝ)
268 dp2cl 30874 . . . . . . . . . . . . . 14 ((2 ∈ ℝ ∧ 63 ∈ ℝ) → 263 ∈ ℝ)
269267, 268ax-mp 5 . . . . . . . . . . . . 13 263 ∈ ℝ
270111, 269pm3.2i 474 . . . . . . . . . . . 12 (4 ∈ ℝ ∧ 263 ∈ ℝ)
271 dp2cl 30874 . . . . . . . . . . . 12 ((4 ∈ ℝ ∧ 263 ∈ ℝ) → 4263 ∈ ℝ)
272270, 271ax-mp 5 . . . . . . . . . . 11 4263 ∈ ℝ
273 dpcl 30885 . . . . . . . . . . 11 ((1 ∈ ℕ04263 ∈ ℝ) → (1.4263) ∈ ℝ)
27456, 272, 273mp2an 692 . . . . . . . . . 10 (1.4263) ∈ ℝ
275274a1i 11 . . . . . . . . 9 (𝜑 → (1.4263) ∈ ℝ)
276275, 126remulcld 10863 . . . . . . . 8 (𝜑 → ((1.4263) · (√‘𝑁)) ∈ ℝ)
277112, 54pm3.2i 474 . . . . . . . . . . . . . . . . . 18 (8 ∈ ℝ ∧ 3 ∈ ℝ)
278 dp2cl 30874 . . . . . . . . . . . . . . . . . 18 ((8 ∈ ℝ ∧ 3 ∈ ℝ) → 83 ∈ ℝ)
279277, 278ax-mp 5 . . . . . . . . . . . . . . . . 17 83 ∈ ℝ
280112, 279pm3.2i 474 . . . . . . . . . . . . . . . 16 (8 ∈ ℝ ∧ 83 ∈ ℝ)
281 dp2cl 30874 . . . . . . . . . . . . . . . 16 ((8 ∈ ℝ ∧ 83 ∈ ℝ) → 883 ∈ ℝ)
282280, 281ax-mp 5 . . . . . . . . . . . . . . 15 883 ∈ ℝ
28354, 282pm3.2i 474 . . . . . . . . . . . . . 14 (3 ∈ ℝ ∧ 883 ∈ ℝ)
284 dp2cl 30874 . . . . . . . . . . . . . 14 ((3 ∈ ℝ ∧ 883 ∈ ℝ) → 3883 ∈ ℝ)
285283, 284ax-mp 5 . . . . . . . . . . . . 13 3883 ∈ ℝ
286133, 285pm3.2i 474 . . . . . . . . . . . 12 (0 ∈ ℝ ∧ 3883 ∈ ℝ)
287 dp2cl 30874 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ 3883 ∈ ℝ) → 03883 ∈ ℝ)
288286, 287ax-mp 5 . . . . . . . . . . 11 03883 ∈ ℝ
289 dpcl 30885 . . . . . . . . . . 11 ((1 ∈ ℕ003883 ∈ ℝ) → (1.03883) ∈ ℝ)
29056, 288, 289mp2an 692 . . . . . . . . . 10 (1.03883) ∈ ℝ
291290a1i 11 . . . . . . . . 9 (𝜑 → (1.03883) ∈ ℝ)
292291, 124remulcld 10863 . . . . . . . 8 (𝜑 → ((1.03883) · 𝑁) ∈ ℝ)
293276, 292remulcld 10863 . . . . . . 7 (𝜑 → (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)) ∈ ℝ)
294123, 293remulcld 10863 . . . . . 6 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) ∈ ℝ)
29582, 294remulcld 10863 . . . . 5 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) ∈ ℝ)
29655, 295remulcld 10863 . . . 4 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) ∈ ℝ)
297 vmage0 26003 . . . . . . . . . . 11 (𝑖 ∈ ℕ → 0 ≤ (Λ‘𝑖))
298243, 297syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤ (Λ‘𝑖))
299235, 244, 298fsumge0 15359 . . . . . . . . 9 (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖))
3001, 209hgt750lemd 32340 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) < ((1.4263) · (√‘𝑁)))
301 fzfid 13546 . . . . . . . . . 10 (𝜑 → (1...𝑁) ∈ Fin)
3029a1i 11 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → Λ:ℕ⟶ℝ)
303238sselda 3901 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
304302, 303ffvelrnd 6905 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ)
305 vmage0 26003 . . . . . . . . . . 11 (𝑗 ∈ ℕ → 0 ≤ (Λ‘𝑗))
306303, 305syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗))
307301, 304, 306fsumge0 15359 . . . . . . . . 9 (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))
3081hgt750lemc 32339 . . . . . . . . 9 (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1.03883) · 𝑁))
309245, 276, 251, 292, 299, 300, 307, 308ltmul12ad 11773 . . . . . . . 8 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) < (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))
310252, 293, 309ltled 10980 . . . . . . 7 (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))
311156a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
312 1lt2 12001 . . . . . . . . . . 11 1 < 2
313312a1i 11 . . . . . . . . . 10 (𝜑 → 1 < 2)
314311, 178, 124, 313, 210ltletrd 10992 . . . . . . . . 9 (𝜑 → 1 < 𝑁)
315124, 314rplogcld 25517 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ+)
316252, 293, 315lemul2d 12672 . . . . . . 7 (𝜑 → ((Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) ≤ (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)) ↔ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))))
317310, 316mpbid 235 . . . . . 6 (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))
318253, 294, 216lemul2d 12672 . . . . . 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) · 𝑁))))))
319317, 318mpbid 235 . . . . 5 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))))
320254, 295, 260lemul2d 12672 . . . . 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) · 𝑁)))))))
321319, 320mpbid 235 . . . 4 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))))
322153resqcli 13755 . . . . . . . . . 10 ((1.079955)↑2) ∈ ℝ
323322, 164remulcli 10849 . . . . . . . . 9 (((1.079955)↑2) · (1.414)) ∈ ℝ
324274, 290remulcli 10849 . . . . . . . . 9 ((1.4263) · (1.03883)) ∈ ℝ
325323, 324remulcli 10849 . . . . . . . 8 ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) ∈ ℝ
32654, 325remulcli 10849 . . . . . . 7 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ∈ ℝ
327 hgt750lem2 32344 . . . . . . 7 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) < (7.348)
328326, 120, 327ltleii 10955 . . . . . 6 (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ≤ (7.348)
329326a1i 11 . . . . . . 7 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) ∈ ℝ)
330315, 127rpdivcld 12645 . . . . . . . 8 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ+)
331122, 214rpexpcld 13814 . . . . . . . 8 (𝜑 → (𝑁↑2) ∈ ℝ+)
332330, 331rpmulcld 12644 . . . . . . 7 (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈ ℝ+)
333329, 121, 332lemul1d 12671 . . . . . 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)))))
334328, 333mpbii 236 . . . . 5 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7.348) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
335275recnd 10861 . . . . . . . . . . . . . 14 (𝜑 → (1.4263) ∈ ℂ)
336126recnd 10861 . . . . . . . . . . . . . 14 (𝜑 → (√‘𝑁) ∈ ℂ)
337291recnd 10861 . . . . . . . . . . . . . 14 (𝜑 → (1.03883) ∈ ℂ)
338124recnd 10861 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℂ)
339335, 336, 337, 338mul4d 11044 . . . . . . . . . . . . 13 (𝜑 → (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)) = (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)))
340339oveq2d 7229 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) = ((log‘𝑁) · (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁))))
341123recnd 10861 . . . . . . . . . . . . 13 (𝜑 → (log‘𝑁) ∈ ℂ)
342335, 337mulcld 10853 . . . . . . . . . . . . . 14 (𝜑 → ((1.4263) · (1.03883)) ∈ ℂ)
343336, 338mulcld 10853 . . . . . . . . . . . . . 14 (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ)
344342, 343mulcld 10853 . . . . . . . . . . . . 13 (𝜑 → (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) ∈ ℂ)
345341, 344mulcomd 10854 . . . . . . . . . . . 12 (𝜑 → ((log‘𝑁) · (((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁))) = ((((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
346340, 345eqtrd 2777 . . . . . . . . . . 11 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) = ((((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)))
347342, 343, 341mulassd 10856 . . . . . . . . . . 11 (𝜑 → ((((1.4263) · (1.03883)) · ((√‘𝑁) · 𝑁)) · (log‘𝑁)) = (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
348346, 347eqtrd 2777 . . . . . . . . . 10 (𝜑 → ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))) = (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
349348oveq2d 7229 . . . . . . . . 9 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) = ((((1.079955)↑2) · (1.414)) · (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
35082recnd 10861 . . . . . . . . . 10 (𝜑 → (((1.079955)↑2) · (1.414)) ∈ ℂ)
351343, 341mulcld 10853 . . . . . . . . . 10 (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ)
352350, 342, 351mulassd 10856 . . . . . . . . 9 (𝜑 → (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((((1.079955)↑2) · (1.414)) · (((1.4263) · (1.03883)) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
353349, 352eqtr4d 2780 . . . . . . . 8 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁)))) = (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
354353oveq2d 7229 . . . . . . 7 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) = (3 · (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
35555recnd 10861 . . . . . . . 8 (𝜑 → 3 ∈ ℂ)
356350, 342mulcld 10853 . . . . . . . 8 (𝜑 → ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) ∈ ℂ)
357355, 356, 351mulassd 10856 . . . . . . 7 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = (3 · (((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))))
358354, 357eqtr4d 2780 . . . . . 6 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) = ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))))
359131recnd 10861 . . . . . . . . 9 (𝜑 → (𝑁↑2) ∈ ℂ)
360341, 336, 359, 128div32d 11631 . . . . . . . 8 (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))))
361359, 336, 128divcld 11608 . . . . . . . . 9 (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ)
362341, 361mulcomd 10854 . . . . . . . 8 (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)))
363338sqvald 13713 . . . . . . . . . . . 12 (𝜑 → (𝑁↑2) = (𝑁 · 𝑁))
364363oveq1d 7228 . . . . . . . . . . 11 (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁)))
365338, 338, 336, 128divassd 11643 . . . . . . . . . . 11 (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁))))
366 divsqrtid 32286 . . . . . . . . . . . . 13 (𝑁 ∈ ℝ+ → (𝑁 / (√‘𝑁)) = (√‘𝑁))
367122, 366syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁))
368367oveq2d 7229 . . . . . . . . . . 11 (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁)))
369364, 365, 3683eqtrd 2781 . . . . . . . . . 10 (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁)))
370338, 336mulcomd 10854 . . . . . . . . . 10 (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁))
371369, 370eqtrd 2777 . . . . . . . . 9 (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁))
372371oveq1d 7228 . . . . . . . 8 (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁)))
373360, 362, 3723eqtrrd 2782 . . . . . . 7 (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))
374373oveq2d 7229 . . . . . 6 (𝜑 → ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
375358, 374eqtrd 2777 . . . . 5 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) = ((3 · ((((1.079955)↑2) · (1.414)) · ((1.4263) · (1.03883)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
376121recnd 10861 . . . . . 6 (𝜑 → (7.348) ∈ ℂ)
377129recnd 10861 . . . . . 6 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℂ)
378376, 377, 359mulassd 10856 . . . . 5 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) = ((7.348) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))))
379334, 375, 3783brtr4d 5085 . . . 4 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (((1.4263) · (√‘𝑁)) · ((1.03883) · 𝑁))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
380255, 296, 132, 321, 379letrd 10989 . . 3 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
381110, 255, 132, 262, 380letrd 10989 . 2 (𝜑 → (3 · ((((1.079955)↑2) · (1.414)) · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
38253, 110, 132, 228, 381letrd 10989 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 399  w3a 1089   = wceq 1543  wcel 2110  {crab 3065  cdif 3863  cun 3864  cin 3865  wss 3866  ifcif 4439  {csn 4541  {cpr 4543  {ctp 4545   class class class wbr 5053  cmpt 5135   I cid 5454  cres 5553  ccom 5555  wf 6376  cfv 6380  (class class class)co 7213  Fincfn 8626  cc 10727  cr 10728  0cc0 10729  1c1 10730   · cmul 10734  +∞cpnf 10864   < clt 10867  cle 10868   / cdiv 11489  cn 11830  2c2 11885  3c3 11886  4c4 11887  5c5 11888  6c6 11889  7c7 11890  8c8 11891  9c9 11892  0cn0 12090  cz 12176  cdc 12293  +crp 12586  [,)cico 12937  ...cfz 13095  ..^cfzo 13238  cexp 13635  csqrt 14796  Σcsu 15249  cdvds 15815  cprime 16228  pmTrspcpmtr 18833  logclog 25443  Λcvma 25974  ψcchp 25975  cdp2 30865  .cdp 30882  reprcrepr 32300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-reg 9208  ax-inf2 9256  ax-ac2 10077  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807  ax-addf 10808  ax-mulf 10809  ax-ros335 32337  ax-ros336 32338
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-of 7469  df-om 7645  df-1st 7761  df-2nd 7762  df-supp 7904  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-2o 8203  df-oadd 8206  df-er 8391  df-map 8510  df-pm 8511  df-ixp 8579  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-fsupp 8986  df-fi 9027  df-sup 9058  df-inf 9059  df-oi 9126  df-r1 9380  df-rank 9381  df-dju 9517  df-card 9555  df-ac 9730  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-xnn0 12163  df-z 12177  df-dec 12294  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ioo 12939  df-ioc 12940  df-ico 12941  df-icc 12942  df-fz 13096  df-fzo 13239  df-fl 13367  df-mod 13443  df-seq 13575  df-exp 13636  df-fac 13840  df-bc 13869  df-hash 13897  df-shft 14630  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-limsup 15032  df-clim 15049  df-rlim 15050  df-sum 15250  df-prod 15468  df-ef 15629  df-sin 15631  df-cos 15632  df-tan 15633  df-pi 15634  df-dvds 15816  df-gcd 16054  df-prm 16229  df-pc 16390  df-struct 16700  df-sets 16717  df-slot 16735  df-ndx 16745  df-base 16761  df-ress 16785  df-plusg 16815  df-mulr 16816  df-starv 16817  df-sca 16818  df-vsca 16819  df-ip 16820  df-tset 16821  df-ple 16822  df-ds 16824  df-unif 16825  df-hom 16826  df-cco 16827  df-rest 16927  df-topn 16928  df-0g 16946  df-gsum 16947  df-topgen 16948  df-pt 16949  df-prds 16952  df-xrs 17007  df-qtop 17012  df-imas 17013  df-xps 17015  df-mre 17089  df-mrc 17090  df-acs 17092  df-mgm 18114  df-sgrp 18163  df-mnd 18174  df-submnd 18219  df-mulg 18489  df-cntz 18711  df-pmtr 18834  df-cmn 19172  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-fbas 20360  df-fg 20361  df-cnfld 20364  df-top 21791  df-topon 21808  df-topsp 21830  df-bases 21843  df-cld 21916  df-ntr 21917  df-cls 21918  df-nei 21995  df-lp 22033  df-perf 22034  df-cn 22124  df-cnp 22125  df-haus 22212  df-cmp 22284  df-tx 22459  df-hmeo 22652  df-fil 22743  df-fm 22835  df-flim 22836  df-flf 22837  df-xms 23218  df-ms 23219  df-tms 23220  df-cncf 23775  df-limc 24763  df-dv 24764  df-ulm 25269  df-log 25445  df-atan 25750  df-cht 25979  df-vma 25980  df-chp 25981  df-dp2 30866  df-dp 30883  df-repr 32301
This theorem is referenced by:  tgoldbachgtde  32352
  Copyright terms: Public domain W3C validator