Metamath Proof Explorer

Theorem nn0ge2m1nn

Description: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018) (Revised by AV, 4-Jan-2020)

Ref Expression
Assertion nn0ge2m1nn ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N ∈ ℕ 0
2 1red ⊢ N ∈ ℕ 0 → 1 ∈ ℝ
3 2re ⊢ 2 ∈ ℝ
4 3 a1i ⊢ N ∈ ℕ 0 → 2 ∈ ℝ
5 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
6 2 4 5 3jca ⊢ N ∈ ℕ 0 → 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ N ∈ ℝ
7 6 adantr ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ N ∈ ℝ
8 simpr ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → 2 ≤ N
9 1lt2 ⊢ 1 < 2
10 8 9 jctil ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → 1 < 2 ∧ 2 ≤ N
11 ltleletr ⊢ 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ N ∈ ℝ → 1 < 2 ∧ 2 ≤ N → 1 ≤ N
12 7 10 11 sylc ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → 1 ≤ N
13 elnnnn0c ⊢ N ∈ ℕ ↔ N ∈ ℕ 0 ∧ 1 ≤ N
14 1 12 13 sylanbrc ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N ∈ ℕ
15 nn1m1nn ⊢ N ∈ ℕ → N = 1 ∨ N − 1 ∈ ℕ
16 14 15 syl ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N = 1 ∨ N − 1 ∈ ℕ
17 breq2 ⊢ N = 1 → 2 ≤ N ↔ 2 ≤ 1
18 1re ⊢ 1 ∈ ℝ
19 18 3 ltnlei ⊢ 1 < 2 ↔ ¬ 2 ≤ 1
20 pm2.21 ⊢ ¬ 2 ≤ 1 → 2 ≤ 1 → N − 1 ∈ ℕ
21 19 20 sylbi ⊢ 1 < 2 → 2 ≤ 1 → N − 1 ∈ ℕ
22 9 21 ax-mp ⊢ 2 ≤ 1 → N − 1 ∈ ℕ
23 17 22 biimtrdi ⊢ N = 1 → 2 ≤ N → N − 1 ∈ ℕ
24 23 adantld ⊢ N = 1 → N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ
25 ax-1 ⊢ N − 1 ∈ ℕ → N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ
26 24 25 jaoi ⊢ N = 1 ∨ N − 1 ∈ ℕ → N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ
27 16 26 mpcom ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ