Theorem gbowge7

Description: Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow , this bound is strict. (Contributed by AV, 20-Jul-2020)

	Ref	Expression
Assertion	gbowge7	⊢ ( 𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		gbowgt5	⊢ ( 𝑍 ∈ GoldbachOddW → 5 < 𝑍 )
2		gbowpos	⊢ ( 𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ )
3		5nn	⊢ 5 ∈ ℕ
4	3	nnzi	⊢ 5 ∈ ℤ
5		nnz	⊢ ( 𝑍 ∈ ℕ → 𝑍 ∈ ℤ )
6		zltp1le	⊢ ( ( 5 ∈ ℤ ∧ 𝑍 ∈ ℤ ) → ( 5 < 𝑍 ↔ ( 5 + 1 ) ≤ 𝑍 ) )
7	4 5 6	sylancr	⊢ ( 𝑍 ∈ ℕ → ( 5 < 𝑍 ↔ ( 5 + 1 ) ≤ 𝑍 ) )
8	7	biimpd	⊢ ( 𝑍 ∈ ℕ → ( 5 < 𝑍 → ( 5 + 1 ) ≤ 𝑍 ) )
9	2 8	syl	⊢ ( 𝑍 ∈ GoldbachOddW → ( 5 < 𝑍 → ( 5 + 1 ) ≤ 𝑍 ) )
10		5p1e6	⊢ ( 5 + 1 ) = 6
11	10	breq1i	⊢ ( ( 5 + 1 ) ≤ 𝑍 ↔ 6 ≤ 𝑍 )
12		6re	⊢ 6 ∈ ℝ
13	2	nnred	⊢ ( 𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℝ )
14		leloe	⊢ ( ( 6 ∈ ℝ ∧ 𝑍 ∈ ℝ ) → ( 6 ≤ 𝑍 ↔ ( 6 < 𝑍 ∨ 6 = 𝑍 ) ) )
15	12 13 14	sylancr	⊢ ( 𝑍 ∈ GoldbachOddW → ( 6 ≤ 𝑍 ↔ ( 6 < 𝑍 ∨ 6 = 𝑍 ) ) )
16	11 15	bitrid	⊢ ( 𝑍 ∈ GoldbachOddW → ( ( 5 + 1 ) ≤ 𝑍 ↔ ( 6 < 𝑍 ∨ 6 = 𝑍 ) ) )
17		6nn	⊢ 6 ∈ ℕ
18	17	nnzi	⊢ 6 ∈ ℤ
19	2	nnzd	⊢ ( 𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℤ )
20		zltp1le	⊢ ( ( 6 ∈ ℤ ∧ 𝑍 ∈ ℤ ) → ( 6 < 𝑍 ↔ ( 6 + 1 ) ≤ 𝑍 ) )
21	20	biimpd	⊢ ( ( 6 ∈ ℤ ∧ 𝑍 ∈ ℤ ) → ( 6 < 𝑍 → ( 6 + 1 ) ≤ 𝑍 ) )
22	18 19 21	sylancr	⊢ ( 𝑍 ∈ GoldbachOddW → ( 6 < 𝑍 → ( 6 + 1 ) ≤ 𝑍 ) )
23		6p1e7	⊢ ( 6 + 1 ) = 7
24	23	breq1i	⊢ ( ( 6 + 1 ) ≤ 𝑍 ↔ 7 ≤ 𝑍 )
25	22 24	imbitrdi	⊢ ( 𝑍 ∈ GoldbachOddW → ( 6 < 𝑍 → 7 ≤ 𝑍 ) )
26		isgbow	⊢ ( 𝑍 ∈ GoldbachOddW ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
27		eleq1	⊢ ( 6 = 𝑍 → ( 6 ∈ Odd ↔ 𝑍 ∈ Odd ) )
28		6even	⊢ 6 ∈ Even
29		evennodd	⊢ ( 6 ∈ Even → ¬ 6 ∈ Odd )
30		pm2.21	⊢ ( ¬ 6 ∈ Odd → ( 6 ∈ Odd → 7 ≤ 𝑍 ) )
31	28 29 30	mp2b	⊢ ( 6 ∈ Odd → 7 ≤ 𝑍 )
32	27 31	biimtrrdi	⊢ ( 6 = 𝑍 → ( 𝑍 ∈ Odd → 7 ≤ 𝑍 ) )
33	32	com12	⊢ ( 𝑍 ∈ Odd → ( 6 = 𝑍 → 7 ≤ 𝑍 ) )
34	33	adantr	⊢ ( ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ( 6 = 𝑍 → 7 ≤ 𝑍 ) )
35	26 34	sylbi	⊢ ( 𝑍 ∈ GoldbachOddW → ( 6 = 𝑍 → 7 ≤ 𝑍 ) )
36	25 35	jaod	⊢ ( 𝑍 ∈ GoldbachOddW → ( ( 6 < 𝑍 ∨ 6 = 𝑍 ) → 7 ≤ 𝑍 ) )
37	16 36	sylbid	⊢ ( 𝑍 ∈ GoldbachOddW → ( ( 5 + 1 ) ≤ 𝑍 → 7 ≤ 𝑍 ) )
38	9 37	syld	⊢ ( 𝑍 ∈ GoldbachOddW → ( 5 < 𝑍 → 7 ≤ 𝑍 ) )
39	1 38	mpd	⊢ ( 𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍 )