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

Metamath Proof Explorer

Theorem fzomaxdiflem

Description: Lemma for fzomaxdif . (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion fzomaxdiflem ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐵 ∈ ℤ )
2 1 adantl ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐵 ∈ ℤ )
3 elfzoelz ⊢ ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐴 ∈ ℤ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐴 ∈ ℤ )
5 2 4 zsubcld ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐵 − 𝐴 ) ∈ ℤ )
6 5 zred ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
7 2 zred ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐵 ∈ ℝ )
8 4 zred ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐴 ∈ ℝ )
9 7 8 subge0d ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 0 ≤ ( 𝐵 − 𝐴 ) ↔ 𝐴 ≤ 𝐵 ) )
10 9 biimpar ⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → 0 ≤ ( 𝐵 − 𝐴 ) )
11 absid ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 𝐵 − 𝐴 ) ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
12 6 10 11 syl2an2r ⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
13 elfzoel1 ⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐶 ∈ ℤ )
14 13 adantl ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐶 ∈ ℤ )
15 14 zred ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐶 ∈ ℝ )
16 7 15 resubcld ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐵 − 𝐶 ) ∈ ℝ )
17 elfzoel2 ⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐷 ∈ ℤ )
18 17 adantl ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐷 ∈ ℤ )
19 18 14 zsubcld ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐷 − 𝐶 ) ∈ ℤ )
20 19 zred ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐷 − 𝐶 ) ∈ ℝ )
21 elfzole1 ⊢ ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐶 ≤ 𝐴 )
22 21 adantr ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐶 ≤ 𝐴 )
23 15 8 7 22 lesub2dd ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐵 − 𝐴 ) ≤ ( 𝐵 − 𝐶 ) )
24 18 zred ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐷 ∈ ℝ )
25 elfzolt2 ⊢ ( 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) → 𝐵 < 𝐷 )
26 25 adantl ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 𝐵 < 𝐷 )
27 7 24 15 26 ltsub1dd ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐵 − 𝐶 ) < ( 𝐷 − 𝐶 ) )
28 6 16 20 23 27 lelttrd ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( 𝐵 − 𝐴 ) < ( 𝐷 − 𝐶 ) )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 − 𝐴 ) < ( 𝐷 − 𝐶 ) )
30 0zd ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → 0 ∈ ℤ )
31 elfzo ⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝐷 − 𝐶 ) ∈ ℤ ) → ( ( 𝐵 − 𝐴 ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) ↔ ( 0 ≤ ( 𝐵 − 𝐴 ) ∧ ( 𝐵 − 𝐴 ) < ( 𝐷 − 𝐶 ) ) ) )
32 5 30 19 31 syl3anc ⊢ ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) → ( ( 𝐵 − 𝐴 ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) ↔ ( 0 ≤ ( 𝐵 − 𝐴 ) ∧ ( 𝐵 − 𝐴 ) < ( 𝐷 − 𝐶 ) ) ) )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐵 − 𝐴 ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) ↔ ( 0 ≤ ( 𝐵 − 𝐴 ) ∧ ( 𝐵 − 𝐴 ) < ( 𝐷 − 𝐶 ) ) ) )
34 10 29 33 mpbir2and ⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )
35 12 34 eqeltrd ⊢ ( ( ( 𝐴 ∈ ( 𝐶 ..^ 𝐷 ) ∧ 𝐵 ∈ ( 𝐶 ..^ 𝐷 ) ) ∧ 𝐴 ≤ 𝐵 ) → ( abs ‘ ( 𝐵 − 𝐴 ) ) ∈ ( 0 ..^ ( 𝐷 − 𝐶 ) ) )