Theorem eluzmn

Description: Membership in an earlier upper set of integers. (Contributed by Thierry Arnoux, 8-Oct-2018)

	Ref	Expression
Assertion	eluzmn	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
2		simpr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
3	2	nn0zd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
4	1 3	zsubcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
5	1	zred	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
6	2	nn0red	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
7	5 6	readdcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
8		nn0addge1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
9	5 8	sylancom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) )
10	5 7 6 9	lesub1dd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 − 𝑁 ) ≤ ( ( 𝑀 + 𝑁 ) − 𝑁 ) )
11	5	recnd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℂ )
12	6	recnd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
13	11 12	pncand	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
14	10 13	breqtrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 − 𝑁 ) ≤ 𝑀 )
15		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) ↔ ( ( 𝑀 − 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ≤ 𝑀 ) )
16	4 1 14 15	syl3anbrc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) )