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

Theorem dvlip 23876
Description: A function with derivative bounded by 𝑀 is Lipschitz continuous with Lipschitz constant equal to 𝑀. (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 6304 . . . . . . . 8 (𝑎 = 𝑌 → (𝐹𝑎) = (𝐹𝑌))
21oveq2d 6781 . . . . . . 7 (𝑎 = 𝑌 → ((𝐹𝑏) − (𝐹𝑎)) = ((𝐹𝑏) − (𝐹𝑌)))
32fveq2d 6308 . . . . . 6 (𝑎 = 𝑌 → (abs‘((𝐹𝑏) − (𝐹𝑎))) = (abs‘((𝐹𝑏) − (𝐹𝑌))))
4 oveq2 6773 . . . . . . . 8 (𝑎 = 𝑌 → (𝑏𝑎) = (𝑏𝑌))
54fveq2d 6308 . . . . . . 7 (𝑎 = 𝑌 → (abs‘(𝑏𝑎)) = (abs‘(𝑏𝑌)))
65oveq2d 6781 . . . . . 6 (𝑎 = 𝑌 → (𝑀 · (abs‘(𝑏𝑎))) = (𝑀 · (abs‘(𝑏𝑌))))
73, 6breq12d 4773 . . . . 5 (𝑎 = 𝑌 → ((abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))) ↔ (abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌)))))
87imbi2d 329 . . . 4 (𝑎 = 𝑌 → ((𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))) ↔ (𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌))))))
9 fveq2 6304 . . . . . . . 8 (𝑏 = 𝑋 → (𝐹𝑏) = (𝐹𝑋))
109oveq1d 6780 . . . . . . 7 (𝑏 = 𝑋 → ((𝐹𝑏) − (𝐹𝑌)) = ((𝐹𝑋) − (𝐹𝑌)))
1110fveq2d 6308 . . . . . 6 (𝑏 = 𝑋 → (abs‘((𝐹𝑏) − (𝐹𝑌))) = (abs‘((𝐹𝑋) − (𝐹𝑌))))
12 oveq1 6772 . . . . . . . 8 (𝑏 = 𝑋 → (𝑏𝑌) = (𝑋𝑌))
1312fveq2d 6308 . . . . . . 7 (𝑏 = 𝑋 → (abs‘(𝑏𝑌)) = (abs‘(𝑋𝑌)))
1413oveq2d 6781 . . . . . 6 (𝑏 = 𝑋 → (𝑀 · (abs‘(𝑏𝑌))) = (𝑀 · (abs‘(𝑋𝑌))))
1511, 14breq12d 4773 . . . . 5 (𝑏 = 𝑋 → ((abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌))) ↔ (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌)))))
1615imbi2d 329 . . . 4 (𝑏 = 𝑋 → ((𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑏𝑌)))) ↔ (𝜑 → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌))))))
17 fveq2 6304 . . . . . . . . . 10 (𝑦 = 𝑏 → (𝐹𝑦) = (𝐹𝑏))
18 fveq2 6304 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝐹𝑥) = (𝐹𝑎))
1917, 18oveqan12d 6784 . . . . . . . . 9 ((𝑦 = 𝑏𝑥 = 𝑎) → ((𝐹𝑦) − (𝐹𝑥)) = ((𝐹𝑏) − (𝐹𝑎)))
2019fveq2d 6308 . . . . . . . 8 ((𝑦 = 𝑏𝑥 = 𝑎) → (abs‘((𝐹𝑦) − (𝐹𝑥))) = (abs‘((𝐹𝑏) − (𝐹𝑎))))
21 oveq12 6774 . . . . . . . . . 10 ((𝑦 = 𝑏𝑥 = 𝑎) → (𝑦𝑥) = (𝑏𝑎))
2221fveq2d 6308 . . . . . . . . 9 ((𝑦 = 𝑏𝑥 = 𝑎) → (abs‘(𝑦𝑥)) = (abs‘(𝑏𝑎)))
2322oveq2d 6781 . . . . . . . 8 ((𝑦 = 𝑏𝑥 = 𝑎) → (𝑀 · (abs‘(𝑦𝑥))) = (𝑀 · (abs‘(𝑏𝑎))))
2420, 23breq12d 4773 . . . . . . 7 ((𝑦 = 𝑏𝑥 = 𝑎) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))))
2524ancoms 468 . . . . . 6 ((𝑥 = 𝑎𝑦 = 𝑏) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))))
26 fveq2 6304 . . . . . . . . . 10 (𝑦 = 𝑎 → (𝐹𝑦) = (𝐹𝑎))
27 fveq2 6304 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝐹𝑥) = (𝐹𝑏))
2826, 27oveqan12d 6784 . . . . . . . . 9 ((𝑦 = 𝑎𝑥 = 𝑏) → ((𝐹𝑦) − (𝐹𝑥)) = ((𝐹𝑎) − (𝐹𝑏)))
2928fveq2d 6308 . . . . . . . 8 ((𝑦 = 𝑎𝑥 = 𝑏) → (abs‘((𝐹𝑦) − (𝐹𝑥))) = (abs‘((𝐹𝑎) − (𝐹𝑏))))
30 oveq12 6774 . . . . . . . . . 10 ((𝑦 = 𝑎𝑥 = 𝑏) → (𝑦𝑥) = (𝑎𝑏))
3130fveq2d 6308 . . . . . . . . 9 ((𝑦 = 𝑎𝑥 = 𝑏) → (abs‘(𝑦𝑥)) = (abs‘(𝑎𝑏)))
3231oveq2d 6781 . . . . . . . 8 ((𝑦 = 𝑎𝑥 = 𝑏) → (𝑀 · (abs‘(𝑦𝑥))) = (𝑀 · (abs‘(𝑎𝑏))))
3329, 32breq12d 4773 . . . . . . 7 ((𝑦 = 𝑎𝑥 = 𝑏) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑎) − (𝐹𝑏))) ≤ (𝑀 · (abs‘(𝑎𝑏)))))
3433ancoms 468 . . . . . 6 ((𝑥 = 𝑏𝑦 = 𝑎) → ((abs‘((𝐹𝑦) − (𝐹𝑥))) ≤ (𝑀 · (abs‘(𝑦𝑥))) ↔ (abs‘((𝐹𝑎) − (𝐹𝑏))) ≤ (𝑀 · (abs‘(𝑎𝑏)))))
35 dvlip.a . . . . . . 7 (𝜑𝐴 ∈ ℝ)
36 dvlip.b . . . . . . 7 (𝜑𝐵 ∈ ℝ)
37 iccssre 12369 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
3835, 36, 37syl2anc 696 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
39 dvlip.f . . . . . . . . . . 11 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
40 cncff 22818 . . . . . . . . . . 11 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
4139, 40syl 17 . . . . . . . . . 10 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
42 ffvelrn 6472 . . . . . . . . . . 11 ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ 𝑎 ∈ (𝐴[,]𝐵)) → (𝐹𝑎) ∈ ℂ)
43 ffvelrn 6472 . . . . . . . . . . 11 ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝐹𝑏) ∈ ℂ)
4442, 43anim12dan 918 . . . . . . . . . 10 ((𝐹:(𝐴[,]𝐵)⟶ℂ ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((𝐹𝑎) ∈ ℂ ∧ (𝐹𝑏) ∈ ℂ))
4541, 44sylan 489 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((𝐹𝑎) ∈ ℂ ∧ (𝐹𝑏) ∈ ℂ))
4645simprd 482 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝐹𝑏) ∈ ℂ)
4745simpld 477 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝐹𝑎) ∈ ℂ)
4846, 47abssubd 14312 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑏) − (𝐹𝑎))) = (abs‘((𝐹𝑎) − (𝐹𝑏))))
49 ax-resscn 10106 . . . . . . . . . . . 12 ℝ ⊆ ℂ
5038, 49syl6ss 3721 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
5150sselda 3709 . . . . . . . . . 10 ((𝜑𝑏 ∈ (𝐴[,]𝐵)) → 𝑏 ∈ ℂ)
5251adantrl 754 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → 𝑏 ∈ ℂ)
5350sselda 3709 . . . . . . . . . 10 ((𝜑𝑎 ∈ (𝐴[,]𝐵)) → 𝑎 ∈ ℂ)
5453adantrr 755 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → 𝑎 ∈ ℂ)
5552, 54abssubd 14312 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘(𝑏𝑎)) = (abs‘(𝑎𝑏)))
5655oveq2d 6781 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (𝑀 · (abs‘(𝑏𝑎))) = (𝑀 · (abs‘(𝑎𝑏))))
5748, 56breq12d 4773 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))) ↔ (abs‘((𝐹𝑎) − (𝐹𝑏))) ≤ (𝑀 · (abs‘(𝑎𝑏)))))
5841adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
59 simpr2 1212 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝐴[,]𝐵))
6058, 59ffvelrnd 6475 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐹𝑏) ∈ ℂ)
61 simpr1 1210 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝐴[,]𝐵))
6258, 61ffvelrnd 6475 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐹𝑎) ∈ ℂ)
6360, 62subeq0ad 10515 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (((𝐹𝑏) − (𝐹𝑎)) = 0 ↔ (𝐹𝑏) = (𝐹𝑎)))
6463biimpar 503 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → ((𝐹𝑏) − (𝐹𝑎)) = 0)
6564abs00bd 14151 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) = 0)
6638adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐴[,]𝐵) ⊆ ℝ)
6766, 61sseldd 3710 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ ℝ)
6867rexrd 10202 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ ℝ*)
6966, 59sseldd 3710 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ ℝ)
7069rexrd 10202 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ ℝ*)
71 ioon0 12315 . . . . . . . . . . . . 13 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏))
7268, 70, 71syl2anc 696 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑎(,)𝑏) ≠ ∅ ↔ 𝑎 < 𝑏))
73 dvlip.m . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℝ)
7473ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 𝑀 ∈ ℝ)
7569, 67resubcld 10571 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑏𝑎) ∈ ℝ)
7675adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝑏𝑎) ∈ ℝ)
7735adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐴 ∈ ℝ)
7877rexrd 10202 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐴 ∈ ℝ*)
7936adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐵 ∈ ℝ)
80 elicc2 12352 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑎 ∈ (𝐴[,]𝐵) ↔ (𝑎 ∈ ℝ ∧ 𝐴𝑎𝑎𝐵)))
8177, 79, 80syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 ∈ (𝐴[,]𝐵) ↔ (𝑎 ∈ ℝ ∧ 𝐴𝑎𝑎𝐵)))
8261, 81mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 ∈ ℝ ∧ 𝐴𝑎𝑎𝐵))
8382simp2d 1135 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐴𝑎)
84 iooss1 12324 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ*𝐴𝑎) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝑏))
8578, 83, 84syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝑏))
8679rexrd 10202 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐵 ∈ ℝ*)
87 elicc2 12352 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑏 ∈ (𝐴[,]𝐵) ↔ (𝑏 ∈ ℝ ∧ 𝐴𝑏𝑏𝐵)))
8877, 79, 87syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑏 ∈ (𝐴[,]𝐵) ↔ (𝑏 ∈ ℝ ∧ 𝐴𝑏𝑏𝐵)))
8959, 88mpbid 222 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑏 ∈ ℝ ∧ 𝐴𝑏𝑏𝐵))
9089simp3d 1136 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏𝐵)
91 iooss2 12325 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℝ*𝑏𝐵) → (𝐴(,)𝑏) ⊆ (𝐴(,)𝐵))
9286, 90, 91syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐴(,)𝑏) ⊆ (𝐴(,)𝐵))
9385, 92sstrd 3719 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝐵))
94 ssn0 4084 . . . . . . . . . . . . . . . 16 (((𝑎(,)𝑏) ⊆ (𝐴(,)𝐵) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅)
9593, 94sylan 489 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → (𝐴(,)𝐵) ≠ ∅)
96 n0 4039 . . . . . . . . . . . . . . . . 17 ((𝐴(,)𝐵) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴(,)𝐵))
97 0red 10154 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ)
98 dvf 23791 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
99 dvlip.d . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
10099feq2d 6144 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
10198, 100mpbii 223 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
102101ffvelrnda 6474 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
103102abscld 14295 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
10473adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑀 ∈ ℝ)
105102absge0d 14303 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ (abs‘((ℝ D 𝐹)‘𝑥)))
106 dvlip.l . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
10797, 103, 104, 105, 106letrd 10307 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝑀)
108107ex 449 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) → 0 ≤ 𝑀))
109108exlimdv 1974 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∃𝑥 𝑥 ∈ (𝐴(,)𝐵) → 0 ≤ 𝑀))
110109imp 444 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ∃𝑥 𝑥 ∈ (𝐴(,)𝐵)) → 0 ≤ 𝑀)
11196, 110sylan2b 493 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴(,)𝐵) ≠ ∅) → 0 ≤ 𝑀)
112111adantlr 753 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐴(,)𝐵) ≠ ∅) → 0 ≤ 𝑀)
11395, 112syldan 488 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ 𝑀)
114 simpr3 1214 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎𝑏)
11569, 67subge0d 10730 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (0 ≤ (𝑏𝑎) ↔ 𝑎𝑏))
116114, 115mpbird 247 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 ≤ (𝑏𝑎))
117116adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ (𝑏𝑎))
11874, 76, 113, 117mulge0d 10717 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝑎(,)𝑏) ≠ ∅) → 0 ≤ (𝑀 · (𝑏𝑎)))
119118ex 449 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑎(,)𝑏) ≠ ∅ → 0 ≤ (𝑀 · (𝑏𝑎))))
12072, 119sylbird 250 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 < 𝑏 → 0 ≤ (𝑀 · (𝑏𝑎))))
12169recnd 10181 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ ℂ)
12267recnd 10181 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ ℂ)
123121, 122subeq0ad 10515 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑏𝑎) = 0 ↔ 𝑏 = 𝑎))
124 equcom 2064 . . . . . . . . . . . . 13 (𝑏 = 𝑎𝑎 = 𝑏)
125123, 124syl6bb 276 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑏𝑎) = 0 ↔ 𝑎 = 𝑏))
126 0re 10153 . . . . . . . . . . . . . 14 0 ∈ ℝ
12773adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑀 ∈ ℝ)
128127recnd 10181 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑀 ∈ ℂ)
129128mul01d 10348 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑀 · 0) = 0)
130129eqcomd 2730 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 = (𝑀 · 0))
131 eqle 10252 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ 0 = (𝑀 · 0)) → 0 ≤ (𝑀 · 0))
132126, 130, 131sylancr 698 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 ≤ (𝑀 · 0))
133 oveq2 6773 . . . . . . . . . . . . . 14 ((𝑏𝑎) = 0 → (𝑀 · (𝑏𝑎)) = (𝑀 · 0))
134133breq2d 4772 . . . . . . . . . . . . 13 ((𝑏𝑎) = 0 → (0 ≤ (𝑀 · (𝑏𝑎)) ↔ 0 ≤ (𝑀 · 0)))
135132, 134syl5ibrcom 237 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝑏𝑎) = 0 → 0 ≤ (𝑀 · (𝑏𝑎))))
136125, 135sylbird 250 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 = 𝑏 → 0 ≤ (𝑀 · (𝑏𝑎))))
13767, 69leloed 10293 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎𝑏 ↔ (𝑎 < 𝑏𝑎 = 𝑏)))
138114, 137mpbid 222 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎 < 𝑏𝑎 = 𝑏))
139120, 136, 138mpjaod 395 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 0 ≤ (𝑀 · (𝑏𝑎)))
140139adantr 472 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → 0 ≤ (𝑀 · (𝑏𝑎)))
14165, 140eqbrtrd 4782 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) = (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎)))
14260, 62subcld 10505 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
143142adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
144143abscld 14295 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℝ)
145144recnd 10181 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
14675adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑏𝑎) ∈ ℝ)
147146recnd 10181 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑏𝑎) ∈ ℂ)
148138ord 391 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (¬ 𝑎 < 𝑏𝑎 = 𝑏))
149 fveq2 6304 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑏 → (𝐹𝑎) = (𝐹𝑏))
150149eqcomd 2730 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑏 → (𝐹𝑏) = (𝐹𝑎))
151148, 150syl6 35 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (¬ 𝑎 < 𝑏 → (𝐹𝑏) = (𝐹𝑎)))
152151necon1ad 2913 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((𝐹𝑏) ≠ (𝐹𝑎) → 𝑎 < 𝑏))
153152imp 444 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑎 < 𝑏)
15467adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑎 ∈ ℝ)
15569adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑏 ∈ ℝ)
156154, 155posdifd 10727 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎 < 𝑏 ↔ 0 < (𝑏𝑎)))
157153, 156mpbid 222 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 0 < (𝑏𝑎))
158157gt0ne0d 10705 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑏𝑎) ≠ 0)
159145, 147, 158divrec2d 10918 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) = ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
160 iccss2 12358 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵))
16161, 59, 160syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵))
162161adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎[,]𝑏) ⊆ (𝐴[,]𝐵))
163162sselda 3709 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → 𝑦 ∈ (𝐴[,]𝐵))
16441ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
165164ffvelrnda 6474 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑦) ∈ ℂ)
166163, 165syldan 488 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (𝐹𝑦) ∈ ℂ)
167142ad2antrr 764 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
16863necon3bid 2940 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (((𝐹𝑏) − (𝐹𝑎)) ≠ 0 ↔ (𝐹𝑏) ≠ (𝐹𝑎)))
169168biimpar 503 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑏) − (𝐹𝑎)) ≠ 0)
170169adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ≠ 0)
171166, 167, 170divcld 10914 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
172164, 162feqresmpt 6364 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹 ↾ (𝑎[,]𝑏)) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (𝐹𝑦)))
173 eqidd 2725 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) = (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))))
174 oveq1 6772 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐹𝑦) → (𝑥 / ((𝐹𝑏) − (𝐹𝑎))) = ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))
175166, 172, 173, 174fmptco 6511 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
176 ref 13972 . . . . . . . . . . . . . . . . 17 ℜ:ℂ⟶ℝ
177176a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℜ:ℂ⟶ℝ)
178177feqmptd 6363 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℜ = (𝑥 ∈ ℂ ↦ (ℜ‘𝑥)))
179 fveq2 6304 . . . . . . . . . . . . . . 15 (𝑥 = ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) → (ℜ‘𝑥) = (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
180171, 175, 178, 179fmptco 6511 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ ∘ ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏)))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
18139adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
182 rescncf 22822 . . . . . . . . . . . . . . . . . 18 ((𝑎[,]𝑏) ⊆ (𝐴[,]𝐵) → (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ)))
183161, 181, 182sylc 65 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ))
184183adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹 ↾ (𝑎[,]𝑏)) ∈ ((𝑎[,]𝑏)–cn→ℂ))
185 eqid 2724 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) = (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎))))
186185divccncf 22831 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ ∧ ((𝐹𝑏) − (𝐹𝑎)) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∈ (ℂ–cn→ℂ))
187143, 169, 186syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∈ (ℂ–cn→ℂ))
188184, 187cncfco 22832 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏))) ∈ ((𝑎[,]𝑏)–cn→ℂ))
189 recncf 22827 . . . . . . . . . . . . . . . 16 ℜ ∈ (ℂ–cn→ℝ)
190189a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℜ ∈ (ℂ–cn→ℝ))
191188, 190cncfco 22832 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ ∘ ((𝑥 ∈ ℂ ↦ (𝑥 / ((𝐹𝑏) − (𝐹𝑎)))) ∘ (𝐹 ↾ (𝑎[,]𝑏)))) ∈ ((𝑎[,]𝑏)–cn→ℝ))
192180, 191eqeltrrd 2804 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) ∈ ((𝑎[,]𝑏)–cn→ℝ))
19349a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℝ ⊆ ℂ)
194 iccssre 12369 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎[,]𝑏) ⊆ ℝ)
195154, 155, 194syl2anc 696 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎[,]𝑏) ⊆ ℝ)
196171recld 14054 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
197196recnd 10181 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎[,]𝑏)) → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℂ)
198 eqid 2724 . . . . . . . . . . . . . . . . . 18 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
199198tgioo2 22728 . . . . . . . . . . . . . . . . 17 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
200 iccntr 22746 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏))
20167, 69, 200syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏))
202201adantr 472 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((int‘(topGen‘ran (,)))‘(𝑎[,]𝑏)) = (𝑎(,)𝑏))
203193, 195, 197, 199, 198, 202dvmptntr 23854 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))))
204 ioossicc 12373 . . . . . . . . . . . . . . . . . . 19 (𝑎(,)𝑏) ⊆ (𝑎[,]𝑏)
205204sseli 3705 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (𝑎(,)𝑏) → 𝑦 ∈ (𝑎[,]𝑏))
206205, 171sylan2 492 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
207 ovexd 6795 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → (((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))) ∈ V)
208 reelprrecn 10141 . . . . . . . . . . . . . . . . . . 19 ℝ ∈ {ℝ, ℂ}
209208a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ℝ ∈ {ℝ, ℂ})
210205, 166sylan2 492 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → (𝐹𝑦) ∈ ℂ)
21193adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎(,)𝑏) ⊆ (𝐴(,)𝐵))
212211sselda 3709 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → 𝑦 ∈ (𝐴(,)𝐵))
213101ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
214213ffvelrnda 6474 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑦) ∈ ℂ)
215212, 214syldan 488 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑦 ∈ (𝑎(,)𝑏)) → ((ℝ D 𝐹)‘𝑦) ∈ ℂ)
21638ad2antrr 764 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐴[,]𝐵) ⊆ ℝ)
217 ioossre 12349 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎(,)𝑏) ⊆ ℝ
218217a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎(,)𝑏) ⊆ ℝ)
219198, 199dvres 23795 . . . . . . . . . . . . . . . . . . . . 21 (((ℝ ⊆ ℂ ∧ 𝐹:(𝐴[,]𝐵)⟶ℂ) ∧ ((𝐴[,]𝐵) ⊆ ℝ ∧ (𝑎(,)𝑏) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))))
220193, 164, 216, 218, 219syl22anc 1440 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))))
221 retop 22687 . . . . . . . . . . . . . . . . . . . . . 22 (topGen‘ran (,)) ∈ Top
222 iooretop 22691 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎(,)𝑏) ∈ (topGen‘ran (,))
223 isopn3i 21009 . . . . . . . . . . . . . . . . . . . . . 22 (((topGen‘ran (,)) ∈ Top ∧ (𝑎(,)𝑏) ∈ (topGen‘ran (,))) → ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏)) = (𝑎(,)𝑏))
224221, 222, 223mp2an 710 . . . . . . . . . . . . . . . . . . . . 21 ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏)) = (𝑎(,)𝑏)
225224reseq2i 5500 . . . . . . . . . . . . . . . . . . . 20 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ (𝑎(,)𝑏))
226220, 225syl6eq 2774 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)))
227204, 162syl5ss 3720 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝑎(,)𝑏) ⊆ (𝐴[,]𝐵))
228164, 227feqresmpt 6364 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹 ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹𝑦)))
229228oveq2d 6781 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝐹 ↾ (𝑎(,)𝑏))) = (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹𝑦))))
230101adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
231230, 93fssresd 6184 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)):(𝑎(,)𝑏)⟶ℂ)
232231feqmptd 6363 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)))
233232adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)))
234 fvres 6320 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝑎(,)𝑏) → (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
235234mpteq2ia 4848 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹) ↾ (𝑎(,)𝑏))‘𝑦)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦))
236233, 235syl6eq 2774 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℝ D 𝐹) ↾ (𝑎(,)𝑏)) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦)))
237226, 229, 2363eqtr3d 2766 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (𝐹𝑦))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ ((ℝ D 𝐹)‘𝑦)))
238209, 210, 215, 237, 143, 169dvmptdivc 23848 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
239206, 207, 238dvmptre 23852 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
240203, 239eqtrd 2758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
241240dmeqd 5433 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → dom (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))
242 dmmptg 5745 . . . . . . . . . . . . . . 15 (∀𝑦 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V → dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑎(,)𝑏))
243 fvex 6314 . . . . . . . . . . . . . . . 16 (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
244243a1i 11 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑎(,)𝑏) → (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V)
245242, 244mprg 3028 . . . . . . . . . . . . . 14 dom (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑎(,)𝑏)
246241, 245syl6eq 2774 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → dom (ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))) = (𝑎(,)𝑏))
247154, 155, 153, 192, 246mvth 23875 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ∃𝑥 ∈ (𝑎(,)𝑏)((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)))
248240fveq1d 6306 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑥))
249 fveq2 6304 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑥 → ((ℝ D 𝐹)‘𝑦) = ((ℝ D 𝐹)‘𝑥))
250249oveq1d 6780 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑥 → (((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))) = (((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))))
251250fveq2d 6308 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑥 → (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
252 eqid 2724 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
253 fvex 6314 . . . . . . . . . . . . . . . 16 (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
254251, 252, 253fvmpt 6396 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝑎(,)𝑏) → ((𝑦 ∈ (𝑎(,)𝑏) ↦ (ℜ‘(((ℝ D 𝐹)‘𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑥) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
255248, 254sylan9eq 2778 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
256 ubicc2 12403 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑎𝑏) → 𝑏 ∈ (𝑎[,]𝑏))
25768, 70, 114, 256syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑏 ∈ (𝑎[,]𝑏))
258257ad2antrr 764 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑏 ∈ (𝑎[,]𝑏))
25917oveq1d 6780 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) = ((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))))
260259fveq2d 6308 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) = (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))))
261 eqid 2724 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))) = (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))
262 fvex 6314 . . . . . . . . . . . . . . . . . . 19 (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
263260, 261, 262fvmpt 6396 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (𝑎[,]𝑏) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) = (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))))
264258, 263syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) = (ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))))
265 lbicc2 12402 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*𝑎𝑏) → 𝑎 ∈ (𝑎[,]𝑏))
26668, 70, 114, 265syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → 𝑎 ∈ (𝑎[,]𝑏))
267266ad2antrr 764 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑎 ∈ (𝑎[,]𝑏))
26826oveq1d 6780 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → ((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))) = ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))
269268fveq2d 6308 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑎 → (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))) = (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
270 fvex 6314 . . . . . . . . . . . . . . . . . . 19 (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ V
271269, 261, 270fvmpt 6396 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ (𝑎[,]𝑏) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎) = (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
272267, 271syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎) = (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
273264, 272oveq12d 6783 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) = ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))))
27460adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹𝑏) ∈ ℂ)
275274, 143, 169divcld 10914 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
27662adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (𝐹𝑎) ∈ ℂ)
277276, 143, 169divcld 10914 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
278275, 277resubd 14076 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ‘(((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))))
279274, 276, 143, 169divsubdird 10953 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((𝐹𝑏) − (𝐹𝑎)) / ((𝐹𝑏) − (𝐹𝑎))) = (((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))))
280143, 169dividd 10912 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((𝐹𝑏) − (𝐹𝑎)) / ((𝐹𝑏) − (𝐹𝑎))) = 1)
281279, 280eqtr3d 2760 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎)))) = 1)
282281fveq2d 6308 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ‘(((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = (ℜ‘1))
283 re1 14014 . . . . . . . . . . . . . . . . . . 19 (ℜ‘1) = 1
284282, 283syl6eq 2774 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (ℜ‘(((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎))) − ((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = 1)
285278, 284eqtr3d 2760 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = 1)
286285adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘((𝐹𝑏) / ((𝐹𝑏) − (𝐹𝑎)))) − (ℜ‘((𝐹𝑎) / ((𝐹𝑏) − (𝐹𝑎))))) = 1)
287273, 286eqtrd 2758 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) = 1)
288287oveq1d 6780 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)) = (1 / (𝑏𝑎)))
289255, 288eqeq12d 2739 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)) ↔ (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎))))
290289rexbidva 3151 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (∃𝑥 ∈ (𝑎(,)𝑏)((ℝ D (𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎))))))‘𝑥) = ((((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑏) − ((𝑦 ∈ (𝑎[,]𝑏) ↦ (ℜ‘((𝐹𝑦) / ((𝐹𝑏) − (𝐹𝑎)))))‘𝑎)) / (𝑏𝑎)) ↔ ∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎))))
291247, 290mpbid 222 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)))
292211sselda 3709 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ (𝐴(,)𝐵))
293213ffvelrnda 6474 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
294292, 293syldan 488 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
295142ad2antrr 764 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ∈ ℂ)
296169adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝐹𝑏) − (𝐹𝑎)) ≠ 0)
297294, 295, 296divcld 10914 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) ∈ ℂ)
298297recld 14054 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
299144adantr 472 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℝ)
300298, 299remulcld 10183 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
301294abscld 14295 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((ℝ D 𝐹)‘𝑥)) ∈ ℝ)
302127ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑀 ∈ ℝ)
303297abscld 14295 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ∈ ℝ)
304143absge0d 14303 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 0 ≤ (abs‘((𝐹𝑏) − (𝐹𝑎))))
305304adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 0 ≤ (abs‘((𝐹𝑏) − (𝐹𝑎))))
306297releabsd 14310 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) ≤ (abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))))
307298, 303, 299, 305, 306lemul1ad 11076 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
308297, 295absmuld 14313 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) · ((𝐹𝑏) − (𝐹𝑎)))) = ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
309294, 295, 296divcan1d 10915 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) · ((𝐹𝑏) − (𝐹𝑎))) = ((ℝ D 𝐹)‘𝑥))
310309fveq2d 6308 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎))) · ((𝐹𝑏) − (𝐹𝑎)))) = (abs‘((ℝ D 𝐹)‘𝑥)))
311308, 310eqtr3d 2760 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((abs‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) = (abs‘((ℝ D 𝐹)‘𝑥)))
312307, 311breqtrd 4786 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ (abs‘((ℝ D 𝐹)‘𝑥)))
313106adantlr 753 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
314313adantlr 753 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
315292, 314syldan 488 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (abs‘((ℝ D 𝐹)‘𝑥)) ≤ 𝑀)
316300, 301, 302, 312, 315letrd 10307 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀)
317 oveq1 6772 . . . . . . . . . . . . . 14 ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) = ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))))
318317breq1d 4770 . . . . . . . . . . . . 13 ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → (((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀 ↔ ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀))
319316, 318syl5ibcom 235 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀))
320319rexlimdva 3133 . . . . . . . . . . 11 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (∃𝑥 ∈ (𝑎(,)𝑏)(ℜ‘(((ℝ D 𝐹)‘𝑥) / ((𝐹𝑏) − (𝐹𝑎)))) = (1 / (𝑏𝑎)) → ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀))
321291, 320mpd 15 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((1 / (𝑏𝑎)) · (abs‘((𝐹𝑏) − (𝐹𝑎)))) ≤ 𝑀)
322159, 321eqbrtrd 4782 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → ((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) ≤ 𝑀)
32373ad2antrr 764 . . . . . . . . . 10 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → 𝑀 ∈ ℝ)
324 ledivmul2 11015 . . . . . . . . . 10 (((abs‘((𝐹𝑏) − (𝐹𝑎))) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑏𝑎) ∈ ℝ ∧ 0 < (𝑏𝑎))) → (((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) ≤ 𝑀 ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎))))
325144, 323, 146, 157, 324syl112anc 1443 . . . . . . . . 9 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (((abs‘((𝐹𝑏) − (𝐹𝑎))) / (𝑏𝑎)) ≤ 𝑀 ↔ (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎))))
326322, 325mpbid 222 . . . . . . . 8 (((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) ∧ (𝐹𝑏) ≠ (𝐹𝑎)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎)))
327141, 326pm2.61dane 2983 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (𝑏𝑎)))
32867, 69, 114abssubge0d 14290 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (abs‘(𝑏𝑎)) = (𝑏𝑎))
329328oveq2d 6781 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (𝑀 · (abs‘(𝑏𝑎))) = (𝑀 · (𝑏𝑎)))
330327, 329breqtrrd 4788 . . . . . 6 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵) ∧ 𝑎𝑏)) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))))
33125, 34, 38, 57, 330wlogle 10674 . . . . 5 ((𝜑 ∧ (𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎))))
332331expcom 450 . . . 4 ((𝑎 ∈ (𝐴[,]𝐵) ∧ 𝑏 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹𝑏) − (𝐹𝑎))) ≤ (𝑀 · (abs‘(𝑏𝑎)))))
3338, 16, 332vtocl2ga 3378 . . 3 ((𝑌 ∈ (𝐴[,]𝐵) ∧ 𝑋 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌)))))
334333ancoms 468 . 2 ((𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵)) → (𝜑 → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌)))))
335334impcom 445 1 ((𝜑 ∧ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑌 ∈ (𝐴[,]𝐵))) → (abs‘((𝐹𝑋) − (𝐹𝑌))) ≤ (𝑀 · (abs‘(𝑋𝑌))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1596  wex 1817  wcel 2103  wne 2896  wrex 3015  Vcvv 3304  wss 3680  c0 4023  {cpr 4287   class class class wbr 4760  cmpt 4837  dom cdm 5218  ran crn 5219  cres 5220  ccom 5222  wf 5997  cfv 6001  (class class class)co 6765  cc 10047  cr 10048  0cc0 10049  1c1 10050   · cmul 10054  *cxr 10186   < clt 10187  cle 10188  cmin 10379   / cdiv 10797  (,)cioo 12289  [,]cicc 12292  cre 13957  abscabs 14094  TopOpenctopn 16205  topGenctg 16221  fldccnfld 19869  Topctop 20821  intcnt 20944  cnccncf 22801   D cdv 23747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-inf2 8651  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127  ax-addf 10128  ax-mulf 10129
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-iin 4631  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-se 5178  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-isom 6010  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-of 7014  df-om 7183  df-1st 7285  df-2nd 7286  df-supp 7416  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-oadd 7684  df-er 7862  df-map 7976  df-pm 7977  df-ixp 8026  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-fsupp 8392  df-fi 8433  df-sup 8464  df-inf 8465  df-oi 8531  df-card 8878  df-cda 9103  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-q 11903  df-rp 11947  df-xneg 12060  df-xadd 12061  df-xmul 12062  df-ioo 12293  df-ico 12295  df-icc 12296  df-fz 12441  df-fzo 12581  df-seq 12917  df-exp 12976  df-hash 13233  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-starv 16079  df-sca 16080  df-vsca 16081  df-ip 16082  df-tset 16083  df-ple 16084  df-ds 16087  df-unif 16088  df-hom 16089  df-cco 16090  df-rest 16206  df-topn 16207  df-0g 16225  df-gsum 16226  df-topgen 16227  df-pt 16228  df-prds 16231  df-xrs 16285  df-qtop 16290  df-imas 16291  df-xps 16293  df-mre 16369  df-mrc 16370  df-acs 16372  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-submnd 17458  df-mulg 17663  df-cntz 17871  df-cmn 18316  df-psmet 19861  df-xmet 19862  df-met 19863  df-bl 19864  df-mopn 19865  df-fbas 19866  df-fg 19867  df-cnfld 19870  df-top 20822  df-topon 20839  df-topsp 20860  df-bases 20873  df-cld 20946  df-ntr 20947  df-cls 20948  df-nei 21025  df-lp 21063  df-perf 21064  df-cn 21154  df-cnp 21155  df-haus 21242  df-cmp 21313  df-tx 21488  df-hmeo 21681  df-fil 21772  df-fm 21864  df-flim 21865  df-flf 21866  df-xms 22247  df-ms 22248  df-tms 22249  df-cncf 22803  df-limc 23750  df-dv 23751
This theorem is referenced by:  dvlipcn  23877  dvlip2  23878  dveq0  23883  dvfsumabs  23906  pige3  24389  lgamgulmlem2  24876
  Copyright terms: Public domain W3C validator