Metamath Proof Explorer

Theorem tgoldbachgtde

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses tgoldbachgtda.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
tgoldbachgtda.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑂 )
tgoldbachgtda.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
tgoldbachgtda.h ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
tgoldbachgtda.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
tgoldbachgtda.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐾 ‘ 𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
tgoldbachgtda.2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ ( 1 . 4 1 4 ) )
tgoldbachgtda.3 ⊢ ( 𝜑 → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
Assertion tgoldbachgtde ( 𝜑 → 0 < Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tgoldbachgtda.o ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 tgoldbachgtda.n ⊢ ( 𝜑 → 𝑁 ∈ 𝑂 )
3 tgoldbachgtda.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
4 tgoldbachgtda.h ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
5 tgoldbachgtda.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
6 tgoldbachgtda.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐾 ‘ 𝑚 ) ≤ ( 1 . 0 7 9 9 5 5 ) )
7 tgoldbachgtda.2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ ( 1 . 4 1 4 ) )
8 tgoldbachgtda.3 ⊢ ( 𝜑 → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
9 1 2 3 tgoldbachgnn ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
10 9 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11 3nn0 ⊢ 3 ∈ ℕ0
12 11 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
13 ssidd ⊢ ( 𝜑 → ℕ ⊆ ℕ )
14 10 12 13 reprfi2 ⊢ ( 𝜑 → ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin )
15 diffi ⊢ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∈ Fin → ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ Fin )
16 14 15 syl ⊢ ( 𝜑 → ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ Fin )
17 difssd ⊢ ( 𝜑 → ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
19 vmaf ⊢ Λ : ℕ ⟶ ℝ
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → Λ : ℕ ⟶ ℝ )
21 ssidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ℕ ⊆ ℕ )
22 10 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑁 ∈ ℤ )
24 11 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 3 ∈ ℕ0 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
26 21 23 24 25 reprf ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 : ( 0 ..^ 3 ) ⟶ ℕ )
27 c0ex ⊢ 0 ∈ V
28 27 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
29 fzo0to3tp ⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
30 28 29 eleqtrri ⊢ 0 ∈ ( 0 ..^ 3 )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 0 ∈ ( 0 ..^ 3 ) )
32 26 31 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝑛 ‘ 0 ) ∈ ℕ )
33 20 32 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
34 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
35 fss ⊢ ( ( 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐻 : ℕ ⟶ ℝ )
36 4 34 35 sylancl ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ℝ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝐻 : ℕ ⟶ ℝ )
38 37 32 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
39 33 38 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) ∈ ℝ )
40 1ex ⊢ 1 ∈ V
41 40 tpid2 ⊢ 1 ∈ { 0 , 1 , 2 }
42 41 29 eleqtrri ⊢ 1 ∈ ( 0 ..^ 3 )
43 42 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 1 ∈ ( 0 ..^ 3 ) )
44 26 43 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
45 20 44 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
46 fss ⊢ ( ( 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐾 : ℕ ⟶ ℝ )
47 5 34 46 sylancl ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ℝ )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 𝐾 : ℕ ⟶ ℝ )
49 48 44 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
50 45 49 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℝ )
51 2ex ⊢ 2 ∈ V
52 51 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
53 52 29 eleqtrri ⊢ 2 ∈ ( 0 ..^ 3 )
54 53 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → 2 ∈ ( 0 ..^ 3 ) )
55 26 54 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
56 20 55 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
57 48 55 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
58 56 57 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
59 50 58 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
60 39 59 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
61 18 60 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
62 16 61 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
63 0nn0 ⊢ 0 ∈ ℕ0
64 qssre ⊢ ℚ ⊆ ℝ
65 4nn0 ⊢ 4 ∈ ℕ0
66 2nn0 ⊢ 2 ∈ ℕ0
67 nn0ssq ⊢ ℕ0 ⊆ ℚ
68 8nn0 ⊢ 8 ∈ ℕ0
69 67 68 sselii ⊢ 8 ∈ ℚ
70 65 69 dp2clq ⊢ 4 8 ∈ ℚ
71 66 70 dp2clq ⊢ 2 4 8 ∈ ℚ
72 66 71 dp2clq ⊢ 2 2 4 8 ∈ ℚ
73 65 72 dp2clq ⊢ 4 2 2 4 8 ∈ ℚ
74 63 73 dp2clq ⊢ 0 4 2 2 4 8 ∈ ℚ
75 63 74 dp2clq ⊢ 0 0 4 2 2 4 8 ∈ ℚ
76 63 75 dp2clq ⊢ 0 0 0 4 2 2 4 8 ∈ ℚ
77 64 76 sselii ⊢ 0 0 0 4 2 2 4 8 ∈ ℝ
78 dpcl ⊢ ( ( 0 ∈ ℕ0 ∧ 0 0 0 4 2 2 4 8 ∈ ℝ ) → ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ )
79 63 77 78 mp2an ⊢ ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ
80 79 a1i ⊢ ( 𝜑 → ( 0 . 0 0 0 4 2 2 4 8 ) ∈ ℝ )
81 9 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
82 81 resqcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℝ )
83 80 82 remulcld ⊢ ( 𝜑 → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ∈ ℝ )
84 14 60 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
85 7nn0 ⊢ 7 ∈ ℕ0
86 11 70 dp2clq ⊢ 3 4 8 ∈ ℚ
87 64 86 sselii ⊢ 3 4 8 ∈ ℝ
88 dpcl ⊢ ( ( 7 ∈ ℕ0 ∧ 3 4 8 ∈ ℝ ) → ( 7 . 3 4 8 ) ∈ ℝ )
89 85 87 88 mp2an ⊢ ( 7 . 3 4 8 ) ∈ ℝ
90 89 a1i ⊢ ( 𝜑 → ( 7 . 3 4 8 ) ∈ ℝ )
91 9 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
92 91 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑁 ) ∈ ℝ )
93 10 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
94 81 93 resqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
95 91 sqrtgt0d ⊢ ( 𝜑 → 0 < ( √ ‘ 𝑁 ) )
96 95 gt0ne0d ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ≠ 0 )
97 92 94 96 redivcld ⊢ ( 𝜑 → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ∈ ℝ )
98 90 97 remulcld ⊢ ( 𝜑 → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
99 98 82 remulcld ⊢ ( 𝜑 → ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) ∈ ℝ )
100 1 9 3 4 5 6 7 hgt750leme ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) )
101 2z ⊢ 2 ∈ ℤ
102 101 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
103 91 102 rpexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℝ+ )
104 hgt750lem ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 1 0 ↑ 2 7 ) ≤ 𝑁 ) → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) )
105 10 3 104 syl2anc ⊢ ( 𝜑 → ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) < ( 0 . 0 0 0 4 2 2 4 8 ) )
106 98 80 103 105 ltmul1dd ⊢ ( 𝜑 → ( ( ( 7 . 3 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) · ( 𝑁 ↑ 2 ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) )
107 62 99 83 100 106 lelttrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) < ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) )
108 36 47 10 circlemethhgt ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ∫ ( 0 (,) 1 ) ( ( ( ( ( Λ ∘f · 𝐻 ) vts 𝑁 ) ‘ 𝑥 ) · ( ( ( ( Λ ∘f · 𝐾 ) vts 𝑁 ) ‘ 𝑥 ) ↑ 2 ) ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
109 8 108 breqtrrd ⊢ ( 𝜑 → ( ( 0 . 0 0 0 4 2 2 4 8 ) · ( 𝑁 ↑ 2 ) ) ≤ Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
110 62 83 84 107 109 ltletrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) < Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
111 62 84 posdifd ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) < Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ↔ 0 < ( Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) − Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) ) )
112 110 111 mpbid ⊢ ( 𝜑 → 0 < ( Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) − Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) )
113 inss2 ⊢ ( 𝑂 ∩ ℙ ) ⊆ ℙ
114 prmssnn ⊢ ℙ ⊆ ℕ
115 113 114 sstri ⊢ ( 𝑂 ∩ ℙ ) ⊆ ℕ
116 115 a1i ⊢ ( 𝜑 → ( 𝑂 ∩ ℙ ) ⊆ ℕ )
117 13 22 12 116 reprss ⊢ ( 𝜑 → ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
118 14 117 ssfid ⊢ ( 𝜑 → ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∈ Fin )
119 117 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) → 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) )
120 60 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℂ )
121 119 120 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℂ )
122 118 121 fsumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℂ )
123 62 recnd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℂ )
124 disjdif ⊢ ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∩ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) = ∅
125 124 a1i ⊢ ( 𝜑 → ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∩ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) = ∅ )
126 undif ⊢ ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ⊆ ( ℕ ( repr ‘ 3 ) 𝑁 ) ↔ ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∪ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) = ( ℕ ( repr ‘ 3 ) 𝑁 ) )
127 117 126 sylib ⊢ ( 𝜑 → ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∪ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) = ( ℕ ( repr ‘ 3 ) 𝑁 ) )
128 127 eqcomd ⊢ ( 𝜑 → ( ℕ ( repr ‘ 3 ) 𝑁 ) = ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∪ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ) )
129 125 128 14 120 fsumsplit ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ( Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) + Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) )
130 122 123 129 mvrraddd ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( ℕ ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) − Σ 𝑛 ∈ ( ( ℕ ( repr ‘ 3 ) 𝑁 ) ∖ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ) = Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
131 112 130 breqtrd ⊢ ( 𝜑 → 0 < Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )