ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  uzsubsubfz GIF version

Theorem uzsubsubfz 9356
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.)
Assertion
Ref Expression
uzsubsubfz ((𝐿 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐿)) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁))

Proof of Theorem uzsubsubfz
StepHypRef Expression
1 eluz2 8920 . . 3 (𝐿 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀𝐿))
2 eluz2 8920 . . . 4 (𝑁 ∈ (ℤ𝐿) ↔ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁))
3 simpr 108 . . . . . . . . . . . . 13 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ)
4 simpr 108 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℤ)
54adantr 270 . . . . . . . . . . . . 13 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → 𝑁 ∈ ℤ)
6 zsubcl 8687 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿𝑀) ∈ ℤ)
76adantlr 461 . . . . . . . . . . . . . 14 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → (𝐿𝑀) ∈ ℤ)
85, 7zsubcld 8769 . . . . . . . . . . . . 13 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → (𝑁 − (𝐿𝑀)) ∈ ℤ)
93, 5, 83jca 1119 . . . . . . . . . . . 12 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ∈ ℤ) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ))
109ex 113 . . . . . . . . . . 11 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ)))
11103adant3 959 . . . . . . . . . 10 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ)))
1211com12 30 . . . . . . . . 9 (𝑀 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ)))
1312adantr 270 . . . . . . . 8 ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ)))
1413imp 122 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ))
15 zre 8650 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
1615adantl 271 . . . . . . . . . . . . . . . 16 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
1716adantr 270 . . . . . . . . . . . . . . 15 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑀𝐿)) → 𝑁 ∈ ℝ)
18 zre 8650 . . . . . . . . . . . . . . . . 17 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
1918adantr 270 . . . . . . . . . . . . . . . 16 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝐿 ∈ ℝ)
2019adantr 270 . . . . . . . . . . . . . . 15 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑀𝐿)) → 𝐿 ∈ ℝ)
2117, 20subge0d 7912 . . . . . . . . . . . . . 14 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 𝑀𝐿)) → (0 ≤ (𝑁𝐿) ↔ 𝐿𝑁))
2221exbiri 374 . . . . . . . . . . . . 13 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → (𝐿𝑁 → 0 ≤ (𝑁𝐿))))
2322com23 77 . . . . . . . . . . . 12 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 → ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → 0 ≤ (𝑁𝐿))))
24233impia 1136 . . . . . . . . . . 11 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → 0 ≤ (𝑁𝐿)))
2524impcom 123 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 0 ≤ (𝑁𝐿))
26 zre 8650 . . . . . . . . . . . . 13 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
2726adantr 270 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → 𝑀 ∈ ℝ)
2827adantr 270 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝑀 ∈ ℝ)
29 resubcl 7649 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑁𝐿) ∈ ℝ)
3015, 18, 29syl2anr 284 . . . . . . . . . . . . 13 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝐿) ∈ ℝ)
31303adant3 959 . . . . . . . . . . . 12 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑁𝐿) ∈ ℝ)
3231adantl 271 . . . . . . . . . . 11 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝑁𝐿) ∈ ℝ)
3328, 32addge02d 7911 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (0 ≤ (𝑁𝐿) ↔ 𝑀 ≤ ((𝑁𝐿) + 𝑀)))
3425, 33mpbid 145 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝑀 ≤ ((𝑁𝐿) + 𝑀))
35 zcn 8651 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
36353ad2ant2 961 . . . . . . . . . . 11 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → 𝑁 ∈ ℂ)
3736adantl 271 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝑁 ∈ ℂ)
38 zcn 8651 . . . . . . . . . . . 12 (𝐿 ∈ ℤ → 𝐿 ∈ ℂ)
39383ad2ant1 960 . . . . . . . . . . 11 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → 𝐿 ∈ ℂ)
4039adantl 271 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝐿 ∈ ℂ)
41 zcn 8651 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
4241adantr 270 . . . . . . . . . . 11 ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → 𝑀 ∈ ℂ)
4342adantr 270 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝑀 ∈ ℂ)
4437, 40, 43subsubd 7724 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝑁 − (𝐿𝑀)) = ((𝑁𝐿) + 𝑀))
4534, 44breqtrrd 3837 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝑀 ≤ (𝑁 − (𝐿𝑀)))
46183ad2ant1 960 . . . . . . . . . . . . 13 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → 𝐿 ∈ ℝ)
47 subge0 7856 . . . . . . . . . . . . 13 ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ (𝐿𝑀) ↔ 𝑀𝐿))
4846, 26, 47syl2anr 284 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (0 ≤ (𝐿𝑀) ↔ 𝑀𝐿))
4948exbiri 374 . . . . . . . . . . 11 (𝑀 ∈ ℤ → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑀𝐿 → 0 ≤ (𝐿𝑀))))
5049com23 77 . . . . . . . . . 10 (𝑀 ∈ ℤ → (𝑀𝐿 → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → 0 ≤ (𝐿𝑀))))
5150imp31 252 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 0 ≤ (𝐿𝑀))
52153ad2ant2 961 . . . . . . . . . . 11 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → 𝑁 ∈ ℝ)
5352adantl 271 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → 𝑁 ∈ ℝ)
54 resubcl 7649 . . . . . . . . . . 11 ((𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝐿𝑀) ∈ ℝ)
5546, 27, 54syl2anr 284 . . . . . . . . . 10 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝐿𝑀) ∈ ℝ)
5653, 55subge02d 7914 . . . . . . . . 9 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (0 ≤ (𝐿𝑀) ↔ (𝑁 − (𝐿𝑀)) ≤ 𝑁))
5751, 56mpbid 145 . . . . . . . 8 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝑁 − (𝐿𝑀)) ≤ 𝑁)
5845, 57jca 300 . . . . . . 7 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝑀 ≤ (𝑁 − (𝐿𝑀)) ∧ (𝑁 − (𝐿𝑀)) ≤ 𝑁))
59 elfz2 9326 . . . . . . 7 ((𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − (𝐿𝑀)) ∈ ℤ) ∧ (𝑀 ≤ (𝑁 − (𝐿𝑀)) ∧ (𝑁 − (𝐿𝑀)) ≤ 𝑁)))
6014, 58, 59sylanbrc 408 . . . . . 6 (((𝑀 ∈ ℤ ∧ 𝑀𝐿) ∧ (𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁)) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁))
6160ex 113 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑀𝐿) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁)))
62613adant2 958 . . . 4 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀𝐿) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐿𝑁) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁)))
632, 62syl5bi 150 . . 3 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀𝐿) → (𝑁 ∈ (ℤ𝐿) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁)))
641, 63sylbi 119 . 2 (𝐿 ∈ (ℤ𝑀) → (𝑁 ∈ (ℤ𝐿) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁)))
6564imp 122 1 ((𝐿 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐿)) → (𝑁 − (𝐿𝑀)) ∈ (𝑀...𝑁))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920  wcel 1434   class class class wbr 3811  cfv 4969  (class class class)co 5591  cc 7251  cr 7252  0cc0 7253   + caddc 7256  cle 7426  cmin 7556  cz 8646  cuz 8914  ...cfz 9319
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000  ax-un 4224  ax-setind 4316  ax-cnex 7339  ax-resscn 7340  ax-1cn 7341  ax-1re 7342  ax-icn 7343  ax-addcl 7344  ax-addrcl 7345  ax-mulcl 7346  ax-addcom 7348  ax-addass 7350  ax-distr 7352  ax-i2m1 7353  ax-0lt1 7354  ax-0id 7356  ax-rnegex 7357  ax-cnre 7359  ax-pre-ltirr 7360  ax-pre-ltwlin 7361  ax-pre-lttrn 7362  ax-pre-ltadd 7364
This theorem depends on definitions:  df-bi 115  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-br 3812  df-opab 3866  df-mpt 3867  df-id 4084  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-ima 4414  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-fv 4977  df-riota 5547  df-ov 5594  df-oprab 5595  df-mpt2 5596  df-pnf 7427  df-mnf 7428  df-xr 7429  df-ltxr 7430  df-le 7431  df-sub 7558  df-neg 7559  df-inn 8317  df-n0 8566  df-z 8647  df-uz 8915  df-fz 9320
This theorem is referenced by:  uzsubsubfz1  9357
  Copyright terms: Public domain W3C validator