Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2elfz2melfz Structured version   Visualization version   GIF version

Theorem 2elfz2melfz 44244
 Description: If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
Assertion
Ref Expression
2elfz2melfz ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁𝐴)) ∈ (0...𝐴)))

Proof of Theorem 2elfz2melfz
StepHypRef Expression
1 elfzelz 12957 . . . . 5 (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℤ)
2 elfzel2 12955 . . . . . 6 (𝐵 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
3 elfzelz 12957 . . . . . 6 (𝐵 ∈ (0...𝑁) → 𝐵 ∈ ℤ)
4 simplr 769 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝐵 ∈ ℤ)
5 zsubcl 12064 . . . . . . . . . . 11 ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝑁𝐴) ∈ ℤ)
65adantlr 715 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁𝐴) ∈ ℤ)
74, 6zsubcld 12132 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝐵 − (𝑁𝐴)) ∈ ℤ)
87adantr 485 . . . . . . . 8 ((((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁𝐴)) ∈ ℤ)
9 zre 12025 . . . . . . . . . . . 12 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
109ad2antrr 726 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝑁 ∈ ℝ)
11 zaddcl 12062 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ)
1211zred 12127 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℝ)
1312expcom 418 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐴 ∈ ℤ → (𝐴 + 𝐵) ∈ ℝ))
1413adantl 486 . . . . . . . . . . . 12 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℤ → (𝐴 + 𝐵) ∈ ℝ))
1514imp 411 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℝ)
1610, 15, 10ltsub1d 11288 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁 < (𝐴 + 𝐵) ↔ (𝑁𝑁) < ((𝐴 + 𝐵) − 𝑁)))
17 zre 12025 . . . . . . . . . . . . . 14 (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
189, 17anim12i 616 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ))
19 zre 12025 . . . . . . . . . . . . 13 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
2018, 19anim12i 616 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ))
21 id 22 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℝ → 𝑁 ∈ ℝ)
2221, 21resubcld 11107 . . . . . . . . . . . . . 14 (𝑁 ∈ ℝ → (𝑁𝑁) ∈ ℝ)
2322ad2antrr 726 . . . . . . . . . . . . 13 (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝑁𝑁) ∈ ℝ)
24 readdcl 10659 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
2524expcom 418 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℝ → (𝐴 ∈ ℝ → (𝐴 + 𝐵) ∈ ℝ))
2625adantl 486 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ∈ ℝ → (𝐴 + 𝐵) ∈ ℝ))
2726imp 411 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
28 simpll 767 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → 𝑁 ∈ ℝ)
2927, 28resubcld 11107 . . . . . . . . . . . . 13 (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → ((𝐴 + 𝐵) − 𝑁) ∈ ℝ)
3023, 29jca 516 . . . . . . . . . . . 12 (((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → ((𝑁𝑁) ∈ ℝ ∧ ((𝐴 + 𝐵) − 𝑁) ∈ ℝ))
31 ltle 10768 . . . . . . . . . . . 12 (((𝑁𝑁) ∈ ℝ ∧ ((𝐴 + 𝐵) − 𝑁) ∈ ℝ) → ((𝑁𝑁) < ((𝐴 + 𝐵) − 𝑁) → (𝑁𝑁) ≤ ((𝐴 + 𝐵) − 𝑁)))
3220, 30, 313syl 18 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁𝑁) < ((𝐴 + 𝐵) − 𝑁) → (𝑁𝑁) ≤ ((𝐴 + 𝐵) − 𝑁)))
33 zcn 12026 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
3433subidd 11024 . . . . . . . . . . . . 13 (𝑁 ∈ ℤ → (𝑁𝑁) = 0)
3534ad2antrr 726 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁𝑁) = 0)
36 zcn 12026 . . . . . . . . . . . . . . 15 (𝐵 ∈ ℤ → 𝐵 ∈ ℂ)
3736adantl 486 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐵 ∈ ℂ)
3837adantr 485 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝐵 ∈ ℂ)
3933ad2antrr 726 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝑁 ∈ ℂ)
40 zcn 12026 . . . . . . . . . . . . . 14 (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
4140adantl 486 . . . . . . . . . . . . 13 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → 𝐴 ∈ ℂ)
42 simp3 1136 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝐴 ∈ ℂ)
43 simp1 1134 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → 𝐵 ∈ ℂ)
4442, 43addcomd 10881 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
4544oveq1d 7166 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐴 + 𝐵) − 𝑁) = ((𝐵 + 𝐴) − 𝑁))
46 subsub3 10957 . . . . . . . . . . . . . 14 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − (𝑁𝐴)) = ((𝐵 + 𝐴) − 𝑁))
4745, 46eqtr4d 2797 . . . . . . . . . . . . 13 ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝐴 + 𝐵) − 𝑁) = (𝐵 − (𝑁𝐴)))
4838, 39, 41, 47syl3anc 1369 . . . . . . . . . . . 12 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝐴 + 𝐵) − 𝑁) = (𝐵 − (𝑁𝐴)))
4935, 48breq12d 5046 . . . . . . . . . . 11 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁𝑁) ≤ ((𝐴 + 𝐵) − 𝑁) ↔ 0 ≤ (𝐵 − (𝑁𝐴))))
5032, 49sylibd 242 . . . . . . . . . 10 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → ((𝑁𝑁) < ((𝐴 + 𝐵) − 𝑁) → 0 ≤ (𝐵 − (𝑁𝐴))))
5116, 50sylbid 243 . . . . . . . . 9 (((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) → (𝑁 < (𝐴 + 𝐵) → 0 ≤ (𝐵 − (𝑁𝐴))))
5251imp 411 . . . . . . . 8 ((((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) ∧ 𝑁 < (𝐴 + 𝐵)) → 0 ≤ (𝐵 − (𝑁𝐴)))
53 elnn0z 12034 . . . . . . . 8 ((𝐵 − (𝑁𝐴)) ∈ ℕ0 ↔ ((𝐵 − (𝑁𝐴)) ∈ ℤ ∧ 0 ≤ (𝐵 − (𝑁𝐴))))
548, 52, 53sylanbrc 587 . . . . . . 7 ((((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ 𝐴 ∈ ℤ) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁𝐴)) ∈ ℕ0)
5554exp31 424 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∈ ℤ → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁𝐴)) ∈ ℕ0)))
562, 3, 55syl2anc 588 . . . . 5 (𝐵 ∈ (0...𝑁) → (𝐴 ∈ ℤ → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁𝐴)) ∈ ℕ0)))
571, 56mpan9 511 . . . 4 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁𝐴)) ∈ ℕ0))
5857imp 411 . . 3 (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁𝐴)) ∈ ℕ0)
59 elfznn0 13050 . . . 4 (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℕ0)
6059ad2antrr 726 . . 3 (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → 𝐴 ∈ ℕ0)
61 elfzle2 12961 . . . . . . 7 (𝐵 ∈ (0...𝑁) → 𝐵𝑁)
6261adantl 486 . . . . . 6 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐵𝑁)
63 elfzel2 12955 . . . . . . . . . 10 (𝐴 ∈ (0...𝑁) → 𝑁 ∈ ℤ)
6463zcnd 12128 . . . . . . . . 9 (𝐴 ∈ (0...𝑁) → 𝑁 ∈ ℂ)
651zcnd 12128 . . . . . . . . 9 (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℂ)
6664, 65jca 516 . . . . . . . 8 (𝐴 ∈ (0...𝑁) → (𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ))
6766adantr 485 . . . . . . 7 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ))
68 npcan 10934 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑁𝐴) + 𝐴) = 𝑁)
6967, 68syl 17 . . . . . 6 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → ((𝑁𝐴) + 𝐴) = 𝑁)
7062, 69breqtrrd 5061 . . . . 5 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐵 ≤ ((𝑁𝐴) + 𝐴))
713zred 12127 . . . . . . 7 (𝐵 ∈ (0...𝑁) → 𝐵 ∈ ℝ)
7271adantl 486 . . . . . 6 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐵 ∈ ℝ)
7363zred 12127 . . . . . . . 8 (𝐴 ∈ (0...𝑁) → 𝑁 ∈ ℝ)
741zred 12127 . . . . . . . 8 (𝐴 ∈ (0...𝑁) → 𝐴 ∈ ℝ)
7573, 74resubcld 11107 . . . . . . 7 (𝐴 ∈ (0...𝑁) → (𝑁𝐴) ∈ ℝ)
7675adantr 485 . . . . . 6 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁𝐴) ∈ ℝ)
7774adantr 485 . . . . . 6 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → 𝐴 ∈ ℝ)
7872, 76, 77lesubadd2d 11278 . . . . 5 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → ((𝐵 − (𝑁𝐴)) ≤ 𝐴𝐵 ≤ ((𝑁𝐴) + 𝐴)))
7970, 78mpbird 260 . . . 4 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐵 − (𝑁𝐴)) ≤ 𝐴)
8079adantr 485 . . 3 (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁𝐴)) ≤ 𝐴)
81 elfz2nn0 13048 . . 3 ((𝐵 − (𝑁𝐴)) ∈ (0...𝐴) ↔ ((𝐵 − (𝑁𝐴)) ∈ ℕ0𝐴 ∈ ℕ0 ∧ (𝐵 − (𝑁𝐴)) ≤ 𝐴))
8258, 60, 80, 81syl3anbrc 1341 . 2 (((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) ∧ 𝑁 < (𝐴 + 𝐵)) → (𝐵 − (𝑁𝐴)) ∈ (0...𝐴))
8382ex 417 1 ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁𝐴)) ∈ (0...𝐴)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   class class class wbr 5033  (class class class)co 7151  ℂcc 10574  ℝcr 10575  0cc0 10576   + caddc 10579   < clt 10714   ≤ cle 10715   − cmin 10909  ℕ0cn0 11935  ℤcz 12021  ...cfz 12940 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-nn 11676  df-n0 11936  df-z 12022  df-uz 12284  df-fz 12941 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator