# Metamath Proof Explorer

## Theorem nnge1

Description: A positive integer is one or greater. (Contributed by NM, 25-Aug-1999)

Ref Expression
Assertion nnge1 ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )

### Proof

Step Hyp Ref Expression
1 breq2 ( 𝑥 = 1 → ( 1 ≤ 𝑥 ↔ 1 ≤ 1 ) )
2 breq2 ( 𝑥 = 𝑦 → ( 1 ≤ 𝑥 ↔ 1 ≤ 𝑦 ) )
3 breq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 1 ≤ 𝑥 ↔ 1 ≤ ( 𝑦 + 1 ) ) )
4 breq2 ( 𝑥 = 𝐴 → ( 1 ≤ 𝑥 ↔ 1 ≤ 𝐴 ) )
5 1le1 1 ≤ 1
6 nnre ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
7 recn ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
8 7 addid1d ( 𝑦 ∈ ℝ → ( 𝑦 + 0 ) = 𝑦 )
9 8 breq2d ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 0 ) ↔ 1 ≤ 𝑦 ) )
10 0lt1 0 < 1
11 0re 0 ∈ ℝ
12 1re 1 ∈ ℝ
13 axltadd ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 < 1 → ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ) )
14 11 12 13 mp3an12 ( 𝑦 ∈ ℝ → ( 0 < 1 → ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ) )
15 10 14 mpi ( 𝑦 ∈ ℝ → ( 𝑦 + 0 ) < ( 𝑦 + 1 ) )
16 readdcl ( ( 𝑦 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝑦 + 0 ) ∈ ℝ )
17 11 16 mpan2 ( 𝑦 ∈ ℝ → ( 𝑦 + 0 ) ∈ ℝ )
18 peano2re ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
19 lttr ( ( ( 𝑦 + 0 ) ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) < 1 ) → ( 𝑦 + 0 ) < 1 ) )
20 12 19 mp3an3 ( ( ( 𝑦 + 0 ) ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) → ( ( ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) < 1 ) → ( 𝑦 + 0 ) < 1 ) )
21 17 18 20 syl2anc ( 𝑦 ∈ ℝ → ( ( ( 𝑦 + 0 ) < ( 𝑦 + 1 ) ∧ ( 𝑦 + 1 ) < 1 ) → ( 𝑦 + 0 ) < 1 ) )
22 15 21 mpand ( 𝑦 ∈ ℝ → ( ( 𝑦 + 1 ) < 1 → ( 𝑦 + 0 ) < 1 ) )
23 22 con3d ( 𝑦 ∈ ℝ → ( ¬ ( 𝑦 + 0 ) < 1 → ¬ ( 𝑦 + 1 ) < 1 ) )
24 lenlt ( ( 1 ∈ ℝ ∧ ( 𝑦 + 0 ) ∈ ℝ ) → ( 1 ≤ ( 𝑦 + 0 ) ↔ ¬ ( 𝑦 + 0 ) < 1 ) )
25 12 17 24 sylancr ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 0 ) ↔ ¬ ( 𝑦 + 0 ) < 1 ) )
26 lenlt ( ( 1 ∈ ℝ ∧ ( 𝑦 + 1 ) ∈ ℝ ) → ( 1 ≤ ( 𝑦 + 1 ) ↔ ¬ ( 𝑦 + 1 ) < 1 ) )
27 12 18 26 sylancr ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 1 ) ↔ ¬ ( 𝑦 + 1 ) < 1 ) )
28 23 25 27 3imtr4d ( 𝑦 ∈ ℝ → ( 1 ≤ ( 𝑦 + 0 ) → 1 ≤ ( 𝑦 + 1 ) ) )
29 9 28 sylbird ( 𝑦 ∈ ℝ → ( 1 ≤ 𝑦 → 1 ≤ ( 𝑦 + 1 ) ) )
30 6 29 syl ( 𝑦 ∈ ℕ → ( 1 ≤ 𝑦 → 1 ≤ ( 𝑦 + 1 ) ) )
31 1 2 3 4 5 30 nnind ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )