Theorem peano2uz

Description: Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005)

	Ref	Expression
Assertion	peano2uz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℤ )
2		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
3	2	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 + 1 ) ∈ ℤ )
4		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
5		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6		letrp1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 + 1 ) )
7	5 6	syl3an2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 + 1 ) )
8	4 7	syl3an1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 + 1 ) )
9	1 3 8	3jca	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 + 1 ) ) )
10		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
11		eluz2	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 + 1 ) ) )
12	9 10 11	3imtr4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )