Proof of Theorem fzomaxdiflem
| Step | Hyp | Ref
| Expression |
| 1 | | elfzoelz 13699 |
. . . . . 6
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐵 ∈ ℤ) |
| 2 | 1 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐵 ∈ ℤ) |
| 3 | | elfzoelz 13699 |
. . . . . 6
⊢ (𝐴 ∈ (𝐶..^𝐷) → 𝐴 ∈ ℤ) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐴 ∈ ℤ) |
| 5 | 2, 4 | zsubcld 12727 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) ∈ ℤ) |
| 6 | 5 | zred 12722 |
. . 3
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) ∈ ℝ) |
| 7 | 2 | zred 12722 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐵 ∈ ℝ) |
| 8 | 4 | zred 12722 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐴 ∈ ℝ) |
| 9 | 7, 8 | subge0d 11853 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (0 ≤ (𝐵 − 𝐴) ↔ 𝐴 ≤ 𝐵)) |
| 10 | 9 | biimpar 477 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → 0 ≤ (𝐵 − 𝐴)) |
| 11 | | absid 15335 |
. . 3
⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 ≤ (𝐵 − 𝐴)) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
| 12 | 6, 10, 11 | syl2an2r 685 |
. 2
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
| 13 | | elfzoel1 13697 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐶 ∈ ℤ) |
| 14 | 13 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐶 ∈ ℤ) |
| 15 | 14 | zred 12722 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐶 ∈ ℝ) |
| 16 | 7, 15 | resubcld 11691 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐶) ∈ ℝ) |
| 17 | | elfzoel2 13698 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐷 ∈ ℤ) |
| 18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐷 ∈ ℤ) |
| 19 | 18, 14 | zsubcld 12727 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐷 − 𝐶) ∈ ℤ) |
| 20 | 19 | zred 12722 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐷 − 𝐶) ∈ ℝ) |
| 21 | | elfzole1 13707 |
. . . . . . 7
⊢ (𝐴 ∈ (𝐶..^𝐷) → 𝐶 ≤ 𝐴) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐶 ≤ 𝐴) |
| 23 | 15, 8, 7, 22 | lesub2dd 11880 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) ≤ (𝐵 − 𝐶)) |
| 24 | 18 | zred 12722 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐷 ∈ ℝ) |
| 25 | | elfzolt2 13708 |
. . . . . . 7
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐵 < 𝐷) |
| 26 | 25 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐵 < 𝐷) |
| 27 | 7, 24, 15, 26 | ltsub1dd 11875 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐶) < (𝐷 − 𝐶)) |
| 28 | 6, 16, 20, 23, 27 | lelttrd 11419 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) < (𝐷 − 𝐶)) |
| 29 | 28 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) < (𝐷 − 𝐶)) |
| 30 | | 0zd 12625 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 0 ∈ ℤ) |
| 31 | | elfzo 13701 |
. . . . 5
⊢ (((𝐵 − 𝐴) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝐷 − 𝐶) ∈ ℤ) → ((𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶)) ↔ (0 ≤ (𝐵 − 𝐴) ∧ (𝐵 − 𝐴) < (𝐷 − 𝐶)))) |
| 32 | 5, 30, 19, 31 | syl3anc 1373 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶)) ↔ (0 ≤ (𝐵 − 𝐴) ∧ (𝐵 − 𝐴) < (𝐷 − 𝐶)))) |
| 33 | 32 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → ((𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶)) ↔ (0 ≤ (𝐵 − 𝐴) ∧ (𝐵 − 𝐴) < (𝐷 − 𝐶)))) |
| 34 | 10, 29, 33 | mpbir2and 713 |
. 2
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶))) |
| 35 | 12, 34 | eqeltrd 2841 |
1
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶))) |