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 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( 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 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( 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 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( 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 ) ) )