Proof of Theorem fzomaxdiflem
Step | Hyp | Ref
| Expression |
1 | | elfzoelz 12339 |
. . . . . . 7
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐵 ∈ ℤ) |
2 | 1 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐵 ∈ ℤ) |
3 | | elfzoelz 12339 |
. . . . . . 7
⊢ (𝐴 ∈ (𝐶..^𝐷) → 𝐴 ∈ ℤ) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐴 ∈ ℤ) |
5 | 2, 4 | zsubcld 11363 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) ∈ ℤ) |
6 | 5 | zred 11358 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) ∈ ℝ) |
7 | 6 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) ∈ ℝ) |
8 | 2 | zred 11358 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐵 ∈ ℝ) |
9 | 4 | zred 11358 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐴 ∈ ℝ) |
10 | 8, 9 | subge0d 10496 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (0 ≤ (𝐵 − 𝐴) ↔ 𝐴 ≤ 𝐵)) |
11 | 10 | biimpar 501 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → 0 ≤ (𝐵 − 𝐴)) |
12 | | absid 13884 |
. . 3
⊢ (((𝐵 − 𝐴) ∈ ℝ ∧ 0 ≤ (𝐵 − 𝐴)) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
13 | 7, 11, 12 | syl2anc 691 |
. 2
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) = (𝐵 − 𝐴)) |
14 | | elfzoel1 12337 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐶 ∈ ℤ) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐶 ∈ ℤ) |
16 | 15 | zred 11358 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐶 ∈ ℝ) |
17 | 8, 16 | resubcld 10337 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐶) ∈ ℝ) |
18 | | elfzoel2 12338 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐷 ∈ ℤ) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐷 ∈ ℤ) |
20 | 19, 15 | zsubcld 11363 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐷 − 𝐶) ∈ ℤ) |
21 | 20 | zred 11358 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐷 − 𝐶) ∈ ℝ) |
22 | | elfzole1 12347 |
. . . . . . 7
⊢ (𝐴 ∈ (𝐶..^𝐷) → 𝐶 ≤ 𝐴) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐶 ≤ 𝐴) |
24 | 16, 9, 8, 23 | lesub2dd 10523 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) ≤ (𝐵 − 𝐶)) |
25 | 19 | zred 11358 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐷 ∈ ℝ) |
26 | | elfzolt2 12348 |
. . . . . . 7
⊢ (𝐵 ∈ (𝐶..^𝐷) → 𝐵 < 𝐷) |
27 | 26 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 𝐵 < 𝐷) |
28 | 8, 25, 16, 27 | ltsub1dd 10518 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐶) < (𝐷 − 𝐶)) |
29 | 6, 17, 21, 24, 28 | lelttrd 10074 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → (𝐵 − 𝐴) < (𝐷 − 𝐶)) |
30 | 29 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) < (𝐷 − 𝐶)) |
31 | | 0zd 11266 |
. . . . 5
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → 0 ∈ ℤ) |
32 | | elfzo 12341 |
. . . . 5
⊢ (((𝐵 − 𝐴) ∈ ℤ ∧ 0 ∈ ℤ
∧ (𝐷 − 𝐶) ∈ ℤ) → ((𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶)) ↔ (0 ≤ (𝐵 − 𝐴) ∧ (𝐵 − 𝐴) < (𝐷 − 𝐶)))) |
33 | 5, 31, 20, 32 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶)) ↔ (0 ≤ (𝐵 − 𝐴) ∧ (𝐵 − 𝐴) < (𝐷 − 𝐶)))) |
34 | 33 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → ((𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶)) ↔ (0 ≤ (𝐵 − 𝐴) ∧ (𝐵 − 𝐴) < (𝐷 − 𝐶)))) |
35 | 11, 30, 34 | mpbir2and 959 |
. 2
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (𝐵 − 𝐴) ∈ (0..^(𝐷 − 𝐶))) |
36 | 13, 35 | eqeltrd 2688 |
1
⊢ (((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) ∧ 𝐴 ≤ 𝐵) → (abs‘(𝐵 − 𝐴)) ∈ (0..^(𝐷 − 𝐶))) |