Metamath Proof Explorer

Theorem 2elfz2melfz

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)

Ref Expression
Assertion 2elfz2melfz ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 < ( 𝐴 + 𝐵 ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ... 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝐴 ∈ ℤ )
2 elfzel2 ⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
3 elfzelz ⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → 𝐵 ∈ ℤ )
4 simplr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → 𝐵 ∈ ℤ )
5 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝑁 − 𝐴 ) ∈ ℤ )
6 5 adantlr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( 𝑁 − 𝐴 ) ∈ ℤ )
7 4 6 zsubcld ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℤ )
8 7 adantr ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℤ )
9 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
10 9 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → 𝑁 ∈ ℝ )
11 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
12 11 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
13 12 expcom ⊢ ( 𝐵 ∈ ℤ → ( 𝐴 ∈ ℤ → ( 𝐴 + 𝐵 ) ∈ ℝ ) )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℤ → ( 𝐴 + 𝐵 ) ∈ ℝ ) )
15 14 imp ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
16 10 15 10 ltsub1d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( 𝑁 < ( 𝐴 + 𝐵 ) ↔ ( 𝑁 − 𝑁 ) < ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
17 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
18 9 17 anim12i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
19 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
20 18 19 anim12i ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) )
21 id ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
22 21 21 resubcld ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 𝑁 ) ∈ ℝ )
23 22 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) → ( 𝑁 − 𝑁 ) ∈ ℝ )
24 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
25 24 expcom ⊢ ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℝ → ( 𝐴 + 𝐵 ) ∈ ℝ ) )
26 25 adantl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ∈ ℝ → ( 𝐴 + 𝐵 ) ∈ ℝ ) )
27 26 imp ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
28 simpll ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) → 𝑁 ∈ ℝ )
29 27 28 resubcld ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) − 𝑁 ) ∈ ℝ )
30 23 29 jca ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝑁 − 𝑁 ) ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) − 𝑁 ) ∈ ℝ ) )
31 ltle ⊢ ( ( ( 𝑁 − 𝑁 ) ∈ ℝ ∧ ( ( 𝐴 + 𝐵 ) − 𝑁 ) ∈ ℝ ) → ( ( 𝑁 − 𝑁 ) < ( ( 𝐴 + 𝐵 ) − 𝑁 ) → ( 𝑁 − 𝑁 ) ≤ ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
32 20 30 31 3syl ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝑁 − 𝑁 ) < ( ( 𝐴 + 𝐵 ) − 𝑁 ) → ( 𝑁 − 𝑁 ) ≤ ( ( 𝐴 + 𝐵 ) − 𝑁 ) ) )
33 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
34 33 subidd ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 𝑁 ) = 0 )
35 34 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( 𝑁 − 𝑁 ) = 0 )
36 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
37 36 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
38 37 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → 𝐵 ∈ ℂ )
39 33 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → 𝑁 ∈ ℂ )
40 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
41 40 adantl ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℂ )
42 simp3 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ℂ )
43 simp1 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → 𝐵 ∈ ℂ )
44 42 43 addcomd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
45 44 oveq1d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝑁 ) = ( ( 𝐵 + 𝐴 ) − 𝑁 ) )
46 subsub3 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) = ( ( 𝐵 + 𝐴 ) − 𝑁 ) )
47 45 46 eqtr4d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) − 𝑁 ) = ( 𝐵 − ( 𝑁 − 𝐴 ) ) )
48 38 39 41 47 syl3anc ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 + 𝐵 ) − 𝑁 ) = ( 𝐵 − ( 𝑁 − 𝐴 ) ) )
49 35 48 breq12d ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝑁 − 𝑁 ) ≤ ( ( 𝐴 + 𝐵 ) − 𝑁 ) ↔ 0 ≤ ( 𝐵 − ( 𝑁 − 𝐴 ) ) ) )
50 32 49 sylibd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( ( 𝑁 − 𝑁 ) < ( ( 𝐴 + 𝐵 ) − 𝑁 ) → 0 ≤ ( 𝐵 − ( 𝑁 − 𝐴 ) ) ) )
51 16 50 sylbid ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) → ( 𝑁 < ( 𝐴 + 𝐵 ) → 0 ≤ ( 𝐵 − ( 𝑁 − 𝐴 ) ) ) )
52 51 imp ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → 0 ≤ ( 𝐵 − ( 𝑁 − 𝐴 ) ) )
53 elnn0z ⊢ ( ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ↔ ( ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℤ ∧ 0 ≤ ( 𝐵 − ( 𝑁 − 𝐴 ) ) ) )
54 8 52 53 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ 𝐴 ∈ ℤ ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 )
55 54 exp31 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ℤ → ( 𝑁 < ( 𝐴 + 𝐵 ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ) ) )
56 2 3 55 syl2anc ⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → ( 𝐴 ∈ ℤ → ( 𝑁 < ( 𝐴 + 𝐵 ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ) ) )
57 1 56 mpan9 ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 < ( 𝐴 + 𝐵 ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ) )
58 57 imp ⊢ ( ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 )
59 elfznn0 ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝐴 ∈ ℕ0 )
60 59 ad2antrr ⊢ ( ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → 𝐴 ∈ ℕ0 )
61 elfzle2 ⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → 𝐵 ≤ 𝑁 )
62 61 adantl ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ≤ 𝑁 )
63 elfzel2 ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
64 63 zcnd ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℂ )
65 1 zcnd ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝐴 ∈ ℂ )
66 64 65 jca ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
67 66 adantr ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
68 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑁 − 𝐴 ) + 𝐴 ) = 𝑁 )
69 67 68 syl ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐴 ) + 𝐴 ) = 𝑁 )
70 62 69 breqtrrd ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ≤ ( ( 𝑁 − 𝐴 ) + 𝐴 ) )
71 3 zred ⊢ ( 𝐵 ∈ ( 0 ... 𝑁 ) → 𝐵 ∈ ℝ )
72 71 adantl ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ ℝ )
73 63 zred ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ )
74 1 zred ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → 𝐴 ∈ ℝ )
75 73 74 resubcld ⊢ ( 𝐴 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
76 75 adantr ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐴 ) ∈ ℝ )
77 74 adantr ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ∈ ℝ )
78 72 76 77 lesubadd2d ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵 − ( 𝑁 − 𝐴 ) ) ≤ 𝐴 ↔ 𝐵 ≤ ( ( 𝑁 − 𝐴 ) + 𝐴 ) ) )
79 70 78 mpbird ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ≤ 𝐴 )
80 79 adantr ⊢ ( ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ≤ 𝐴 )
81 elfz2nn0 ⊢ ( ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ... 𝐴 ) ↔ ( ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0 ∧ ( 𝐵 − ( 𝑁 − 𝐴 ) ) ≤ 𝐴 ) )
82 58 60 80 81 syl3anbrc ⊢ ( ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑁 < ( 𝐴 + 𝐵 ) ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ... 𝐴 ) )
83 82 ex ⊢ ( ( 𝐴 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 < ( 𝐴 + 𝐵 ) → ( 𝐵 − ( 𝑁 − 𝐴 ) ) ∈ ( 0 ... 𝐴 ) ) )