Theorem eluzp1p1

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

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

Proof

Step	Hyp	Ref	Expression
1		peano2z	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
2	1	3ad2ant1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 + 1 ) ∈ ℤ )
3		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
4	3	3ad2ant2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑁 + 1 ) ∈ ℤ )
5		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
6		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
7		1re	⊢ 1 ∈ ℝ
8		leadd1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
9	7 8	mp3an3	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
10	5 6 9	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
11	10	biimp3a	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) )
12	2 4 11	3jca	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝑀 + 1 ) ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
13		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁 ) )
14		eluz2	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( ( 𝑀 + 1 ) ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
15	12 13 14	3imtr4i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )