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

Metamath Proof Explorer

Theorem fz0fzdiffz0

Description: The difference of an integer in a finite set of sequential nonnegative integers and and an integer of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 6-Jun-2018)

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

Proof

Step Hyp Ref Expression
1 fz0fzelfz0 ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
2 elfzle1 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑀 ≤ 𝐾 )
3 2 adantl ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ≤ 𝐾 )
4 3 adantl ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑀 ≤ 𝐾 )
5 elfznn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → 𝑀 ∈ ℕ0 )
6 5 adantr ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑀 ∈ ℕ0 )
7 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
8 nn0sub ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
9 6 7 8 syl2anr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
10 4 9 mpbid ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 )
11 elfz3nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
12 11 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
13 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
14 elfz2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
15 zsubcl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℤ )
16 15 zred ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℝ )
17 16 ancoms ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℝ )
18 17 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℝ )
19 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
20 19 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℝ )
21 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
22 21 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℝ )
23 18 20 22 3jca ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
24 23 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
25 24 adantr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
26 nn0ge0 ⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
27 26 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → 0 ≤ 𝑀 )
28 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
29 subge02 ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ 𝑀 ↔ ( 𝐾 − 𝑀 ) ≤ 𝐾 ) )
30 20 28 29 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → ( 0 ≤ 𝑀 ↔ ( 𝐾 − 𝑀 ) ≤ 𝐾 ) )
31 27 30 mpbid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 − 𝑀 ) ≤ 𝐾 )
32 31 anim1i ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝐾 − 𝑀 ) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) )
33 letr ⊢ ( ( ( 𝐾 − 𝑀 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝐾 − 𝑀 ) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
34 25 32 33 sylc ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐾 ≤ 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
35 34 exp31 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑁 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
36 35 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝑁 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
37 36 com14 ⊢ ( 𝐾 ≤ 𝑁 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
38 37 adantl ⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
39 38 impcom ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
40 14 39 sylbi ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
41 40 com13 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
42 41 impcom ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
43 42 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
44 13 43 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
45 44 imp ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
46 45 adantl ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
47 10 12 46 3jca ⊢ ( ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
48 1 47 mpancom ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
49 elfz2nn0 ⊢ ( ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
50 48 49 sylibr ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝐾 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )