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

Metamath Proof Explorer

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 ) ∈ ( ℤ≥ ‘ 𝑀 ) )