tgoldbachgtda

	Ref	Expression
Hypotheses	tgoldbachgtda.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	tgoldbachgtda.n	$⊢ φ \to N \in O$
	tgoldbachgtda.0	$⊢ φ \to 10^{27} \leq N$
	tgoldbachgtda.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
	tgoldbachgtda.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
	tgoldbachgtda.1	$⊢ (φ \land m \in ℕ) \to K (m) \leq 1.079955$
	tgoldbachgtda.2	$⊢ (φ \land m \in ℕ) \to H (m) \leq 1.414$
	tgoldbachgtda.3	$⊢ φ \to 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} H) vts N) (x) {((Λ \times_{f} K) vts N) (x)}^{2} e^{i 2 π -N x} d x$
Assertion	tgoldbachgtda	$⊢ φ \to 0 < \|(O \cap ℙ) repr (3) N\|$

Proof

Step	Hyp	Ref	Expression
1		tgoldbachgtda.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		tgoldbachgtda.n	$⊢ φ \to N \in O$
3		tgoldbachgtda.0	$⊢ φ \to 10^{27} \leq N$
4		tgoldbachgtda.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
5		tgoldbachgtda.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
6		tgoldbachgtda.1	$⊢ (φ \land m \in ℕ) \to K (m) \leq 1.079955$
7		tgoldbachgtda.2	$⊢ (φ \land m \in ℕ) \to H (m) \leq 1.414$
8		tgoldbachgtda.3	$⊢ φ \to 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} H) vts N) (x) {((Λ \times_{f} K) vts N) (x)}^{2} e^{i 2 π -N x} d x$
9	1 2 3	tgoldbachgnn	$⊢ φ \to N \in ℕ$
10	9	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
11		3nn0	$⊢ 3 \in ℕ_{0}$
12	11	a1i	$⊢ φ \to 3 \in ℕ_{0}$
13		inss2	$⊢ O \cap ℙ \subseteq ℙ$
14		prmssnn	$⊢ ℙ \subseteq ℕ$
15	13 14	sstri	$⊢ O \cap ℙ \subseteq ℕ$
16	15	a1i	$⊢ φ \to O \cap ℙ \subseteq ℕ$
17	10 12 16	reprfi2	$⊢ φ \to (O \cap ℙ) repr (3) N \in Fin$
18	1 2 3 4 5 6 7 8	tgoldbachgtde	$⊢ φ \to 0 < \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$
19	18	gt0ne0d	$⊢ φ \to \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \neq 0$
20	19	neneqd	$⊢ φ \to \neg \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = 0$
21		simpr	$⊢ (φ \land (O \cap ℙ) repr (3) N = \emptyset) \to (O \cap ℙ) repr (3) N = \emptyset$
22	21	sumeq1d	$⊢ (φ \land (O \cap ℙ) repr (3) N = \emptyset) \to \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = \sum_{n \in \emptyset} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2))$
23		sum0	$⊢ \sum_{n \in \emptyset} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = 0$
24	22 23	eqtrdi	$⊢ (φ \land (O \cap ℙ) repr (3) N = \emptyset) \to \sum_{n \in (O \cap ℙ) repr (3) N} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) = 0$
25	20 24	mtand	$⊢ φ \to \neg (O \cap ℙ) repr (3) N = \emptyset$
26	25	neqned	$⊢ φ \to (O \cap ℙ) repr (3) N \neq \emptyset$
27		hashnncl	$⊢ (O \cap ℙ) repr (3) N \in Fin \to (\|(O \cap ℙ) repr (3) N\| \in ℕ \leftrightarrow (O \cap ℙ) repr (3) N \neq \emptyset)$
28	27	biimpar	$⊢ ((O \cap ℙ) repr (3) N \in Fin \land (O \cap ℙ) repr (3) N \neq \emptyset) \to \|(O \cap ℙ) repr (3) N\| \in ℕ$
29	17 26 28	syl2anc	$⊢ φ \to \|(O \cap ℙ) repr (3) N\| \in ℕ$
30		nngt0	$⊢ \|(O \cap ℙ) repr (3) N\| \in ℕ \to 0 < \|(O \cap ℙ) repr (3) N\|$
31	29 30	syl	$⊢ φ \to 0 < \|(O \cap ℙ) repr (3) N\|$

Metamath Proof Explorer

Theorem tgoldbachgtda

Proof