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

Theorem cmvth 25355
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 2736 . . . 4 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
54subcn 24229 . . . 4 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
64mulcn 24230 . . . . 5 · ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
7 cmvth.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
8 cncff 24256 . . . . . . . . 9 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
97, 8syl 17 . . . . . . . 8 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
101rexrd 11205 . . . . . . . . 9 (𝜑𝐴 ∈ ℝ*)
112rexrd 11205 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ*)
121, 2, 3ltled 11303 . . . . . . . . 9 (𝜑𝐴𝐵)
13 ubicc2 13382 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
1410, 11, 12, 13syl3anc 1371 . . . . . . . 8 (𝜑𝐵 ∈ (𝐴[,]𝐵))
159, 14ffvelcdmd 7036 . . . . . . 7 (𝜑 → (𝐹𝐵) ∈ ℝ)
16 lbicc2 13381 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
1710, 11, 12, 16syl3anc 1371 . . . . . . . 8 (𝜑𝐴 ∈ (𝐴[,]𝐵))
189, 17ffvelcdmd 7036 . . . . . . 7 (𝜑 → (𝐹𝐴) ∈ ℝ)
1915, 18resubcld 11583 . . . . . 6 (𝜑 → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ)
20 iccssre 13346 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
211, 2, 20syl2anc 584 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
22 ax-resscn 11108 . . . . . . 7 ℝ ⊆ ℂ
2321, 22sstrdi 3956 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
2422a1i 11 . . . . . 6 (𝜑 → ℝ ⊆ ℂ)
25 cncfmptc 24275 . . . . . 6 ((((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹𝐵) − (𝐹𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
2619, 23, 24, 25syl3anc 1371 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹𝐵) − (𝐹𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
27 cmvth.g . . . . . . . 8 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))
28 cncff 24256 . . . . . . . 8 (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ)
2927, 28syl 17 . . . . . . 7 (𝜑𝐺:(𝐴[,]𝐵)⟶ℝ)
3029feqmptd 6910 . . . . . 6 (𝜑𝐺 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧)))
3130, 27eqeltrrd 2839 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
32 remulcl 11136 . . . . 5 ((((𝐹𝐵) − (𝐹𝐴)) ∈ ℝ ∧ (𝐺𝑧) ∈ ℝ) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℝ)
334, 6, 26, 31, 22, 32cncfmpt2ss 24279 . . . 4 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
3429, 14ffvelcdmd 7036 . . . . . . 7 (𝜑 → (𝐺𝐵) ∈ ℝ)
3529, 17ffvelcdmd 7036 . . . . . . 7 (𝜑 → (𝐺𝐴) ∈ ℝ)
3634, 35resubcld 11583 . . . . . 6 (𝜑 → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ)
37 cncfmptc 24275 . . . . . 6 ((((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺𝐵) − (𝐺𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
3836, 23, 24, 37syl3anc 1371 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺𝐵) − (𝐺𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
399feqmptd 6910 . . . . . 6 (𝜑𝐹 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧)))
4039, 7eqeltrrd 2839 . . . . 5 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
41 remulcl 11136 . . . . 5 ((((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ)
424, 6, 38, 40, 22, 41cncfmpt2ss 24279 . . . 4 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
43 resubcl 11465 . . . 4 (((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℝ ∧ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ) → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ℝ)
444, 5, 33, 42, 22, 43cncfmpt2ss 24279 . . 3 (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4519recnd 11183 . . . . . . . . . 10 (𝜑 → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
4645adantr 481 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
4729ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐺𝑧) ∈ ℝ)
4847recnd 11183 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐺𝑧) ∈ ℂ)
4946, 48mulcld 11175 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℂ)
5036adantr 481 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℝ)
519ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹𝑧) ∈ ℝ)
5250, 51remulcld 11185 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℝ)
5352recnd 11183 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℂ)
5449, 53subcld 11512 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ ℂ)
554tgioo2 24166 . . . . . . 7 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
56 iccntr 24184 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
571, 2, 56syl2anc 584 . . . . . . 7 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5824, 21, 54, 55, 4, 57dvmptntr 25335 . . . . . 6 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))))
59 reelprrecn 11143 . . . . . . . 8 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ {ℝ, ℂ})
61 ioossicc 13350 . . . . . . . . 9 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6261sseli 3940 . . . . . . . 8 (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵))
6362, 49sylan2 593 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) ∈ ℂ)
64 ovex 7390 . . . . . . . 8 (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V
6564a1i 11 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V)
6662, 48sylan2 593 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐺𝑧) ∈ ℂ)
67 fvexd 6857 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ V)
6830oveq2d 7373 . . . . . . . . 9 (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧))))
69 dvf 25271 . . . . . . . . . . 11 (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
70 cmvth.dg . . . . . . . . . . . 12 (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
7170feq2d 6654 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
7269, 71mpbii 232 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
7372feqmptd 6910 . . . . . . . . 9 (𝜑 → (ℝ D 𝐺) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
7424, 21, 48, 55, 4, 57dvmptntr 25335 . . . . . . . . 9 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑧))))
7568, 73, 743eqtr3rd 2785 . . . . . . . 8 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
7660, 66, 67, 75, 45dvmptcmul 25328 . . . . . . 7 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧))))
7762, 53sylan2 593 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) ∈ ℂ)
78 ovex 7390 . . . . . . . 8 (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V
7978a1i 11 . . . . . . 7 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V)
8051recnd 11183 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹𝑧) ∈ ℂ)
8162, 80sylan2 593 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → (𝐹𝑧) ∈ ℂ)
82 fvexd 6857 . . . . . . . 8 ((𝜑𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ V)
8339oveq2d 7373 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧))))
84 dvf 25271 . . . . . . . . . . 11 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
85 cmvth.df . . . . . . . . . . . 12 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
8685feq2d 6654 . . . . . . . . . . 11 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
8784, 86mpbii 232 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
8887feqmptd 6910 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
8924, 21, 80, 55, 4, 57dvmptntr 25335 . . . . . . . . 9 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑧))))
9083, 88, 893eqtr3rd 2785 . . . . . . . 8 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
9136recnd 11183 . . . . . . . 8 (𝜑 → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℂ)
9260, 81, 82, 90, 91dvmptcmul 25328 . . . . . . 7 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))
9360, 63, 65, 76, 77, 79, 92dvmptsub 25331 . . . . . 6 (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
9458, 93eqtrd 2776 . . . . 5 (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
9594dmeqd 5861 . . . 4 (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
96 ovex 7390 . . . . 5 ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))) ∈ V
97 eqid 2736 . . . . 5 (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))
9896, 97dmmpti 6645 . . . 4 dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝐴(,)𝐵)
9995, 98eqtrdi 2792 . . 3 (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))) = (𝐴(,)𝐵))
10015recnd 11183 . . . . . . . 8 (𝜑 → (𝐹𝐵) ∈ ℂ)
10135recnd 11183 . . . . . . . 8 (𝜑 → (𝐺𝐴) ∈ ℂ)
102100, 101mulcld 11175 . . . . . . 7 (𝜑 → ((𝐹𝐵) · (𝐺𝐴)) ∈ ℂ)
10318recnd 11183 . . . . . . . 8 (𝜑 → (𝐹𝐴) ∈ ℂ)
10434recnd 11183 . . . . . . . 8 (𝜑 → (𝐺𝐵) ∈ ℂ)
105103, 104mulcld 11175 . . . . . . 7 (𝜑 → ((𝐹𝐴) · (𝐺𝐵)) ∈ ℂ)
106103, 101mulcld 11175 . . . . . . 7 (𝜑 → ((𝐹𝐴) · (𝐺𝐴)) ∈ ℂ)
107102, 105, 106nnncan2d 11547 . . . . . 6 (𝜑 → ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐵))))
108100, 104mulcld 11175 . . . . . . 7 (𝜑 → ((𝐹𝐵) · (𝐺𝐵)) ∈ ℂ)
109108, 105, 102nnncan1d 11546 . . . . . 6 (𝜑 → ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐵))))
110107, 109eqtr4d 2779 . . . . 5 (𝜑 → ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))) = ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))))
111100, 103, 101subdird 11612 . . . . . 6 (𝜑 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) = (((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))))
11291, 103mulcomd 11176 . . . . . . 7 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)) = ((𝐹𝐴) · ((𝐺𝐵) − (𝐺𝐴))))
113103, 104, 101subdid 11611 . . . . . . 7 (𝜑 → ((𝐹𝐴) · ((𝐺𝐵) − (𝐺𝐴))) = (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴))))
114112, 113eqtrd 2776 . . . . . 6 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)) = (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴))))
115111, 114oveq12d 7375 . . . . 5 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))) = ((((𝐹𝐵) · (𝐺𝐴)) − ((𝐹𝐴) · (𝐺𝐴))) − (((𝐹𝐴) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐴)))))
116100, 103, 104subdird 11612 . . . . . 6 (𝜑 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))))
11791, 100mulcomd 11176 . . . . . . 7 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)) = ((𝐹𝐵) · ((𝐺𝐵) − (𝐺𝐴))))
118100, 104, 101subdid 11611 . . . . . . 7 (𝜑 → ((𝐹𝐵) · ((𝐺𝐵) − (𝐺𝐴))) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴))))
119117, 118eqtrd 2776 . . . . . 6 (𝜑 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)) = (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴))))
120116, 119oveq12d 7375 . . . . 5 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))) = ((((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐴) · (𝐺𝐵))) − (((𝐹𝐵) · (𝐺𝐵)) − ((𝐹𝐵) · (𝐺𝐴)))))
121110, 115, 1203eqtr4d 2786 . . . 4 (𝜑 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
122 fveq2 6842 . . . . . . . 8 (𝑧 = 𝐴 → (𝐺𝑧) = (𝐺𝐴))
123122oveq2d 7373 . . . . . . 7 (𝑧 = 𝐴 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)))
124 fveq2 6842 . . . . . . . 8 (𝑧 = 𝐴 → (𝐹𝑧) = (𝐹𝐴))
125124oveq2d 7373 . . . . . . 7 (𝑧 = 𝐴 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴)))
126123, 125oveq12d 7375 . . . . . 6 (𝑧 = 𝐴 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
127 eqid 2736 . . . . . 6 (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))) = (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))
128 ovex 7390 . . . . . 6 ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) ∈ V
129126, 127, 128fvmpt3i 6953 . . . . 5 (𝐴 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
13017, 129syl 17 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐴)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐴))))
131 fveq2 6842 . . . . . . . 8 (𝑧 = 𝐵 → (𝐺𝑧) = (𝐺𝐵))
132131oveq2d 7373 . . . . . . 7 (𝑧 = 𝐵 → (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)))
133 fveq2 6842 . . . . . . . 8 (𝑧 = 𝐵 → (𝐹𝑧) = (𝐹𝐵))
134133oveq2d 7373 . . . . . . 7 (𝑧 = 𝐵 → (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵)))
135132, 134oveq12d 7375 . . . . . 6 (𝑧 = 𝐵 → ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
136135, 127, 128fvmpt3i 6953 . . . . 5 (𝐵 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
13714, 136syl 17 . . . 4 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵) = ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝐵)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝐵))))
138121, 130, 1373eqtr4d 2786 . . 3 (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐴) = ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧))))‘𝐵))
1391, 2, 3, 44, 99, 138rolle 25354 . 2 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0)
14094fveq1d 6844 . . . . . 6 (𝜑 → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥))
141 fveq2 6842 . . . . . . . . 9 (𝑧 = 𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘𝑥))
142141oveq2d 7373 . . . . . . . 8 (𝑧 = 𝑥 → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) = (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)))
143 fveq2 6842 . . . . . . . . 9 (𝑧 = 𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘𝑥))
144143oveq2d 7373 . . . . . . . 8 (𝑧 = 𝑥 → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
145142, 144oveq12d 7375 . . . . . . 7 (𝑧 = 𝑥 → ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
146145, 97, 96fvmpt3i 6953 . . . . . 6 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
147140, 146sylan9eq 2796 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
148147eqeq1d 2738 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ ((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0))
14945adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹𝐵) − (𝐹𝐴)) ∈ ℂ)
15072ffvelcdmda 7035 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑥) ∈ ℂ)
151149, 150mulcld 11175 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) ∈ ℂ)
15291adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺𝐵) − (𝐺𝐴)) ∈ ℂ)
15387ffvelcdmda 7035 . . . . . 6 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
154152, 153mulcld 11175 . . . . 5 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)) ∈ ℂ)
155151, 154subeq0ad 11522 . . . 4 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0 ↔ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
156148, 155bitrd 278 . . 3 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ (((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
157156rexbidva 3173 . 2 (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹𝐵) − (𝐹𝐴)) · (𝐺𝑧)) − (((𝐺𝐵) − (𝐺𝐴)) · (𝐹𝑧)))))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥))))
158139, 157mpbid 231 1 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹𝐵) − (𝐹𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺𝐵) − (𝐺𝐴)) · ((ℝ D 𝐹)‘𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wrex 3073  Vcvv 3445  wss 3910  {cpr 4588   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385  (,)cioo 13264  [,]cicc 13267  TopOpenctopn 17303  topGenctg 17319  fldccnfld 20796  intcnt 22368  cnccncf 24239   D cdv 25227
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231
This theorem is referenced by:  mvth  25356  lhop1lem  25377
  Copyright terms: Public domain W3C validator