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 ) 𝑁 ) ) )