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

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 ⊢ A ∈ ℕ → A ≤ 1 ↔ A = 1

Proof

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