Metamath Proof Explorer

Theorem nnge1

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

Ref Expression
Assertion nnge1 ⊢A∈ℕ→1≤A

Proof

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