tgoldbach

Description: The ternary Goldbach conjecture is valid. Main theorem in Helfgott p. 2. This follows from tgoldbachlt and ax-tgoldbachgt . (Contributed by AV, 2-Aug-2020) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	tgoldbach	$⊢ \forall n \in Odd (7 < n \to n \in GoldbachOdd)$

Proof

Step	Hyp	Ref	Expression
1		oddz	$⊢ n \in Odd \to n \in ℤ$
2	1	zred	$⊢ n \in Odd \to n \in ℝ$
3		10re	$⊢ 10 \in ℝ$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5		7nn	$⊢ 7 \in ℕ$
6	4 5	decnncl	$⊢ 27 \in ℕ$
7	6	nnnn0i	$⊢ 27 \in ℕ_{0}$
8		reexpcl	$⊢ (10 \in ℝ \land 27 \in ℕ_{0}) \to 10^{27} \in ℝ$
9	3 7 8	mp2an	$⊢ 10^{27} \in ℝ$
10		lelttric	$⊢ (n \in ℝ \land 10^{27} \in ℝ) \to (n \leq 10^{27} \lor 10^{27} < n)$
11	2 9 10	sylancl	$⊢ n \in Odd \to (n \leq 10^{27} \lor 10^{27} < n)$
12		tgoldbachlt	$⊢ \exists m \in ℕ (8 10^{30} < m \land \forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd))$
13		breq2	$⊢ o = n \to (7 < o \leftrightarrow 7 < n)$
14		breq1	$⊢ o = n \to (o < m \leftrightarrow n < m)$
15	13 14	anbi12d	$⊢ o = n \to ((7 < o \land o < m) \leftrightarrow (7 < n \land n < m))$
16		eleq1w	$⊢ o = n \to (o \in GoldbachOdd \leftrightarrow n \in GoldbachOdd)$
17	15 16	imbi12d	$⊢ o = n \to (((7 < o \land o < m) \to o \in GoldbachOdd) \leftrightarrow ((7 < n \land n < m) \to n \in GoldbachOdd))$
18	17	rspcv	$⊢ n \in Odd \to (\forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd) \to ((7 < n \land n < m) \to n \in GoldbachOdd))$
19	9	recni	$⊢ 10^{27} \in ℂ$
20	19	mulid2i	$⊢ 1 10^{27} = 10^{27}$
21		1re	$⊢ 1 \in ℝ$
22		8re	$⊢ 8 \in ℝ$
23	21 22	pm3.2i	$⊢ (1 \in ℝ \land 8 \in ℝ)$
24	23	a1i	$⊢ (n \in Odd \land m \in ℕ) \to (1 \in ℝ \land 8 \in ℝ)$
25		0le1	$⊢ 0 \leq 1$
26		1lt8	$⊢ 1 < 8$
27	25 26	pm3.2i	$⊢ (0 \leq 1 \land 1 < 8)$
28	27	a1i	$⊢ (n \in Odd \land m \in ℕ) \to (0 \leq 1 \land 1 < 8)$
29		3nn	$⊢ 3 \in ℕ$
30	29	decnncl2	$⊢ 30 \in ℕ$
31	30	nnnn0i	$⊢ 30 \in ℕ_{0}$
32		reexpcl	$⊢ (10 \in ℝ \land 30 \in ℕ_{0}) \to 10^{30} \in ℝ$
33	3 31 32	mp2an	$⊢ 10^{30} \in ℝ$
34	9 33	pm3.2i	$⊢ (10^{27} \in ℝ \land 10^{30} \in ℝ)$
35	34	a1i	$⊢ (n \in Odd \land m \in ℕ) \to (10^{27} \in ℝ \land 10^{30} \in ℝ)$
36		10nn0	$⊢ 10 \in ℕ_{0}$
37	36 7	nn0expcli	$⊢ 10^{27} \in ℕ_{0}$
38	37	nn0ge0i	$⊢ 0 \leq 10^{27}$
39	6	nnzi	$⊢ 27 \in ℤ$
40	30	nnzi	$⊢ 30 \in ℤ$
41	3 39 40	3pm3.2i	$⊢ (10 \in ℝ \land 27 \in ℤ \land 30 \in ℤ)$
42		1lt10	$⊢ 1 < 10$
43		3nn0	$⊢ 3 \in ℕ_{0}$
44		7nn0	$⊢ 7 \in ℕ_{0}$
45		0nn0	$⊢ 0 \in ℕ_{0}$
46		7lt10	$⊢ 7 < 10$
47		2lt3	$⊢ 2 < 3$
48	4 43 44 45 46 47	decltc	$⊢ 27 < 30$
49	42 48	pm3.2i	$⊢ (1 < 10 \land 27 < 30)$
50		ltexp2a	$⊢ ((10 \in ℝ \land 27 \in ℤ \land 30 \in ℤ) \land (1 < 10 \land 27 < 30)) \to 10^{27} < 10^{30}$
51	41 49 50	mp2an	$⊢ 10^{27} < 10^{30}$
52	38 51	pm3.2i	$⊢ (0 \leq 10^{27} \land 10^{27} < 10^{30})$
53	52	a1i	$⊢ (n \in Odd \land m \in ℕ) \to (0 \leq 10^{27} \land 10^{27} < 10^{30})$
54		ltmul12a	$⊢ (((1 \in ℝ \land 8 \in ℝ) \land (0 \leq 1 \land 1 < 8)) \land ((10^{27} \in ℝ \land 10^{30} \in ℝ) \land (0 \leq 10^{27} \land 10^{27} < 10^{30}))) \to 1 10^{27} < 8 10^{30}$
55	24 28 35 53 54	syl22anc	$⊢ (n \in Odd \land m \in ℕ) \to 1 10^{27} < 8 10^{30}$
56	20 55	eqbrtrrid	$⊢ (n \in Odd \land m \in ℕ) \to 10^{27} < 8 10^{30}$
57	9	a1i	$⊢ (n \in Odd \land m \in ℕ) \to 10^{27} \in ℝ$
58	22 33	remulcli	$⊢ 8 10^{30} \in ℝ$
59	58	a1i	$⊢ (n \in Odd \land m \in ℕ) \to 8 10^{30} \in ℝ$
60		nnre	$⊢ m \in ℕ \to m \in ℝ$
61	60	adantl	$⊢ (n \in Odd \land m \in ℕ) \to m \in ℝ$
62		lttr	$⊢ (10^{27} \in ℝ \land 8 10^{30} \in ℝ \land m \in ℝ) \to ((10^{27} < 8 10^{30} \land 8 10^{30} < m) \to 10^{27} < m)$
63	57 59 61 62	syl3anc	$⊢ (n \in Odd \land m \in ℕ) \to ((10^{27} < 8 10^{30} \land 8 10^{30} < m) \to 10^{27} < m)$
64	56 63	mpand	$⊢ (n \in Odd \land m \in ℕ) \to (8 10^{30} < m \to 10^{27} < m)$
65	64	imp	$⊢ ((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \to 10^{27} < m$
66	2	adantr	$⊢ (n \in Odd \land m \in ℕ) \to n \in ℝ$
67	66 57 61	3jca	$⊢ (n \in Odd \land m \in ℕ) \to (n \in ℝ \land 10^{27} \in ℝ \land m \in ℝ)$
68	67	adantr	$⊢ ((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \to (n \in ℝ \land 10^{27} \in ℝ \land m \in ℝ)$
69		lelttr	$⊢ (n \in ℝ \land 10^{27} \in ℝ \land m \in ℝ) \to ((n \leq 10^{27} \land 10^{27} < m) \to n < m)$
70	68 69	syl	$⊢ ((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \to ((n \leq 10^{27} \land 10^{27} < m) \to n < m)$
71	65 70	mpan2d	$⊢ ((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \to (n \leq 10^{27} \to n < m)$
72	71	imp	$⊢ (((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \land n \leq 10^{27}) \to n < m$
73	72	anim1i	$⊢ ((((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \land n \leq 10^{27}) \land 7 < n) \to (n < m \land 7 < n)$
74	73	ancomd	$⊢ ((((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \land n \leq 10^{27}) \land 7 < n) \to (7 < n \land n < m)$
75		pm2.27	$⊢ (7 < n \land n < m) \to (((7 < n \land n < m) \to n \in GoldbachOdd) \to n \in GoldbachOdd)$
76	74 75	syl	$⊢ ((((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \land n \leq 10^{27}) \land 7 < n) \to (((7 < n \land n < m) \to n \in GoldbachOdd) \to n \in GoldbachOdd)$
77	76	ex	$⊢ (((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \land n \leq 10^{27}) \to (7 < n \to (((7 < n \land n < m) \to n \in GoldbachOdd) \to n \in GoldbachOdd))$
78	77	com23	$⊢ (((n \in Odd \land m \in ℕ) \land 8 10^{30} < m) \land n \leq 10^{27}) \to (((7 < n \land n < m) \to n \in GoldbachOdd) \to (7 < n \to n \in GoldbachOdd))$
79	78	exp41	$⊢ n \in Odd \to (m \in ℕ \to (8 10^{30} < m \to (n \leq 10^{27} \to (((7 < n \land n < m) \to n \in GoldbachOdd) \to (7 < n \to n \in GoldbachOdd)))))$
80	79	com25	$⊢ n \in Odd \to (((7 < n \land n < m) \to n \in GoldbachOdd) \to (8 10^{30} < m \to (n \leq 10^{27} \to (m \in ℕ \to (7 < n \to n \in GoldbachOdd)))))$
81	18 80	syld	$⊢ n \in Odd \to (\forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd) \to (8 10^{30} < m \to (n \leq 10^{27} \to (m \in ℕ \to (7 < n \to n \in GoldbachOdd)))))$
82	81	com15	$⊢ m \in ℕ \to (\forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd) \to (8 10^{30} < m \to (n \leq 10^{27} \to (n \in Odd \to (7 < n \to n \in GoldbachOdd)))))$
83	82	com23	$⊢ m \in ℕ \to (8 10^{30} < m \to (\forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd) \to (n \leq 10^{27} \to (n \in Odd \to (7 < n \to n \in GoldbachOdd)))))$
84	83	imp32	$⊢ (m \in ℕ \land (8 10^{30} < m \land \forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd))) \to (n \leq 10^{27} \to (n \in Odd \to (7 < n \to n \in GoldbachOdd)))$
85	84	rexlimiva	$⊢ \exists m \in ℕ (8 10^{30} < m \land \forall o \in Odd ((7 < o \land o < m) \to o \in GoldbachOdd)) \to (n \leq 10^{27} \to (n \in Odd \to (7 < n \to n \in GoldbachOdd)))$
86	12 85	ax-mp	$⊢ n \leq 10^{27} \to (n \in Odd \to (7 < n \to n \in GoldbachOdd))$
87		tgoldbachgtALTV	$⊢ \exists m \in ℕ (m \leq 10^{27} \land \forall o \in Odd (m < o \to o \in GoldbachOdd))$
88		breq2	$⊢ o = n \to (m < o \leftrightarrow m < n)$
89	88 16	imbi12d	$⊢ o = n \to ((m < o \to o \in GoldbachOdd) \leftrightarrow (m < n \to n \in GoldbachOdd))$
90	89	rspcv	$⊢ n \in Odd \to (\forall o \in Odd (m < o \to o \in GoldbachOdd) \to (m < n \to n \in GoldbachOdd))$
91		lelttr	$⊢ (m \in ℝ \land 10^{27} \in ℝ \land n \in ℝ) \to ((m \leq 10^{27} \land 10^{27} < n) \to m < n)$
92	61 57 66 91	syl3anc	$⊢ (n \in Odd \land m \in ℕ) \to ((m \leq 10^{27} \land 10^{27} < n) \to m < n)$
93	92	expcomd	$⊢ (n \in Odd \land m \in ℕ) \to (10^{27} < n \to (m \leq 10^{27} \to m < n))$
94	93	ex	$⊢ n \in Odd \to (m \in ℕ \to (10^{27} < n \to (m \leq 10^{27} \to m < n)))$
95	94	com23	$⊢ n \in Odd \to (10^{27} < n \to (m \in ℕ \to (m \leq 10^{27} \to m < n)))$
96	95	imp43	$⊢ ((n \in Odd \land 10^{27} < n) \land (m \in ℕ \land m \leq 10^{27})) \to m < n$
97		pm2.27	$⊢ m < n \to ((m < n \to n \in GoldbachOdd) \to n \in GoldbachOdd)$
98	96 97	syl	$⊢ ((n \in Odd \land 10^{27} < n) \land (m \in ℕ \land m \leq 10^{27})) \to ((m < n \to n \in GoldbachOdd) \to n \in GoldbachOdd)$
99	98	a1dd	$⊢ ((n \in Odd \land 10^{27} < n) \land (m \in ℕ \land m \leq 10^{27})) \to ((m < n \to n \in GoldbachOdd) \to (7 < n \to n \in GoldbachOdd))$
100	99	ex	$⊢ (n \in Odd \land 10^{27} < n) \to ((m \in ℕ \land m \leq 10^{27}) \to ((m < n \to n \in GoldbachOdd) \to (7 < n \to n \in GoldbachOdd)))$
101	100	com23	$⊢ (n \in Odd \land 10^{27} < n) \to ((m < n \to n \in GoldbachOdd) \to ((m \in ℕ \land m \leq 10^{27}) \to (7 < n \to n \in GoldbachOdd)))$
102	101	ex	$⊢ n \in Odd \to (10^{27} < n \to ((m < n \to n \in GoldbachOdd) \to ((m \in ℕ \land m \leq 10^{27}) \to (7 < n \to n \in GoldbachOdd))))$
103	102	com23	$⊢ n \in Odd \to ((m < n \to n \in GoldbachOdd) \to (10^{27} < n \to ((m \in ℕ \land m \leq 10^{27}) \to (7 < n \to n \in GoldbachOdd))))$
104	90 103	syld	$⊢ n \in Odd \to (\forall o \in Odd (m < o \to o \in GoldbachOdd) \to (10^{27} < n \to ((m \in ℕ \land m \leq 10^{27}) \to (7 < n \to n \in GoldbachOdd))))$
105	104	com14	$⊢ (m \in ℕ \land m \leq 10^{27}) \to (\forall o \in Odd (m < o \to o \in GoldbachOdd) \to (10^{27} < n \to (n \in Odd \to (7 < n \to n \in GoldbachOdd))))$
106	105	impr	$⊢ (m \in ℕ \land (m \leq 10^{27} \land \forall o \in Odd (m < o \to o \in GoldbachOdd))) \to (10^{27} < n \to (n \in Odd \to (7 < n \to n \in GoldbachOdd)))$
107	106	rexlimiva	$⊢ \exists m \in ℕ (m \leq 10^{27} \land \forall o \in Odd (m < o \to o \in GoldbachOdd)) \to (10^{27} < n \to (n \in Odd \to (7 < n \to n \in GoldbachOdd)))$
108	87 107	ax-mp	$⊢ 10^{27} < n \to (n \in Odd \to (7 < n \to n \in GoldbachOdd))$
109	86 108	jaoi	$⊢ (n \leq 10^{27} \lor 10^{27} < n) \to (n \in Odd \to (7 < n \to n \in GoldbachOdd))$
110	11 109	mpcom	$⊢ n \in Odd \to (7 < n \to n \in GoldbachOdd)$
111	110	rgen	$⊢ \forall n \in Odd (7 < n \to n \in GoldbachOdd)$

Metamath Proof Explorer

Theorem tgoldbach

Proof