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 ) ∈ ℕ )