Metamath Proof Explorer

Theorem tgoldbachgtda

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

Ref Expression
Hypotheses tgoldbachgtda.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
tgoldbachgtda.n ⊢ φ → N ∈ O
tgoldbachgtda.0 ⊢ φ → 10 27 ≤ N
tgoldbachgtda.h ⊢ φ → H : ℕ ⟶ 0 +∞
tgoldbachgtda.k ⊢ φ → K : ℕ ⟶ 0 +∞
tgoldbachgtda.1 ⊢ φ ∧ m ∈ ℕ → K ⁡ m ≤ 1.079955
tgoldbachgtda.2 ⊢ φ ∧ m ∈ ℕ → H ⁡ m ≤ 1.414
tgoldbachgtda.3 ⊢ φ → 0.00042248 ⁢ N 2 ≤ ∫ 0 1 Λ × f H vts N ⁡ x ⁢ Λ × f K vts N ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ -N ⁢ x dx
Assertion tgoldbachgtda ⊢ φ → 0 < O ∩ ℙ repr ⁡ 3 N

Proof

Step Hyp Ref Expression
1 tgoldbachgtda.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
2 tgoldbachgtda.n ⊢ φ → N ∈ O
3 tgoldbachgtda.0 ⊢ φ → 10 27 ≤ N
4 tgoldbachgtda.h ⊢ φ → H : ℕ ⟶ 0 +∞
5 tgoldbachgtda.k ⊢ φ → K : ℕ ⟶ 0 +∞
6 tgoldbachgtda.1 ⊢ φ ∧ m ∈ ℕ → K ⁡ m ≤ 1.079955
7 tgoldbachgtda.2 ⊢ φ ∧ m ∈ ℕ → H ⁡ m ≤ 1.414
8 tgoldbachgtda.3 ⊢ φ → 0.00042248 ⁢ N 2 ≤ ∫ 0 1 Λ × f H vts N ⁡ x ⁢ Λ × f K vts N ⁡ x 2 ⁢ e i ⁢ 2 ⁢ π ⁢ -N ⁢ x dx
9 1 2 3 tgoldbachgnn ⊢ φ → N ∈ ℕ
10 9 nnnn0d ⊢ φ → N ∈ ℕ 0
11 3nn0 ⊢ 3 ∈ ℕ 0
12 11 a1i ⊢ φ → 3 ∈ ℕ 0
13 inss2 ⊢ O ∩ ℙ ⊆ ℙ
14 prmssnn ⊢ ℙ ⊆ ℕ
15 13 14 sstri ⊢ O ∩ ℙ ⊆ ℕ
16 15 a1i ⊢ φ → O ∩ ℙ ⊆ ℕ
17 10 12 16 reprfi2 ⊢ φ → O ∩ ℙ repr ⁡ 3 N ∈ Fin
18 1 2 3 4 5 6 7 8 tgoldbachgtde ⊢ φ → 0 < ∑ n ∈ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2
19 18 gt0ne0d ⊢ φ → ∑ n ∈ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2 ≠ 0
20 19 neneqd ⊢ φ → ¬ ∑ n ∈ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2 = 0
21 simpr ⊢ φ ∧ O ∩ ℙ repr ⁡ 3 N = ∅ → O ∩ ℙ repr ⁡ 3 N = ∅
22 21 sumeq1d ⊢ φ ∧ O ∩ ℙ repr ⁡ 3 N = ∅ → ∑ n ∈ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2 = ∑ n ∈ ∅ Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2
23 sum0 ⊢ ∑ n ∈ ∅ Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2 = 0
24 22 23 eqtrdi ⊢ φ ∧ O ∩ ℙ repr ⁡ 3 N = ∅ → ∑ n ∈ O ∩ ℙ repr ⁡ 3 N Λ ⁡ n ⁡ 0 ⁢ H ⁡ n ⁡ 0 ⁢ Λ ⁡ n ⁡ 1 ⁢ K ⁡ n ⁡ 1 ⁢ Λ ⁡ n ⁡ 2 ⁢ K ⁡ n ⁡ 2 = 0
25 20 24 mtand ⊢ φ → ¬ O ∩ ℙ repr ⁡ 3 N = ∅
26 25 neqned ⊢ φ → O ∩ ℙ repr ⁡ 3 N ≠ ∅
27 hashnncl ⊢ O ∩ ℙ repr ⁡ 3 N ∈ Fin → O ∩ ℙ repr ⁡ 3 N ∈ ℕ ↔ O ∩ ℙ repr ⁡ 3 N ≠ ∅
28 27 biimpar ⊢ O ∩ ℙ repr ⁡ 3 N ∈ Fin ∧ O ∩ ℙ repr ⁡ 3 N ≠ ∅ → O ∩ ℙ repr ⁡ 3 N ∈ ℕ
29 17 26 28 syl2anc ⊢ φ → O ∩ ℙ repr ⁡ 3 N ∈ ℕ
30 nngt0 ⊢ O ∩ ℙ repr ⁡ 3 N ∈ ℕ → 0 < O ∩ ℙ repr ⁡ 3 N
31 29 30 syl ⊢ φ → 0 < O ∩ ℙ repr ⁡ 3 N