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

Theorem rolle 24516
Description: Rolle's theorem. If 𝐹 is a real continuous function on [𝐴, 𝐵] which is differentiable on (𝐴, 𝐵), and 𝐹(𝐴) = 𝐹(𝐵), then there is some 𝑥 ∈ (𝐴, 𝐵) such that (ℝ D 𝐹)‘𝑥 = 0. (Contributed by Mario Carneiro, 1-Sep-2014.)
Hypotheses
Ref Expression
rolle.a (𝜑𝐴 ∈ ℝ)
rolle.b (𝜑𝐵 ∈ ℝ)
rolle.lt (𝜑𝐴 < 𝐵)
rolle.f (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
rolle.d (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
rolle.e (𝜑 → (𝐹𝐴) = (𝐹𝐵))
Assertion
Ref Expression
rolle (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝐵   𝑥,𝐹

Proof of Theorem rolle
Dummy variables 𝑢 𝑡 𝑣 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rolle.a . . . 4 (𝜑𝐴 ∈ ℝ)
2 rolle.b . . . 4 (𝜑𝐵 ∈ ℝ)
3 rolle.lt . . . . 5 (𝜑𝐴 < 𝐵)
41, 2, 3ltled 10777 . . . 4 (𝜑𝐴𝐵)
5 rolle.f . . . 4 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
61, 2, 4, 5evthicc 23989 . . 3 (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
7 reeanv 3368 . . 3 (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) ↔ (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
86, 7sylibr 235 . 2 (𝜑 → ∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
9 r19.26 3170 . . . 4 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
101ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ)
112ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ)
123ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵)
135ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
14 rolle.d . . . . . . . . 9 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
1514ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
16 simpl 483 . . . . . . . . . . 11 (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → (𝐹𝑦) ≤ (𝐹𝑢))
1716ralimi 3160 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢))
18 fveq2 6664 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (𝐹𝑦) = (𝐹𝑡))
1918breq1d 5068 . . . . . . . . . . 11 (𝑦 = 𝑡 → ((𝐹𝑦) ≤ (𝐹𝑢) ↔ (𝐹𝑡) ≤ (𝐹𝑢)))
2019cbvralvw 3450 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
2117, 20sylib 219 . . . . . . . . 9 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
2221ad2antrl 724 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
23 simplrl 773 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝑢 ∈ (𝐴[,]𝐵))
24 simprr 769 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ¬ 𝑢 ∈ {𝐴, 𝐵})
2510, 11, 12, 13, 15, 22, 23, 24rollelem 24515 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
2625expr 457 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (¬ 𝑢 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
271ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ)
282ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ)
293ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵)
30 cncff 23430 . . . . . . . . . . . . . . 15 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
315, 30syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
3231ffvelrnda 6844 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐹𝑢) ∈ ℝ)
3332renegcld 11056 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹𝑢) ∈ ℝ)
3433fmpttd 6872 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ)
35 ax-resscn 10583 . . . . . . . . . . . 12 ℝ ⊆ ℂ
36 ssid 3988 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
37 cncfss 23436 . . . . . . . . . . . . . . 15 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ))
3835, 36, 37mp2an 688 . . . . . . . . . . . . . 14 ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)
3938, 5sseldi 3964 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
40 eqid 2821 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) = (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))
4140negfcncf 23456 . . . . . . . . . . . . 13 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
4239, 41syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
43 cncffvrn 23435 . . . . . . . . . . . 12 ((ℝ ⊆ ℂ ∧ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ))
4435, 42, 43sylancr 587 . . . . . . . . . . 11 (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ))
4534, 44mpbird 258 . . . . . . . . . 10 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4645ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4735a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ⊆ ℂ)
48 iccssre 12808 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
491, 2, 48syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
50 fss 6521 . . . . . . . . . . . . . . . . 17 ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
5131, 35, 50sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
5251ffvelrnda 6844 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐹𝑢) ∈ ℂ)
5352negcld 10973 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹𝑢) ∈ ℂ)
54 eqid 2821 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5554tgioo2 23340 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
56 iccntr 23358 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
571, 2, 56syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5847, 49, 53, 55, 54, 57dvmptntr 24497 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹𝑢))))
59 reelprrecn 10618 . . . . . . . . . . . . . . 15 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
61 ioossicc 12812 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6261sseli 3962 . . . . . . . . . . . . . . 15 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ (𝐴[,]𝐵))
6362, 52sylan2 592 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑢) ∈ ℂ)
64 fvexd 6679 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑢) ∈ V)
6531feqmptd 6727 . . . . . . . . . . . . . . . 16 (𝜑𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢)))
6665oveq2d 7161 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢))))
67 dvf 24434 . . . . . . . . . . . . . . . . 17 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
6814feq2d 6494 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
6967, 68mpbii 234 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
7069feqmptd 6727 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢)))
7147, 49, 52, 55, 54, 57dvmptntr 24497 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑢))))
7266, 70, 713eqtr3rd 2865 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢)))
7360, 63, 64, 72dvmptneg 24492 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
7458, 73eqtrd 2856 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
7574dmeqd 5768 . . . . . . . . . . 11 (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
76 dmmptg 6090 . . . . . . . . . . . 12 (∀𝑢 ∈ (𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑢) ∈ V → dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵))
77 negex 10873 . . . . . . . . . . . . 13 -((ℝ D 𝐹)‘𝑢) ∈ V
7877a1i 11 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑢) ∈ V)
7976, 78mprg 3152 . . . . . . . . . . 11 dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵)
8075, 79syl6eq 2872 . . . . . . . . . 10 (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝐴(,)𝐵))
8180ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝐴(,)𝐵))
82 simpr 485 . . . . . . . . . . . . . 14 (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → (𝐹𝑣) ≤ (𝐹𝑦))
8331ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
84 simplrr 774 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑣 ∈ (𝐴[,]𝐵))
8583, 84ffvelrnd 6845 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑣) ∈ ℝ)
8631adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
8786ffvelrnda 6844 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑦) ∈ ℝ)
8885, 87lenegd 11208 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ -(𝐹𝑦) ≤ -(𝐹𝑣)))
89 fveq2 6664 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑦 → (𝐹𝑢) = (𝐹𝑦))
9089negeqd 10869 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑦 → -(𝐹𝑢) = -(𝐹𝑦))
91 negex 10873 . . . . . . . . . . . . . . . . . 18 -(𝐹𝑦) ∈ V
9290, 40, 91fvmpt 6762 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = -(𝐹𝑦))
9392adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = -(𝐹𝑦))
94 fveq2 6664 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑣 → (𝐹𝑢) = (𝐹𝑣))
9594negeqd 10869 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑣 → -(𝐹𝑢) = -(𝐹𝑣))
96 negex 10873 . . . . . . . . . . . . . . . . . 18 -(𝐹𝑣) ∈ V
9795, 40, 96fvmpt 6762 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) = -(𝐹𝑣))
9884, 97syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) = -(𝐹𝑣))
9993, 98breq12d 5071 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ -(𝐹𝑦) ≤ -(𝐹𝑣)))
10088, 99bitr4d 283 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
10182, 100syl5ib 245 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
102101ralimdva 3177 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
103102imp 407 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
104 fveq2 6664 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡))
105104breq1d 5068 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
106105cbvralvw 3450 . . . . . . . . . . 11 (∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
107103, 106sylib 219 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
108107adantrr 713 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
109 simplrr 774 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝑣 ∈ (𝐴[,]𝐵))
110 simprr 769 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ¬ 𝑣 ∈ {𝐴, 𝐵})
11127, 28, 29, 46, 81, 108, 109, 110rollelem 24515 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0)
11274fveq1d 6666 . . . . . . . . . . . . 13 (𝜑 → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥))
113 fveq2 6664 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ((ℝ D 𝐹)‘𝑢) = ((ℝ D 𝐹)‘𝑥))
114113negeqd 10869 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → -((ℝ D 𝐹)‘𝑢) = -((ℝ D 𝐹)‘𝑥))
115 eqid 2821 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))
116 negex 10873 . . . . . . . . . . . . . 14 -((ℝ D 𝐹)‘𝑥) ∈ V
117114, 115, 116fvmpt 6762 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥) = -((ℝ D 𝐹)‘𝑥))
118112, 117sylan9eq 2876 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = -((ℝ D 𝐹)‘𝑥))
119118eqeq1d 2823 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0))
12014eleq2d 2898 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ dom (ℝ D 𝐹) ↔ 𝑥 ∈ (𝐴(,)𝐵)))
121120biimpar 478 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ dom (ℝ D 𝐹))
12267ffvelrni 6843 . . . . . . . . . . . . 13 (𝑥 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
123121, 122syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
124123negeq0d 10978 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0))
125119, 124bitr4d 283 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ((ℝ D 𝐹)‘𝑥) = 0))
126125rexbidva 3296 . . . . . . . . 9 (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
127126ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
128111, 127mpbid 233 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
129128expr 457 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (¬ 𝑣 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
130 vex 3498 . . . . . . . . . . 11 𝑢 ∈ V
131130elpr 4582 . . . . . . . . . 10 (𝑢 ∈ {𝐴, 𝐵} ↔ (𝑢 = 𝐴𝑢 = 𝐵))
132 fveq2 6664 . . . . . . . . . . . 12 (𝑢 = 𝐴 → (𝐹𝑢) = (𝐹𝐴))
133132a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑢 = 𝐴 → (𝐹𝑢) = (𝐹𝐴)))
134 rolle.e . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
135134eqcomd 2827 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐵) = (𝐹𝐴))
136 fveqeq2 6673 . . . . . . . . . . . 12 (𝑢 = 𝐵 → ((𝐹𝑢) = (𝐹𝐴) ↔ (𝐹𝐵) = (𝐹𝐴)))
137135, 136syl5ibrcom 248 . . . . . . . . . . 11 (𝜑 → (𝑢 = 𝐵 → (𝐹𝑢) = (𝐹𝐴)))
138133, 137jaod 853 . . . . . . . . . 10 (𝜑 → ((𝑢 = 𝐴𝑢 = 𝐵) → (𝐹𝑢) = (𝐹𝐴)))
139131, 138syl5bi 243 . . . . . . . . 9 (𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴)))
140 eleq1w 2895 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝑢 ∈ {𝐴, 𝐵} ↔ 𝑣 ∈ {𝐴, 𝐵}))
141 fveqeq2 6673 . . . . . . . . . . . 12 (𝑢 = 𝑣 → ((𝐹𝑢) = (𝐹𝐴) ↔ (𝐹𝑣) = (𝐹𝐴)))
142140, 141imbi12d 346 . . . . . . . . . . 11 (𝑢 = 𝑣 → ((𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴)) ↔ (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴))))
143142imbi2d 342 . . . . . . . . . 10 (𝑢 = 𝑣 → ((𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴))) ↔ (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴)))))
144143, 139chvarvv 1996 . . . . . . . . 9 (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴)))
145139, 144anim12d 608 . . . . . . . 8 (𝜑 → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))))
146145ad2antrr 722 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))))
1471rexrd 10680 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ*)
1482rexrd 10680 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
149 lbicc2 12842 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
150147, 148, 4, 149syl3anc 1363 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ (𝐴[,]𝐵))
15131, 150ffvelrnd 6845 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝐴) ∈ ℝ)
152151ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝐴) ∈ ℝ)
15387, 152letri3d 10771 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦))))
154 breq2 5062 . . . . . . . . . . . . . . 15 ((𝐹𝑢) = (𝐹𝐴) → ((𝐹𝑦) ≤ (𝐹𝑢) ↔ (𝐹𝑦) ≤ (𝐹𝐴)))
155 breq1 5061 . . . . . . . . . . . . . . 15 ((𝐹𝑣) = (𝐹𝐴) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ (𝐹𝐴) ≤ (𝐹𝑦)))
156154, 155bi2anan9 635 . . . . . . . . . . . . . 14 (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦))))
157156bibi2d 344 . . . . . . . . . . . . 13 (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → (((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) ↔ ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦)))))
158153, 157syl5ibrcom 248 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)))))
159158impancom 452 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)))))
160159imp 407 . . . . . . . . . 10 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))))
161160ralbidva 3196 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))))
16231ffnd 6509 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (𝐴[,]𝐵))
163 fnconstg 6561 . . . . . . . . . . . . . 14 ((𝐹𝐴) ∈ ℝ → ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵))
164151, 163syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵))
165 eqfnfv 6795 . . . . . . . . . . . . 13 ((𝐹 Fn (𝐴[,]𝐵) ∧ ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵)) → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦)))
166162, 164, 165syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦)))
167 fvex 6677 . . . . . . . . . . . . . . 15 (𝐹𝐴) ∈ V
168167fvconst2 6959 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) = (𝐹𝐴))
169168eqeq2d 2832 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) ↔ (𝐹𝑦) = (𝐹𝐴)))
170169ralbiia 3164 . . . . . . . . . . . 12 (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴))
171166, 170syl6bb 288 . . . . . . . . . . 11 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴)))
172 ioon0 12754 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵))
173147, 148, 172syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵))
1743, 173mpbird 258 . . . . . . . . . . . . 13 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
175 fconstmpt 5608 . . . . . . . . . . . . . . . . . . . 20 ((𝐴[,]𝐵) × {(𝐹𝐴)}) = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))
176175eqeq2i 2834 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴)))
177176biimpi 217 . . . . . . . . . . . . . . . . . 18 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴)))
178177oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))))
179151recnd 10658 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹𝐴) ∈ ℂ)
180179adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ ℝ) → (𝐹𝐴) ∈ ℂ)
181 0cnd 10623 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ ℝ) → 0 ∈ ℂ)
18260, 179dvmptc 24484 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑢 ∈ ℝ ↦ (𝐹𝐴))) = (𝑢 ∈ ℝ ↦ 0))
18360, 180, 181, 182, 49, 55, 54, 57dvmptres2 24488 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0))
184178, 183sylan9eqr 2878 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0))
185184fveq1d 6666 . . . . . . . . . . . . . . 15 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ((ℝ D 𝐹)‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥))
186 eqidd 2822 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 0 = 0)
187 eqid 2821 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (𝐴(,)𝐵) ↦ 0) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0)
188 c0ex 10624 . . . . . . . . . . . . . . . 16 0 ∈ V
189186, 187, 188fvmpt 6762 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥) = 0)
190185, 189sylan9eq 2876 . . . . . . . . . . . . . 14 (((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) = 0)
191190ralrimiva 3182 . . . . . . . . . . . . 13 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
192 r19.2z 4438 . . . . . . . . . . . . 13 (((𝐴(,)𝐵) ≠ ∅ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
193174, 191, 192syl2an2r 681 . . . . . . . . . . . 12 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
194193ex 413 . . . . . . . . . . 11 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
195171, 194sylbird 261 . . . . . . . . . 10 (𝜑 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
196195ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
197161, 196sylbird 261 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
198197impancom 452 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
199146, 198syld 47 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
20026, 129, 199ecased 1027 . . . . 5 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
201200ex 413 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
2029, 201syl5bir 244 . . 3 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → ((∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
203202rexlimdvva 3294 . 2 (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
2048, 203mpd 15 1 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wne 3016  wral 3138  wrex 3139  Vcvv 3495  wss 3935  c0 4290  {csn 4559  {cpr 4561   class class class wbr 5058  cmpt 5138   × cxp 5547  dom cdm 5549  ran crn 5550   Fn wfn 6344  wf 6345  cfv 6349  (class class class)co 7145  cc 10524  cr 10525  0cc0 10526  *cxr 10663   < clt 10664  cle 10665  -cneg 10860  (,)cioo 12728  [,]cicc 12731  TopOpenctopn 16685  topGenctg 16701  fldccnfld 20475  intcnt 21555  cnccncf 23413   D cdv 24390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8451  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-fi 8864  df-sup 8895  df-inf 8896  df-oi 8963  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-q 12338  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ico 12734  df-icc 12735  df-fz 12883  df-fzo 13024  df-seq 13360  df-exp 13420  df-hash 13681  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-sca 16571  df-vsca 16572  df-ip 16573  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-hom 16579  df-cco 16580  df-rest 16686  df-topn 16687  df-0g 16705  df-gsum 16706  df-topgen 16707  df-pt 16708  df-prds 16711  df-xrs 16765  df-qtop 16770  df-imas 16771  df-xps 16773  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17891  df-mnd 17902  df-submnd 17947  df-mulg 18165  df-cntz 18387  df-cmn 18839  df-psmet 20467  df-xmet 20468  df-met 20469  df-bl 20470  df-mopn 20471  df-fbas 20472  df-fg 20473  df-cnfld 20476  df-top 21432  df-topon 21449  df-topsp 21471  df-bases 21484  df-cld 21557  df-ntr 21558  df-cls 21559  df-nei 21636  df-lp 21674  df-perf 21675  df-cn 21765  df-cnp 21766  df-haus 21853  df-cmp 21925  df-tx 22100  df-hmeo 22293  df-fil 22384  df-fm 22476  df-flim 22477  df-flf 22478  df-xms 22859  df-ms 22860  df-tms 22861  df-cncf 23415  df-limc 24393  df-dv 24394
This theorem is referenced by:  cmvth  24517  lhop1lem  24539
  Copyright terms: Public domain W3C validator