cmvth - Metamath Proof Explorer

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

Theorem cmvth 26247

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.) Avoid ax-mulf 11226. (Revised by GG, 16-Mar-2025.)

**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 variables 𝑧 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cmvth.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		cmvth.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		cmvth.lt	. . 3 ⊢ (𝜑 → 𝐴 < 𝐵)
4		eqid 2760	. . . 4 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
5	4	subcn 25122	. . . 4 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
6		cmvth.f	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
7		cncff 25150	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
8	6, 7	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ)
9	1	rexrd 11305	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
10	2	rexrd 11305	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
11	1, 2, 3	ltled 11404	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
12		ubicc2 13540	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
13	9, 10, 11, 12	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
14	8, 13	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ)
15		lbicc2 13539	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
16	9, 10, 11, 15	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
17	8, 16	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ)
18	14, 17	resubcld 11688	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ)
19	18	recnd 11283	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ)
20	19	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ)
21		cmvth.g	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ))
22		cncff 25150	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐺:(𝐴[,]𝐵)⟶ℝ)
23	21, 22	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℝ)
24	23	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑧) ∈ ℝ)
25	24	recnd 11283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑧) ∈ ℂ)
26		ovmpot 7576	. . . . . . . . . 10 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))
27	20, 25, 26	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))
28	27	eqeq2d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ↔ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧))))
29	28	pm5.32da 590	. . . . . . 7 ⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ↔ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))))
30	29	opabbidv 5171	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))})
31		df-mpt 5187	. . . . . 6 ⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))}
32	30, 31	eqtr4di 2813	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} = (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧))))
33		df-mpt 5187	. . . . . 6 ⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))}
34	4	mpomulcn 25124	. . . . . . 7 ⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
35	1, 2	iccssred 13509	. . . . . . . . 9 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
36		ax-resscn 11203	. . . . . . . . 9 ⊢ ℝ ⊆ ℂ
37	35, 36	sstrdi 3943	. . . . . . . 8 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
38	36	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ ⊆ ℂ)
39		cncfmptc 25169	. . . . . . . 8 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹‘𝐵) − (𝐹‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
40	18, 37, 38, 39	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐹‘𝐵) − (𝐹‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
41	23	feqmptd 6948	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧)))
42	41, 21	eqeltrrd 2861	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
43		simpl 488	. . . . . . . . . 10 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ)
44	43	recnd 11283	. . . . . . . . 9 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ)
45		simpr 490	. . . . . . . . . 10 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → (𝐺‘𝑧) ∈ ℝ)
46	45	recnd 11283	. . . . . . . . 9 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → (𝐺‘𝑧) ∈ ℂ)
47	26	eqcomd 2766	. . . . . . . . 9 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ ∧ (𝐺‘𝑧) ∈ ℂ) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))
48	44, 46, 47	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))
49		remulcl 11231	. . . . . . . 8 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℝ)
50	48, 49	eqeltrrd 2861	. . . . . . 7 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℝ ∧ (𝐺‘𝑧) ∈ ℝ) → (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)) ∈ ℝ)
51	4, 34, 40, 42, 36, 50	cncfmpt2ss 25173	. . . . . 6 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
52	33, 51	eqeltrrid 2865	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐹‘𝐵) − (𝐹‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐺‘𝑧)))} ∈ ((𝐴[,]𝐵)–cn→ℝ))
53	32, 52	eqeltrrd 2861	. . . 4 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
54	23, 13	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘𝐵) ∈ ℝ)
55	23, 16	ffvelcdmd 7080	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐺‘𝐴) ∈ ℝ)
56	54, 55	resubcld 11688	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ)
57	56	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ)
58	57	recnd 11283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ)
59	8	ffvelcdmda 7079	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑧) ∈ ℝ)
60	59	recnd 11283	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑧) ∈ ℂ)
61		ovmpot 7576	. . . . . . . . . 10 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ) → (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))
62	58, 60, 61	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))
63	62	eqeq2d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)) ↔ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))
64	63	pm5.32da 590	. . . . . . 7 ⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧))) ↔ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))
65	64	opabbidv 5171	. . . . . 6 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)))} = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))})
66		df-mpt 5187	. . . . . 6 ⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))}
67	65, 66	eqtr4di 2813	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)))} = (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))
68		df-mpt 5187	. . . . . 6 ⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧))) = {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)))}
69		cncfmptc 25169	. . . . . . . 8 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺‘𝐵) − (𝐺‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
70	56, 37, 38, 69	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((𝐺‘𝐵) − (𝐺‘𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
71	8	feqmptd 6948	. . . . . . . 8 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧)))
72	71, 6	eqeltrrd 2861	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
73		simpl 488	. . . . . . . . . 10 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ)
74	73	recnd 11283	. . . . . . . . 9 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ)
75		simpr 490	. . . . . . . . . 10 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (𝐹‘𝑧) ∈ ℝ)
76	75	recnd 11283	. . . . . . . . 9 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (𝐹‘𝑧) ∈ ℂ)
77	61	eqcomd 2766	. . . . . . . . 9 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ ∧ (𝐹‘𝑧) ∈ ℂ) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)))
78	74, 76, 77	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)))
79		remulcl 11231	. . . . . . . 8 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℝ)
80	78, 79	eqeltrrd 2861	. . . . . . 7 ⊢ ((((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)) ∈ ℝ)
81	4, 34, 70, 72, 36, 80	cncfmpt2ss 25173	. . . . . 6 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
82	68, 81	eqeltrrid 2865	. . . . 5 ⊢ (𝜑 → {⟨𝑧, 𝑤⟩ ∣ (𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑤 = (((𝐺‘𝐵) − (𝐺‘𝐴))(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))(𝐹‘𝑧)))} ∈ ((𝐴[,]𝐵)–cn→ℝ))
83	67, 82	eqeltrrd 2861	. . . 4 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
84		resubcl 11568	. . . 4 ⊢ (((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℝ ∧ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℝ) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ ℝ)
85	4, 5, 53, 83, 36, 84	cncfmpt2ss 25173	. . 3 ⊢ (𝜑 → (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) ∈ ((𝐴[,]𝐵)–cn→ℝ))
86	20, 25	mulcld 11275	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℂ)
87	57, 59	remulcld 11285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℝ)
88	87	recnd 11283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℂ)
89	86, 88	subcld 11615	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ ℂ)
90		tgioo4 25060	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
91		iccntr 25077	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
92	1, 2, 91	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
93	38, 35, 89, 90, 4, 92	dvmptntr 26227	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))))
94		reelprrecn 11238	. . . . . . . 8 ⊢ ℝ ∈ {ℝ, ℂ}
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ {ℝ, ℂ})
96		ioossicc 13508	. . . . . . . . 9 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
97	96	sseli 3927	. . . . . . . 8 ⊢ (𝑧 ∈ (𝐴(,)𝐵) → 𝑧 ∈ (𝐴[,]𝐵))
98	97, 86	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) ∈ ℂ)
99		ovexd 7450	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) ∈ V)
100	97, 25	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐺‘𝑧) ∈ ℂ)
101		fvexd 6895	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑧) ∈ V)
102	41	oveq2d 7431	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐺) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧))))
103		dvf 26163	. . . . . . . . . . 11 ⊢ (ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ
104		cmvth.dg	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D 𝐺) = (𝐴(,)𝐵))
105	104	feq2d 6688	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℝ D 𝐺):dom (ℝ D 𝐺)⟶ℂ ↔ (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ))
106	103, 105	mpbii 236	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐺):(𝐴(,)𝐵)⟶ℂ)
107	106	feqmptd 6948	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐺) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
108	38, 35, 25, 90, 4, 92	dvmptntr 26227	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐺‘𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑧))))
109	102, 107, 108	3eqtr3rd 2804	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐺‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐺)‘𝑧)))
110	95, 100, 101, 109, 19	dvmptcmul 26220	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧))))
111	97, 88	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) ∈ ℂ)
112		ovexd 7450	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)) ∈ V)
113	97, 60	sylan2 605	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑧) ∈ ℂ)
114		fvexd 6895	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑧) ∈ V)
115	71	oveq2d 7431	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧))))
116		dvf 26163	. . . . . . . . . . 11 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
117		cmvth.df	. . . . . . . . . . . 12 ⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
118	117	feq2d 6688	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
119	116, 118	mpbii 236	. . . . . . . . . 10 ⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
120	119	feqmptd 6948	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D 𝐹) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
121	38, 35, 60, 90, 4, 92	dvmptntr 26227	. . . . . . . . 9 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑧))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑧))))
122	115, 120, 121	3eqtr3rd 2804	. . . . . . . 8 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑧))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑧)))
123	56	recnd 11283	. . . . . . . 8 ⊢ (𝜑 → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ)
124	95, 113, 114, 122, 123	dvmptcmul 26220	. . . . . . 7 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))
125	95, 98, 99, 110, 111, 112, 124	dvmptsub 26223	. . . . . 6 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
126	93, 125	eqtrd 2795	. . . . 5 ⊢ (𝜑 → (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
127	126	dmeqd 5890	. . . 4 ⊢ (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))))
128		ovex 7448	. . . . 5 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))) ∈ V
129		eqid 2760	. . . . 5 ⊢ (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))
130	128, 129	dmmpti 6678	. . . 4 ⊢ dom (𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)))) = (𝐴(,)𝐵)
131	127, 130	eqtrdi 2811	. . 3 ⊢ (𝜑 → dom (ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))) = (𝐴(,)𝐵))
132	14	recnd 11283	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
133	55	recnd 11283	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐴) ∈ ℂ)
134	132, 133	mulcld 11275	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐵) · (𝐺‘𝐴)) ∈ ℂ)
135	17	recnd 11283	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ)
136	54	recnd 11283	. . . . . . . 8 ⊢ (𝜑 → (𝐺‘𝐵) ∈ ℂ)
137	135, 136	mulcld 11275	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐴) · (𝐺‘𝐵)) ∈ ℂ)
138	135, 133	mulcld 11275	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐴) · (𝐺‘𝐴)) ∈ ℂ)
139	134, 137, 138	nnncan2d 11650	. . . . . 6 ⊢ (𝜑 → ((((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))) − (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) = (((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐵))))
140	132, 136	mulcld 11275	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐵) · (𝐺‘𝐵)) ∈ ℂ)
141	140, 137, 134	nnncan1d 11649	. . . . . 6 ⊢ (𝜑 → ((((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))) − (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴)))) = (((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐵))))
142	139, 141	eqtr4d 2798	. . . . 5 ⊢ (𝜑 → ((((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))) − (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))) = ((((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))) − (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴)))))
143	132, 135, 133	subdird 11717	. . . . . 6 ⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) = (((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))))
144	123, 135	mulcomd 11276	. . . . . . 7 ⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)) = ((𝐹‘𝐴) · ((𝐺‘𝐵) − (𝐺‘𝐴))))
145	135, 136, 133	subdid 11716	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐴) · ((𝐺‘𝐵) − (𝐺‘𝐴))) = (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴))))
146	144, 145	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)) = (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴))))
147	143, 146	oveq12d 7433	. . . . 5 ⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))) = ((((𝐹‘𝐵) · (𝐺‘𝐴)) − ((𝐹‘𝐴) · (𝐺‘𝐴))) − (((𝐹‘𝐴) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐴)))))
148	132, 135, 136	subdird 11717	. . . . . 6 ⊢ (𝜑 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) = (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))))
149	123, 132	mulcomd 11276	. . . . . . 7 ⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)) = ((𝐹‘𝐵) · ((𝐺‘𝐵) − (𝐺‘𝐴))))
150	132, 136, 133	subdid 11716	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐵) · ((𝐺‘𝐵) − (𝐺‘𝐴))) = (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴))))
151	149, 150	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)) = (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴))))
152	148, 151	oveq12d 7433	. . . . 5 ⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))) = ((((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐴) · (𝐺‘𝐵))) − (((𝐹‘𝐵) · (𝐺‘𝐵)) − ((𝐹‘𝐵) · (𝐺‘𝐴)))))
153	142, 147, 152	3eqtr4d 2805	. . . 4 ⊢ (𝜑 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))))
154		fveq2 6880	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝐺‘𝑧) = (𝐺‘𝐴))
155	154	oveq2d 7431	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)))
156		fveq2 6880	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝐹‘𝑧) = (𝐹‘𝐴))
157	156	oveq2d 7431	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴)))
158	155, 157	oveq12d 7433	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))))
159		eqid 2760	. . . . . 6 ⊢ (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))) = (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))
160		ovex 7448	. . . . . 6 ⊢ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) ∈ V
161	158, 159, 160	fvmpt3i 6994	. . . . 5 ⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐴) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))))
162	16, 161	syl 18	. . . 4 ⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐴) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐴)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐴))))
163		fveq2 6880	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵))
164	163	oveq2d 7431	. . . . . . 7 ⊢ (𝑧 = 𝐵 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)))
165		fveq2 6880	. . . . . . . 8 ⊢ (𝑧 = 𝐵 → (𝐹‘𝑧) = (𝐹‘𝐵))
166	165	oveq2d 7431	. . . . . . 7 ⊢ (𝑧 = 𝐵 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵)))
167	164, 166	oveq12d 7433	. . . . . 6 ⊢ (𝑧 = 𝐵 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))))
168	167, 159, 160	fvmpt3i 6994	. . . . 5 ⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐵) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))))
169	13, 168	syl 18	. . . 4 ⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐵) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝐵)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝐵))))
170	153, 162, 169	3eqtr4d 2805	. . 3 ⊢ (𝜑 → ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐴) = ((𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧))))‘𝐵))
171	1, 2, 3, 85, 131, 170	rolle 26246	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0)
172	126	fveq1d 6882	. . . . . 6 ⊢ (𝜑 → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥))
173		fveq2 6880	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((ℝ D 𝐺)‘𝑧) = ((ℝ D 𝐺)‘𝑥))
174	173	oveq2d 7431	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) = (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)))
175		fveq2 6880	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → ((ℝ D 𝐹)‘𝑧) = ((ℝ D 𝐹)‘𝑥))
176	175	oveq2d 7431	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))
177	174, 176	oveq12d 7433	. . . . . . 7 ⊢ (𝑧 = 𝑥 → ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))))
178	177, 129, 128	fvmpt3i 6994	. . . . . 6 ⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑧 ∈ (𝐴(,)𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑧))))‘𝑥) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))))
179	172, 178	sylan9eq 2815	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))))
180	179	eqeq1d 2762	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0 ↔ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0))
181	19	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐹‘𝐵) − (𝐹‘𝐴)) ∈ ℂ)
182	106	ffvelcdmda 7079	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐺)‘𝑥) ∈ ℂ)
183	181, 182	mulcld 11275	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) ∈ ℂ)
184	123	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((𝐺‘𝐵) − (𝐺‘𝐴)) ∈ ℂ)
185	119	ffvelcdmda 7079	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
186	184, 185	mulcld 11275	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)) ∈ ℂ)
187	183, 186	subeq0ad 11623	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))) = 0 ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))))
188	180, 187	bitrd 282	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0 ↔ (((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))))
189	188	rexbidva 3184	. 2 ⊢ (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑧 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘𝐵) − (𝐹‘𝐴)) · (𝐺‘𝑧)) − (((𝐺‘𝐵) − (𝐺‘𝐴)) · (𝐹‘𝑧)))))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥))))
190	171, 189	mpbid 235	1 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)(((𝐹‘𝐵) − (𝐹‘𝐴)) · ((ℝ D 𝐺)‘𝑥)) = (((𝐺‘𝐵) − (𝐺‘𝐴)) · ((ℝ D 𝐹)‘𝑥)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∃wrex 3086 Vcvv 3450 ⊆ wss 3899 {cpr 4586 class class class wbr 5103 {copab 5167 ↦ cmpt 5186 dom cdm 5655 ran crn 5656 ⟶wf 6530 ‘cfv 6534 (class class class)co 7415 ∈ cmpo 7417 ℂcc 11144 ℝcr 11145 0cc0 11146 · cmul 11151 ℝ^*cxr 11288 < clt 11289 ≤ cle 11290 − cmin 11487 (,)cioo 13420 [,]cicc 13423 TopOpenctopn 17528 topGenctg 17544 ℂ_fldccnfld 21614 intcnt 23271 –cn→ccncf 25133 D cdv 26119

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7738 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 ax-pre-sup 11224 ax-addf 11225

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-isom 6543 df-riota 7372 df-ov 7418 df-oprab 7419 df-mpo 7420 df-of 7680 df-om 7865 df-1st 7988 df-2nd 7989 df-supp 8161 df-frecs 8282 df-wrecs 8313 df-recs 8362 df-rdg 8401 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-card 9966 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11489 df-neg 11490 df-div 11918 df-nn 12280 df-2 12349 df-3 12350 df-4 12351 df-5 12352 df-6 12353 df-7 12354 df-8 12355 df-9 12356 df-n0 12551 df-z 12638 df-dec 12759 df-uz 12910 df-q 13020 df-rp 13065 df-xneg 13185 df-xadd 13186 df-xmul 13187 df-ioo 13424 df-ico 13426 df-icc 13427 df-fz 13584 df-fzo 13732 df-seq 14088 df-exp 14148 df-hash 14417 df-cj 15208 df-re 15209 df-im 15210 df-sqrt 15344 df-abs 15345 df-struct 17261 df-sets 17278 df-slot 17296 df-ndx 17308 df-base 17324 df-ress 17345 df-plusg 17377 df-mulr 17378 df-starv 17379 df-sca 17380 df-vsca 17381 df-ip 17382 df-tset 17383 df-ple 17384 df-ds 17386 df-unif 17387 df-hom 17388 df-cco 17389 df-rest 17529 df-topn 17530 df-0g 17548 df-gsum 17549 df-topgen 17550 df-pt 17551 df-prds 17554 df-xrs 17610 df-qtop 17615 df-imas 17616 df-xps 17618 df-mre 17692 df-mrc 17693 df-acs 17695 df-mgm 18752 df-sgrp 18844 df-mnd 18860 df-submnd 18915 df-mulg 19214 df-cntz 19467 df-cmn 19932 df-psmet 21606 df-xmet 21607 df-met 21608 df-bl 21609 df-mopn 21610 df-fbas 21611 df-fg 21612 df-cnfld 21615 df-top 23148 df-topon 23165 df-topsp 23187 df-bases 23200 df-cld 23273 df-ntr 23274 df-cls 23275 df-nei 23352 df-lp 23390 df-perf 23391 df-cn 23481 df-cnp 23482 df-haus 23569 df-cmp 23641 df-tx 23817 df-hmeo 24010 df-fil 24101 df-fm 24193 df-flim 24194 df-flf 24195 df-xms 24575 df-ms 24576 df-tms 24577 df-cncf 25135 df-limc 26122 df-dv 26123

This theorem is used by: mvth 26248 lhop1lem 26269

W3C validator