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