This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )