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