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

Theorem cmvth 24195
Description: Cauchy's Mean Value Theorem. If 𝐹, 𝐺 are real continuous functions on [𝐴, 𝐵] differentiable on (𝐴, 𝐵), then there is some 𝑥 ∈ (𝐴, 𝐵) such that 𝐹' (𝑥) / 𝐺' (𝑥) = (𝐹(𝐴) − 𝐹(𝐵)) / (𝐺(𝐴) − 𝐺(𝐵)). (We express the condition without division, so that we need no nonzero constraints.) (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
cmvth.a (𝜑𝐴 ∈ ℝ)
cmvth.b (𝜑𝐵 ∈ ℝ)
cmvth.lt (𝜑𝐴 < 𝐵)
cmvth.f (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
cmvth.g (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))
cmvth.df (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
cmvth.dg (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
Assertion
Ref Expression
cmvth (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐺   𝜑,𝑥

Proof of Theorem cmvth
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cmvth.a . . 3 (𝜑𝐴 ∈ ℝ)
2 cmvth.b . . 3 (𝜑𝐵 ∈ ℝ)
3 cmvth.lt . . 3 (𝜑𝐴 < 𝐵)
4 eqid 2778 . . . 4 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
54subcn 23081 . . . 4 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
64mulcn 23082 . . . . 5 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
7 cmvth.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
8 cncff 23108 . . . . . . . . 9 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
97, 8syl 17 . . . . . . . 8 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
101rexrd 10428 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ*)
112rexrd 10428 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ*)
121, 2, 3ltled 10526 . . . . . . . . 9 (𝜑𝐴𝐵)
13 ubicc2 12607 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
1410, 11, 12, 13syl3anc 1439 . . . . . . . 8 (𝜑𝐵 ∈ (𝐴[,]𝐵))
159, 14ffvelrnd 6626 . . . . . . 7 (𝜑 → (𝐹𝐵) ∈ ℝ)
16 lbicc2 12606 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
1710, 11, 12, 16syl3anc 1439 . . . . . . . 8 (𝜑𝐴 ∈ (𝐴[,]𝐵))
189, 17ffvelrnd 6626 . . . . . . 7 (𝜑 → (𝐹𝐴) ∈ ℝ)
1915, 18resubcld 10805 . . . . . 6 (𝜑 → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ)
20 iccssre 12571 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
211, 2, 20syl2anc 579 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
22 ax-resscn 10331 . . . . . . 7 ℝ ⊆ ℂ
2321, 22syl6ss 3833 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
2422a1i 11 . . . . . 6 (𝜑 → ℝ ⊆ ℂ)
25 cncfmptc 23126 . . . . . 6 ((((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹𝐵) − (𝐹𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
2619, 23, 24, 25syl3anc 1439 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹𝐵) − (𝐹𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
27 cmvth.g . . . . . . . 8 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))
28 cncff 23108 . . . . . . . 8 (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ)
2927, 28syl 17 . . . . . . 7 (𝜑𝐺:(𝐴[,]𝐵)⟶ℝ)
3029feqmptd 6511 . . . . . 6 (𝜑𝐺 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧)))
3130, 27eqeltrrd 2860 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
32 remulcl 10359 . . . . 5 ((((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ ∧ (𝐺𝑧) ∈ ℝ) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℝ)
334, 6, 26, 31, 22, 32cncfmpt2ss 23130 . . . 4 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
3429, 14ffvelrnd 6626 . . . . . . 7 (𝜑 → (𝐺𝐵) ∈ ℝ)
3529, 17ffvelrnd 6626 . . . . . . 7 (𝜑 → (𝐺𝐴) ∈ ℝ)
3634, 35resubcld 10805 . . . . . 6 (𝜑 → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ)
37 cncfmptc 23126 . . . . . 6 ((((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺𝐵) − (𝐺𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
3836, 23, 24, 37syl3anc 1439 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺𝐵) − (𝐺𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
399feqmptd 6511 . . . . . 6 (𝜑𝐹 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧)))
4039, 7eqeltrrd 2860 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
41 remulcl 10359 . . . . 5 ((((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ)
424, 6, 38, 40, 22, 41cncfmpt2ss 23130 . . . 4 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
43 resubcl 10689 . . . 4 (((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℝ ∧ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ) → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ℝ)
444, 5, 33, 42, 22, 43cncfmpt2ss 23130 . . 3 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4519recnd 10407 . . . . . . . . . 10 (𝜑 → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
4645adantr 474 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
4729ffvelrnda 6625 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐺𝑧) ∈ ℝ)
4847recnd 10407 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐺𝑧) ∈ ℂ)
4946, 48mulcld 10399 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℂ)
5036adantr 474 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ)
519ffvelrnda 6625 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹𝑧) ∈ ℝ)
5250, 51remulcld 10409 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ)
5352recnd 10407 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℂ)
5449, 53subcld 10736 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ℂ)
554tgioo2 23018 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
56 iccntr 23036 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
571, 2, 56syl2anc 579 . . . . . . 7 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5824, 21, 54, 55, 4, 57dvmptntr 24175 . . . . . 6 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))))
59 reelprrecn 10366 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
61 ioossicc 12575 . . . . . . . . 9 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6261sseli 3817 . . . . . . . 8 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵))
6362, 49sylan2 586 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℂ)
64 ovex 6956 . . . . . . . 8 (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V
6564a1i 11 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V)
6662, 48sylan2 586 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
67 fvexd 6463 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ V)
6830oveq2d 6940 . . . . . . . . 9 (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧))))
69 dvf 24112 . . . . . . . . . . 11 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
70 cmvth.dg . . . . . . . . . . . 12 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
7170feq2d 6279 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
7269, 71mpbii 225 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
7372feqmptd 6511 . . . . . . . . 9 (𝜑 → (ℝ D 𝐺) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
7424, 21, 48, 55, 4, 57dvmptntr 24175 . . . . . . . . 9 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑧))))
7568, 73, 743eqtr3rd 2823 . . . . . . . 8 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
7660, 66, 67, 75, 45dvmptcmul 24168 . . . . . . 7 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧))))
7762, 53sylan2 586 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℂ)
78 ovex 6956 . . . . . . . 8 (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V
7978a1i 11 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V)
8051recnd 10407 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹𝑧) ∈ ℂ)
8162, 80sylan2 586 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
82 fvexd 6463 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ V)
8339oveq2d 6940 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧))))
84 dvf 24112 . . . . . . . . . . 11 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
85 cmvth.df . . . . . . . . . . . 12 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
8685feq2d 6279 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
8784, 86mpbii 225 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
8887feqmptd 6511 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
8924, 21, 80, 55, 4, 57dvmptntr 24175 . . . . . . . . 9 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑧))))
9083, 88, 893eqtr3rd 2823 . . . . . . . 8 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
9136recnd 10407 . . . . . . . 8 (𝜑 → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℂ)
9260, 81, 82, 90, 91dvmptcmul 24168 . . . . . . 7 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))
9360, 63, 65, 76, 77, 79, 92dvmptsub 24171 . . . . . 6 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
9458, 93eqtrd 2814 . . . . 5 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
9594dmeqd 5573 . . . 4 (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
96 ovex 6956 . . . . 5 ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))) ∈ V
97 eqid 2778 . . . . 5 (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))
9896, 97dmmpti 6271 . . . 4 dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝐴(,)𝐵)
9995, 98syl6eq 2830 . . 3 (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝐴(,)𝐵))
10015recnd 10407 . . . . . . . 8 (𝜑 → (𝐹𝐵) ∈ ℂ)
10135recnd 10407 . . . . . . . 8 (𝜑 → (𝐺𝐴) ∈ ℂ)
102100, 101mulcld 10399 . . . . . . 7 (𝜑 → ((𝐹𝐵) · (𝐺𝐴)) ∈ ℂ)
10318recnd 10407 . . . . . . . 8 (𝜑 → (𝐹𝐴) ∈ ℂ)
10434recnd 10407 . . . . . . . 8 (𝜑 → (𝐺𝐵) ∈ ℂ)
105103, 104mulcld 10399 . . . . . . 7 (𝜑 → ((𝐹𝐴) · (𝐺𝐵)) ∈ ℂ)
106103, 101mulcld 10399 . . . . . . 7 (𝜑 → ((𝐹𝐴) · (𝐺𝐴)) ∈ ℂ)
107102, 105, 106nnncan2d 10771 . . . . . 6 (𝜑 → ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐵))))
108100, 104mulcld 10399 . . . . . . 7 (𝜑 → ((𝐹𝐵) · (𝐺𝐵)) ∈ ℂ)
109108, 105, 102nnncan1d 10770 . . . . . 6 (𝜑 → ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐵))))
110107, 109eqtr4d 2817 . . . . 5 (𝜑 → ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))) = ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))))
111100, 103, 101subdird 10834 . . . . . 6 (𝜑 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))))
11291, 103mulcomd 10400 . . . . . . 7 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)) = ((𝐹𝐴) · ((𝐺𝐵) − (𝐺𝐴))))
113103, 104, 101subdid 10833 . . . . . . 7 (𝜑 → ((𝐹𝐴) · ((𝐺𝐵) − (𝐺𝐴))) = (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴))))
114112, 113eqtrd 2814 . . . . . 6 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)) = (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴))))
115111, 114oveq12d 6942 . . . . 5 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))) = ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))))
116100, 103, 104subdird 10834 . . . . . 6 (𝜑 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))))
11791, 100mulcomd 10400 . . . . . . 7 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)) = ((𝐹𝐵) · ((𝐺𝐵) − (𝐺𝐴))))
118100, 104, 101subdid 10833 . . . . . . 7 (𝜑 → ((𝐹𝐵) · ((𝐺𝐵) − (𝐺𝐴))) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴))))
119117, 118eqtrd 2814 . . . . . 6 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴))))
120116, 119oveq12d 6942 . . . . 5 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))) = ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))))
121110, 115, 1203eqtr4d 2824 . . . 4 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
122 fveq2 6448 . . . . . . . 8 (𝑧 = 𝐴 → (𝐺𝑧) = (𝐺𝐴))
123122oveq2d 6940 . . . . . . 7 (𝑧 = 𝐴 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)))
124 fveq2 6448 . . . . . . . 8 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
125124oveq2d 6940 . . . . . . 7 (𝑧 = 𝐴 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)))
126123, 125oveq12d 6942 . . . . . 6 (𝑧 = 𝐴 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
127 eqid 2778 . . . . . 6 (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) = (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))
128 ovex 6956 . . . . . 6 ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ V
129126, 127, 128fvmpt3i 6549 . . . . 5 (𝐴 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
13017, 129syl 17 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
131 fveq2 6448 . . . . . . . 8 (𝑧 = 𝐵 → (𝐺𝑧) = (𝐺𝐵))
132131oveq2d 6940 . . . . . . 7 (𝑧 = 𝐵 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)))
133 fveq2 6448 . . . . . . . 8 (𝑧 = 𝐵 → (𝐹𝑧) = (𝐹𝐵))
134133oveq2d 6940 . . . . . . 7 (𝑧 = 𝐵 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)))
135132, 134oveq12d 6942 . . . . . 6 (𝑧 = 𝐵 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
136135, 127, 128fvmpt3i 6549 . . . . 5 (𝐵 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
13714, 136syl 17 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
138121, 130, 1373eqtr4d 2824 . . 3 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵))
1391, 2, 3, 44, 99, 138rolle 24194 . 2 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0)
14094fveq1d 6450 . . . . . 6 (𝜑 → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥))
141 fveq2 6448 . . . . . . . . 9 (𝑧 = 𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘𝑥))
142141oveq2d 6940 . . . . . . . 8 (𝑧 = 𝑥 → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)))
143 fveq2 6448 . . . . . . . . 9 (𝑧 = 𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘𝑥))
144143oveq2d 6940 . . . . . . . 8 (𝑧 = 𝑥 → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
145142, 144oveq12d 6942 . . . . . . 7 (𝑧 = 𝑥 → ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
146145, 97, 96fvmpt3i 6549 . . . . . 6 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
147140, 146sylan9eq 2834 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
148147eqeq1d 2780 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0))
14945adantr 474 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
15072ffvelrnda 6625 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑥) ∈ ℂ)
151149, 150mulcld 10399 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) ∈ ℂ)
15291adantr 474 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℂ)
15387ffvelrnda 6625 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
154152, 153mulcld 10399 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)) ∈ ℂ)
155151, 154subeq0ad 10746 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0 ↔ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
156148, 155bitrd 271 . . 3 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
157156rexbidva 3234 . 2 (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
158139, 157mpbid 224 1 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2107  wrex 3091  Vcvv 3398  wss 3792  {cpr 4400   class class class wbr 4888  cmpt 4967  dom cdm 5357  ran crn 5358  wf 6133  cfv 6137  (class class class)co 6924  cc 10272  cr 10273  0cc0 10274   · cmul 10279  *cxr 10412   < clt 10413  cle 10414  cmin 10608  (,)cioo 12491  [,]cicc 12494  TopOpenctopn 16472  topGenctg 16488  fldccnfld 20146  intcnt 21233  cnccncf 23091   D cdv 24068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-iin 4758  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-supp 7579  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-2o 7846  df-oadd 7849  df-er 8028  df-map 8144  df-pm 8145  df-ixp 8197  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-fsupp 8566  df-fi 8607  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-4 11444  df-5 11445  df-6 11446  df-7 11447  df-8 11448  df-9 11449  df-n0 11647  df-z 11733  df-dec 11850  df-uz 11997  df-q 12100  df-rp 12142  df-xneg 12261  df-xadd 12262  df-xmul 12263  df-ioo 12495  df-ico 12497  df-icc 12498  df-fz 12648  df-fzo 12789  df-seq 13124  df-exp 13183  df-hash 13440  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-struct 16261  df-ndx 16262  df-slot 16263  df-base 16265  df-sets 16266  df-ress 16267  df-plusg 16355  df-mulr 16356  df-starv 16357  df-sca 16358  df-vsca 16359  df-ip 16360  df-tset 16361  df-ple 16362  df-ds 16364  df-unif 16365  df-hom 16366  df-cco 16367  df-rest 16473  df-topn 16474  df-0g 16492  df-gsum 16493  df-topgen 16494  df-pt 16495  df-prds 16498  df-xrs 16552  df-qtop 16557  df-imas 16558  df-xps 16560  df-mre 16636  df-mrc 16637  df-acs 16639  df-mgm 17632  df-sgrp 17674  df-mnd 17685  df-submnd 17726  df-mulg 17932  df-cntz 18137  df-cmn 18585  df-psmet 20138  df-xmet 20139  df-met 20140  df-bl 20141  df-mopn 20142  df-fbas 20143  df-fg 20144  df-cnfld 20147  df-top 21110  df-topon 21127  df-topsp 21149  df-bases 21162  df-cld 21235  df-ntr 21236  df-cls 21237  df-nei 21314  df-lp 21352  df-perf 21353  df-cn 21443  df-cnp 21444  df-haus 21531  df-cmp 21603  df-tx 21778  df-hmeo 21971  df-fil 22062  df-fm 22154  df-flim 22155  df-flf 22156  df-xms 22537  df-ms 22538  df-tms 22539  df-cncf 23093  df-limc 24071  df-dv 24072
This theorem is referenced by:  mvth  24196  lhop1lem  24217
  Copyright terms: Public domain W3C validator