bgoldbachlt

Description: The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big m ). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva . (Contributed by AV, 3-Aug-2020) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Assertion	bgoldbachlt	$⊢ \exists m \in ℕ (4 10^{18} \leq m \land \forall n \in Even ((4 < n \land n < m) \to n \in GoldbachEven))$

Proof

Step	Hyp	Ref	Expression
1		4nn	$⊢ 4 \in ℕ$
2		10nn	$⊢ 10 \in ℕ$
3		1nn0	$⊢ 1 \in ℕ_{0}$
4		8nn0	$⊢ 8 \in ℕ_{0}$
5	3 4	deccl	$⊢ 18 \in ℕ_{0}$
6		nnexpcl	$⊢ (10 \in ℕ \land 18 \in ℕ_{0}) \to 10^{18} \in ℕ$
7	2 5 6	mp2an	$⊢ 10^{18} \in ℕ$
8	1 7	nnmulcli	$⊢ 4 10^{18} \in ℕ$
9		id	$⊢ 4 10^{18} \in ℕ \to 4 10^{18} \in ℕ$
10		breq2	$⊢ m = 4 10^{18} \to (4 10^{18} \leq m \leftrightarrow 4 10^{18} \leq 4 10^{18})$
11		breq2	$⊢ m = 4 10^{18} \to (n < m \leftrightarrow n < 4 10^{18})$
12	11	anbi2d	$⊢ m = 4 10^{18} \to ((4 < n \land n < m) \leftrightarrow (4 < n \land n < 4 10^{18}))$
13	12	imbi1d	$⊢ m = 4 10^{18} \to (((4 < n \land n < m) \to n \in GoldbachEven) \leftrightarrow ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven))$
14	13	ralbidv	$⊢ m = 4 10^{18} \to (\forall n \in Even ((4 < n \land n < m) \to n \in GoldbachEven) \leftrightarrow \forall n \in Even ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven))$
15	10 14	anbi12d	$⊢ m = 4 10^{18} \to ((4 10^{18} \leq m \land \forall n \in Even ((4 < n \land n < m) \to n \in GoldbachEven)) \leftrightarrow (4 10^{18} \leq 4 10^{18} \land \forall n \in Even ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven)))$
16	15	adantl	$⊢ (4 10^{18} \in ℕ \land m = 4 10^{18}) \to ((4 10^{18} \leq m \land \forall n \in Even ((4 < n \land n < m) \to n \in GoldbachEven)) \leftrightarrow (4 10^{18} \leq 4 10^{18} \land \forall n \in Even ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven)))$
17		nnre	$⊢ 4 10^{18} \in ℕ \to 4 10^{18} \in ℝ$
18	17	leidd	$⊢ 4 10^{18} \in ℕ \to 4 10^{18} \leq 4 10^{18}$
19		simplr	$⊢ ((4 10^{18} \in ℕ \land n \in Even) \land (4 < n \land n < 4 10^{18})) \to n \in Even$
20		simprl	$⊢ ((4 10^{18} \in ℕ \land n \in Even) \land (4 < n \land n < 4 10^{18})) \to 4 < n$
21		evenz	$⊢ n \in Even \to n \in ℤ$
22	21	zred	$⊢ n \in Even \to n \in ℝ$
23		ltle	$⊢ (n \in ℝ \land 4 10^{18} \in ℝ) \to (n < 4 10^{18} \to n \leq 4 10^{18})$
24	22 17 23	syl2anr	$⊢ (4 10^{18} \in ℕ \land n \in Even) \to (n < 4 10^{18} \to n \leq 4 10^{18})$
25	24	a1d	$⊢ (4 10^{18} \in ℕ \land n \in Even) \to (4 < n \to (n < 4 10^{18} \to n \leq 4 10^{18}))$
26	25	imp32	$⊢ ((4 10^{18} \in ℕ \land n \in Even) \land (4 < n \land n < 4 10^{18})) \to n \leq 4 10^{18}$
27		ax-bgbltosilva	$⊢ (n \in Even \land 4 < n \land n \leq 4 10^{18}) \to n \in GoldbachEven$
28	19 20 26 27	syl3anc	$⊢ ((4 10^{18} \in ℕ \land n \in Even) \land (4 < n \land n < 4 10^{18})) \to n \in GoldbachEven$
29	28	ex	$⊢ (4 10^{18} \in ℕ \land n \in Even) \to ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven)$
30	29	ralrimiva	$⊢ 4 10^{18} \in ℕ \to \forall n \in Even ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven)$
31	18 30	jca	$⊢ 4 10^{18} \in ℕ \to (4 10^{18} \leq 4 10^{18} \land \forall n \in Even ((4 < n \land n < 4 10^{18}) \to n \in GoldbachEven))$
32	9 16 31	rspcedvd	$⊢ 4 10^{18} \in ℕ \to \exists m \in ℕ (4 10^{18} \leq m \land \forall n \in Even ((4 < n \land n < m) \to n \in GoldbachEven))$
33	8 32	ax-mp	$⊢ \exists m \in ℕ (4 10^{18} \leq m \land \forall n \in Even ((4 < n \land n < m) \to n \in GoldbachEven))$

Metamath Proof Explorer

Theorem bgoldbachlt

Proof