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

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 ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )

Proof

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