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

Metamath Proof Explorer

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