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 syl6bi ⊢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∈ℕ