tgoldbachlt

Description: The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big m greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott . (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	tgoldbachlt	$⊢ \exists m \in ℕ (8 10^{30} < m \land \forall n \in Odd ((7 < n \land n < m) \to n \in GoldbachOdd))$

Proof

Step	Hyp	Ref	Expression
1		8nn0	$⊢ 8 \in ℕ_{0}$
2		8nn	$⊢ 8 \in ℕ$
3	1 2	decnncl	$⊢ 88 \in ℕ$
4		10nn	$⊢ 10 \in ℕ$
5		2nn0	$⊢ 2 \in ℕ_{0}$
6		9nn0	$⊢ 9 \in ℕ_{0}$
7	5 6	deccl	$⊢ 29 \in ℕ_{0}$
8		nnexpcl	$⊢ (10 \in ℕ \land 29 \in ℕ_{0}) \to 10^{29} \in ℕ$
9	4 7 8	mp2an	$⊢ 10^{29} \in ℕ$
10	3 9	nnmulcli	$⊢ 88 10^{29} \in ℕ$
11		id	$⊢ 88 10^{29} \in ℕ \to 88 10^{29} \in ℕ$
12		breq2	$⊢ m = 88 10^{29} \to (8 10^{30} < m \leftrightarrow 8 10^{30} < 88 10^{29})$
13		breq2	$⊢ m = 88 10^{29} \to (n < m \leftrightarrow n < 88 10^{29})$
14	13	anbi2d	$⊢ m = 88 10^{29} \to ((7 < n \land n < m) \leftrightarrow (7 < n \land n < 88 10^{29}))$
15	14	imbi1d	$⊢ m = 88 10^{29} \to (((7 < n \land n < m) \to n \in GoldbachOdd) \leftrightarrow ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd))$
16	15	ralbidv	$⊢ m = 88 10^{29} \to (\forall n \in Odd ((7 < n \land n < m) \to n \in GoldbachOdd) \leftrightarrow \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd))$
17	12 16	anbi12d	$⊢ m = 88 10^{29} \to ((8 10^{30} < m \land \forall n \in Odd ((7 < n \land n < m) \to n \in GoldbachOdd)) \leftrightarrow (8 10^{30} < 88 10^{29} \land \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd)))$
18	17	adantl	$⊢ (88 10^{29} \in ℕ \land m = 88 10^{29}) \to ((8 10^{30} < m \land \forall n \in Odd ((7 < n \land n < m) \to n \in GoldbachOdd)) \leftrightarrow (8 10^{30} < 88 10^{29} \land \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd)))$
19		simplr	$⊢ ((88 10^{29} \in ℕ \land n \in Odd) \land (7 < n \land n < 88 10^{29})) \to n \in Odd$
20		simprl	$⊢ ((88 10^{29} \in ℕ \land n \in Odd) \land (7 < n \land n < 88 10^{29})) \to 7 < n$
21		simprr	$⊢ ((88 10^{29} \in ℕ \land n \in Odd) \land (7 < n \land n < 88 10^{29})) \to n < 88 10^{29}$
22		tgblthelfgott	$⊢ (n \in Odd \land 7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd$
23	19 20 21 22	syl3anc	$⊢ ((88 10^{29} \in ℕ \land n \in Odd) \land (7 < n \land n < 88 10^{29})) \to n \in GoldbachOdd$
24	23	ex	$⊢ (88 10^{29} \in ℕ \land n \in Odd) \to ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd)$
25	24	ralrimiva	$⊢ 88 10^{29} \in ℕ \to \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd)$
26	2 9	nnmulcli	$⊢ 8 10^{29} \in ℕ$
27	26	nngt0i	$⊢ 0 < 8 10^{29}$
28	26	nnrei	$⊢ 8 10^{29} \in ℝ$
29		3nn0	$⊢ 3 \in ℕ_{0}$
30		0nn0	$⊢ 0 \in ℕ_{0}$
31	29 30	deccl	$⊢ 30 \in ℕ_{0}$
32		nnexpcl	$⊢ (10 \in ℕ \land 30 \in ℕ_{0}) \to 10^{30} \in ℕ$
33	4 31 32	mp2an	$⊢ 10^{30} \in ℕ$
34	2 33	nnmulcli	$⊢ 8 10^{30} \in ℕ$
35	34	nnrei	$⊢ 8 10^{30} \in ℝ$
36	28 35	ltaddposi	$⊢ 0 < 8 10^{29} \leftrightarrow 8 10^{30} < 8 10^{30} + 8 10^{29}$
37	27 36	mpbi	$⊢ 8 10^{30} < 8 10^{30} + 8 10^{29}$
38		dfdec10	$⊢ 88 = 10 \cdot 8 + 8$
39	38	oveq1i	$⊢ 88 10^{29} = (10 \cdot 8 + 8) 10^{29}$
40	4 2	nnmulcli	$⊢ 10 \cdot 8 \in ℕ$
41	40	nncni	$⊢ 10 \cdot 8 \in ℂ$
42		8cn	$⊢ 8 \in ℂ$
43	9	nncni	$⊢ 10^{29} \in ℂ$
44	41 42 43	adddiri	$⊢ (10 \cdot 8 + 8) 10^{29} = 10 \cdot 8 10^{29} + 8 10^{29}$
45	41 43	mulcomi	$⊢ 10 \cdot 8 10^{29} = 10^{29} 10 \cdot 8$
46	4	nncni	$⊢ 10 \in ℂ$
47	43 46 42	mulassi	$⊢ 10^{29} \cdot 10 \cdot 8 = 10^{29} 10 \cdot 8$
48		nncn	$⊢ 10 \in ℕ \to 10 \in ℂ$
49	7	a1i	$⊢ 10 \in ℕ \to 29 \in ℕ_{0}$
50	48 49	expp1d	$⊢ 10 \in ℕ \to 10^{29 + 1} = 10^{29} \cdot 10$
51	4 50	ax-mp	$⊢ 10^{29 + 1} = 10^{29} \cdot 10$
52	51	eqcomi	$⊢ 10^{29} \cdot 10 = 10^{29 + 1}$
53	52	oveq1i	$⊢ 10^{29} \cdot 10 \cdot 8 = 10^{29 + 1} \cdot 8$
54	45 47 53	3eqtr2i	$⊢ 10 \cdot 8 10^{29} = 10^{29 + 1} \cdot 8$
55	54	oveq1i	$⊢ 10 \cdot 8 10^{29} + 8 10^{29} = 10^{29 + 1} \cdot 8 + 8 10^{29}$
56		2p1e3	$⊢ 2 + 1 = 3$
57		eqid	$⊢ 29 = 29$
58	5 56 57	decsucc	$⊢ 29 + 1 = 30$
59	58	oveq2i	$⊢ 10^{29 + 1} = 10^{30}$
60	59	oveq1i	$⊢ 10^{29 + 1} \cdot 8 = 10^{30} \cdot 8$
61	60	oveq1i	$⊢ 10^{29 + 1} \cdot 8 + 8 10^{29} = 10^{30} \cdot 8 + 8 10^{29}$
62	33	nncni	$⊢ 10^{30} \in ℂ$
63		mulcom	$⊢ (10^{30} \in ℂ \land 8 \in ℂ) \to 10^{30} \cdot 8 = 8 10^{30}$
64	63	oveq1d	$⊢ (10^{30} \in ℂ \land 8 \in ℂ) \to 10^{30} \cdot 8 + 8 10^{29} = 8 10^{30} + 8 10^{29}$
65	62 42 64	mp2an	$⊢ 10^{30} \cdot 8 + 8 10^{29} = 8 10^{30} + 8 10^{29}$
66	55 61 65	3eqtri	$⊢ 10 \cdot 8 10^{29} + 8 10^{29} = 8 10^{30} + 8 10^{29}$
67	39 44 66	3eqtri	$⊢ 88 10^{29} = 8 10^{30} + 8 10^{29}$
68	37 67	breqtrri	$⊢ 8 10^{30} < 88 10^{29}$
69	25 68	jctil	$⊢ 88 10^{29} \in ℕ \to (8 10^{30} < 88 10^{29} \land \forall n \in Odd ((7 < n \land n < 88 10^{29}) \to n \in GoldbachOdd))$
70	11 18 69	rspcedvd	$⊢ 88 10^{29} \in ℕ \to \exists m \in ℕ (8 10^{30} < m \land \forall n \in Odd ((7 < n \land n < m) \to n \in GoldbachOdd))$
71	10 70	ax-mp	$⊢ \exists m \in ℕ (8 10^{30} < m \land \forall n \in Odd ((7 < n \land n < m) \to n \in GoldbachOdd))$

Metamath Proof Explorer

Theorem tgoldbachlt

Proof