evengpoap3

Description: If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020) (Proof shortened by AV, 15-Sep-2021)

		Ref	Expression
	Assertion	evengpoap3	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to ((N \in ℤ_{\geq 12} \land N \in Even) \to \exists o \in GoldbachOdd N = o + 3)$

Proof

Step	Hyp	Ref	Expression
1		3odd	$⊢ 3 \in Odd$
2	1	a1i	$⊢ N \in ℤ_{\geq 12} \to 3 \in Odd$
3	2	anim1i	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to (3 \in Odd \land N \in Even)$
4	3	ancomd	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to (N \in Even \land 3 \in Odd)$
5		emoo	$⊢ (N \in Even \land 3 \in Odd) \to N - 3 \in Odd$
6	4 5	syl	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to N - 3 \in Odd$
7		breq2	$⊢ m = N - 3 \to (7 < m \leftrightarrow 7 < N - 3)$
8		eleq1	$⊢ m = N - 3 \to (m \in GoldbachOdd \leftrightarrow N - 3 \in GoldbachOdd)$
9	7 8	imbi12d	$⊢ m = N - 3 \to ((7 < m \to m \in GoldbachOdd) \leftrightarrow (7 < N - 3 \to N - 3 \in GoldbachOdd))$
10	9	adantl	$⊢ ((N \in ℤ_{\geq 12} \land N \in Even) \land m = N - 3) \to ((7 < m \to m \in GoldbachOdd) \leftrightarrow (7 < N - 3 \to N - 3 \in GoldbachOdd))$
11	6 10	rspcdv	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to (\forall m \in Odd (7 < m \to m \in GoldbachOdd) \to (7 < N - 3 \to N - 3 \in GoldbachOdd))$
12		eluz2	$⊢ N \in ℤ_{\geq 12} \leftrightarrow (12 \in ℤ \land N \in ℤ \land 12 \leq N)$
13		7p3e10	$⊢ 7 + 3 = 10$
14		1nn0	$⊢ 1 \in ℕ_{0}$
15		0nn0	$⊢ 0 \in ℕ_{0}$
16		2nn	$⊢ 2 \in ℕ$
17		2pos	$⊢ 0 < 2$
18	14 15 16 17	declt	$⊢ 10 < 12$
19	13 18	eqbrtri	$⊢ 7 + 3 < 12$
20		7re	$⊢ 7 \in ℝ$
21		3re	$⊢ 3 \in ℝ$
22	20 21	readdcli	$⊢ 7 + 3 \in ℝ$
23		2nn0	$⊢ 2 \in ℕ_{0}$
24	14 23	deccl	$⊢ 12 \in ℕ_{0}$
25	24	nn0rei	$⊢ 12 \in ℝ$
26		zre	$⊢ N \in ℤ \to N \in ℝ$
27		ltletr	$⊢ (7 + 3 \in ℝ \land 12 \in ℝ \land N \in ℝ) \to ((7 + 3 < 12 \land 12 \leq N) \to 7 + 3 < N)$
28	22 25 26 27	mp3an12i	$⊢ N \in ℤ \to ((7 + 3 < 12 \land 12 \leq N) \to 7 + 3 < N)$
29	19 28	mpani	$⊢ N \in ℤ \to (12 \leq N \to 7 + 3 < N)$
30	29	imp	$⊢ (N \in ℤ \land 12 \leq N) \to 7 + 3 < N$
31	30	3adant1	$⊢ (12 \in ℤ \land N \in ℤ \land 12 \leq N) \to 7 + 3 < N$
32	20	a1i	$⊢ (12 \in ℤ \land N \in ℤ \land 12 \leq N) \to 7 \in ℝ$
33	21	a1i	$⊢ (12 \in ℤ \land N \in ℤ \land 12 \leq N) \to 3 \in ℝ$
34	26	3ad2ant2	$⊢ (12 \in ℤ \land N \in ℤ \land 12 \leq N) \to N \in ℝ$
35	32 33 34	ltaddsubd	$⊢ (12 \in ℤ \land N \in ℤ \land 12 \leq N) \to (7 + 3 < N \leftrightarrow 7 < N - 3)$
36	31 35	mpbid	$⊢ (12 \in ℤ \land N \in ℤ \land 12 \leq N) \to 7 < N - 3$
37	12 36	sylbi	$⊢ N \in ℤ_{\geq 12} \to 7 < N - 3$
38	37	adantr	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to 7 < N - 3$
39		simpr	$⊢ ((N \in ℤ_{\geq 12} \land N \in Even) \land N - 3 \in GoldbachOdd) \to N - 3 \in GoldbachOdd$
40		oveq1	$⊢ o = N - 3 \to o + 3 = N - 3 + 3$
41	40	eqeq2d	$⊢ o = N - 3 \to (N = o + 3 \leftrightarrow N = N - 3 + 3)$
42	41	adantl	$⊢ (((N \in ℤ_{\geq 12} \land N \in Even) \land N - 3 \in GoldbachOdd) \land o = N - 3) \to (N = o + 3 \leftrightarrow N = N - 3 + 3)$
43		eluzelcn	$⊢ N \in ℤ_{\geq 12} \to N \in ℂ$
44		3cn	$⊢ 3 \in ℂ$
45	43 44	jctir	$⊢ N \in ℤ_{\geq 12} \to (N \in ℂ \land 3 \in ℂ)$
46	45	adantr	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to (N \in ℂ \land 3 \in ℂ)$
47	46	adantr	$⊢ ((N \in ℤ_{\geq 12} \land N \in Even) \land N - 3 \in GoldbachOdd) \to (N \in ℂ \land 3 \in ℂ)$
48		npcan	$⊢ (N \in ℂ \land 3 \in ℂ) \to N - 3 + 3 = N$
49	48	eqcomd	$⊢ (N \in ℂ \land 3 \in ℂ) \to N = N - 3 + 3$
50	47 49	syl	$⊢ ((N \in ℤ_{\geq 12} \land N \in Even) \land N - 3 \in GoldbachOdd) \to N = N - 3 + 3$
51	39 42 50	rspcedvd	$⊢ ((N \in ℤ_{\geq 12} \land N \in Even) \land N - 3 \in GoldbachOdd) \to \exists o \in GoldbachOdd N = o + 3$
52	51	ex	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to (N - 3 \in GoldbachOdd \to \exists o \in GoldbachOdd N = o + 3)$
53	38 52	embantd	$⊢ (N \in ℤ_{\geq 12} \land N \in Even) \to ((7 < N - 3 \to N - 3 \in GoldbachOdd) \to \exists o \in GoldbachOdd N = o + 3)$
54	11 53	syldc	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to ((N \in ℤ_{\geq 12} \land N \in Even) \to \exists o \in GoldbachOdd N = o + 3)$

Metamath Proof Explorer

Theorem evengpoap3

Proof