Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvlip Structured version   Visualization version   GIF version

Theorem dvlip 24692
 Description: A function with derivative bounded by 𝑀 is 𝑀-Lipschitz continuous. (Contributed by Mario Carneiro, 3-Mar-2015.)
Hypotheses
Ref Expression
dvlip.a (𝜑𝐴 ∈ ℝ)
dvlip.b (𝜑𝐵 ∈ ℝ)
dvlip.f (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
dvlip.d (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
dvlip.m (𝜑𝑀 ∈ ℝ)
dvlip.l ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
Assertion
Ref Expression
dvlip ((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥   𝑥,𝐹   𝑥,𝑀
Allowed substitution hints:   𝑋(𝑥)   𝑌(𝑥)

Proof of Theorem dvlip
Dummy variables 𝑎 𝑏 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6658 . . . . . . . 8 (𝑎 = 𝑌 → (𝐹𝑎) = (𝐹𝑌))
21oveq2d 7166 . . . . . . 7 (𝑎 = 𝑌 → ((𝐹𝑏) − (𝐹𝑎)) = ((𝐹𝑏) − (𝐹𝑌)))
32fveq2d 6662 . . . . . 6 (𝑎 = 𝑌 → (abs‘((𝐹𝑏) − (𝐹𝑎))) = (abs‘((𝐹𝑏) − (𝐹𝑌))))
4 oveq2 7158 . . . . . . . 8 (𝑎 = 𝑌 → (𝑏𝑎) = (𝑏𝑌))
54fveq2d 6662 . . . . . . 7 (𝑎 = 𝑌 → (abs‘(𝑏𝑎)) = (abs‘(𝑏𝑌)))
65oveq2d 7166 . . . . . 6 (𝑎 = 𝑌 → (𝑀 · (abs‘(𝑏𝑎))) = (𝑀 · (abs‘(𝑏𝑌))))
73, 6breq12d 5045 . . . . 5 (𝑎 = 𝑌 → ((abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))) ↔ (abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌)))))
87imbi2d 344 . . . 4 (𝑎 = 𝑌 → ((𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))) ↔ (𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌))))))
9 fveq2 6658 . . . . . . 7 (𝑏 = 𝑋 → (𝐹𝑏) = (𝐹𝑋))
109fvoveq1d 7172 . . . . . 6 (𝑏 = 𝑋 → (abs‘((𝐹𝑏) − (𝐹𝑌))) = (abs‘((𝐹𝑋) − (𝐹𝑌))))
11 fvoveq1 7173 . . . . . . 7 (𝑏 = 𝑋 → (abs‘(𝑏𝑌)) = (abs‘(𝑋𝑌)))
1211oveq2d 7166 . . . . . 6 (𝑏 = 𝑋 → (𝑀 · (abs‘(𝑏𝑌))) = (𝑀 · (abs‘(𝑋𝑌))))
1310, 12breq12d 5045 . . . . 5 (𝑏 = 𝑋 → ((abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌))) ↔ (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌)))))
1413imbi2d 344 . . . 4 (𝑏 = 𝑋 → ((𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌)))) ↔ (𝜑 → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌))))))
15 fveq2 6658 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝐹𝑦) = (𝐹𝑏))
16 fveq2 6658 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝐹𝑥) = (𝐹𝑎))
1715, 16oveqan12d 7169 . . . . . . . . 9 ((𝑦 = 𝑏𝑥 = 𝑎) → ((𝐹𝑦) − (𝐹𝑥)) = ((𝐹𝑏) − (𝐹𝑎)))
1817fveq2d 6662 . . . . . . . 8 ((𝑦 = 𝑏𝑥 = 𝑎) → (abs‘((𝐹𝑦) − (𝐹𝑥))) = (abs‘((𝐹𝑏) − (𝐹𝑎))))
19 oveq12 7159 . . . . . . . . . 10 ((𝑦 = 𝑏𝑥 = 𝑎) → (𝑦𝑥) = (𝑏𝑎))
2019fveq2d 6662 . . . . . . . . 9 ((𝑦 = 𝑏𝑥 = 𝑎) → (abs‘(𝑦𝑥)) = (abs‘(𝑏𝑎)))
2120oveq2d 7166 . . . . . . . 8 ((𝑦 = 𝑏𝑥 = 𝑎) → (𝑀 · (abs‘(𝑦𝑥))) = (𝑀 · (abs‘(𝑏𝑎))))
2218, 21breq12d 5045 . . . . . . 7 ((𝑦 = 𝑏𝑥 = 𝑎) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))))
2322ancoms 462 . . . . . 6 ((𝑥 = 𝑎𝑦 = 𝑏) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))))
24 fveq2 6658 . . . . . . . . . 10 (𝑦 = 𝑎 → (𝐹𝑦) = (𝐹𝑎))
25 fveq2 6658 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝐹𝑥) = (𝐹𝑏))
2624, 25oveqan12d 7169 . . . . . . . . 9 ((𝑦 = 𝑎𝑥 = 𝑏) → ((𝐹𝑦) − (𝐹𝑥)) = ((𝐹𝑎) − (𝐹𝑏)))
2726fveq2d 6662 . . . . . . . 8 ((𝑦 = 𝑎𝑥 = 𝑏) → (abs‘((𝐹𝑦) − (𝐹𝑥))) = (abs‘((𝐹𝑎) − (𝐹𝑏))))
28 oveq12 7159 . . . . . . . . . 10 ((𝑦 = 𝑎𝑥 = 𝑏) → (𝑦𝑥) = (𝑎𝑏))
2928fveq2d 6662 . . . . . . . . 9 ((𝑦 = 𝑎𝑥 = 𝑏) → (abs‘(𝑦𝑥)) = (abs‘(𝑎𝑏)))
3029oveq2d 7166 . . . . . . . 8 ((𝑦 = 𝑎𝑥 = 𝑏) → (𝑀 · (abs‘(𝑦𝑥))) = (𝑀 · (abs‘(𝑎𝑏))))
3127, 30breq12d 5045 . . . . . . 7 ((𝑦 = 𝑎𝑥 = 𝑏) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑎) − (𝐹𝑏))) ≤ (𝑀 · (abs‘(𝑎𝑏)))))
3231ancoms 462 . . . . . 6 ((𝑥 = 𝑏𝑦 = 𝑎) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑎) − (𝐹𝑏))) ≤ (𝑀 · (abs‘(𝑎𝑏)))))
33 dvlip.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
34 dvlip.b . . . . . . 7 (𝜑𝐵 ∈ ℝ)
35 iccssre 12861 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
3633, 34, 35syl2anc 587 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
37 dvlip.f . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
38 cncff 23594 . . . . . . . . . . 11 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
3937, 38syl 17 . . . . . . . . . 10 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
40 ffvelrn 6840 . . . . . . . . . . 11 ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ 𝑎 ∈ (𝐴[,]𝐵)) → (𝐹𝑎) ∈ ℂ)
41 ffvelrn 6840 . . . . . . . . . . 11 ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝐹𝑏) ∈ ℂ)
4240, 41anim12dan 621 . . . . . . . . . 10 ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((𝐹𝑎) ∈ ℂ ∧ (𝐹𝑏) ∈ ℂ))
4339, 42sylan 583 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((𝐹𝑎) ∈ ℂ ∧ (𝐹𝑏) ∈ ℂ))
4443simprd 499 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝐹𝑏) ∈ ℂ)
4543simpld 498 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝐹𝑎) ∈ ℂ)
4644, 45abssubd 14861 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑏) − (𝐹𝑎))) = (abs‘((𝐹𝑎) − (𝐹𝑏))))
47 ax-resscn 10632 . . . . . . . . . . . 12 ℝ ⊆ ℂ
4836, 47sstrdi 3904 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
4948sselda 3892 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐴[,]𝐵)) → 𝑏 ∈ ℂ)
5049adantrl 715 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → 𝑏 ∈ ℂ)
5148sselda 3892 . . . . . . . . . 10 ((𝜑𝑎 ∈ (𝐴[,]𝐵)) → 𝑎 ∈ ℂ)
5251adantrr 716 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → 𝑎 ∈ ℂ)
5350, 52abssubd 14861 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘(𝑏𝑎)) = (abs‘(𝑎𝑏)))
5453oveq2d 7166 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝑀 · (abs‘(𝑏𝑎))) = (𝑀 · (abs‘(𝑎𝑏))))
5546, 54breq12d 5045 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))) ↔ (abs‘((𝐹𝑎) − (𝐹𝑏))) ≤ (𝑀 · (abs‘(𝑎𝑏)))))
5639adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
57 simpr2 1192 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐴[,]𝐵))
5856, 57ffvelrnd 6843 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐹𝑏) ∈ ℂ)
59 simpr1 1191 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝐴[,]𝐵))
6056, 59ffvelrnd 6843 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐹𝑎) ∈ ℂ)
6158, 60subeq0ad 11045 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (((𝐹𝑏) − (𝐹𝑎)) = 0 ↔ (𝐹𝑏) = (𝐹𝑎)))
6261biimpar 481 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → ((𝐹𝑏) − (𝐹𝑎)) = 0)
6362abs00bd 14699 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) = 0)
6436adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐴[,]𝐵) ⊆ ℝ)
6564, 59sseldd 3893 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ ℝ)
6665rexrd 10729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ ℝ*)
6764, 57sseldd 3893 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ ℝ)
6867rexrd 10729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ ℝ*)
69 ioon0 12805 . . . . . . . . . . . . 13 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏))
7066, 68, 69syl2anc 587 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏))
71 dvlip.m . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℝ)
7271ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 𝑀 ∈ ℝ)
7367, 65resubcld 11106 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑏𝑎) ∈ ℝ)
7473adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝑏𝑎) ∈ ℝ)
7533adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐴 ∈ ℝ)
7675rexrd 10729 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐴 ∈ ℝ*)
7734adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐵 ∈ ℝ)
78 elicc2 12844 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑎 ∈ (𝐴[,]𝐵) ↔ (𝑎 ∈ ℝ ∧ 𝐴𝑎𝑎𝐵)))
7975, 77, 78syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 ∈ (𝐴[,]𝐵) ↔ (𝑎 ∈ ℝ ∧ 𝐴𝑎𝑎𝐵)))
8059, 79mpbid 235 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 ∈ ℝ ∧ 𝐴𝑎𝑎𝐵))
8180simp2d 1140 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐴𝑎)
82 iooss1 12814 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ*𝐴𝑎) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝑏))
8376, 81, 82syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝑏))
8477rexrd 10729 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐵 ∈ ℝ*)
85 elicc2 12844 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑏 ∈ (𝐴[,]𝐵) ↔ (𝑏 ∈ ℝ ∧ 𝐴𝑏𝑏𝐵)))
8675, 77, 85syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑏 ∈ (𝐴[,]𝐵) ↔ (𝑏 ∈ ℝ ∧ 𝐴𝑏𝑏𝐵)))
8757, 86mpbid 235 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑏 ∈ ℝ ∧ 𝐴𝑏𝑏𝐵))
8887simp3d 1141 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏𝐵)
89 iooss2 12815 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℝ*𝑏𝐵) → (𝐴(,)𝑏) ⊆ (𝐴(,)𝐵))
9084, 88, 89syl2anc 587 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐴(,)𝑏) ⊆ (𝐴(,)𝐵))
9183, 90sstrd 3902 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝐵))
92 ssn0 4296 . . . . . . . . . . . . . . . 16 (((𝑎(,)𝑏) ⊆ (𝐴(,)𝐵) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅)
9391, 92sylan 583 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅)
94 n0 4245 . . . . . . . . . . . . . . . . 17 ((𝐴(,)𝐵) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴(,)𝐵))
95 0red 10682 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
96 dvf 24606 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
97 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
9897feq2d 6484 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
9996, 98mpbii 236 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
10099ffvelrnda 6842 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
101100abscld 14844 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
10271adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑀 ∈ ℝ)
103100absge0d 14852 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑥)))
104 dvlip.l . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
10595, 101, 102, 103, 104letrd 10835 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝑀)
106105ex 416 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) → 0 ≤ 𝑀))
107106exlimdv 1934 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∃𝑥 𝑥 ∈ (𝐴(,)𝐵) → 0 ≤ 𝑀))
108107imp 410 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∃𝑥 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝑀)
10994, 108sylan2b 596 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴(,)𝐵) ≠ ∅) → 0 ≤ 𝑀)
110109adantlr 714 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐴(,)𝐵) ≠ ∅) → 0 ≤ 𝑀)
11193, 110syldan 594 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ 𝑀)
112 simpr3 1193 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎𝑏)
11367, 65subge0d 11268 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (0 ≤ (𝑏𝑎) ↔ 𝑎𝑏))
114112, 113mpbird 260 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 ≤ (𝑏𝑎))
115114adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ (𝑏𝑎))
11672, 74, 111, 115mulge0d 11255 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ (𝑀 · (𝑏𝑎)))
117116ex 416 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑎(,)𝑏) ≠ ∅ → 0 ≤ (𝑀 · (𝑏𝑎))))
11870, 117sylbird 263 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 < 𝑏 → 0 ≤ (𝑀 · (𝑏𝑎))))
11967recnd 10707 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ ℂ)
12065recnd 10707 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ ℂ)
121119, 120subeq0ad 11045 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑏𝑎) = 0 ↔ 𝑏 = 𝑎))
122 equcom 2025 . . . . . . . . . . . . 13 (𝑏 = 𝑎𝑎 = 𝑏)
123121, 122bitrdi 290 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑏𝑎) = 0 ↔ 𝑎 = 𝑏))
124 0re 10681 . . . . . . . . . . . . . 14 0 ∈ ℝ
12571adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑀 ∈ ℝ)
126125recnd 10707 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑀 ∈ ℂ)
127126mul01d 10877 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑀 · 0) = 0)
128127eqcomd 2764 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 = (𝑀 · 0))
129 eqle 10780 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ 0 = (𝑀 · 0)) → 0 ≤ (𝑀 · 0))
130124, 128, 129sylancr 590 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 ≤ (𝑀 · 0))
131 oveq2 7158 . . . . . . . . . . . . . 14 ((𝑏𝑎) = 0 → (𝑀 · (𝑏𝑎)) = (𝑀 · 0))
132131breq2d 5044 . . . . . . . . . . . . 13 ((𝑏𝑎) = 0 → (0 ≤ (𝑀 · (𝑏𝑎)) ↔ 0 ≤ (𝑀 · 0)))
133130, 132syl5ibrcom 250 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑏𝑎) = 0 → 0 ≤ (𝑀 · (𝑏𝑎))))
134123, 133sylbird 263 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 = 𝑏 → 0 ≤ (𝑀 · (𝑏𝑎))))
13565, 67leloed 10821 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎𝑏 ↔ (𝑎 < 𝑏𝑎 = 𝑏)))
136112, 135mpbid 235 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 < 𝑏𝑎 = 𝑏))
137118, 134, 136mpjaod 857 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 ≤ (𝑀 · (𝑏𝑎)))
138137adantr 484 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → 0 ≤ (𝑀 · (𝑏𝑎)))
13963, 138eqbrtrd 5054 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎)))
14058, 60subcld 11035 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
141140adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
142141abscld 14844 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℝ)
143142recnd 10707 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
14473adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑏𝑎) ∈ ℝ)
145144recnd 10707 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑏𝑎) ∈ ℂ)
146136ord 861 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (¬ 𝑎 < 𝑏𝑎 = 𝑏))
147 fveq2 6658 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
148147eqcomd 2764 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑏 → (𝐹𝑏) = (𝐹𝑎))
149146, 148syl6 35 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (¬ 𝑎 < 𝑏 → (𝐹𝑏) = (𝐹𝑎)))
150149necon1ad 2968 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝐹𝑏) ≠ (𝐹𝑎) → 𝑎 < 𝑏))
151150imp 410 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑎 < 𝑏)
15265adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑎 ∈ ℝ)
15367adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑏 ∈ ℝ)
154152, 153posdifd 11265 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎 < 𝑏 ↔ 0 < (𝑏𝑎)))
155151, 154mpbid 235 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 0 < (𝑏𝑎))
156155gt0ne0d 11242 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑏𝑎) ≠ 0)
157143, 145, 156divrec2d 11458 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) = ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
158 iccss2 12850 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵))
15959, 57, 158syl2anc 587 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵))
160159adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵))
161160sselda 3892 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → 𝑦 ∈ (𝐴[,]𝐵))
16239ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
163162ffvelrnda 6842 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑦) ∈ ℂ)
164161, 163syldan 594 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (𝐹𝑦) ∈ ℂ)
165140ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
16661necon3bid 2995 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (((𝐹𝑏) − (𝐹𝑎)) ≠ 0 ↔ (𝐹𝑏) ≠ (𝐹𝑎)))
167166biimpar 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑏) − (𝐹𝑎)) ≠ 0)
168167adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ≠ 0)
169164, 165, 168divcld 11454 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
170162, 160feqresmpt 6722 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹 ↾ (𝑎[,]𝑏)) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (𝐹𝑦)))
171 eqidd 2759 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) = (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))))
172 oveq1 7157 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑦) → (𝑥 / ((𝐹𝑏) − (𝐹𝑎))) = ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))
173164, 170, 171, 172fmptco 6882 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
174 ref 14519 . . . . . . . . . . . . . . . . 17 ℜ:ℂ⟶ℝ
175174a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℜ:ℂ⟶ℝ)
176175feqmptd 6721 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℜ = (𝑥 ∈ ℂ ↦ (ℜ‘𝑥)))
177 fveq2 6658 . . . . . . . . . . . . . . 15 (𝑥 = ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) → (ℜ‘𝑥) = (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
178169, 173, 176, 177fmptco 6882 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ ∘ ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏)))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
17937adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
180 rescncf 23598 . . . . . . . . . . . . . . . . . 18 ((𝑎[,]𝑏) ⊆ (𝐴[,]𝐵) → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ)))
181159, 179, 180sylc 65 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ))
182181adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ))
183 eqid 2758 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) = (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎))))
184183divccncf 23607 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ ∧ ((𝐹𝑏) − (𝐹𝑎)) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∈ (ℂ–cn→ℂ))
185141, 167, 184syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∈ (ℂ–cn→ℂ))
186182, 185cncfco 23608 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏))) ∈ ((𝑎[,]𝑏)–cn→ℂ))
187 recncf 23603 . . . . . . . . . . . . . . . 16 ℜ ∈ (ℂ–cn→ℝ)
188187a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℜ ∈ (ℂ–cn→ℝ))
189186, 188cncfco 23608 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ ∘ ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏)))) ∈ ((𝑎[,]𝑏)–cn→ℝ))
190178, 189eqeltrrd 2853 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) ∈ ((𝑎[,]𝑏)–cn→ℝ))
19147a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℝ ⊆ ℂ)
192 iccssre 12861 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎[,]𝑏) ⊆ ℝ)
193152, 153, 192syl2anc 587 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎[,]𝑏) ⊆ ℝ)
194169recld 14601 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
195194recnd 10707 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℂ)
196 eqid 2758 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
197196tgioo2 23504 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
198 iccntr 23522 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏))
19965, 67, 198syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏))
200199adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏))
201191, 193, 195, 197, 196, 200dvmptntr 24670 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))))
202 ioossicc 12865 . . . . . . . . . . . . . . . . . . 19 (𝑎(,)𝑏) ⊆ (𝑎[,]𝑏)
203202sseli 3888 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑎[,]𝑏))
204203, 169sylan2 595 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
205 ovexd 7185 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → (((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))) ∈ V)
206 reelprrecn 10667 . . . . . . . . . . . . . . . . . . 19 ℝ ∈ {ℝ, ℂ}
207206a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℝ ∈ {ℝ, ℂ})
208203, 164sylan2 595 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → (𝐹𝑦) ∈ ℂ)
20991adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝐵))
210209sselda 3892 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → 𝑦 ∈ (𝐴(,)𝐵))
21199ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
212211ffvelrnda 6842 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ ℂ)
213210, 212syldan 594 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → ((ℝ D 𝐹)‘𝑦) ∈ ℂ)
21436ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐴[,]𝐵) ⊆ ℝ)
215 ioossre 12840 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎(,)𝑏) ⊆ ℝ
216215a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎(,)𝑏) ⊆ ℝ)
217196, 197dvres 24610 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ (𝑎(,)𝑏) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))))
218191, 162, 214, 216, 217syl22anc 837 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))))
219 retop 23463 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) ∈ Top
220 iooretop 23467 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎(,)𝑏) ∈ (topGen‘ran (,))
221 isopn3i 21782 . . . . . . . . . . . . . . . . . . . . . 22 (((topGen‘ran (,)) ∈ Top ∧ (𝑎(,)𝑏) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏)) = (𝑎(,)𝑏))
222219, 220, 221mp2an 691 . . . . . . . . . . . . . . . . . . . . 21 ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏)) = (𝑎(,)𝑏)
223222reseq2i 5820 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ (𝑎(,)𝑏))
224218, 223eqtrdi 2809 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)))
225202, 160sstrid 3903 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎(,)𝑏) ⊆ (𝐴[,]𝐵))
226162, 225feqresmpt 6722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹 ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹𝑦)))
227226oveq2d 7166 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹𝑦))))
22899adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
229228, 91fssresd 6530 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)):(𝑎(,)𝑏)⟶ℂ)
230229feqmptd 6721 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)))
231230adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)))
232 fvres 6677 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑎(,)𝑏) → (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
233232mpteq2ia 5123 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦))
234231, 233eqtrdi 2809 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦)))
235224, 227, 2343eqtr3d 2801 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹𝑦))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦)))
236207, 208, 213, 235, 141, 167dvmptdivc 24664 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
237204, 205, 236dvmptre 24668 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
238201, 237eqtrd 2793 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
239238dmeqd 5745 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → dom (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
240 dmmptg 6071 . . . . . . . . . . . . . . 15 (∀𝑦 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V → dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑎(,)𝑏))
241 fvex 6671 . . . . . . . . . . . . . . . 16 (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
242241a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑎(,)𝑏) → (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V)
243240, 242mprg 3084 . . . . . . . . . . . . . 14 dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑎(,)𝑏)
244239, 243eqtrdi 2809 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → dom (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (𝑎(,)𝑏))
245152, 153, 151, 190, 244mvth 24691 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ∃𝑥 ∈ (𝑎(,)𝑏)((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)))
246238fveq1d 6660 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑥))
247 fveq2 6658 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥))
248247fvoveq1d 7172 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
249 eqid 2758 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
250 fvex 6671 . . . . . . . . . . . . . . . 16 (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
251248, 249, 250fvmpt 6759 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑥) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
252246, 251sylan9eq 2813 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
253 ubicc2 12897 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑎𝑏) → 𝑏 ∈ (𝑎[,]𝑏))
25466, 68, 112, 253syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝑎[,]𝑏))
255254ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑏 ∈ (𝑎[,]𝑏))
25615fvoveq1d 7172 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) = (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))))
257 eqid 2758 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
258 fvex 6671 . . . . . . . . . . . . . . . . . . 19 (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
259256, 257, 258fvmpt 6759 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑎[,]𝑏) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) = (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))))
260255, 259syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) = (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))))
261 lbicc2 12896 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑎𝑏) → 𝑎 ∈ (𝑎[,]𝑏))
26266, 68, 112, 261syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝑎[,]𝑏))
263262ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑎 ∈ (𝑎[,]𝑏))
26424fvoveq1d 7172 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑎 → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) = (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
265 fvex 6671 . . . . . . . . . . . . . . . . . . 19 (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
266264, 257, 265fvmpt 6759 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑎[,]𝑏) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎) = (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
267263, 266syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎) = (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
268260, 267oveq12d 7168 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) = ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))))
26958adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹𝑏) ∈ ℂ)
270269, 141, 167divcld 11454 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
27160adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹𝑎) ∈ ℂ)
272271, 141, 167divcld 11454 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
273270, 272resubd 14623 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ‘(((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))))
274269, 271, 141, 167divsubdird 11493 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((𝐹𝑏) − (𝐹𝑎)) / ((𝐹𝑏) − (𝐹𝑎))) = (((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
275141, 167dividd 11452 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((𝐹𝑏) − (𝐹𝑎)) / ((𝐹𝑏) − (𝐹𝑎))) = 1)
276274, 275eqtr3d 2795 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))) = 1)
277276fveq2d 6662 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ‘(((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = (ℜ‘1))
278 re1 14561 . . . . . . . . . . . . . . . . . . 19 (ℜ‘1) = 1
279277, 278eqtrdi 2809 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ‘(((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = 1)
280273, 279eqtr3d 2795 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = 1)
281280adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = 1)
282268, 281eqtrd 2793 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) = 1)
283282oveq1d 7165 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)) = (1 / (𝑏𝑎)))
284252, 283eqeq12d 2774 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)) ↔ (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎))))
285284rexbidva 3220 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (∃𝑥 ∈ (𝑎(,)𝑏)((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)) ↔ ∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎))))
286245, 285mpbid 235 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)))
287209sselda 3892 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ (𝐴(,)𝐵))
288211ffvelrnda 6842 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
289287, 288syldan 594 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
290140ad2antrr 725 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
291167adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ≠ 0)
292289, 290, 291divcld 11454 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
293292recld 14601 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
294142adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℝ)
295293, 294remulcld 10709 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
296289abscld 14844 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
297125ad2antrr 725 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑀 ∈ ℝ)
298292abscld 14844 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
299141absge0d 14852 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 0 ≤ (abs‘((𝐹𝑏) − (𝐹𝑎))))
300299adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 0 ≤ (abs‘((𝐹𝑏) − (𝐹𝑎))))
301292releabsd 14859 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ≤ (abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
302293, 298, 294, 300, 301lemul1ad 11617 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
303292, 290absmuld 14862 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) · ((𝐹𝑏) − (𝐹𝑎)))) = ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
304289, 290, 291divcan1d 11455 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) · ((𝐹𝑏) − (𝐹𝑎))) = ((ℝ D 𝐹)‘𝑥))
305304fveq2d 6662 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) · ((𝐹𝑏) − (𝐹𝑎)))) = (abs‘((ℝ D 𝐹)‘𝑥)))
306303, 305eqtr3d 2795 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) = (abs‘((ℝ D 𝐹)‘𝑥)))
307302, 306breqtrd 5058 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ (abs‘((ℝ D 𝐹)‘𝑥)))
308104ad4ant14 751 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
309287, 308syldan 594 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
310295, 296, 297, 307, 309letrd 10835 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀)
311 oveq1 7157 . . . . . . . . . . . . . 14 ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) = ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
312311breq1d 5042 . . . . . . . . . . . . 13 ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → (((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀 ↔ ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀))
313310, 312syl5ibcom 248 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀))
314313rexlimdva 3208 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀))
315286, 314mpd 15 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀)
316157, 315eqbrtrd 5054 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) ≤ 𝑀)
31771ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑀 ∈ ℝ)
318 ledivmul2 11557 . . . . . . . . . 10 (((abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑏𝑎) ∈ ℝ ∧ 0 < (𝑏𝑎))) → (((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) ≤ 𝑀 ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎))))
319142, 317, 144, 155, 318syl112anc 1371 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) ≤ 𝑀 ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎))))
320316, 319mpbid 235 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎)))
321139, 320pm2.61dane 3038 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎)))
32265, 67, 112abssubge0d 14839 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (abs‘(𝑏𝑎)) = (𝑏𝑎))
323322oveq2d 7166 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑀 · (abs‘(𝑏𝑎))) = (𝑀 · (𝑏𝑎)))
324321, 323breqtrrd 5060 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))))
32523, 32, 36, 55, 324wlogle 11211 . . . . 5 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))))
326325expcom 417 . . . 4 ((𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))))
3278, 14, 326vtocl2ga 3493 . . 3 ((𝑌 ∈ (𝐴[,]𝐵) ∧ 𝑋 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌)))))
328327ancoms 462 . 2 ((𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌)))))
329328impcom 411 1 ((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2951  ∃wrex 3071  Vcvv 3409   ⊆ wss 3858  ∅c0 4225  {cpr 4524   class class class wbr 5032   ↦ cmpt 5112  dom cdm 5524  ran crn 5525   ↾ cres 5526   ∘ ccom 5528  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   · cmul 10580  ℝ*cxr 10712   < clt 10713   ≤ cle 10714   − cmin 10908   / cdiv 11335  (,)cioo 12779  [,]cicc 12782  ℜcre 14504  abscabs 14641  TopOpenctopn 16753  topGenctg 16769  ℂfldccnfld 20166  Topctop 21593  intcnt 21717  –cn→ccncf 23577   D cdv 24562 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653  ax-addf 10654  ax-mulf 10655 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-iin 4886  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-om 7580  df-1st 7693  df-2nd 7694  df-supp 7836  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-er 8299  df-map 8418  df-pm 8419  df-ixp 8480  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-fsupp 8867  df-fi 8908  df-sup 8939  df-inf 8940  df-oi 9007  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-z 12021  df-dec 12138  df-uz 12283  df-q 12389  df-rp 12431  df-xneg 12548  df-xadd 12549  df-xmul 12550  df-ioo 12783  df-ico 12785  df-icc 12786  df-fz 12940  df-fzo 13083  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-mulr 16637  df-starv 16638  df-sca 16639  df-vsca 16640  df-ip 16641  df-tset 16642  df-ple 16643  df-ds 16645  df-unif 16646  df-hom 16647  df-cco 16648  df-rest 16754  df-topn 16755  df-0g 16773  df-gsum 16774  df-topgen 16775  df-pt 16776  df-prds 16779  df-xrs 16833  df-qtop 16838  df-imas 16839  df-xps 16841  df-mre 16915  df-mrc 16916  df-acs 16918  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-submnd 18023  df-mulg 18292  df-cntz 18514  df-cmn 18975  df-psmet 20158  df-xmet 20159  df-met 20160  df-bl 20161  df-mopn 20162  df-fbas 20163  df-fg 20164  df-cnfld 20167  df-top 21594  df-topon 21611  df-topsp 21633  df-bases 21646  df-cld 21719  df-ntr 21720  df-cls 21721  df-nei 21798  df-lp 21836  df-perf 21837  df-cn 21927  df-cnp 21928  df-haus 22015  df-cmp 22087  df-tx 22262  df-hmeo 22455  df-fil 22546  df-fm 22638  df-flim 22639  df-flf 22640  df-xms 23022  df-ms 23023  df-tms 23024  df-cncf 23579  df-limc 24565  df-dv 24566 This theorem is referenced by:  dvlipcn  24693  dvlip2  24694  dveq0  24699  dvfsumabs  24722  pige3ALT  25211  lgamgulmlem2  25714
 Copyright terms: Public domain W3C validator