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 ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}\in {ℤ}_{\ge \left({M}-{N}\right)}$

Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}\in ℤ$
2 simpr ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in {ℕ}_{0}$
3 2 nn0zd ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℤ$
4 1 3 zsubcld ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}-{N}\in ℤ$
5 1 zred ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}\in ℝ$
6 2 nn0red ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℝ$
7 5 6 readdcld ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}+{N}\in ℝ$
8 nn0addge1 ${⊢}\left({M}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to {M}\le {M}+{N}$
9 5 8 sylancom ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}\le {M}+{N}$
10 5 7 6 9 lesub1dd ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}-{N}\le {M}+{N}-{N}$
11 5 recnd ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}\in ℂ$
12 6 recnd ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {N}\in ℂ$
13 11 12 pncand ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}+{N}-{N}={M}$
14 10 13 breqtrd ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}-{N}\le {M}$
15 eluz2 ${⊢}{M}\in {ℤ}_{\ge \left({M}-{N}\right)}↔\left({M}-{N}\in ℤ\wedge {M}\in ℤ\wedge {M}-{N}\le {M}\right)$
16 4 1 14 15 syl3anbrc ${⊢}\left({M}\in ℤ\wedge {N}\in {ℕ}_{0}\right)\to {M}\in {ℤ}_{\ge \left({M}-{N}\right)}$