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

Metamath Proof Explorer

Theorem difelfzle

Description: The difference of two integers from a finite set of sequential nonnegative integers is also element of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 12-Jun-2018)

Ref Expression
Assertion difelfzle ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
2 elfznn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
3 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
4 nn0z ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
5 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
6 3 4 5 syl2anr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
7 6 adantr ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ℤ )
8 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
9 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
10 subge0 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ ( 𝑀 − 𝐾 ) ↔ 𝐾 ≤ 𝑀 ) )
11 8 9 10 syl2anr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ ( 𝑀 − 𝐾 ) ↔ 𝐾 ≤ 𝑀 ) )
12 11 biimpar ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑀 ) → 0 ≤ ( 𝑀 − 𝐾 ) )
13 7 12 jca ⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) )
14 13 exp31 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑀 → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) ) ) )
15 1 2 14 syl2im ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ≤ 𝑀 → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) ) ) )
16 15 3imp ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) )
17 elnn0z ⊢ ( ( 𝑀 − 𝐾 ) ∈ ℕ0 ↔ ( ( 𝑀 − 𝐾 ) ∈ ℤ ∧ 0 ≤ ( 𝑀 − 𝐾 ) ) )
18 16 17 sylibr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ℕ0 )
19 elfz3nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
20 19 3ad2ant1 ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → 𝑁 ∈ ℕ0 )
21 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
22 8 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑀 ∈ ℝ )
23 resubcl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 − 𝐾 ) ∈ ℝ )
24 22 9 23 syl2an ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ∈ ℝ )
25 22 adantr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
26 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
27 26 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
28 27 adantr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
29 nn0ge0 ⊢ ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
30 29 adantl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 0 ≤ 𝐾 )
31 subge02 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 0 ≤ 𝐾 ↔ ( 𝑀 − 𝐾 ) ≤ 𝑀 ) )
32 22 9 31 syl2an ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 0 ≤ 𝐾 ↔ ( 𝑀 − 𝐾 ) ≤ 𝑀 ) )
33 30 32 mpbid ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ≤ 𝑀 )
34 simpl3 ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → 𝑀 ≤ 𝑁 )
35 24 25 28 33 34 letrd ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 − 𝐾 ) ≤ 𝑁 )
36 35 ex ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
37 21 36 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
38 1 37 syl5com ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
39 38 a1dd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ≤ 𝑀 → ( 𝑀 − 𝐾 ) ≤ 𝑁 ) ) )
40 39 3imp ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ≤ 𝑁 )
41 elfz2nn0 ⊢ ( ( 𝑀 − 𝐾 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝑀 − 𝐾 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝑀 − 𝐾 ) ≤ 𝑁 ) )
42 18 20 40 41 syl3anbrc ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ≤ 𝑀 ) → ( 𝑀 − 𝐾 ) ∈ ( 0 ... 𝑁 ) )