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

Metamath Proof Explorer

Theorem eluzgtdifelfzo

Description: Membership of the difference of integers in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 17-Sep-2018)

Ref Expression
Assertion eluzgtdifelfzo ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) )
3 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝐴 ∈ ℤ )
5 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℤ )
6 5 ad2antrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
7 simprr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
8 6 7 zsubcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ) → ( 𝑁 − 𝐵 ) ∈ ℤ )
9 8 ancoms ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝑁 − 𝐵 ) ∈ ℤ )
10 4 9 zaddcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝐴 + ( 𝑁 − 𝐵 ) ) ∈ ℤ )
11 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
12 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
13 posdif ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ 0 < ( 𝐴 − 𝐵 ) ) )
14 13 biimpd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 → 0 < ( 𝐴 − 𝐵 ) ) )
15 11 12 14 syl2anr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐵 < 𝐴 → 0 < ( 𝐴 − 𝐵 ) ) )
16 15 adantld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → 0 < ( 𝐴 − 𝐵 ) ) )
17 16 imp ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 0 < ( 𝐴 − 𝐵 ) )
18 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
19 12 11 18 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
20 19 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
21 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℝ )
22 21 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ℝ )
23 20 22 ltaddposd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 0 < ( 𝐴 − 𝐵 ) ↔ 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) ) )
24 17 23 mpbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) )
25 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
26 25 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝐴 ∈ ℂ )
27 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) → 𝑁 ∈ ℂ )
28 27 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ℂ )
29 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
30 29 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
31 30 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝐵 ∈ ℂ )
32 addsub12 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( 𝑁 − 𝐵 ) ) = ( 𝑁 + ( 𝐴 − 𝐵 ) ) )
33 32 breq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) ↔ 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) ) )
34 26 28 31 33 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) ↔ 𝑁 < ( 𝑁 + ( 𝐴 − 𝐵 ) ) ) )
35 24 34 mpbird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) )
36 elfzo2 ⊢ ( 𝑁 ∈ ( 𝐴 ..^ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ∈ ℤ ∧ 𝑁 < ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) )
37 2 10 35 36 syl3anbrc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → 𝑁 ∈ ( 𝐴 ..^ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) )
38 fzosubel3 ⊢ ( ( 𝑁 ∈ ( 𝐴 ..^ ( 𝐴 + ( 𝑁 − 𝐵 ) ) ) ∧ ( 𝑁 − 𝐵 ) ∈ ℤ ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) )
39 37 9 38 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) )
40 39 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐵 < 𝐴 ) → ( 𝑁 − 𝐴 ) ∈ ( 0 ..^ ( 𝑁 − 𝐵 ) ) ) )