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