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