Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝑌 → (𝐹‘𝑎) = (𝐹‘𝑌)) |
2 | 1 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑎 = 𝑌 → ((𝐹‘𝑏) − (𝐹‘𝑎)) = ((𝐹‘𝑏) − (𝐹‘𝑌))) |
3 | 2 | fveq2d 6195 |
. . . . . 6
⊢ (𝑎 = 𝑌 → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑏) − (𝐹‘𝑌)))) |
4 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑎 = 𝑌 → (𝑏 − 𝑎) = (𝑏 − 𝑌)) |
5 | 4 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑎 = 𝑌 → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑏 − 𝑌))) |
6 | 5 | oveq2d 6666 |
. . . . . 6
⊢ (𝑎 = 𝑌 → (𝑀 · (abs‘(𝑏 − 𝑎))) = (𝑀 · (abs‘(𝑏 − 𝑌)))) |
7 | 3, 6 | breq12d 4666 |
. . . . 5
⊢ (𝑎 = 𝑌 → ((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎))) ↔ (abs‘((𝐹‘𝑏) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑏 − 𝑌))))) |
8 | 7 | imbi2d 330 |
. . . 4
⊢ (𝑎 = 𝑌 → ((𝜑 → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎)))) ↔ (𝜑 → (abs‘((𝐹‘𝑏) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑏 − 𝑌)))))) |
9 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑏 = 𝑋 → (𝐹‘𝑏) = (𝐹‘𝑋)) |
10 | 9 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑏 = 𝑋 → ((𝐹‘𝑏) − (𝐹‘𝑌)) = ((𝐹‘𝑋) − (𝐹‘𝑌))) |
11 | 10 | fveq2d 6195 |
. . . . . 6
⊢ (𝑏 = 𝑋 → (abs‘((𝐹‘𝑏) − (𝐹‘𝑌))) = (abs‘((𝐹‘𝑋) − (𝐹‘𝑌)))) |
12 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑏 = 𝑋 → (𝑏 − 𝑌) = (𝑋 − 𝑌)) |
13 | 12 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑏 = 𝑋 → (abs‘(𝑏 − 𝑌)) = (abs‘(𝑋 − 𝑌))) |
14 | 13 | oveq2d 6666 |
. . . . . 6
⊢ (𝑏 = 𝑋 → (𝑀 · (abs‘(𝑏 − 𝑌))) = (𝑀 · (abs‘(𝑋 − 𝑌)))) |
15 | 11, 14 | breq12d 4666 |
. . . . 5
⊢ (𝑏 = 𝑋 → ((abs‘((𝐹‘𝑏) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑏 − 𝑌))) ↔ (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌))))) |
16 | 15 | imbi2d 330 |
. . . 4
⊢ (𝑏 = 𝑋 → ((𝜑 → (abs‘((𝐹‘𝑏) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑏 − 𝑌)))) ↔ (𝜑 → (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌)))))) |
17 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → (𝐹‘𝑦) = (𝐹‘𝑏)) |
18 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
19 | 17, 18 | oveqan12d 6669 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑏 ∧ 𝑥 = 𝑎) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑏) − (𝐹‘𝑎))) |
20 | 19 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑦 = 𝑏 ∧ 𝑥 = 𝑎) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) |
21 | | oveq12 6659 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑏 ∧ 𝑥 = 𝑎) → (𝑦 − 𝑥) = (𝑏 − 𝑎)) |
22 | 21 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑏 ∧ 𝑥 = 𝑎) → (abs‘(𝑦 − 𝑥)) = (abs‘(𝑏 − 𝑎))) |
23 | 22 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑦 = 𝑏 ∧ 𝑥 = 𝑎) → (𝑀 · (abs‘(𝑦 − 𝑥))) = (𝑀 · (abs‘(𝑏 − 𝑎)))) |
24 | 20, 23 | breq12d 4666 |
. . . . . . 7
⊢ ((𝑦 = 𝑏 ∧ 𝑥 = 𝑎) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑀 · (abs‘(𝑦 − 𝑥))) ↔ (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎))))) |
25 | 24 | ancoms 469 |
. . . . . 6
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑀 · (abs‘(𝑦 − 𝑥))) ↔ (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎))))) |
26 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎)) |
27 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝐹‘𝑥) = (𝐹‘𝑏)) |
28 | 26, 27 | oveqan12d 6669 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → ((𝐹‘𝑦) − (𝐹‘𝑥)) = ((𝐹‘𝑎) − (𝐹‘𝑏))) |
29 | 28 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → (abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) = (abs‘((𝐹‘𝑎) − (𝐹‘𝑏)))) |
30 | | oveq12 6659 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → (𝑦 − 𝑥) = (𝑎 − 𝑏)) |
31 | 30 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → (abs‘(𝑦 − 𝑥)) = (abs‘(𝑎 − 𝑏))) |
32 | 31 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → (𝑀 · (abs‘(𝑦 − 𝑥))) = (𝑀 · (abs‘(𝑎 − 𝑏)))) |
33 | 29, 32 | breq12d 4666 |
. . . . . . 7
⊢ ((𝑦 = 𝑎 ∧ 𝑥 = 𝑏) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑀 · (abs‘(𝑦 − 𝑥))) ↔ (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) ≤ (𝑀 · (abs‘(𝑎 − 𝑏))))) |
34 | 33 | ancoms 469 |
. . . . . 6
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑎) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑥))) ≤ (𝑀 · (abs‘(𝑦 − 𝑥))) ↔ (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) ≤ (𝑀 · (abs‘(𝑎 − 𝑏))))) |
35 | | dvlip.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
36 | | dvlip.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | | iccssre 12255 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
38 | 35, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
39 | | dvlip.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
40 | | cncff 22696 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
42 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ 𝑎 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑎) ∈ ℂ) |
43 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑏) ∈ ℂ) |
44 | 42, 43 | anim12dan 882 |
. . . . . . . . . 10
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((𝐹‘𝑎) ∈ ℂ ∧ (𝐹‘𝑏) ∈ ℂ)) |
45 | 41, 44 | sylan 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((𝐹‘𝑎) ∈ ℂ ∧ (𝐹‘𝑏) ∈ ℂ)) |
46 | 45 | simprd 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝐹‘𝑏) ∈ ℂ) |
47 | 45 | simpld 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝐹‘𝑎) ∈ ℂ) |
48 | 46, 47 | abssubd 14192 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) = (abs‘((𝐹‘𝑎) − (𝐹‘𝑏)))) |
49 | | ax-resscn 9993 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
50 | 38, 49 | syl6ss 3615 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
51 | 50 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴[,]𝐵)) → 𝑏 ∈ ℂ) |
52 | 51 | adantrl 752 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → 𝑏 ∈ ℂ) |
53 | 50 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴[,]𝐵)) → 𝑎 ∈ ℂ) |
54 | 53 | adantrr 753 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → 𝑎 ∈ ℂ) |
55 | 52, 54 | abssubd 14192 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑎 − 𝑏))) |
56 | 55 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝑀 · (abs‘(𝑏 − 𝑎))) = (𝑀 · (abs‘(𝑎 − 𝑏)))) |
57 | 48, 56 | breq12d 4666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎))) ↔ (abs‘((𝐹‘𝑎) − (𝐹‘𝑏))) ≤ (𝑀 · (abs‘(𝑎 − 𝑏))))) |
58 | 41 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
59 | | simpr2 1068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑏 ∈ (𝐴[,]𝐵)) |
60 | 58, 59 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝐹‘𝑏) ∈ ℂ) |
61 | | simpr1 1067 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑎 ∈ (𝐴[,]𝐵)) |
62 | 58, 61 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝐹‘𝑎) ∈ ℂ) |
63 | 60, 62 | subeq0ad 10402 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (((𝐹‘𝑏) − (𝐹‘𝑎)) = 0 ↔ (𝐹‘𝑏) = (𝐹‘𝑎))) |
64 | 63 | biimpar 502 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) = 0) |
65 | 64 | abs00bd 14031 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) = 0) |
66 | 38 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝐴[,]𝐵) ⊆ ℝ) |
67 | 66, 61 | sseldd 3604 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑎 ∈ ℝ) |
68 | 67 | rexrd 10089 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑎 ∈ ℝ*) |
69 | 66, 59 | sseldd 3604 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑏 ∈ ℝ) |
70 | 69 | rexrd 10089 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑏 ∈ ℝ*) |
71 | | ioon0 12201 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏)) |
72 | 68, 70, 71 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏)) |
73 | | dvlip.m |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℝ) |
74 | 73 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 𝑀 ∈ ℝ) |
75 | 69, 67 | resubcld 10458 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑏 − 𝑎) ∈ ℝ) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝑏 − 𝑎) ∈ ℝ) |
77 | 35 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐴 ∈ ℝ) |
78 | 77 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐴 ∈
ℝ*) |
79 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐵 ∈ ℝ) |
80 | | elicc2 12238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑎 ∈ (𝐴[,]𝐵) ↔ (𝑎 ∈ ℝ ∧ 𝐴 ≤ 𝑎 ∧ 𝑎 ≤ 𝐵))) |
81 | 77, 79, 80 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎 ∈ (𝐴[,]𝐵) ↔ (𝑎 ∈ ℝ ∧ 𝐴 ≤ 𝑎 ∧ 𝑎 ≤ 𝐵))) |
82 | 61, 81 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎 ∈ ℝ ∧ 𝐴 ≤ 𝑎 ∧ 𝑎 ≤ 𝐵)) |
83 | 82 | simp2d 1074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐴 ≤ 𝑎) |
84 | | iooss1 12210 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑎) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝑏)) |
85 | 78, 83, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝑏)) |
86 | 79 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐵 ∈
ℝ*) |
87 | | elicc2 12238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑏 ∈ (𝐴[,]𝐵) ↔ (𝑏 ∈ ℝ ∧ 𝐴 ≤ 𝑏 ∧ 𝑏 ≤ 𝐵))) |
88 | 77, 79, 87 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑏 ∈ (𝐴[,]𝐵) ↔ (𝑏 ∈ ℝ ∧ 𝐴 ≤ 𝑏 ∧ 𝑏 ≤ 𝐵))) |
89 | 59, 88 | mpbid 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑏 ∈ ℝ ∧ 𝐴 ≤ 𝑏 ∧ 𝑏 ≤ 𝐵)) |
90 | 89 | simp3d 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑏 ≤ 𝐵) |
91 | | iooss2 12211 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ ℝ*
∧ 𝑏 ≤ 𝐵) → (𝐴(,)𝑏) ⊆ (𝐴(,)𝐵)) |
92 | 86, 90, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝐴(,)𝑏) ⊆ (𝐴(,)𝐵)) |
93 | 85, 92 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝐵)) |
94 | | ssn0 3976 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎(,)𝑏) ⊆ (𝐴(,)𝐵) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅) |
95 | 93, 94 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅) |
96 | | n0 3931 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴(,)𝐵) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴(,)𝐵)) |
97 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) |
98 | | dvf 23671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ |
99 | | dvlip.d |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) |
100 | 99 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) |
101 | 98, 100 | mpbii 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
102 | 101 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
103 | 102 | abscld 14175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ) |
104 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑀 ∈ ℝ) |
105 | 102 | absge0d 14183 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘((ℝ D
𝐹)‘𝑥))) |
106 | | dvlip.l |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀) |
107 | 97, 103, 104, 105, 106 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝑀) |
108 | 107 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) → 0 ≤ 𝑀)) |
109 | 108 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∃𝑥 𝑥 ∈ (𝐴(,)𝐵) → 0 ≤ 𝑀)) |
110 | 109 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ∃𝑥 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝑀) |
111 | 96, 110 | sylan2b 492 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐴(,)𝐵) ≠ ∅) → 0 ≤ 𝑀) |
112 | 111 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐴(,)𝐵) ≠ ∅) → 0 ≤ 𝑀) |
113 | 95, 112 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ 𝑀) |
114 | | simpr3 1069 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑎 ≤ 𝑏) |
115 | 69, 67 | subge0d 10617 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (0 ≤ (𝑏 − 𝑎) ↔ 𝑎 ≤ 𝑏)) |
116 | 114, 115 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 0 ≤ (𝑏 − 𝑎)) |
117 | 116 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ (𝑏 − 𝑎)) |
118 | 74, 76, 113, 117 | mulge0d 10604 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ (𝑀 · (𝑏 − 𝑎))) |
119 | 118 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝑎(,)𝑏) ≠ ∅ → 0 ≤ (𝑀 · (𝑏 − 𝑎)))) |
120 | 72, 119 | sylbird 250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎 < 𝑏 → 0 ≤ (𝑀 · (𝑏 − 𝑎)))) |
121 | 69 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑏 ∈ ℂ) |
122 | 67 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑎 ∈ ℂ) |
123 | 121, 122 | subeq0ad 10402 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝑏 − 𝑎) = 0 ↔ 𝑏 = 𝑎)) |
124 | | equcom 1945 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑎 ↔ 𝑎 = 𝑏) |
125 | 123, 124 | syl6bb 276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝑏 − 𝑎) = 0 ↔ 𝑎 = 𝑏)) |
126 | | 0re 10040 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
127 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑀 ∈ ℝ) |
128 | 127 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑀 ∈ ℂ) |
129 | 128 | mul01d 10235 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑀 · 0) = 0) |
130 | 129 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 0 = (𝑀 · 0)) |
131 | | eqle 10139 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ 0 = (𝑀
· 0)) → 0 ≤ (𝑀 · 0)) |
132 | 126, 130,
131 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 0 ≤ (𝑀 · 0)) |
133 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 − 𝑎) = 0 → (𝑀 · (𝑏 − 𝑎)) = (𝑀 · 0)) |
134 | 133 | breq2d 4665 |
. . . . . . . . . . . . 13
⊢ ((𝑏 − 𝑎) = 0 → (0 ≤ (𝑀 · (𝑏 − 𝑎)) ↔ 0 ≤ (𝑀 · 0))) |
135 | 132, 134 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝑏 − 𝑎) = 0 → 0 ≤ (𝑀 · (𝑏 − 𝑎)))) |
136 | 125, 135 | sylbird 250 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎 = 𝑏 → 0 ≤ (𝑀 · (𝑏 − 𝑎)))) |
137 | 67, 69 | leloed 10180 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎 ≤ 𝑏 ↔ (𝑎 < 𝑏 ∨ 𝑎 = 𝑏))) |
138 | 114, 137 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎 < 𝑏 ∨ 𝑎 = 𝑏)) |
139 | 120, 136,
138 | mpjaod 396 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 0 ≤ (𝑀 · (𝑏 − 𝑎))) |
140 | 139 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → 0 ≤ (𝑀 · (𝑏 − 𝑎))) |
141 | 65, 140 | eqbrtrd 4675 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (𝑏 − 𝑎))) |
142 | 60, 62 | subcld 10392 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ∈ ℂ) |
143 | 142 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ∈ ℂ) |
144 | 143 | abscld 14175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℝ) |
145 | 144 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℂ) |
146 | 75 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑏 − 𝑎) ∈ ℝ) |
147 | 146 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑏 − 𝑎) ∈ ℂ) |
148 | 138 | ord 392 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (¬ 𝑎 < 𝑏 → 𝑎 = 𝑏)) |
149 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) |
150 | 149 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑏 → (𝐹‘𝑏) = (𝐹‘𝑎)) |
151 | 148, 150 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (¬ 𝑎 < 𝑏 → (𝐹‘𝑏) = (𝐹‘𝑎))) |
152 | 151 | necon1ad 2811 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((𝐹‘𝑏) ≠ (𝐹‘𝑎) → 𝑎 < 𝑏)) |
153 | 152 | imp 445 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 𝑎 < 𝑏) |
154 | 67 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 𝑎 ∈ ℝ) |
155 | 69 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 𝑏 ∈ ℝ) |
156 | 154, 155 | posdifd 10614 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑎 < 𝑏 ↔ 0 < (𝑏 − 𝑎))) |
157 | 153, 156 | mpbid 222 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 0 < (𝑏 − 𝑎)) |
158 | 157 | gt0ne0d 10592 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑏 − 𝑎) ≠ 0) |
159 | 145, 147,
158 | divrec2d 10805 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) / (𝑏 − 𝑎)) = ((1 / (𝑏 − 𝑎)) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))))) |
160 | | iccss2 12244 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵)) |
161 | 61, 59, 160 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵)) |
162 | 161 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵)) |
163 | 162 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → 𝑦 ∈ (𝐴[,]𝐵)) |
164 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
165 | 164 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑦) ∈ ℂ) |
166 | 163, 165 | syldan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (𝐹‘𝑦) ∈ ℂ) |
167 | 142 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ∈ ℂ) |
168 | 63 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (((𝐹‘𝑏) − (𝐹‘𝑎)) ≠ 0 ↔ (𝐹‘𝑏) ≠ (𝐹‘𝑎))) |
169 | 168 | biimpar 502 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ≠ 0) |
170 | 169 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ≠ 0) |
171 | 166, 167,
170 | divcld 10801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℂ) |
172 | 164, 162 | feqresmpt 6250 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝐹 ↾ (𝑎[,]𝑏)) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (𝐹‘𝑦))) |
173 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
174 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐹‘𝑦) → (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎))) = ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) |
175 | 166, 172,
173, 174 | fmptco 6396 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
176 | | ref 13852 |
. . . . . . . . . . . . . . . . 17
⊢
ℜ:ℂ⟶ℝ |
177 | 176 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) →
ℜ:ℂ⟶ℝ) |
178 | 177 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ℜ = (𝑥 ∈ ℂ ↦ (ℜ‘𝑥))) |
179 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) → (ℜ‘𝑥) = (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
180 | 171, 175,
178, 179 | fmptco 6396 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℜ ∘ ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏)))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) |
181 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
182 | | rescncf 22700 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎[,]𝑏) ⊆ (𝐴[,]𝐵) → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ))) |
183 | 161, 181,
182 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ)) |
184 | 183 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ)) |
185 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) |
186 | 185 | divccncf 22709 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑏) − (𝐹‘𝑎)) ∈ ℂ ∧ ((𝐹‘𝑏) − (𝐹‘𝑎)) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ (ℂ–cn→ℂ)) |
187 | 143, 169,
186 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ (ℂ–cn→ℂ)) |
188 | 184, 187 | cncfco 22710 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏))) ∈ ((𝑎[,]𝑏)–cn→ℂ)) |
189 | | recncf 22705 |
. . . . . . . . . . . . . . . 16
⊢ ℜ
∈ (ℂ–cn→ℝ) |
190 | 189 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ℜ ∈ (ℂ–cn→ℝ)) |
191 | 188, 190 | cncfco 22710 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℜ ∘ ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏)))) ∈ ((𝑎[,]𝑏)–cn→ℝ)) |
192 | 180, 191 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) ∈ ((𝑎[,]𝑏)–cn→ℝ)) |
193 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ℝ ⊆
ℂ) |
194 | | iccssre 12255 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎[,]𝑏) ⊆ ℝ) |
195 | 154, 155,
194 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑎[,]𝑏) ⊆ ℝ) |
196 | 171 | recld 13934 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ ℝ) |
197 | 196 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ ℂ) |
198 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
199 | 198 | tgioo2 22606 |
. . . . . . . . . . . . . . . . 17
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
200 | | iccntr 22624 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏)) |
201 | 67, 69, 200 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((int‘(topGen‘ran
(,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏)) |
202 | 201 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((int‘(topGen‘ran
(,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏)) |
203 | 193, 195,
197, 199, 198, 202 | dvmptntr 23734 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) = (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))))) |
204 | | ioossicc 12259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎(,)𝑏) ⊆ (𝑎[,]𝑏) |
205 | 204 | sseli 3599 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑎[,]𝑏)) |
206 | 205, 171 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℂ) |
207 | | ovexd 6680 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → (((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ V) |
208 | | reelprrecn 10028 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
∈ {ℝ, ℂ} |
209 | 208 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ℝ ∈ {ℝ,
ℂ}) |
210 | 205, 166 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → (𝐹‘𝑦) ∈ ℂ) |
211 | 93 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝐵)) |
212 | 211 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → 𝑦 ∈ (𝐴(,)𝐵)) |
213 | 101 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
214 | 213 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ ℂ) |
215 | 212, 214 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → ((ℝ D 𝐹)‘𝑦) ∈ ℂ) |
216 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝐴[,]𝐵) ⊆ ℝ) |
217 | | ioossre 12235 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎(,)𝑏) ⊆ ℝ |
218 | 217 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑎(,)𝑏) ⊆ ℝ) |
219 | 198, 199 | dvres 23675 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ (𝑎(,)𝑏) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑎(,)𝑏)))) |
220 | 193, 164,
216, 218, 219 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝑎(,)𝑏)))) |
221 | | retop 22565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(topGen‘ran (,)) ∈ Top |
222 | | iooretop 22569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎(,)𝑏) ∈ (topGen‘ran
(,)) |
223 | | isopn3i 20886 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝑎(,)𝑏) ∈ (topGen‘ran (,))) →
((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏)) = (𝑎(,)𝑏)) |
224 | 221, 222,
223 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏)) = (𝑎(,)𝑏) |
225 | 224 | reseq2i 5393 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℝ
D 𝐹) ↾
((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) |
226 | 220, 225 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ (𝑎(,)𝑏))) |
227 | 204, 162 | syl5ss 3614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝑎(,)𝑏) ⊆ (𝐴[,]𝐵)) |
228 | 164, 227 | feqresmpt 6250 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝐹 ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹‘𝑦))) |
229 | 228 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹‘𝑦)))) |
230 | 101 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
231 | 230, 93 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)):(𝑎(,)𝑏)⟶ℂ) |
232 | 231 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦))) |
233 | 232 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦))) |
234 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ (𝑎(,)𝑏) → (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
235 | 234 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦)) |
236 | 233, 235 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦))) |
237 | 226, 229,
236 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹‘𝑦))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦))) |
238 | 209, 210,
215, 237, 143, 169 | dvmptdivc 23728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
239 | 206, 207,
238 | dvmptre 23732 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) |
240 | 203, 239 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) |
241 | 240 | dmeqd 5326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → dom (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) = dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) |
242 | | dmmptg 5632 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
(𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ V → dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = (𝑎(,)𝑏)) |
243 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ V |
244 | 243 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝑎(,)𝑏) → (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ V) |
245 | 242, 244 | mprg 2926 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = (𝑎(,)𝑏) |
246 | 241, 245 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → dom (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) = (𝑎(,)𝑏)) |
247 | 154, 155,
153, 192, 246 | mvth 23755 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ∃𝑥 ∈ (𝑎(,)𝑏)((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎)) / (𝑏 − 𝑎))) |
248 | 240 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))))‘𝑥) = ((𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑥)) |
249 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥)) |
250 | 249 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) = (((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) |
251 | 250 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
252 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
253 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ V |
254 | 251, 252,
253 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑥) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
255 | 248, 254 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))))‘𝑥) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
256 | | ubicc2 12289 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ* ∧ 𝑎
≤ 𝑏) → 𝑏 ∈ (𝑎[,]𝑏)) |
257 | 68, 70, 114, 256 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑏 ∈ (𝑎[,]𝑏)) |
258 | 257 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑏 ∈ (𝑎[,]𝑏)) |
259 | 17 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑏 → ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) = ((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) |
260 | 259 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑏 → (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
261 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
262 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ V |
263 | 260, 261,
262 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (𝑎[,]𝑏) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) = (ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
264 | 258, 263 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) = (ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
265 | | lbicc2 12288 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ* ∧ 𝑎
≤ 𝑏) → 𝑎 ∈ (𝑎[,]𝑏)) |
266 | 68, 70, 114, 265 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → 𝑎 ∈ (𝑎[,]𝑏)) |
267 | 266 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑎 ∈ (𝑎[,]𝑏)) |
268 | 26 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑎 → ((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))) = ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) |
269 | 268 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑎 → (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
270 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ V |
271 | 269, 261,
270 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (𝑎[,]𝑏) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎) = (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
272 | 267, 271 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎) = (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
273 | 264, 272 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎)) = ((ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) − (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) |
274 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝐹‘𝑏) ∈ ℂ) |
275 | 274, 143,
169 | divcld 10801 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℂ) |
276 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (𝐹‘𝑎) ∈ ℂ) |
277 | 276, 143,
169 | divcld 10801 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℂ) |
278 | 275, 277 | resubd 13956 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℜ‘(((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))) − ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = ((ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) − (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))) |
279 | 274, 276,
143, 169 | divsubdird 10840 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (((𝐹‘𝑏) − (𝐹‘𝑎)) / ((𝐹‘𝑏) − (𝐹‘𝑎))) = (((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))) − ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
280 | 143, 169 | dividd 10799 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (((𝐹‘𝑏) − (𝐹‘𝑎)) / ((𝐹‘𝑏) − (𝐹‘𝑎))) = 1) |
281 | 279, 280 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))) − ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = 1) |
282 | 281 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℜ‘(((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))) − ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = (ℜ‘1)) |
283 | | re1 13894 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℜ‘1) = 1 |
284 | 282, 283 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (ℜ‘(((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎))) − ((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = 1) |
285 | 278, 284 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) − (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = 1) |
286 | 285 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘((𝐹‘𝑏) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) − (ℜ‘((𝐹‘𝑎) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) = 1) |
287 | 273, 286 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎)) = 1) |
288 | 287 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎)) / (𝑏 − 𝑎)) = (1 / (𝑏 − 𝑎))) |
289 | 255, 288 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎)) / (𝑏 − 𝑎)) ↔ (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎)))) |
290 | 289 | rexbidva 3049 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (∃𝑥 ∈ (𝑎(,)𝑏)((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹‘𝑦) / ((𝐹‘𝑏) − (𝐹‘𝑎)))))‘𝑎)) / (𝑏 − 𝑎)) ↔ ∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎)))) |
291 | 247, 290 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎))) |
292 | 211 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ (𝐴(,)𝐵)) |
293 | 213 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
294 | 292, 293 | syldan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
295 | 142 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ∈ ℂ) |
296 | 169 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝐹‘𝑏) − (𝐹‘𝑎)) ≠ 0) |
297 | 294, 295,
296 | divcld 10801 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℂ) |
298 | 297 | recld 13934 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ ℝ) |
299 | 144 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℝ) |
300 | 298, 299 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ ℝ) |
301 | 294 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ) |
302 | 127 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑀 ∈ ℝ) |
303 | 297 | abscld 14175 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ∈ ℝ) |
304 | 143 | absge0d 14183 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 0 ≤ (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) |
305 | 304 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 0 ≤ (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) |
306 | 297 | releabsd 14190 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ (abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))))) |
307 | 298, 303,
299, 305, 306 | lemul1ad 10963 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))))) |
308 | 297, 295 | absmuld 14193 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))) · ((𝐹‘𝑏) − (𝐹‘𝑎)))) = ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))))) |
309 | 294, 295,
296 | divcan1d 10802 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))) · ((𝐹‘𝑏) − (𝐹‘𝑎))) = ((ℝ D 𝐹)‘𝑥)) |
310 | 309 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎))) · ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (abs‘((ℝ D 𝐹)‘𝑥))) |
311 | 308, 310 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) = (abs‘((ℝ D 𝐹)‘𝑥))) |
312 | 307, 311 | breqtrd 4679 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ (abs‘((ℝ D 𝐹)‘𝑥))) |
313 | 106 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀) |
314 | 313 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀) |
315 | 292, 314 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀) |
316 | 300, 301,
302, 312, 315 | letrd 10194 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ 𝑀) |
317 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢
((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) = ((1 / (𝑏 − 𝑎)) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))))) |
318 | 317 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢
((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎)) → (((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ 𝑀 ↔ ((1 / (𝑏 − 𝑎)) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ 𝑀)) |
319 | 316, 318 | syl5ibcom 235 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎)) → ((1 / (𝑏 − 𝑎)) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ 𝑀)) |
320 | 319 | rexlimdva 3031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹‘𝑏) − (𝐹‘𝑎)))) = (1 / (𝑏 − 𝑎)) → ((1 / (𝑏 − 𝑎)) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ 𝑀)) |
321 | 291, 320 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((1 / (𝑏 − 𝑎)) · (abs‘((𝐹‘𝑏) − (𝐹‘𝑎)))) ≤ 𝑀) |
322 | 159, 321 | eqbrtrd 4675 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → ((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) / (𝑏 − 𝑎)) ≤ 𝑀) |
323 | 73 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → 𝑀 ∈ ℝ) |
324 | | ledivmul2 10902 |
. . . . . . . . . 10
⊢
(((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑏 − 𝑎) ∈ ℝ ∧ 0 < (𝑏 − 𝑎))) → (((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) / (𝑏 − 𝑎)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (𝑏 − 𝑎)))) |
325 | 144, 323,
146, 157, 324 | syl112anc 1330 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (((abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) / (𝑏 − 𝑎)) ≤ 𝑀 ↔ (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (𝑏 − 𝑎)))) |
326 | 322, 325 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) ∧ (𝐹‘𝑏) ≠ (𝐹‘𝑎)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (𝑏 − 𝑎))) |
327 | 141, 326 | pm2.61dane 2881 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (𝑏 − 𝑎))) |
328 | 67, 69, 114 | abssubge0d 14170 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (abs‘(𝑏 − 𝑎)) = (𝑏 − 𝑎)) |
329 | 328 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (𝑀 · (abs‘(𝑏 − 𝑎))) = (𝑀 · (𝑏 − 𝑎))) |
330 | 327, 329 | breqtrrd 4681 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎 ≤ 𝑏)) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎)))) |
331 | 25, 34, 38, 57, 330 | wlogle 10561 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎)))) |
332 | 331 | expcom 451 |
. . . 4
⊢ ((𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹‘𝑏) − (𝐹‘𝑎))) ≤ (𝑀 · (abs‘(𝑏 − 𝑎))))) |
333 | 8, 16, 332 | vtocl2ga 3274 |
. . 3
⊢ ((𝑌 ∈ (𝐴[,]𝐵) ∧ 𝑋 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌))))) |
334 | 333 | ancoms 469 |
. 2
⊢ ((𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌))))) |
335 | 334 | impcom 446 |
1
⊢ ((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹‘𝑋) − (𝐹‘𝑌))) ≤ (𝑀 · (abs‘(𝑋 − 𝑌)))) |