tgblthelfgott

Description: The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in Helfgott p. 4, using bgoldbachlt , ax-hgprmladder and bgoldbtbnd . (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	tgblthelfgott	$⊢ (N \in Odd \land 7 < N \land N < 88 10^{29}) \to N \in GoldbachOdd$

Proof

Step	Hyp	Ref	Expression
1		ax-hgprmladder	$⊢ \exists d \in ℤ_{\geq 3} \exists f \in RePart (d) ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		1nn	$⊢ 1 \in ℕ$
4	2 3	decnncl	$⊢ 11 \in ℕ$
5	4	nnzi	$⊢ 11 \in ℤ$
6		8nn0	$⊢ 8 \in ℕ_{0}$
7		8nn	$⊢ 8 \in ℕ$
8	6 7	decnncl	$⊢ 88 \in ℕ$
9		10nn	$⊢ 10 \in ℕ$
10		2nn0	$⊢ 2 \in ℕ_{0}$
11		9nn	$⊢ 9 \in ℕ$
12	10 11	decnncl	$⊢ 29 \in ℕ$
13	12	nnnn0i	$⊢ 29 \in ℕ_{0}$
14		nnexpcl	$⊢ (10 \in ℕ \land 29 \in ℕ_{0}) \to 10^{29} \in ℕ$
15	9 13 14	mp2an	$⊢ 10^{29} \in ℕ$
16	8 15	nnmulcli	$⊢ 88 10^{29} \in ℕ$
17	16	nnzi	$⊢ 88 10^{29} \in ℤ$
18		1re	$⊢ 1 \in ℝ$
19	8	nnrei	$⊢ 88 \in ℝ$
20	18 19	pm3.2i	$⊢ (1 \in ℝ \land 88 \in ℝ)$
21		0le1	$⊢ 0 \leq 1$
22		1lt10	$⊢ 1 < 10$
23	7 6 2 22	declti	$⊢ 1 < 88$
24	21 23	pm3.2i	$⊢ (0 \leq 1 \land 1 < 88)$
25		nnexpcl	$⊢ (10 \in ℕ \land 1 \in ℕ_{0}) \to 10^{1} \in ℕ$
26	9 2 25	mp2an	$⊢ 10^{1} \in ℕ$
27	26	nnrei	$⊢ 10^{1} \in ℝ$
28	15	nnrei	$⊢ 10^{29} \in ℝ$
29	27 28	pm3.2i	$⊢ (10^{1} \in ℝ \land 10^{29} \in ℝ)$
30		0re	$⊢ 0 \in ℝ$
31		10re	$⊢ 10 \in ℝ$
32		10pos	$⊢ 0 < 10$
33	30 31 32	ltleii	$⊢ 0 \leq 10$
34	9	nncni	$⊢ 10 \in ℂ$
35		exp1	$⊢ 10 \in ℂ \to 10^{1} = 10$
36	34 35	ax-mp	$⊢ 10^{1} = 10$
37	33 36	breqtrri	$⊢ 0 \leq 10^{1}$
38		1z	$⊢ 1 \in ℤ$
39	12	nnzi	$⊢ 29 \in ℤ$
40	31 38 39	3pm3.2i	$⊢ (10 \in ℝ \land 1 \in ℤ \land 29 \in ℤ)$
41		2nn	$⊢ 2 \in ℕ$
42		9nn0	$⊢ 9 \in ℕ_{0}$
43	41 42 2 22	declti	$⊢ 1 < 29$
44	22 43	pm3.2i	$⊢ (1 < 10 \land 1 < 29)$
45		ltexp2a	$⊢ ((10 \in ℝ \land 1 \in ℤ \land 29 \in ℤ) \land (1 < 10 \land 1 < 29)) \to 10^{1} < 10^{29}$
46	40 44 45	mp2an	$⊢ 10^{1} < 10^{29}$
47	37 46	pm3.2i	$⊢ (0 \leq 10^{1} \land 10^{1} < 10^{29})$
48		ltmul12a	$⊢ (((1 \in ℝ \land 88 \in ℝ) \land (0 \leq 1 \land 1 < 88)) \land ((10^{1} \in ℝ \land 10^{29} \in ℝ) \land (0 \leq 10^{1} \land 10^{1} < 10^{29}))) \to 1 10^{1} < 88 10^{29}$
49	20 24 29 47 48	mp4an	$⊢ 1 10^{1} < 88 10^{29}$
50	26	nnzi	$⊢ 10^{1} \in ℤ$
51		zmulcl	$⊢ (1 \in ℤ \land 10^{1} \in ℤ) \to 1 10^{1} \in ℤ$
52	38 50 51	mp2an	$⊢ 1 10^{1} \in ℤ$
53		zltp1le	$⊢ (1 10^{1} \in ℤ \land 88 10^{29} \in ℤ) \to (1 10^{1} < 88 10^{29} \leftrightarrow 1 10^{1} + 1 \leq 88 10^{29})$
54	52 17 53	mp2an	$⊢ 1 10^{1} < 88 10^{29} \leftrightarrow 1 10^{1} + 1 \leq 88 10^{29}$
55		1t10e1p1e11	$⊢ 11 = 1 10^{1} + 1$
56	55	eqcomi	$⊢ 1 10^{1} + 1 = 11$
57	56	breq1i	$⊢ 1 10^{1} + 1 \leq 88 10^{29} \leftrightarrow 11 \leq 88 10^{29}$
58	54 57	bitri	$⊢ 1 10^{1} < 88 10^{29} \leftrightarrow 11 \leq 88 10^{29}$
59	49 58	mpbi	$⊢ 11 \leq 88 10^{29}$
60		eluz2	$⊢ 88 10^{29} \in ℤ_{\geq 11} \leftrightarrow (11 \in ℤ \land 88 10^{29} \in ℤ \land 11 \leq 88 10^{29})$
61	5 17 59 60	mpbir3an	$⊢ 88 10^{29} \in ℤ_{\geq 11}$
62	61	a1i	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to 88 10^{29} \in ℤ_{\geq 11}$
63		4nn	$⊢ 4 \in ℕ$
64	2 7	decnncl	$⊢ 18 \in ℕ$
65	64	nnnn0i	$⊢ 18 \in ℕ_{0}$
66		nnexpcl	$⊢ (10 \in ℕ \land 18 \in ℕ_{0}) \to 10^{18} \in ℕ$
67	9 65 66	mp2an	$⊢ 10^{18} \in ℕ$
68	63 67	nnmulcli	$⊢ 4 10^{18} \in ℕ$
69	68	nnzi	$⊢ 4 10^{18} \in ℤ$
70		4re	$⊢ 4 \in ℝ$
71	18 70	pm3.2i	$⊢ (1 \in ℝ \land 4 \in ℝ)$
72		1lt4	$⊢ 1 < 4$
73	21 72	pm3.2i	$⊢ (0 \leq 1 \land 1 < 4)$
74	67	nnrei	$⊢ 10^{18} \in ℝ$
75	27 74	pm3.2i	$⊢ (10^{1} \in ℝ \land 10^{18} \in ℝ)$
76	64	nnzi	$⊢ 18 \in ℤ$
77	31 38 76	3pm3.2i	$⊢ (10 \in ℝ \land 1 \in ℤ \land 18 \in ℤ)$
78	3 6 2 22	declti	$⊢ 1 < 18$
79	22 78	pm3.2i	$⊢ (1 < 10 \land 1 < 18)$
80		ltexp2a	$⊢ ((10 \in ℝ \land 1 \in ℤ \land 18 \in ℤ) \land (1 < 10 \land 1 < 18)) \to 10^{1} < 10^{18}$
81	77 79 80	mp2an	$⊢ 10^{1} < 10^{18}$
82	37 81	pm3.2i	$⊢ (0 \leq 10^{1} \land 10^{1} < 10^{18})$
83		ltmul12a	$⊢ (((1 \in ℝ \land 4 \in ℝ) \land (0 \leq 1 \land 1 < 4)) \land ((10^{1} \in ℝ \land 10^{18} \in ℝ) \land (0 \leq 10^{1} \land 10^{1} < 10^{18}))) \to 1 10^{1} < 4 10^{18}$
84	71 73 75 82 83	mp4an	$⊢ 1 10^{1} < 4 10^{18}$
85		4z	$⊢ 4 \in ℤ$
86	67	nnzi	$⊢ 10^{18} \in ℤ$
87		zmulcl	$⊢ (4 \in ℤ \land 10^{18} \in ℤ) \to 4 10^{18} \in ℤ$
88	85 86 87	mp2an	$⊢ 4 10^{18} \in ℤ$
89		zltp1le	$⊢ (1 10^{1} \in ℤ \land 4 10^{18} \in ℤ) \to (1 10^{1} < 4 10^{18} \leftrightarrow 1 10^{1} + 1 \leq 4 10^{18})$
90	52 88 89	mp2an	$⊢ 1 10^{1} < 4 10^{18} \leftrightarrow 1 10^{1} + 1 \leq 4 10^{18}$
91	56	breq1i	$⊢ 1 10^{1} + 1 \leq 4 10^{18} \leftrightarrow 11 \leq 4 10^{18}$
92	90 91	bitri	$⊢ 1 10^{1} < 4 10^{18} \leftrightarrow 11 \leq 4 10^{18}$
93	84 92	mpbi	$⊢ 11 \leq 4 10^{18}$
94		eluz2	$⊢ 4 10^{18} \in ℤ_{\geq 11} \leftrightarrow (11 \in ℤ \land 4 10^{18} \in ℤ \land 11 \leq 4 10^{18})$
95	5 69 93 94	mpbir3an	$⊢ 4 10^{18} \in ℤ_{\geq 11}$
96	95	a1i	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to 4 10^{18} \in ℤ_{\geq 11}$
97		simpl	$⊢ (n \in Even \land (4 < n \land n < 4 10^{18})) \to n \in Even$
98		simprl	$⊢ (n \in Even \land (4 < n \land n < 4 10^{18})) \to 4 < n$
99		evenz	$⊢ n \in Even \to n \in ℤ$
100	99	zred	$⊢ n \in Even \to n \in ℝ$
101	68	nnrei	$⊢ 4 10^{18} \in ℝ$
102		ltle	$⊢ (n \in ℝ \land 4 10^{18} \in ℝ) \to (n < 4 10^{18} \to n \leq 4 10^{18})$
103	100 101 102	sylancl	$⊢ n \in Even \to (n < 4 10^{18} \to n \leq 4 10^{18})$
104	103	a1d	$⊢ n \in Even \to (4 < n \to (n < 4 10^{18} \to n \leq 4 10^{18}))$
105	104	imp32	$⊢ (n \in Even \land (4 < n \land n < 4 10^{18})) \to n \leq 4 10^{18}$
106		ax-bgbltosilva	$⊢ (n \in Even \land 4 < n \land n \leq 4 10^{18}) \to n \in GoldbachEven$
107	97 98 105 106	syl3anc	$⊢ (n \in Even \land (4 < n \land n < 4 10^{18})) \to n \in GoldbachEven$
108	107	ex	$⊢ n \in Even \to ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven)$
109	108	a1i	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to (n \in Even \to ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven))$
110	109	ralrimiv	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to \forall n \in Even ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven)$
111		simpl	$⊢ (d \in ℤ_{\geq 3} \land f \in RePart (d)) \to d \in ℤ_{\geq 3}$
112	111	ad2antrr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to d \in ℤ_{\geq 3}$
113		simpr	$⊢ (d \in ℤ_{\geq 3} \land f \in RePart (d)) \to f \in RePart (d)$
114	113	ad2antrr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to f \in RePart (d)$
115		simpr	$⊢ ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))$
116	115	ad2antlr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))$
117		simpl1	$⊢ ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to f (0) = 7$
118	117	ad2antlr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to f (0) = 7$
119		simpl2	$⊢ ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to f (1) = 13$
120	119	ad2antlr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to f (1) = 13$
121	6 11	decnncl	$⊢ 89 \in ℕ$
122	121	nnrei	$⊢ 89 \in ℝ$
123	15	nngt0i	$⊢ 0 < 10^{29}$
124	28 123	pm3.2i	$⊢ (10^{29} \in ℝ \land 0 < 10^{29})$
125	19 122 124	3pm3.2i	$⊢ (88 \in ℝ \land 89 \in ℝ \land (10^{29} \in ℝ \land 0 < 10^{29}))$
126		8lt9	$⊢ 8 < 9$
127	6 6 11 126	declt	$⊢ 88 < 89$
128		ltmul1a	$⊢ ((88 \in ℝ \land 89 \in ℝ \land (10^{29} \in ℝ \land 0 < 10^{29})) \land 88 < 89) \to 88 10^{29} < 89 10^{29}$
129	125 127 128	mp2an	$⊢ 88 10^{29} < 89 10^{29}$
130		breq2	$⊢ f (d) = 89 10^{29} \to (88 10^{29} < f (d) \leftrightarrow 88 10^{29} < 89 10^{29})$
131	129 130	mpbiri	$⊢ f (d) = 89 10^{29} \to 88 10^{29} < f (d)$
132	131	3ad2ant3	$⊢ (f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \to 88 10^{29} < f (d)$
133	132	adantr	$⊢ ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to 88 10^{29} < f (d)$
134	133	ad2antlr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to 88 10^{29} < f (d)$
135	121 15	nnmulcli	$⊢ 89 10^{29} \in ℕ$
136	135	nnrei	$⊢ 89 10^{29} \in ℝ$
137		eleq1	$⊢ f (d) = 89 10^{29} \to (f (d) \in ℝ \leftrightarrow 89 10^{29} \in ℝ)$
138	136 137	mpbiri	$⊢ f (d) = 89 10^{29} \to f (d) \in ℝ$
139	138	3ad2ant3	$⊢ (f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \to f (d) \in ℝ$
140	139	adantr	$⊢ ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to f (d) \in ℝ$
141	140	ad2antlr	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to f (d) \in ℝ$
142	62 96 110 112 114 116 118 120 134 141	bgoldbtbnd	$⊢ (((d \in ℤ_{\geq 3} \land f \in RePart (d)) \land ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i)))) \land (N \in Odd \land 7 < N \land N < 88 10^{29})) \to \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd)$
143	142	exp31	$⊢ (d \in ℤ_{\geq 3} \land f \in RePart (d)) \to (((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to ((N \in Odd \land 7 < N \land N < 88 10^{29}) \to \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd)))$
144	143	rexlimivv	$⊢ \exists d \in ℤ_{\geq 3} \exists f \in RePart (d) ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to ((N \in Odd \land 7 < N \land N < 88 10^{29}) \to \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd))$
145		breq2	$⊢ n = N \to (7 < n \leftrightarrow 7 < N)$
146		breq1	$⊢ n = N \to (n < 88 10^{29} \leftrightarrow N < 88 10^{29})$
147	145 146	anbi12d	$⊢ n = N \to ((7 < n \land n < 88 10^{29}) \leftrightarrow (7 < N \land N < 88 10^{29}))$
148		eleq1	$⊢ n = N \to (n \in GoldbachOdd \leftrightarrow N \in GoldbachOdd)$
149	147 148	imbi12d	$⊢ n = N \to (((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd) \leftrightarrow ((7 < N \land N < 88 10^{29}) \to N \in GoldbachOdd))$
150	149	rspcv	$⊢ N \in Odd \to (\forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd) \to ((7 < N \land N < 88 10^{29}) \to N \in GoldbachOdd))$
151	150	com23	$⊢ N \in Odd \to ((7 < N \land N < 88 10^{29}) \to (\forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd) \to N \in GoldbachOdd))$
152	151	3impib	$⊢ (N \in Odd \land 7 < N \land N < 88 10^{29}) \to (\forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd) \to N \in GoldbachOdd)$
153	144 152	sylcom	$⊢ \exists d \in ℤ_{\geq 3} \exists f \in RePart (d) ((f (0) = 7 \land f (1) = 13 \land f (d) = 89 10^{29}) \land \forall i \in (0 ..^d) (f (i) \in (ℙ ∖ \{2\}) \land f (i + 1) - f (i) < 4 10^{18} - 4 \land 4 < f (i + 1) - f (i))) \to ((N \in Odd \land 7 < N \land N < 88 10^{29}) \to N \in GoldbachOdd)$
154	1 153	ax-mp	$⊢ (N \in Odd \land 7 < N \land N < 88 10^{29}) \to N \in GoldbachOdd$

Metamath Proof Explorer

Theorem tgblthelfgott

Proof