gbowgt5

Description: Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020)

		Ref	Expression
	Assertion	gbowgt5	$⊢ Z \in GoldbachOddW \to 5 < Z$

Proof

Step	Hyp	Ref	Expression
1		isgbow	$⊢ Z \in GoldbachOddW \leftrightarrow (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r)$
2		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
3		eluz2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land p \in ℤ \land 2 \leq p)$
4	2 3	sylib	$⊢ p \in ℙ \to (2 \in ℤ \land p \in ℤ \land 2 \leq p)$
5		prmuz2	$⊢ q \in ℙ \to q \in ℤ_{\geq 2}$
6		eluz2	$⊢ q \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land q \in ℤ \land 2 \leq q)$
7	5 6	sylib	$⊢ q \in ℙ \to (2 \in ℤ \land q \in ℤ \land 2 \leq q)$
8	4 7	anim12i	$⊢ (p \in ℙ \land q \in ℙ) \to ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q))$
9		prmuz2	$⊢ r \in ℙ \to r \in ℤ_{\geq 2}$
10		eluz2	$⊢ r \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land r \in ℤ \land 2 \leq r)$
11	9 10	sylib	$⊢ r \in ℙ \to (2 \in ℤ \land r \in ℤ \land 2 \leq r)$
12		zre	$⊢ p \in ℤ \to p \in ℝ$
13	12	3ad2ant2	$⊢ (2 \in ℤ \land p \in ℤ \land 2 \leq p) \to p \in ℝ$
14		zre	$⊢ q \in ℤ \to q \in ℝ$
15	14	3ad2ant2	$⊢ (2 \in ℤ \land q \in ℤ \land 2 \leq q) \to q \in ℝ$
16	13 15	anim12i	$⊢ ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \to (p \in ℝ \land q \in ℝ)$
17		2re	$⊢ 2 \in ℝ$
18	17 17	pm3.2i	$⊢ (2 \in ℝ \land 2 \in ℝ)$
19	16 18	jctil	$⊢ ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \to ((2 \in ℝ \land 2 \in ℝ) \land (p \in ℝ \land q \in ℝ))$
20		simp3	$⊢ (2 \in ℤ \land p \in ℤ \land 2 \leq p) \to 2 \leq p$
21		simp3	$⊢ (2 \in ℤ \land q \in ℤ \land 2 \leq q) \to 2 \leq q$
22	20 21	anim12i	$⊢ ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \to (2 \leq p \land 2 \leq q)$
23		le2add	$⊢ ((2 \in ℝ \land 2 \in ℝ) \land (p \in ℝ \land q \in ℝ)) \to ((2 \leq p \land 2 \leq q) \to 2 + 2 \leq p + q)$
24	19 22 23	sylc	$⊢ ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \to 2 + 2 \leq p + q$
25		2p2e4	$⊢ 2 + 2 = 4$
26	25	breq1i	$⊢ 2 + 2 \leq p + q \leftrightarrow 4 \leq p + q$
27		zaddcl	$⊢ (p \in ℤ \land q \in ℤ) \to p + q \in ℤ$
28	27	zred	$⊢ (p \in ℤ \land q \in ℤ) \to p + q \in ℝ$
29	28	adantr	$⊢ ((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \to p + q \in ℝ$
30		zre	$⊢ r \in ℤ \to r \in ℝ$
31	30	3ad2ant2	$⊢ (2 \in ℤ \land r \in ℤ \land 2 \leq r) \to r \in ℝ$
32	29 31	anim12i	$⊢ (((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to (p + q \in ℝ \land r \in ℝ)$
33		4re	$⊢ 4 \in ℝ$
34	33 17	pm3.2i	$⊢ (4 \in ℝ \land 2 \in ℝ)$
35	32 34	jctil	$⊢ (((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to ((4 \in ℝ \land 2 \in ℝ) \land (p + q \in ℝ \land r \in ℝ))$
36		simpr	$⊢ ((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \to 4 \leq p + q$
37		simp3	$⊢ (2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 2 \leq r$
38	36 37	anim12i	$⊢ (((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to (4 \leq p + q \land 2 \leq r)$
39		le2add	$⊢ ((4 \in ℝ \land 2 \in ℝ) \land (p + q \in ℝ \land r \in ℝ)) \to ((4 \leq p + q \land 2 \leq r) \to 4 + 2 \leq p + q + r)$
40	35 38 39	sylc	$⊢ (((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to 4 + 2 \leq p + q + r$
41		4p2e6	$⊢ 4 + 2 = 6$
42	41	breq1i	$⊢ 4 + 2 \leq p + q + r \leftrightarrow 6 \leq p + q + r$
43		5lt6	$⊢ 5 < 6$
44		5re	$⊢ 5 \in ℝ$
45	44	a1i	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to 5 \in ℝ$
46		6re	$⊢ 6 \in ℝ$
47	46	a1i	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to 6 \in ℝ$
48	27	adantr	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to p + q \in ℤ$
49		simpr	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to r \in ℤ$
50	48 49	zaddcld	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to p + q + r \in ℤ$
51	50	zred	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to p + q + r \in ℝ$
52		ltletr	$⊢ (5 \in ℝ \land 6 \in ℝ \land p + q + r \in ℝ) \to ((5 < 6 \land 6 \leq p + q + r) \to 5 < p + q + r)$
53	45 47 51 52	syl3anc	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to ((5 < 6 \land 6 \leq p + q + r) \to 5 < p + q + r)$
54	43 53	mpani	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to (6 \leq p + q + r \to 5 < p + q + r)$
55	42 54	syl5bi	$⊢ ((p \in ℤ \land q \in ℤ) \land r \in ℤ) \to (4 + 2 \leq p + q + r \to 5 < p + q + r)$
56	55	expcom	$⊢ r \in ℤ \to ((p \in ℤ \land q \in ℤ) \to (4 + 2 \leq p + q + r \to 5 < p + q + r))$
57	56	3ad2ant2	$⊢ (2 \in ℤ \land r \in ℤ \land 2 \leq r) \to ((p \in ℤ \land q \in ℤ) \to (4 + 2 \leq p + q + r \to 5 < p + q + r))$
58	57	com12	$⊢ (p \in ℤ \land q \in ℤ) \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to (4 + 2 \leq p + q + r \to 5 < p + q + r))$
59	58	adantr	$⊢ ((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to (4 + 2 \leq p + q + r \to 5 < p + q + r))$
60	59	imp	$⊢ (((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to (4 + 2 \leq p + q + r \to 5 < p + q + r)$
61	40 60	mpd	$⊢ (((p \in ℤ \land q \in ℤ) \land 4 \leq p + q) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to 5 < p + q + r$
62	61	exp31	$⊢ (p \in ℤ \land q \in ℤ) \to (4 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r))$
63	26 62	syl5bi	$⊢ (p \in ℤ \land q \in ℤ) \to (2 + 2 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r))$
64	63	expcom	$⊢ q \in ℤ \to (p \in ℤ \to (2 + 2 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r)))$
65	64	3ad2ant2	$⊢ (2 \in ℤ \land q \in ℤ \land 2 \leq q) \to (p \in ℤ \to (2 + 2 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r)))$
66	65	com12	$⊢ p \in ℤ \to ((2 \in ℤ \land q \in ℤ \land 2 \leq q) \to (2 + 2 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r)))$
67	66	3ad2ant2	$⊢ (2 \in ℤ \land p \in ℤ \land 2 \leq p) \to ((2 \in ℤ \land q \in ℤ \land 2 \leq q) \to (2 + 2 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r)))$
68	67	imp	$⊢ ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \to (2 + 2 \leq p + q \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r))$
69	24 68	mpd	$⊢ ((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \to ((2 \in ℤ \land r \in ℤ \land 2 \leq r) \to 5 < p + q + r)$
70	69	imp	$⊢ (((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to 5 < p + q + r$
71		breq2	$⊢ Z = p + q + r \to (5 < Z \leftrightarrow 5 < p + q + r)$
72	70 71	syl5ibrcom	$⊢ (((2 \in ℤ \land p \in ℤ \land 2 \leq p) \land (2 \in ℤ \land q \in ℤ \land 2 \leq q)) \land (2 \in ℤ \land r \in ℤ \land 2 \leq r)) \to (Z = p + q + r \to 5 < Z)$
73	8 11 72	syl2an	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (Z = p + q + r \to 5 < Z)$
74	73	rexlimdva	$⊢ (p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ Z = p + q + r \to 5 < Z)$
75	74	adantl	$⊢ (Z \in Odd \land (p \in ℙ \land q \in ℙ)) \to (\exists r \in ℙ Z = p + q + r \to 5 < Z)$
76	75	rexlimdvva	$⊢ Z \in Odd \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r \to 5 < Z)$
77	76	imp	$⊢ (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r) \to 5 < Z$
78	1 77	sylbi	$⊢ Z \in GoldbachOddW \to 5 < Z$

Metamath Proof Explorer

Theorem gbowgt5

Proof