Theorem oddprmge3

Description: An odd prime is greater than or equal to 3. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 20-Aug-2021)

	Ref	Expression
Assertion	oddprmge3	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 3 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
2		oddprmgt2	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 < 𝑃 )
3		3z	⊢ 3 ∈ ℤ
4	3	a1i	⊢ ( ( 𝑃 ∈ ℙ ∧ 2 < 𝑃 ) → 3 ∈ ℤ )
5		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
6	5	adantr	⊢ ( ( 𝑃 ∈ ℙ ∧ 2 < 𝑃 ) → 𝑃 ∈ ℤ )
7		df-3	⊢ 3 = ( 2 + 1 )
8		2z	⊢ 2 ∈ ℤ
9		zltp1le	⊢ ( ( 2 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 2 < 𝑃 ↔ ( 2 + 1 ) ≤ 𝑃 ) )
10	8 5 9	sylancr	⊢ ( 𝑃 ∈ ℙ → ( 2 < 𝑃 ↔ ( 2 + 1 ) ≤ 𝑃 ) )
11	10	biimpa	⊢ ( ( 𝑃 ∈ ℙ ∧ 2 < 𝑃 ) → ( 2 + 1 ) ≤ 𝑃 )
12	7 11	eqbrtrid	⊢ ( ( 𝑃 ∈ ℙ ∧ 2 < 𝑃 ) → 3 ≤ 𝑃 )
13	4 6 12	3jca	⊢ ( ( 𝑃 ∈ ℙ ∧ 2 < 𝑃 ) → ( 3 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 3 ≤ 𝑃 ) )
14	1 2 13	syl2anc	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 3 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 3 ≤ 𝑃 ) )
15		eluz2	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 3 ≤ 𝑃 ) )
16	14 15	sylibr	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 3 ) )