Theorem eluzsub

Description: Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by SN, 7-Feb-2025)

	Ref	Expression
Assertion	eluzsub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝑀 ∈ ℤ )
2		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑁 ∈ ℤ )
3	2	3ad2ant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝑁 ∈ ℤ )
4		simp2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝐾 ∈ ℤ )
5	3 4	zsubcld	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
6		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → ( 𝑀 + 𝐾 ) ≤ 𝑁 )
7	6	3ad2ant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑀 + 𝐾 ) ≤ 𝑁 )
8		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
9		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
10		eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) → 𝑁 ∈ ℝ )
11		leaddsub	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
12	8 9 10 11	syl3an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( ( 𝑀 + 𝐾 ) ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
13	7 12	mpbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → 𝑀 ≤ ( 𝑁 − 𝐾 ) )
14		eluz2	⊢ ( ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑁 − 𝐾 ) ) )
15	1 5 13 14	syl3anbrc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )