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

Metamath Proof Explorer

Theorem eluzp1m1

Description: Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005)

Ref Expression
Assertion eluzp1m1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
2 1 ad2antrl ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → ( 𝑁 − 1 ) ∈ ℤ )
3 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
4 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
5 1re ⊢ 1 ∈ ℝ
6 leaddsub ⊢ ( ( 𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 1 ) ) )
7 5 6 mp3an2 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 1 ) ) )
8 3 4 7 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 1 ) ) )
9 8 biimpa ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 − 1 ) )
10 9 anasss ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → 𝑀 ≤ ( 𝑁 − 1 ) )
11 2 10 jca ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 1 ) ) )
12 11 ex ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 1 ) ) ) )
13 peano2z ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
14 eluz1 ⊢ ( ( 𝑀 + 1 ) ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) )
15 13 14 syl ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) ) )
16 eluz1 ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 1 ) ) ) )
17 12 15 16 3imtr4d ⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ) )
18 17 imp ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )