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

Metamath Proof Explorer

Theorem uzsubsubfz

Description: Membership of an integer greater than L decreased by ( L - M ) in an M-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018)

Ref Expression
Assertion uzsubsubfz ( ( 𝐿 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) )
2 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ↔ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) )
3 simpr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
4 simpr ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
5 4 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → 𝑁 ∈ ℤ )
6 zsubcl ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
7 6 adantlr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → ( 𝐿 − 𝑀 ) ∈ ℤ )
8 5 7 zsubcld ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ )
9 3 5 8 3jca ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ℤ ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) )
10 9 ex ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) ) )
11 10 3adant3 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) ) )
12 11 com12 ⊢ ( 𝑀 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) ) )
13 12 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) ) )
14 13 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) )
15 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
16 15 adantl ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
17 16 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ) → 𝑁 ∈ ℝ )
18 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
19 18 adantr ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝐿 ∈ ℝ )
20 19 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ) → 𝐿 ∈ ℝ )
21 17 20 subge0d ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ) → ( 0 ≤ ( 𝑁 − 𝐿 ) ↔ 𝐿 ≤ 𝑁 ) )
22 21 exbiri ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → ( 𝐿 ≤ 𝑁 → 0 ≤ ( 𝑁 − 𝐿 ) ) ) )
23 22 com23 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ≤ 𝑁 → ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → 0 ≤ ( 𝑁 − 𝐿 ) ) ) )
24 23 3impia ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → 0 ≤ ( 𝑁 − 𝐿 ) ) )
25 24 impcom ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 0 ≤ ( 𝑁 − 𝐿 ) )
26 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → 𝑀 ∈ ℝ )
28 27 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝑀 ∈ ℝ )
29 resubcl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑁 − 𝐿 ) ∈ ℝ )
30 15 18 29 syl2anr ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℝ )
31 30 3adant3 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑁 − 𝐿 ) ∈ ℝ )
32 31 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑁 − 𝐿 ) ∈ ℝ )
33 28 32 addge02d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 0 ≤ ( 𝑁 − 𝐿 ) ↔ 𝑀 ≤ ( ( 𝑁 − 𝐿 ) + 𝑀 ) ) )
34 25 33 mpbid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝑀 ≤ ( ( 𝑁 − 𝐿 ) + 𝑀 ) )
35 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
36 35 3ad2ant2 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → 𝑁 ∈ ℂ )
37 36 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝑁 ∈ ℂ )
38 zcn ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℂ )
39 38 3ad2ant1 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → 𝐿 ∈ ℂ )
40 39 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝐿 ∈ ℂ )
41 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
42 41 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → 𝑀 ∈ ℂ )
43 42 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝑀 ∈ ℂ )
44 37 40 43 subsubd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) = ( ( 𝑁 − 𝐿 ) + 𝑀 ) )
45 34 44 breqtrrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝑀 ≤ ( 𝑁 − ( 𝐿 − 𝑀 ) ) )
46 18 3ad2ant1 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → 𝐿 ∈ ℝ )
47 subge0 ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 0 ≤ ( 𝐿 − 𝑀 ) ↔ 𝑀 ≤ 𝐿 ) )
48 46 26 47 syl2anr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 0 ≤ ( 𝐿 − 𝑀 ) ↔ 𝑀 ≤ 𝐿 ) )
49 48 exbiri ⊢ ( 𝑀 ∈ ℤ → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑀 ≤ 𝐿 → 0 ≤ ( 𝐿 − 𝑀 ) ) ) )
50 49 com23 ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ≤ 𝐿 → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → 0 ≤ ( 𝐿 − 𝑀 ) ) ) )
51 50 imp31 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 0 ≤ ( 𝐿 − 𝑀 ) )
52 15 3ad2ant2 ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
53 52 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → 𝑁 ∈ ℝ )
54 resubcl ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝐿 − 𝑀 ) ∈ ℝ )
55 46 27 54 syl2anr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝐿 − 𝑀 ) ∈ ℝ )
56 53 55 subge02d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 0 ≤ ( 𝐿 − 𝑀 ) ↔ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ≤ 𝑁 ) )
57 51 56 mpbid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ≤ 𝑁 )
58 45 57 jca ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑀 ≤ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ≤ 𝑁 ) )
59 elfz2 ⊢ ( ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ℤ ) ∧ ( 𝑀 ≤ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∧ ( 𝑁 − ( 𝐿 − 𝑀 ) ) ≤ 𝑁 ) ) )
60 14 58 59 sylanbrc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) )
61 60 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
62 61 3adant2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿 ≤ 𝑁 ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
63 2 62 biimtrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
64 1 63 sylbi ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) ) )
65 64 imp ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 𝑀 ) ) ∈ ( 𝑀 ... 𝑁 ) )