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

Theorem cmvth 24570
 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 2820 . . . 4 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
54subcn 23447 . . . 4 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
64mulcn 23448 . . . . 5 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
7 cmvth.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
8 cncff 23474 . . . . . . . . 9 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
97, 8syl 17 . . . . . . . 8 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
101rexrd 10667 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ*)
112rexrd 10667 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ*)
121, 2, 3ltled 10764 . . . . . . . . 9 (𝜑𝐴𝐵)
13 ubicc2 12832 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
1410, 11, 12, 13syl3anc 1367 . . . . . . . 8 (𝜑𝐵 ∈ (𝐴[,]𝐵))
159, 14ffvelrnd 6826 . . . . . . 7 (𝜑 → (𝐹𝐵) ∈ ℝ)
16 lbicc2 12831 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
1710, 11, 12, 16syl3anc 1367 . . . . . . . 8 (𝜑𝐴 ∈ (𝐴[,]𝐵))
189, 17ffvelrnd 6826 . . . . . . 7 (𝜑 → (𝐹𝐴) ∈ ℝ)
1915, 18resubcld 11044 . . . . . 6 (𝜑 → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ)
20 iccssre 12796 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
211, 2, 20syl2anc 586 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
22 ax-resscn 10570 . . . . . . 7 ℝ ⊆ ℂ
2321, 22sstrdi 3955 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
2422a1i 11 . . . . . 6 (𝜑 → ℝ ⊆ ℂ)
25 cncfmptc 23493 . . . . . 6 ((((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹𝐵) − (𝐹𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
2619, 23, 24, 25syl3anc 1367 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹𝐵) − (𝐹𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
27 cmvth.g . . . . . . . 8 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))
28 cncff 23474 . . . . . . . 8 (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ)
2927, 28syl 17 . . . . . . 7 (𝜑𝐺:(𝐴[,]𝐵)⟶ℝ)
3029feqmptd 6707 . . . . . 6 (𝜑𝐺 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧)))
3130, 27eqeltrrd 2912 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
32 remulcl 10598 . . . . 5 ((((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ ∧ (𝐺𝑧) ∈ ℝ) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℝ)
334, 6, 26, 31, 22, 32cncfmpt2ss 23497 . . . 4 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
3429, 14ffvelrnd 6826 . . . . . . 7 (𝜑 → (𝐺𝐵) ∈ ℝ)
3529, 17ffvelrnd 6826 . . . . . . 7 (𝜑 → (𝐺𝐴) ∈ ℝ)
3634, 35resubcld 11044 . . . . . 6 (𝜑 → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ)
37 cncfmptc 23493 . . . . . 6 ((((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺𝐵) − (𝐺𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
3836, 23, 24, 37syl3anc 1367 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺𝐵) − (𝐺𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
399feqmptd 6707 . . . . . 6 (𝜑𝐹 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧)))
4039, 7eqeltrrd 2912 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
41 remulcl 10598 . . . . 5 ((((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ)
424, 6, 38, 40, 22, 41cncfmpt2ss 23497 . . . 4 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
43 resubcl 10926 . . . 4 (((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℝ ∧ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ) → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ℝ)
444, 5, 33, 42, 22, 43cncfmpt2ss 23497 . . 3 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4519recnd 10645 . . . . . . . . . 10 (𝜑 → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
4645adantr 483 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
4729ffvelrnda 6825 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐺𝑧) ∈ ℝ)
4847recnd 10645 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐺𝑧) ∈ ℂ)
4946, 48mulcld 10637 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℂ)
5036adantr 483 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ)
519ffvelrnda 6825 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹𝑧) ∈ ℝ)
5250, 51remulcld 10647 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ)
5352recnd 10645 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℂ)
5449, 53subcld 10973 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ℂ)
554tgioo2 23384 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
56 iccntr 23402 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
571, 2, 56syl2anc 586 . . . . . . 7 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5824, 21, 54, 55, 4, 57dvmptntr 24550 . . . . . 6 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))))
59 reelprrecn 10605 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
61 ioossicc 12800 . . . . . . . . 9 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6261sseli 3939 . . . . . . . 8 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵))
6362, 49sylan2 594 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℂ)
64 ovex 7164 . . . . . . . 8 (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V
6564a1i 11 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V)
6662, 48sylan2 594 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
67 fvexd 6659 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ V)
6830oveq2d 7147 . . . . . . . . 9 (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧))))
69 dvf 24486 . . . . . . . . . . 11 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
70 cmvth.dg . . . . . . . . . . . 12 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
7170feq2d 6474 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
7269, 71mpbii 235 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
7372feqmptd 6707 . . . . . . . . 9 (𝜑 → (ℝ D 𝐺) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
7424, 21, 48, 55, 4, 57dvmptntr 24550 . . . . . . . . 9 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑧))))
7568, 73, 743eqtr3rd 2864 . . . . . . . 8 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
7660, 66, 67, 75, 45dvmptcmul 24543 . . . . . . 7 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧))))
7762, 53sylan2 594 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℂ)
78 ovex 7164 . . . . . . . 8 (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V
7978a1i 11 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V)
8051recnd 10645 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹𝑧) ∈ ℂ)
8162, 80sylan2 594 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
82 fvexd 6659 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ V)
8339oveq2d 7147 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧))))
84 dvf 24486 . . . . . . . . . . 11 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
85 cmvth.df . . . . . . . . . . . 12 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
8685feq2d 6474 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
8784, 86mpbii 235 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
8887feqmptd 6707 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
8924, 21, 80, 55, 4, 57dvmptntr 24550 . . . . . . . . 9 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑧))))
9083, 88, 893eqtr3rd 2864 . . . . . . . 8 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
9136recnd 10645 . . . . . . . 8 (𝜑 → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℂ)
9260, 81, 82, 90, 91dvmptcmul 24543 . . . . . . 7 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))
9360, 63, 65, 76, 77, 79, 92dvmptsub 24546 . . . . . 6 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
9458, 93eqtrd 2855 . . . . 5 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
9594dmeqd 5748 . . . 4 (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
96 ovex 7164 . . . . 5 ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))) ∈ V
97 eqid 2820 . . . . 5 (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))
9896, 97dmmpti 6466 . . . 4 dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝐴(,)𝐵)
9995, 98syl6eq 2871 . . 3 (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝐴(,)𝐵))
10015recnd 10645 . . . . . . . 8 (𝜑 → (𝐹𝐵) ∈ ℂ)
10135recnd 10645 . . . . . . . 8 (𝜑 → (𝐺𝐴) ∈ ℂ)
102100, 101mulcld 10637 . . . . . . 7 (𝜑 → ((𝐹𝐵) · (𝐺𝐴)) ∈ ℂ)
10318recnd 10645 . . . . . . . 8 (𝜑 → (𝐹𝐴) ∈ ℂ)
10434recnd 10645 . . . . . . . 8 (𝜑 → (𝐺𝐵) ∈ ℂ)
105103, 104mulcld 10637 . . . . . . 7 (𝜑 → ((𝐹𝐴) · (𝐺𝐵)) ∈ ℂ)
106103, 101mulcld 10637 . . . . . . 7 (𝜑 → ((𝐹𝐴) · (𝐺𝐴)) ∈ ℂ)
107102, 105, 106nnncan2d 11008 . . . . . 6 (𝜑 → ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐵))))
108100, 104mulcld 10637 . . . . . . 7 (𝜑 → ((𝐹𝐵) · (𝐺𝐵)) ∈ ℂ)
109108, 105, 102nnncan1d 11007 . . . . . 6 (𝜑 → ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐵))))
110107, 109eqtr4d 2858 . . . . 5 (𝜑 → ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))) = ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))))
111100, 103, 101subdird 11073 . . . . . 6 (𝜑 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))))
11291, 103mulcomd 10638 . . . . . . 7 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)) = ((𝐹𝐴) · ((𝐺𝐵) − (𝐺𝐴))))
113103, 104, 101subdid 11072 . . . . . . 7 (𝜑 → ((𝐹𝐴) · ((𝐺𝐵) − (𝐺𝐴))) = (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴))))
114112, 113eqtrd 2855 . . . . . 6 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)) = (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴))))
115111, 114oveq12d 7149 . . . . 5 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))) = ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))))
116100, 103, 104subdird 11073 . . . . . 6 (𝜑 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))))
11791, 100mulcomd 10638 . . . . . . 7 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)) = ((𝐹𝐵) · ((𝐺𝐵) − (𝐺𝐴))))
118100, 104, 101subdid 11072 . . . . . . 7 (𝜑 → ((𝐹𝐵) · ((𝐺𝐵) − (𝐺𝐴))) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴))))
119117, 118eqtrd 2855 . . . . . 6 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴))))
120116, 119oveq12d 7149 . . . . 5 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))) = ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))))
121110, 115, 1203eqtr4d 2865 . . . 4 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
122 fveq2 6644 . . . . . . . 8 (𝑧 = 𝐴 → (𝐺𝑧) = (𝐺𝐴))
123122oveq2d 7147 . . . . . . 7 (𝑧 = 𝐴 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)))
124 fveq2 6644 . . . . . . . 8 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
125124oveq2d 7147 . . . . . . 7 (𝑧 = 𝐴 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)))
126123, 125oveq12d 7149 . . . . . 6 (𝑧 = 𝐴 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
127 eqid 2820 . . . . . 6 (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) = (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))
128 ovex 7164 . . . . . 6 ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ V
129126, 127, 128fvmpt3i 6747 . . . . 5 (𝐴 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
13017, 129syl 17 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
131 fveq2 6644 . . . . . . . 8 (𝑧 = 𝐵 → (𝐺𝑧) = (𝐺𝐵))
132131oveq2d 7147 . . . . . . 7 (𝑧 = 𝐵 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)))
133 fveq2 6644 . . . . . . . 8 (𝑧 = 𝐵 → (𝐹𝑧) = (𝐹𝐵))
134133oveq2d 7147 . . . . . . 7 (𝑧 = 𝐵 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)))
135132, 134oveq12d 7149 . . . . . 6 (𝑧 = 𝐵 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
136135, 127, 128fvmpt3i 6747 . . . . 5 (𝐵 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
13714, 136syl 17 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
138121, 130, 1373eqtr4d 2865 . . 3 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵))
1391, 2, 3, 44, 99, 138rolle 24569 . 2 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0)
14094fveq1d 6646 . . . . . 6 (𝜑 → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥))
141 fveq2 6644 . . . . . . . . 9 (𝑧 = 𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘𝑥))
142141oveq2d 7147 . . . . . . . 8 (𝑧 = 𝑥 → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)))
143 fveq2 6644 . . . . . . . . 9 (𝑧 = 𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘𝑥))
144143oveq2d 7147 . . . . . . . 8 (𝑧 = 𝑥 → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
145142, 144oveq12d 7149 . . . . . . 7 (𝑧 = 𝑥 → ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
146145, 97, 96fvmpt3i 6747 . . . . . 6 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
147140, 146sylan9eq 2875 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
148147eqeq1d 2822 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0))
14945adantr 483 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
15072ffvelrnda 6825 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑥) ∈ ℂ)
151149, 150mulcld 10637 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) ∈ ℂ)
15291adantr 483 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℂ)
15387ffvelrnda 6825 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
154152, 153mulcld 10637 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)) ∈ ℂ)
155151, 154subeq0ad 10983 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0 ↔ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
156148, 155bitrd 281 . . 3 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
157156rexbidva 3283 . 2 (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
158139, 157mpbid 234 1 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3126  Vcvv 3473   ⊆ wss 3912  {cpr 4543   class class class wbr 5040   ↦ cmpt 5120  dom cdm 5529  ran crn 5530  ⟶wf 6325  ‘cfv 6329  (class class class)co 7131  ℂcc 10511  ℝcr 10512  0cc0 10513   · cmul 10518  ℝ*cxr 10650   < clt 10651   ≤ cle 10652   − cmin 10846  (,)cioo 12715  [,]cicc 12718  TopOpenctopn 16671  topGenctg 16687  ℂfldccnfld 20518  intcnt 21598  –cn→ccncf 23457   D cdv 24442 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5240  ax-pr 5304  ax-un 7437  ax-cnex 10569  ax-resscn 10570  ax-1cn 10571  ax-icn 10572  ax-addcl 10573  ax-addrcl 10574  ax-mulcl 10575  ax-mulrcl 10576  ax-mulcom 10577  ax-addass 10578  ax-mulass 10579  ax-distr 10580  ax-i2m1 10581  ax-1ne0 10582  ax-1rid 10583  ax-rnegex 10584  ax-rrecex 10585  ax-cnre 10586  ax-pre-lttri 10587  ax-pre-lttrn 10588  ax-pre-ltadd 10589  ax-pre-mulgt0 10590  ax-pre-sup 10591  ax-addf 10592  ax-mulf 10593 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3752  df-csb 3860  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-pss 3930  df-nul 4268  df-if 4442  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4813  df-int 4851  df-iun 4895  df-iin 4896  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5434  df-eprel 5439  df-po 5448  df-so 5449  df-fr 5488  df-se 5489  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6122  df-ord 6168  df-on 6169  df-lim 6170  df-suc 6171  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7089  df-ov 7134  df-oprab 7135  df-mpo 7136  df-of 7385  df-om 7557  df-1st 7665  df-2nd 7666  df-supp 7807  df-wrecs 7923  df-recs 7984  df-rdg 8022  df-1o 8078  df-2o 8079  df-oadd 8082  df-er 8265  df-map 8384  df-pm 8385  df-ixp 8438  df-en 8486  df-dom 8487  df-sdom 8488  df-fin 8489  df-fsupp 8810  df-fi 8851  df-sup 8882  df-inf 8883  df-oi 8950  df-card 9344  df-pnf 10653  df-mnf 10654  df-xr 10655  df-ltxr 10656  df-le 10657  df-sub 10848  df-neg 10849  df-div 11274  df-nn 11615  df-2 11677  df-3 11678  df-4 11679  df-5 11680  df-6 11681  df-7 11682  df-8 11683  df-9 11684  df-n0 11875  df-z 11959  df-dec 12076  df-uz 12221  df-q 12326  df-rp 12367  df-xneg 12484  df-xadd 12485  df-xmul 12486  df-ioo 12719  df-ico 12721  df-icc 12722  df-fz 12875  df-fzo 13016  df-seq 13352  df-exp 13413  df-hash 13674  df-cj 14436  df-re 14437  df-im 14438  df-sqrt 14572  df-abs 14573  df-struct 16461  df-ndx 16462  df-slot 16463  df-base 16465  df-sets 16466  df-ress 16467  df-plusg 16554  df-mulr 16555  df-starv 16556  df-sca 16557  df-vsca 16558  df-ip 16559  df-tset 16560  df-ple 16561  df-ds 16563  df-unif 16564  df-hom 16565  df-cco 16566  df-rest 16672  df-topn 16673  df-0g 16691  df-gsum 16692  df-topgen 16693  df-pt 16694  df-prds 16697  df-xrs 16751  df-qtop 16756  df-imas 16757  df-xps 16759  df-mre 16833  df-mrc 16834  df-acs 16836  df-mgm 17828  df-sgrp 17877  df-mnd 17888  df-submnd 17933  df-mulg 18201  df-cntz 18423  df-cmn 18884  df-psmet 20510  df-xmet 20511  df-met 20512  df-bl 20513  df-mopn 20514  df-fbas 20515  df-fg 20516  df-cnfld 20519  df-top 21475  df-topon 21492  df-topsp 21514  df-bases 21527  df-cld 21600  df-ntr 21601  df-cls 21602  df-nei 21679  df-lp 21717  df-perf 21718  df-cn 21808  df-cnp 21809  df-haus 21896  df-cmp 21968  df-tx 22143  df-hmeo 22336  df-fil 22427  df-fm 22519  df-flim 22520  df-flf 22521  df-xms 22903  df-ms 22904  df-tms 22905  df-cncf 23459  df-limc 24445  df-dv 24446 This theorem is referenced by:  mvth  24571  lhop1lem  24592
 Copyright terms: Public domain W3C validator