Metamath Proof Explorer

Theorem hgt750leme

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)

Ref Expression
Hypotheses hgt750leme.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
hgt750leme.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
hgt750leme.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
hgt750leme.h ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
hgt750leme.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
hgt750leme.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐾 ‘ 𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
hgt750leme.2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ ( 1 . 4 1 4 ) )
Assertion hgt750leme ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 hgt750leme.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 hgt750leme.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 hgt750leme.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
4 hgt750leme.h ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
5 hgt750leme.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
6 hgt750leme.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐾 ‘ 𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
7 hgt750leme.2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ ( 1 . 4 1 4 ) )
8 2 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 3nn0 ⊢ 3 ∈ ℕ0
10 9 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
11 ssidd ⊢ ( 𝜑 → ℕ ⊆ ℕ )
12 8 10 11 reprfi2 ⊢ ( 𝜑 → ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin )
13 diffi ⊢ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin → ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ Fin )
14 12 13 syl ⊢ ( 𝜑 → ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ Fin )
15 vmaf ⊢ Λ : ℕ ⟶ ℝ
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → Λ : ℕ ⟶ ℝ )
17 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ℕ ⊆ ℕ )
18 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝑁 ∈ ℤ )
20 9 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 3 ∈ ℕ0 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )
22 21 eldifad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
23 17 19 20 22 reprf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
24 c0ex ⊢ 0 ∈ V
25 24 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
26 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
27 25 26 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 0 ∈ ( 0 ..^ 3 ) )
29 23 28 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝑛 ‘ 0 ) ∈ ℕ )
30 16 29 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
31 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
32 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
33 32 29 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ( 0 [,) +∞ ) )
34 31 33 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
35 30 34 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) ∈ ℝ )
36 1eltp012 ⊢ 1 ∈ { 0 , 1 , 2 }
37 36 26 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
38 37 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 1 ∈ ( 0 ..^ 3 ) )
39 23 38 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
40 16 39 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
41 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
42 41 39 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ( 0 [,) +∞ ) )
43 31 42 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
44 40 43 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℝ )
45 2ex ⊢ 2 ∈ V
46 45 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
47 46 26 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 2 ∈ ( 0 ..^ 3 ) )
49 23 48 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
50 16 49 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
51 41 49 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ( 0 [,) +∞ ) )
52 31 51 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
53 50 52 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
54 44 53 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
55 35 54 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
56 14 55 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
57 3re ⊢ 3 ∈ ℝ
58 57 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
59 1nn0 ⊢ 1 ∈ ℕ0
60 0nn0 ⊢ 0 ∈ ℕ0
61 7nn0 ⊢ 7 ∈ ℕ0
62 9nn0 ⊢ 9 ∈ ℕ0
63 5nn0 ⊢ 5 ∈ ℕ0
64 5nn ⊢ 5 ∈ ℕ
65 nnrp ⊢ ( 5 ∈ ℕ → 5 ∈ ℝ+ )
66 64 65 ax-mp ⊢ 5 ∈ ℝ+
67 63 66 rpdp2cl ⊢ 5 5 ∈ ℝ+
68 62 67 rpdp2cl ⊢ 9 5 5 ∈ ℝ+
69 62 68 rpdp2cl ⊢ 9 9 5 5 ∈ ℝ+
70 61 69 rpdp2cl ⊢ 7 9 9 5 5 ∈ ℝ+
71 60 70 rpdp2cl ⊢ 0 7 9 9 5 5 ∈ ℝ+
72 59 71 rpdpcl ⊢ ( 1 . 0 7 9 9 5 5 ) ∈ ℝ+
73 72 a1i ⊢ ( 𝜑 → ( 1 . 0 7 9 9 5 5 ) ∈ ℝ+ )
74 73 rpred ⊢ ( 𝜑 → ( 1 . 0 7 9 9 5 5 ) ∈ ℝ )
75 74 resqcld ⊢ ( 𝜑 → ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) ∈ ℝ )
76 4nn0 ⊢ 4 ∈ ℕ0
77 4nn ⊢ 4 ∈ ℕ
78 nnrp ⊢ ( 4 ∈ ℕ → 4 ∈ ℝ+ )
79 77 78 ax-mp ⊢ 4 ∈ ℝ+
80 59 79 rpdp2cl ⊢ 1 4 ∈ ℝ+
81 76 80 rpdp2cl ⊢ 4 1 4 ∈ ℝ+
82 59 81 rpdpcl ⊢ ( 1 . 4 1 4 ) ∈ ℝ+
83 82 a1i ⊢ ( 𝜑 → ( 1 . 4 1 4 ) ∈ ℝ+ )
84 83 rpred ⊢ ( 𝜑 → ( 1 . 4 1 4 ) ∈ ℝ )
85 75 84 remulcld ⊢ ( 𝜑 → ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) ∈ ℝ )
86 fveq1 ⊢ ( 𝑑 = 𝑐 → ( 𝑑 ‘ 0 ) = ( 𝑐 ‘ 0 ) )
87 86 eleq1d ⊢ ( 𝑑 = 𝑐 → ( ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ↔ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ) )
88 87 notbid ⊢ ( 𝑑 = 𝑐 → ( ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ↔ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) ) )
89 88 cbvrabv ⊢ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } = { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) }
90 89 ssrab3 ⊢ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 )
91 ssfi ⊢ ( ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin ∧ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ∈ Fin )
92 12 90 91 sylancl ⊢ ( 𝜑 → { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ∈ Fin )
93 15 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → Λ : ℕ ⟶ ℝ )
94 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ℕ ⊆ ℕ )
95 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑁 ∈ ℤ )
96 9 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 3 ∈ ℕ0 )
97 90 a1i ⊢ ( 𝜑 → { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
98 97 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
99 94 95 96 98 reprf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
100 27 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 0 ∈ ( 0 ..^ 3 ) )
101 99 100 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 0 ) ∈ ℕ )
102 93 101 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
103 37 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 1 ∈ ( 0 ..^ 3 ) )
104 99 103 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
105 93 104 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
106 47 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → 2 ∈ ( 0 ..^ 3 ) )
107 99 106 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
108 93 107 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
109 105 108 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
110 102 109 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
111 92 110 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
112 85 111 remulcld ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
113 58 112 remulcld ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ∈ ℝ )
114 4re ⊢ 4 ∈ ℝ
115 8re ⊢ 8 ∈ ℝ
116 114 115 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 8 ∈ ℝ )
117 dp2cl ⊢ ( ( 4 ∈ ℝ ∧ 8 ∈ ℝ ) → 4 8 ∈ ℝ )
118 116 117 ax-mp ⊢ 4 8 ∈ ℝ
119 57 118 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 4 8 ∈ ℝ )
120 dp2cl ⊢ ( ( 3 ∈ ℝ ∧ 4 8 ∈ ℝ ) → 3 4 8 ∈ ℝ )
121 119 120 ax-mp ⊢ 3 4 8 ∈ ℝ
122 dpcl ⊢ ( ( 7 ∈ ℕ0 ∧ 3 4 8 ∈ ℝ ) → ( 7 . 3 4 8 ) ∈ ℝ )
123 61 121 122 mp2an ⊢ ( 7 . 3 4 8 ) ∈ ℝ
124 123 a1i ⊢ ( 𝜑 → ( 7 . 3 4 8 ) ∈ ℝ )
125 2 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
126 125 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
127 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
128 125 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
129 127 128 resqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
130 125 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ+ )
131 130 rpne0d ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ≠ 0 )
132 126 129 131 redivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ∈ ℝ )
133 124 132 remulcld ⊢ ( 𝜑 → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
134 127 resqcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℝ )
135 133 134 remulcld ⊢ ( 𝜑 → ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) ∈ ℝ )
136 0re ⊢ 0 ∈ ℝ
137 7re ⊢ 7 ∈ ℝ
138 9re ⊢ 9 ∈ ℝ
139 5re ⊢ 5 ∈ ℝ
140 139 139 pm3.2i ⊢ ( 5 ∈ ℝ ∧ 5 ∈ ℝ )
141 dp2cl ⊢ ( ( 5 ∈ ℝ ∧ 5 ∈ ℝ ) → 5 5 ∈ ℝ )
142 140 141 ax-mp ⊢ 5 5 ∈ ℝ
143 138 142 pm3.2i ⊢ ( 9 ∈ ℝ ∧ 5 5 ∈ ℝ )
144 dp2cl ⊢ ( ( 9 ∈ ℝ ∧ 5 5 ∈ ℝ ) → 9 5 5 ∈ ℝ )
145 143 144 ax-mp ⊢ 9 5 5 ∈ ℝ
146 138 145 pm3.2i ⊢ ( 9 ∈ ℝ ∧ 9 5 5 ∈ ℝ )
147 dp2cl ⊢ ( ( 9 ∈ ℝ ∧ 9 5 5 ∈ ℝ ) → 9 9 5 5 ∈ ℝ )
148 146 147 ax-mp ⊢ 9 9 5 5 ∈ ℝ
149 137 148 pm3.2i ⊢ ( 7 ∈ ℝ ∧ 9 9 5 5 ∈ ℝ )
150 dp2cl ⊢ ( ( 7 ∈ ℝ ∧ 9 9 5 5 ∈ ℝ ) → 7 9 9 5 5 ∈ ℝ )
151 149 150 ax-mp ⊢ 7 9 9 5 5 ∈ ℝ
152 136 151 pm3.2i ⊢ ( 0 ∈ ℝ ∧ 7 9 9 5 5 ∈ ℝ )
153 dp2cl ⊢ ( ( 0 ∈ ℝ ∧ 7 9 9 5 5 ∈ ℝ ) → 0 7 9 9 5 5 ∈ ℝ )
154 152 153 ax-mp ⊢ 0 7 9 9 5 5 ∈ ℝ
155 dpcl ⊢ ( ( 1 ∈ ℕ0 ∧ 0 7 9 9 5 5 ∈ ℝ ) → ( 1 . 0 7 9 9 5 5 ) ∈ ℝ )
156 59 154 155 mp2an ⊢ ( 1 . 0 7 9 9 5 5 ) ∈ ℝ
157 156 a1i ⊢ ( 𝜑 → ( 1 . 0 7 9 9 5 5 ) ∈ ℝ )
158 157 resqcld ⊢ ( 𝜑 → ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) ∈ ℝ )
159 1re ⊢ 1 ∈ ℝ
160 159 114 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 4 ∈ ℝ )
161 dp2cl ⊢ ( ( 1 ∈ ℝ ∧ 4 ∈ ℝ ) → 1 4 ∈ ℝ )
162 160 161 ax-mp ⊢ 1 4 ∈ ℝ
163 114 162 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 1 4 ∈ ℝ )
164 dp2cl ⊢ ( ( 4 ∈ ℝ ∧ 1 4 ∈ ℝ ) → 4 1 4 ∈ ℝ )
165 163 164 ax-mp ⊢ 4 1 4 ∈ ℝ
166 dpcl ⊢ ( ( 1 ∈ ℕ0 ∧ 4 1 4 ∈ ℝ ) → ( 1 . 4 1 4 ) ∈ ℝ )
167 59 165 166 mp2an ⊢ ( 1 . 4 1 4 ) ∈ ℝ
168 167 a1i ⊢ ( 𝜑 → ( 1 . 4 1 4 ) ∈ ℝ )
169 158 168 remulcld ⊢ ( 𝜑 → ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) ∈ ℝ )
170 40 50 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
171 30 170 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
172 14 171 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
173 169 172 remulcld ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
174 58 111 remulcld ⊢ ( 𝜑 → ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
175 169 174 remulcld ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ∈ ℝ )
176 14 157 168 4 5 29 39 49 6 7 hgt750lemf ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
177 2re ⊢ 2 ∈ ℝ
178 177 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
179 10nn0 ⊢ 1 0 ∈ ℕ0
180 2nn0 ⊢ 2 ∈ ℕ0
181 180 61 deccl ⊢ 2 7 ∈ ℕ0
182 179 181 nn0expcli ⊢ ( 1 0 ↑ 2 7 ) ∈ ℕ0
183 182 nn0rei ⊢ ( 1 0 ↑ 2 7 ) ∈ ℝ
184 183 a1i ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ∈ ℝ )
185 179 numexp1 ⊢ ( 1 0 ↑ 1 ) = 1 0
186 179 nn0rei ⊢ 1 0 ∈ ℝ
187 185 186 eqeltri ⊢ ( 1 0 ↑ 1 ) ∈ ℝ
188 187 a1i ⊢ ( 𝜑 → ( 1 0 ↑ 1 ) ∈ ℝ )
189 1nn ⊢ 1 ∈ ℕ
190 2lt9 ⊢ 2 < 9
191 177 138 190 ltleii ⊢ 2 ≤ 9
192 189 60 180 191 declei ⊢ 2 ≤ 1 0
193 192 185 breqtrri ⊢ 2 ≤ ( 1 0 ↑ 1 )
194 193 a1i ⊢ ( 𝜑 → 2 ≤ ( 1 0 ↑ 1 ) )
195 1z ⊢ 1 ∈ ℤ
196 181 nn0zi ⊢ 2 7 ∈ ℤ
197 186 195 196 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 7 ∈ ℤ )
198 1lt10 ⊢ 1 < 1 0
199 197 198 pm3.2i ⊢ ( ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ 1 < 1 0 )
200 2nn ⊢ 2 ∈ ℕ
201 1lt9 ⊢ 1 < 9
202 159 138 201 ltleii ⊢ 1 ≤ 9
203 200 61 59 202 declei ⊢ 1 ≤ 2 7
204 leexp2 ⊢ ( ( ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ 1 < 1 0 ) → ( 1 ≤ 2 7 ↔ ( 1 0 ↑ 1 ) ≤ ( 1 0 ↑ 2 7 ) ) )
205 204 biimpa ⊢ ( ( ( ( 1 0 ∈ ℝ ∧ 1 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ 1 < 1 0 ) ∧ 1 ≤ 2 7 ) → ( 1 0 ↑ 1 ) ≤ ( 1 0 ↑ 2 7 ) )
206 199 203 205 mp2an ⊢ ( 1 0 ↑ 1 ) ≤ ( 1 0 ↑ 2 7 )
207 206 a1i ⊢ ( 𝜑 → ( 1 0 ↑ 1 ) ≤ ( 1 0 ↑ 2 7 ) )
208 178 188 184 194 207 letrd ⊢ ( 𝜑 → 2 ≤ ( 1 0 ↑ 2 7 ) )
209 178 184 127 208 3 letrd ⊢ ( 𝜑 → 2 ≤ 𝑁 )
210 eqid ⊢ ( 𝑒 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ↦ ( 𝑒 ∘ if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) ) ) = ( 𝑒 ∈ { 𝑐 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑐 ‘ 𝑎 ) ∈ ( 𝑂 ∩ ℙ ) } ↦ ( 𝑒 ∘ if ( 𝑎 = 0 , ( I ↾ ( 0 ..^ 3 ) ) , ( ( pmTrsp ‘ ( 0 ..^ 3 ) ) ‘ { 𝑎 , 0 } ) ) ) )
211 1 2 209 89 210 hgt750lema ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
212 2z ⊢ 2 ∈ ℤ
213 212 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
214 73 213 rpexpcld ⊢ ( 𝜑 → ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) ∈ ℝ+ )
215 214 83 rpmulcld ⊢ ( 𝜑 → ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) ∈ ℝ+ )
216 172 174 215 lemul2d ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ↔ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ) )
217 211 216 mpbid ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) )
218 56 173 175 176 217 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) )
219 157 recnd ⊢ ( 𝜑 → ( 1 . 0 7 9 9 5 5 ) ∈ ℂ )
220 219 sqcld ⊢ ( 𝜑 → ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) ∈ ℂ )
221 168 recnd ⊢ ( 𝜑 → ( 1 . 4 1 4 ) ∈ ℂ )
222 220 221 mulcld ⊢ ( 𝜑 → ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) ∈ ℂ )
223 3cn ⊢ 3 ∈ ℂ
224 223 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
225 111 recnd ⊢ ( 𝜑 → Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℂ )
226 222 224 225 mul12d ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( 3 · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) = ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) )
227 218 226 breqtrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) )
228 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
229 diffi ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
230 228 229 ax-mp ⊢ ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin
231 snfi ⊢ { 2 } ∈ Fin
232 unfi ⊢ ( ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin ∧ { 2 } ∈ Fin ) → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin )
233 230 231 232 mp2an ⊢ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin
234 233 a1i ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ∈ Fin )
235 15 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → Λ : ℕ ⟶ ℝ )
236 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
237 236 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
238 237 ssdifssd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ℕ )
239 200 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
240 239 snssd ⊢ ( 𝜑 → { 2 } ⊆ ℕ )
241 238 240 unssd ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ⊆ ℕ )
242 241 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → 𝑖 ∈ ℕ )
243 235 242 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
244 234 243 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) ∈ ℝ )
245 chpvalz ⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) )
246 18 245 syl ⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) )
247 chpf ⊢ ψ : ℝ ⟶ ℝ
248 247 a1i ⊢ ( 𝜑 → ψ : ℝ ⟶ ℝ )
249 248 127 ffvelcdmd ⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) ∈ ℝ )
250 246 249 eqeltrrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ∈ ℝ )
251 244 250 remulcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ∈ ℝ )
252 126 251 remulcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ∈ ℝ )
253 85 252 remulcld ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ∈ ℝ )
254 58 253 remulcld ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) ∈ ℝ )
255 1 2 209 89 hgt750lemb ⊢ ( 𝜑 → Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) )
256 111 252 215 lemul2d ⊢ ( 𝜑 → ( Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ↔ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) )
257 255 256 mpbid ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) )
258 3rp ⊢ 3 ∈ ℝ+
259 258 a1i ⊢ ( 𝜑 → 3 ∈ ℝ+ )
260 112 253 259 lemul2d ⊢ ( 𝜑 → ( ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ↔ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ≤ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) ) )
261 257 260 mpbid ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ≤ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) )
262 6re ⊢ 6 ∈ ℝ
263 262 57 pm3.2i ⊢ ( 6 ∈ ℝ ∧ 3 ∈ ℝ )
264 dp2cl ⊢ ( ( 6 ∈ ℝ ∧ 3 ∈ ℝ ) → 6 3 ∈ ℝ )
265 263 264 ax-mp ⊢ 6 3 ∈ ℝ
266 177 265 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 6 3 ∈ ℝ )
267 dp2cl ⊢ ( ( 2 ∈ ℝ ∧ 6 3 ∈ ℝ ) → 2 6 3 ∈ ℝ )
268 266 267 ax-mp ⊢ 2 6 3 ∈ ℝ
269 114 268 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 2 6 3 ∈ ℝ )
270 dp2cl ⊢ ( ( 4 ∈ ℝ ∧ 2 6 3 ∈ ℝ ) → 4 2 6 3 ∈ ℝ )
271 269 270 ax-mp ⊢ 4 2 6 3 ∈ ℝ
272 dpcl ⊢ ( ( 1 ∈ ℕ0 ∧ 4 2 6 3 ∈ ℝ ) → ( 1 . 4 2 6 3 ) ∈ ℝ )
273 59 271 272 mp2an ⊢ ( 1 . 4 2 6 3 ) ∈ ℝ
274 273 a1i ⊢ ( 𝜑 → ( 1 . 4 2 6 3 ) ∈ ℝ )
275 274 129 remulcld ⊢ ( 𝜑 → ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
276 115 57 pm3.2i ⊢ ( 8 ∈ ℝ ∧ 3 ∈ ℝ )
277 dp2cl ⊢ ( ( 8 ∈ ℝ ∧ 3 ∈ ℝ ) → 8 3 ∈ ℝ )
278 276 277 ax-mp ⊢ 8 3 ∈ ℝ
279 115 278 pm3.2i ⊢ ( 8 ∈ ℝ ∧ 8 3 ∈ ℝ )
280 dp2cl ⊢ ( ( 8 ∈ ℝ ∧ 8 3 ∈ ℝ ) → 8 8 3 ∈ ℝ )
281 279 280 ax-mp ⊢ 8 8 3 ∈ ℝ
282 57 281 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 8 8 3 ∈ ℝ )
283 dp2cl ⊢ ( ( 3 ∈ ℝ ∧ 8 8 3 ∈ ℝ ) → 3 8 8 3 ∈ ℝ )
284 282 283 ax-mp ⊢ 3 8 8 3 ∈ ℝ
285 136 284 pm3.2i ⊢ ( 0 ∈ ℝ ∧ 3 8 8 3 ∈ ℝ )
286 dp2cl ⊢ ( ( 0 ∈ ℝ ∧ 3 8 8 3 ∈ ℝ ) → 0 3 8 8 3 ∈ ℝ )
287 285 286 ax-mp ⊢ 0 3 8 8 3 ∈ ℝ
288 dpcl ⊢ ( ( 1 ∈ ℕ0 ∧ 0 3 8 8 3 ∈ ℝ ) → ( 1 . 0 3 8 8 3 ) ∈ ℝ )
289 59 287 288 mp2an ⊢ ( 1 . 0 3 8 8 3 ) ∈ ℝ
290 289 a1i ⊢ ( 𝜑 → ( 1 . 0 3 8 8 3 ) ∈ ℝ )
291 290 127 remulcld ⊢ ( 𝜑 → ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ∈ ℝ )
292 275 291 remulcld ⊢ ( 𝜑 → ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ∈ ℝ )
293 126 292 remulcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ∈ ℝ )
294 85 293 remulcld ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ∈ ℝ )
295 58 294 remulcld ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) ∈ ℝ )
296 vmage0 ⊢ ( 𝑖 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑖 ) )
297 242 296 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ) → 0 ≤ ( Λ ‘ 𝑖 ) )
298 234 243 297 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) )
299 2 3 hgt750lemd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) )
300 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
301 15 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → Λ : ℕ ⟶ ℝ )
302 237 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ℕ )
303 301 302 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑗 ) ∈ ℝ )
304 vmage0 ⊢ ( 𝑗 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑗 ) )
305 302 304 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ ( Λ ‘ 𝑗 ) )
306 300 303 305 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) )
307 2 hgt750lemc ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) < ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) )
308 244 275 250 291 298 299 306 307 ltmul12ad ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) < ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) )
309 251 292 308 ltled ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ≤ ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) )
310 159 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
311 1lt2 ⊢ 1 < 2
312 311 a1i ⊢ ( 𝜑 → 1 < 2 )
313 310 178 127 312 209 ltletrd ⊢ ( 𝜑 → 1 < 𝑁 )
314 127 313 rplogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ+ )
315 251 292 314 lemul2d ⊢ ( 𝜑 → ( ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ≤ ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ↔ ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) )
316 309 315 mpbid ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) )
317 252 293 215 lemul2d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ≤ ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ↔ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) )
318 316 317 mpbid ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) )
319 253 294 259 lemul2d ⊢ ( 𝜑 → ( ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ≤ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ↔ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) ≤ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) ) )
320 318 319 mpbid ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) ≤ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) )
321 156 resqcli ⊢ ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) ∈ ℝ
322 321 167 remulcli ⊢ ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) ∈ ℝ
323 273 289 remulcli ⊢ ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ∈ ℝ
324 322 323 remulcli ⊢ ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ∈ ℝ
325 57 324 remulcli ⊢ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) ∈ ℝ
326 hgt750lem2 ⊢ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) < ( 7 . 3 4 8 )
327 325 123 326 ltleii ⊢ ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) ≤ ( 7 . 3 4 8 )
328 325 a1i ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) ∈ ℝ )
329 314 130 rpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ∈ ℝ+ )
330 125 213 rpexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℝ+ )
331 329 330 rpmulcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ∈ ℝ+ )
332 328 124 331 lemul1d ⊢ ( 𝜑 → ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) ≤ ( 7 . 3 4 8 ) ↔ ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) ≤ ( ( 7 . 3 4 8 ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) ) )
333 327 332 mpbii ⊢ ( 𝜑 → ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) ≤ ( ( 7 . 3 4 8 ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) )
334 274 recnd ⊢ ( 𝜑 → ( 1 . 4 2 6 3 ) ∈ ℂ )
335 129 recnd ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℂ )
336 290 recnd ⊢ ( 𝜑 → ( 1 . 0 3 8 8 3 ) ∈ ℂ )
337 127 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
338 334 335 336 337 mul4d ⊢ ( 𝜑 → ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) = ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) )
339 338 oveq2d ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) = ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) ) )
340 126 recnd ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℂ )
341 334 336 mulcld ⊢ ( 𝜑 → ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ∈ ℂ )
342 335 337 mulcld ⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) · 𝑁 ) ∈ ℂ )
343 341 342 mulcld ⊢ ( 𝜑 → ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) ∈ ℂ )
344 340 343 mulcomd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) ) = ( ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) · ( log ‘ 𝑁 ) ) )
345 339 344 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) = ( ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) · ( log ‘ 𝑁 ) ) )
346 341 342 340 mulassd ⊢ ( 𝜑 → ( ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( √ ‘ 𝑁 ) · 𝑁 ) ) · ( log ‘ 𝑁 ) ) = ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
347 345 346 eqtrd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) = ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
348 347 oveq2d ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) = ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) ) )
349 85 recnd ⊢ ( 𝜑 → ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) ∈ ℂ )
350 342 340 mulcld ⊢ ( 𝜑 → ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ∈ ℂ )
351 349 341 350 mulassd ⊢ ( 𝜑 → ( ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) ) )
352 348 351 eqtr4d ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) = ( ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
353 352 oveq2d ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) = ( 3 · ( ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) ) )
354 58 recnd ⊢ ( 𝜑 → 3 ∈ ℂ )
355 349 341 mulcld ⊢ ( 𝜑 → ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ∈ ℂ )
356 354 355 350 mulassd ⊢ ( 𝜑 → ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( 3 · ( ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) ) )
357 353 356 eqtr4d ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) = ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) )
358 134 recnd ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
359 340 335 358 131 div32d ⊢ ( 𝜑 → ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) = ( ( log ‘ 𝑁 ) · ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) ) )
360 358 335 131 divcld ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) ∈ ℂ )
361 340 360 mulcomd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) · ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) ) = ( ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) · ( log ‘ 𝑁 ) ) )
362 337 sqvald ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) = ( 𝑁 · 𝑁 ) )
363 362 oveq1d ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) = ( ( 𝑁 · 𝑁 ) / ( √ ‘ 𝑁 ) ) )
364 337 337 335 131 divassd ⊢ ( 𝜑 → ( ( 𝑁 · 𝑁 ) / ( √ ‘ 𝑁 ) ) = ( 𝑁 · ( 𝑁 / ( √ ‘ 𝑁 ) ) ) )
365 divsqrtid ⊢ ( 𝑁 ∈ ℝ+ → ( 𝑁 / ( √ ‘ 𝑁 ) ) = ( √ ‘ 𝑁 ) )
366 125 365 syl ⊢ ( 𝜑 → ( 𝑁 / ( √ ‘ 𝑁 ) ) = ( √ ‘ 𝑁 ) )
367 366 oveq2d ⊢ ( 𝜑 → ( 𝑁 · ( 𝑁 / ( √ ‘ 𝑁 ) ) ) = ( 𝑁 · ( √ ‘ 𝑁 ) ) )
368 363 364 367 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) = ( 𝑁 · ( √ ‘ 𝑁 ) ) )
369 337 335 mulcomd ⊢ ( 𝜑 → ( 𝑁 · ( √ ‘ 𝑁 ) ) = ( ( √ ‘ 𝑁 ) · 𝑁 ) )
370 368 369 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) = ( ( √ ‘ 𝑁 ) · 𝑁 ) )
371 370 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) / ( √ ‘ 𝑁 ) ) · ( log ‘ 𝑁 ) ) = ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) )
372 359 361 371 3eqtrrd ⊢ ( 𝜑 → ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) = ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) )
373 372 oveq2d ⊢ ( 𝜑 → ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( √ ‘ 𝑁 ) · 𝑁 ) · ( log ‘ 𝑁 ) ) ) = ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) )
374 357 373 eqtrd ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) = ( ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( 1 . 4 2 6 3 ) · ( 1 . 0 3 8 8 3 ) ) ) ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) )
375 124 recnd ⊢ ( 𝜑 → ( 7 . 3 4 8 ) ∈ ℂ )
376 132 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ∈ ℂ )
377 375 376 358 mulassd ⊢ ( 𝜑 → ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) = ( ( 7 . 3 4 8 ) · ( ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) · ( 𝑁 ↑ 2 ) ) ) )
378 333 374 377 3brtr4d ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) · ( ( 1 . 0 3 8 8 3 ) · 𝑁 ) ) ) ) ) ≤ ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) )
379 254 295 135 320 378 letrd ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · ( ( log ‘ 𝑁 ) · ( Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑗 ) ) ) ) ) ≤ ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) )
380 113 254 135 261 379 letrd ⊢ ( 𝜑 → ( 3 · ( ( ( ( 1 . 0 7 9 9 5 5 ) ↑ 2 ) · ( 1 . 4 1 4 ) ) · Σ 𝑛 ∈ { 𝑑 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ∣ ¬ ( 𝑑 ‘ 0 ) ∈ ( 𝑂 ∩ ℙ ) } ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ≤ ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) )
381 56 113 135 227 380 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) )