# Metamath Proof Explorer

## Theorem nnge1

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

Ref Expression
Assertion nnge1 ${⊢}{A}\in ℕ\to 1\le {A}$

### Proof

Step Hyp Ref Expression
1 breq2 ${⊢}{x}=1\to \left(1\le {x}↔1\le 1\right)$
2 breq2 ${⊢}{x}={y}\to \left(1\le {x}↔1\le {y}\right)$
3 breq2 ${⊢}{x}={y}+1\to \left(1\le {x}↔1\le {y}+1\right)$
4 breq2 ${⊢}{x}={A}\to \left(1\le {x}↔1\le {A}\right)$
5 1le1 ${⊢}1\le 1$
6 nnre ${⊢}{y}\in ℕ\to {y}\in ℝ$
7 recn ${⊢}{y}\in ℝ\to {y}\in ℂ$
8 7 addid1d ${⊢}{y}\in ℝ\to {y}+0={y}$
9 8 breq2d ${⊢}{y}\in ℝ\to \left(1\le {y}+0↔1\le {y}\right)$
10 0lt1 ${⊢}0<1$
11 0re ${⊢}0\in ℝ$
12 1re ${⊢}1\in ℝ$
13 axltadd ${⊢}\left(0\in ℝ\wedge 1\in ℝ\wedge {y}\in ℝ\right)\to \left(0<1\to {y}+0<{y}+1\right)$
14 11 12 13 mp3an12 ${⊢}{y}\in ℝ\to \left(0<1\to {y}+0<{y}+1\right)$
15 10 14 mpi ${⊢}{y}\in ℝ\to {y}+0<{y}+1$
16 readdcl ${⊢}\left({y}\in ℝ\wedge 0\in ℝ\right)\to {y}+0\in ℝ$
17 11 16 mpan2 ${⊢}{y}\in ℝ\to {y}+0\in ℝ$
18 peano2re ${⊢}{y}\in ℝ\to {y}+1\in ℝ$
19 lttr ${⊢}\left({y}+0\in ℝ\wedge {y}+1\in ℝ\wedge 1\in ℝ\right)\to \left(\left({y}+0<{y}+1\wedge {y}+1<1\right)\to {y}+0<1\right)$
20 12 19 mp3an3 ${⊢}\left({y}+0\in ℝ\wedge {y}+1\in ℝ\right)\to \left(\left({y}+0<{y}+1\wedge {y}+1<1\right)\to {y}+0<1\right)$
21 17 18 20 syl2anc ${⊢}{y}\in ℝ\to \left(\left({y}+0<{y}+1\wedge {y}+1<1\right)\to {y}+0<1\right)$
22 15 21 mpand ${⊢}{y}\in ℝ\to \left({y}+1<1\to {y}+0<1\right)$
23 22 con3d ${⊢}{y}\in ℝ\to \left(¬{y}+0<1\to ¬{y}+1<1\right)$
24 lenlt ${⊢}\left(1\in ℝ\wedge {y}+0\in ℝ\right)\to \left(1\le {y}+0↔¬{y}+0<1\right)$
25 12 17 24 sylancr ${⊢}{y}\in ℝ\to \left(1\le {y}+0↔¬{y}+0<1\right)$
26 lenlt ${⊢}\left(1\in ℝ\wedge {y}+1\in ℝ\right)\to \left(1\le {y}+1↔¬{y}+1<1\right)$
27 12 18 26 sylancr ${⊢}{y}\in ℝ\to \left(1\le {y}+1↔¬{y}+1<1\right)$
28 23 25 27 3imtr4d ${⊢}{y}\in ℝ\to \left(1\le {y}+0\to 1\le {y}+1\right)$
29 9 28 sylbird ${⊢}{y}\in ℝ\to \left(1\le {y}\to 1\le {y}+1\right)$
30 6 29 syl ${⊢}{y}\in ℕ\to \left(1\le {y}\to 1\le {y}+1\right)$
31 1 2 3 4 5 30 nnind ${⊢}{A}\in ℕ\to 1\le {A}$