Metamath Proof Explorer

Theorem fzomaxdiflem

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

Ref Expression
Assertion fzomaxdiflem ⊢ A ∈ C ..^ D ∧ B ∈ C ..^ D ∧ A ≤ B → B − A ∈ 0 ..^ D − C

Proof

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