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

Metamath Proof Explorer

Theorem elfzmlbp

Description: Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018)

Ref Expression
Assertion elfzmlbp ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfz2 ⊢ ( 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) )
2 znn0sub ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
3 2 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝐾 ↔ ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
4 3 biimpcd ⊢ ( 𝑀 ≤ 𝐾 → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
5 4 adantr ⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 ) )
6 5 impcom ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ℕ0 )
7 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
8 7 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝑀 ∈ ℝ )
9 8 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
10 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
11 10 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℝ )
12 11 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → 𝐾 ∈ ℝ )
13 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
14 13 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
15 14 zred ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℝ )
16 letr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ ( 𝑀 + 𝑁 ) ∈ ℝ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
17 9 12 15 16 syl3anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
18 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
19 addge01 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 0 ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
20 8 18 19 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 ↔ 𝑀 ≤ ( 𝑀 + 𝑁 ) ) )
21 elnn0z ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℤ ∧ 0 ≤ 𝑁 ) )
22 21 simplbi2 ⊢ ( 𝑁 ∈ ℤ → ( 0 ≤ 𝑁 → 𝑁 ∈ ℕ0 ) )
23 22 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ 𝑁 → 𝑁 ∈ ℕ0 ) )
24 20 23 sylbird ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ ( 𝑀 + 𝑁 ) → 𝑁 ∈ ℕ0 ) )
25 17 24 syld ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → 𝑁 ∈ ℕ0 ) )
26 25 imp ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
27 df-3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) )
28 3ancoma ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
29 27 28 bitr3i ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
30 10 7 18 3anim123i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
31 29 30 sylbi ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
32 lesubadd2 ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐾 − 𝑀 ) ≤ 𝑁 ↔ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
33 31 32 syl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 − 𝑀 ) ≤ 𝑁 ↔ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) )
34 33 biimprcd ⊢ ( 𝐾 ≤ ( 𝑀 + 𝑁 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
35 34 adantl ⊢ ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
36 35 impcom ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ≤ 𝑁 )
37 6 26 36 3jca ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
38 37 exp31 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ℤ → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
39 38 com23 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
40 39 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) ) )
41 40 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( 𝑁 ∈ ℤ → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
42 41 com12 ⊢ ( 𝑁 ∈ ℤ → ( ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
43 1 42 biimtrid ⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) ) )
44 43 imp ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ) → ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
45 elfz2nn0 ⊢ ( ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐾 − 𝑀 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 𝑀 ) ≤ 𝑁 ) )
46 44 45 sylibr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( 𝑀 ... ( 𝑀 + 𝑁 ) ) ) → ( 𝐾 − 𝑀 ) ∈ ( 0 ... 𝑁 ) )