Metamath Proof Explorer

Theorem tgoldbachgtda

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 tgoldbachgtda ( 𝜑 → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )

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 inss2 ⊢ ( 𝑂 ∩ ℙ ) ⊆ ℙ
14 prmssnn ⊢ ℙ ⊆ ℕ
15 13 14 sstri ⊢ ( 𝑂 ∩ ℙ ) ⊆ ℕ
16 15 a1i ⊢ ( 𝜑 → ( 𝑂 ∩ ℙ ) ⊆ ℕ )
17 10 12 16 reprfi2 ⊢ ( 𝜑 → ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∈ Fin )
18 1 2 3 4 5 6 7 8 tgoldbachgtde ⊢ ( 𝜑 → 0 < Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
19 18 gt0ne0d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≠ 0 )
20 19 neneqd ⊢ ( 𝜑 → ¬ Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = 0 )
21 simpr ⊢ ( ( 𝜑 ∧ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) = ∅ ) → ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) = ∅ )
22 21 sumeq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) = ∅ ) → Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = Σ 𝑛 ∈ ∅ ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
23 sum0 ⊢ Σ 𝑛 ∈ ∅ ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = 0
24 22 23 eqtrdi ⊢ ( ( 𝜑 ∧ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) = ∅ ) → Σ 𝑛 ∈ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = 0 )
25 20 24 mtand ⊢ ( 𝜑 → ¬ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) = ∅ )
26 25 neqned ⊢ ( 𝜑 → ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ≠ ∅ )
27 hashnncl ⊢ ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∈ Fin → ( ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ ℕ ↔ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ≠ ∅ ) )
28 27 biimpar ⊢ ( ( ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ∈ Fin ∧ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ≠ ∅ ) → ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ ℕ )
29 17 26 28 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ ℕ )
30 nngt0 ⊢ ( ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) ∈ ℕ → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )
31 29 30 syl ⊢ ( 𝜑 → 0 < ( ♯ ‘ ( ( 𝑂 ∩ ℙ ) ( repr ‘ 3 ) 𝑁 ) ) )