tgoldbachgtd

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70. (Contributed by Thierry Arnoux, 15-Dec-2021)

	Ref	Expression
Hypotheses	tgoldbachgtd.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	tgoldbachgtd.n	$⊢ φ \to N \in O$
	tgoldbachgtd.1	$⊢ φ \to 10^{27} \leq N$
Assertion	tgoldbachgtd	$⊢ φ \to 0 < \|(O \cap ℙ) repr (3) N\|$

Proof

Step	Hyp	Ref	Expression
1		tgoldbachgtd.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		tgoldbachgtd.n	$⊢ φ \to N \in O$
3		tgoldbachgtd.1	$⊢ φ \to 10^{27} \leq N$
4	2	ad3antrrr	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to N \in O$
5	3	ad3antrrr	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to 10^{27} \leq N$
6		elmapi	$⊢ h \in ({[0, +∞)}^{ℕ}) \to h : ℕ ⟶ [0, +∞)$
7	6	ad3antlr	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to h : ℕ ⟶ [0, +∞)$
8		elmapi	$⊢ k \in ({[0, +∞)}^{ℕ}) \to k : ℕ ⟶ [0, +∞)$
9	8	ad2antlr	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to k : ℕ ⟶ [0, +∞)$
10		simpr1	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to \forall m \in ℕ k (m) \leq 1.079955$
11		fveq2	$⊢ m = n \to k (m) = k (n)$
12	11	breq1d	$⊢ m = n \to (k (m) \leq 1.079955 \leftrightarrow k (n) \leq 1.079955)$
13	12	cbvralvw	$⊢ \forall m \in ℕ k (m) \leq 1.079955 \leftrightarrow \forall n \in ℕ k (n) \leq 1.079955$
14	10 13	sylib	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to \forall n \in ℕ k (n) \leq 1.079955$
15	14	r19.21bi	$⊢ ((((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \land n \in ℕ) \to k (n) \leq 1.079955$
16		simpr2	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to \forall m \in ℕ h (m) \leq 1.414$
17		fveq2	$⊢ m = n \to h (m) = h (n)$
18	17	breq1d	$⊢ m = n \to (h (m) \leq 1.414 \leftrightarrow h (n) \leq 1.414)$
19	18	cbvralvw	$⊢ \forall m \in ℕ h (m) \leq 1.414 \leftrightarrow \forall n \in ℕ h (n) \leq 1.414$
20	16 19	sylib	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to \forall n \in ℕ h (n) \leq 1.414$
21	20	r19.21bi	$⊢ ((((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \land n \in ℕ) \to h (n) \leq 1.414$
22		simpr3	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \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$
23		fveq2	$⊢ x = y \to ((Λ \times_{f} h) vts N) (x) = ((Λ \times_{f} h) vts N) (y)$
24		fveq2	$⊢ x = y \to ((Λ \times_{f} k) vts N) (x) = ((Λ \times_{f} k) vts N) (y)$
25	24	oveq1d	$⊢ x = y \to {((Λ \times_{f} k) vts N) (x)}^{2} = {((Λ \times_{f} k) vts N) (y)}^{2}$
26	23 25	oveq12d	$⊢ x = y \to ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} = ((Λ \times_{f} h) vts N) (y) {((Λ \times_{f} k) vts N) (y)}^{2}$
27		oveq2	$⊢ x = y \to -N x = -N y$
28	27	oveq2d	$⊢ x = y \to i 2 π -N x = i 2 π -N y$
29	28	fveq2d	$⊢ x = y \to e^{i 2 π -N x} = e^{i 2 π -N y}$
30	26 29	oveq12d	$⊢ x = y \to ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} = ((Λ \times_{f} h) vts N) (y) {((Λ \times_{f} k) vts N) (y)}^{2} e^{i 2 π -N y}$
31	30	cbvitgv	$⊢ \int_{(0, 1)} ((Λ \times_{f} h) vts N) (x) {((Λ \times_{f} k) vts N) (x)}^{2} e^{i 2 π -N x} d x = \int_{(0, 1)} ((Λ \times_{f} h) vts N) (y) {((Λ \times_{f} k) vts N) (y)}^{2} e^{i 2 π -N y} d y$
32	22 31	breqtrdi	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to 0.00042248 N^{2} \leq \int_{(0, 1)} ((Λ \times_{f} h) vts N) (y) {((Λ \times_{f} k) vts N) (y)}^{2} e^{i 2 π -N y} d y$
33	1 4 5 7 9 15 21 32	tgoldbachgtda	$⊢ (((φ \land h \in ({[0, +∞)}^{ℕ})) \land k \in ({[0, +∞)}^{ℕ})) \land (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)) \to 0 < \|(O \cap ℙ) repr (3) N\|$
34	1 2 3	hgt749d	$⊢ φ \to \exists h \in ({[0, +∞)}^{ℕ}) \exists k \in ({[0, +∞)}^{ℕ}) (\forall m \in ℕ k (m) \leq 1.079955 \land \forall m \in ℕ h (m) \leq 1.414 \land 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)$
35	33 34	r19.29vva	$⊢ φ \to 0 < \|(O \cap ℙ) repr (3) N\|$

Metamath Proof Explorer

Theorem tgoldbachgtd

Proof