Metamath Proof Explorer


Theorem nnle1eq1

Description: A positive integer is less than or equal to one iff it is equal to one. (Contributed by NM, 3-Apr-2005)

Ref Expression
Assertion nnle1eq1 ( 𝐴 ∈ ℕ → ( 𝐴 ≤ 1 ↔ 𝐴 = 1 ) )

Proof

Step Hyp Ref Expression
1 nnge1 ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )
2 1 biantrud ( 𝐴 ∈ ℕ → ( 𝐴 ≤ 1 ↔ ( 𝐴 ≤ 1 ∧ 1 ≤ 𝐴 ) ) )
3 nnre ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
4 1re 1 ∈ ℝ
5 letri3 ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 = 1 ↔ ( 𝐴 ≤ 1 ∧ 1 ≤ 𝐴 ) ) )
6 3 4 5 sylancl ( 𝐴 ∈ ℕ → ( 𝐴 = 1 ↔ ( 𝐴 ≤ 1 ∧ 1 ≤ 𝐴 ) ) )
7 2 6 bitr4d ( 𝐴 ∈ ℕ → ( 𝐴 ≤ 1 ↔ 𝐴 = 1 ) )