This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 addridd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 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 ≤ 𝐴 )