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

Theorem rolle 23973
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 10387 . . . 4 (𝜑𝐴𝐵)
5 rolle.f . . . 4 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
61, 2, 4, 5evthicc 23447 . . 3 (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
7 reeanv 3255 . . 3 (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) ↔ (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
86, 7sylibr 224 . 2 (𝜑 → ∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
9 r19.26 3212 . . . 4 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
101ad2antrr 697 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ)
112ad2antrr 697 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ)
123ad2antrr 697 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵)
135ad2antrr 697 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
14 rolle.d . . . . . . . . 9 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
1514ad2antrr 697 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
16 simpl 468 . . . . . . . . . . 11 (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → (𝐹𝑦) ≤ (𝐹𝑢))
1716ralimi 3101 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢))
18 fveq2 6332 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (𝐹𝑦) = (𝐹𝑡))
1918breq1d 4796 . . . . . . . . . . 11 (𝑦 = 𝑡 → ((𝐹𝑦) ≤ (𝐹𝑢) ↔ (𝐹𝑡) ≤ (𝐹𝑢)))
2019cbvralv 3320 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
2117, 20sylib 208 . . . . . . . . 9 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
2221ad2antrl 699 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
23 simplrl 754 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝑢 ∈ (𝐴[,]𝐵))
24 simprr 748 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ¬ 𝑢 ∈ {𝐴, 𝐵})
2510, 11, 12, 13, 15, 22, 23, 24rollelem 23972 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
2625expr 444 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (¬ 𝑢 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
271ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ)
282ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ)
293ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵)
30 cncff 22916 . . . . . . . . . . . . . . 15 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
315, 30syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
3231ffvelrnda 6502 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐹𝑢) ∈ ℝ)
3332renegcld 10659 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹𝑢) ∈ ℝ)
34 eqid 2771 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) = (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))
3533, 34fmptd 6527 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ)
36 ax-resscn 10195 . . . . . . . . . . . 12 ℝ ⊆ ℂ
37 ssid 3773 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
38 cncfss 22922 . . . . . . . . . . . . . . 15 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ))
3936, 37, 38mp2an 664 . . . . . . . . . . . . . 14 ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)
4039, 5sseldi 3750 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
4134negfcncf 22942 . . . . . . . . . . . . 13 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
4240, 41syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
43 cncffvrn 22921 . . . . . . . . . . . 12 ((ℝ ⊆ ℂ ∧ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ))
4436, 42, 43sylancr 567 . . . . . . . . . . 11 (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ))
4535, 44mpbird 247 . . . . . . . . . 10 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4645ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4736a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ⊆ ℂ)
48 iccssre 12460 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
491, 2, 48syl2anc 565 . . . . . . . . . . . . . 14 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
50 fss 6196 . . . . . . . . . . . . . . . . 17 ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
5131, 36, 50sylancl 566 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
5251ffvelrnda 6502 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐹𝑢) ∈ ℂ)
5352negcld 10581 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹𝑢) ∈ ℂ)
54 eqid 2771 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5554tgioo2 22826 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
56 iccntr 22844 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
571, 2, 56syl2anc 565 . . . . . . . . . . . . . 14 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5847, 49, 53, 55, 54, 57dvmptntr 23954 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹𝑢))))
59 reelprrecn 10230 . . . . . . . . . . . . . . 15 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
61 ioossicc 12464 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6261sseli 3748 . . . . . . . . . . . . . . 15 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ (𝐴[,]𝐵))
6362, 52sylan2 572 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑢) ∈ ℂ)
64 fvexd 6344 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑢) ∈ V)
6531feqmptd 6391 . . . . . . . . . . . . . . . 16 (𝜑𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢)))
6665oveq2d 6809 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢))))
67 dvf 23891 . . . . . . . . . . . . . . . . 17 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
6814feq2d 6171 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
6967, 68mpbii 223 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
7069feqmptd 6391 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢)))
7147, 49, 52, 55, 54, 57dvmptntr 23954 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑢))))
7266, 70, 713eqtr3rd 2814 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢)))
7360, 63, 64, 72dvmptneg 23949 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
7458, 73eqtrd 2805 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
7574dmeqd 5464 . . . . . . . . . . 11 (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
76 dmmptg 5776 . . . . . . . . . . . 12 (∀𝑢 ∈ (𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑢) ∈ V → dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵))
77 negex 10481 . . . . . . . . . . . . 13 -((ℝ D 𝐹)‘𝑢) ∈ V
7877a1i 11 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑢) ∈ V)
7976, 78mprg 3075 . . . . . . . . . . 11 dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵)
8075, 79syl6eq 2821 . . . . . . . . . 10 (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝐴(,)𝐵))
8180ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝐴(,)𝐵))
82 simpr 471 . . . . . . . . . . . . . 14 (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → (𝐹𝑣) ≤ (𝐹𝑦))
8331ad2antrr 697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
84 simplrr 755 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑣 ∈ (𝐴[,]𝐵))
8583, 84ffvelrnd 6503 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑣) ∈ ℝ)
8631adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
8786ffvelrnda 6502 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑦) ∈ ℝ)
8885, 87lenegd 10808 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ -(𝐹𝑦) ≤ -(𝐹𝑣)))
89 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑦 → (𝐹𝑢) = (𝐹𝑦))
9089negeqd 10477 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑦 → -(𝐹𝑢) = -(𝐹𝑦))
91 negex 10481 . . . . . . . . . . . . . . . . . 18 -(𝐹𝑦) ∈ V
9290, 34, 91fvmpt 6424 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = -(𝐹𝑦))
9392adantl 467 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = -(𝐹𝑦))
94 fveq2 6332 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑣 → (𝐹𝑢) = (𝐹𝑣))
9594negeqd 10477 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑣 → -(𝐹𝑢) = -(𝐹𝑣))
96 negex 10481 . . . . . . . . . . . . . . . . . 18 -(𝐹𝑣) ∈ V
9795, 34, 96fvmpt 6424 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) = -(𝐹𝑣))
9884, 97syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) = -(𝐹𝑣))
9993, 98breq12d 4799 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ -(𝐹𝑦) ≤ -(𝐹𝑣)))
10088, 99bitr4d 271 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
10182, 100syl5ib 234 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
102101ralimdva 3111 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
103102imp 393 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
104 fveq2 6332 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡))
105104breq1d 4796 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
106105cbvralv 3320 . . . . . . . . . . 11 (∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
107103, 106sylib 208 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
108107adantrr 688 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
109 simplrr 755 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝑣 ∈ (𝐴[,]𝐵))
110 simprr 748 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ¬ 𝑣 ∈ {𝐴, 𝐵})
11127, 28, 29, 46, 81, 108, 109, 110rollelem 23972 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0)
11274fveq1d 6334 . . . . . . . . . . . . 13 (𝜑 → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥))
113 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ((ℝ D 𝐹)‘𝑢) = ((ℝ D 𝐹)‘𝑥))
114113negeqd 10477 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → -((ℝ D 𝐹)‘𝑢) = -((ℝ D 𝐹)‘𝑥))
115 eqid 2771 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))
116 negex 10481 . . . . . . . . . . . . . 14 -((ℝ D 𝐹)‘𝑥) ∈ V
117114, 115, 116fvmpt 6424 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥) = -((ℝ D 𝐹)‘𝑥))
118112, 117sylan9eq 2825 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = -((ℝ D 𝐹)‘𝑥))
119118eqeq1d 2773 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0))
12014eleq2d 2836 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ dom (ℝ D 𝐹) ↔ 𝑥 ∈ (𝐴(,)𝐵)))
121120biimpar 463 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ dom (ℝ D 𝐹))
12267ffvelrni 6501 . . . . . . . . . . . . 13 (𝑥 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
123121, 122syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
124123negeq0d 10586 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0))
125119, 124bitr4d 271 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ((ℝ D 𝐹)‘𝑥) = 0))
126125rexbidva 3197 . . . . . . . . 9 (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
127126ad2antrr 697 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
128111, 127mpbid 222 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
129128expr 444 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (¬ 𝑣 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
130 vex 3354 . . . . . . . . . . 11 𝑢 ∈ V
131130elpr 4338 . . . . . . . . . 10 (𝑢 ∈ {𝐴, 𝐵} ↔ (𝑢 = 𝐴𝑢 = 𝐵))
132 fveq2 6332 . . . . . . . . . . . 12 (𝑢 = 𝐴 → (𝐹𝑢) = (𝐹𝐴))
133132a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑢 = 𝐴 → (𝐹𝑢) = (𝐹𝐴)))
134 rolle.e . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
135134eqcomd 2777 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐵) = (𝐹𝐴))
136 fveq2 6332 . . . . . . . . . . . . 13 (𝑢 = 𝐵 → (𝐹𝑢) = (𝐹𝐵))
137136eqeq1d 2773 . . . . . . . . . . . 12 (𝑢 = 𝐵 → ((𝐹𝑢) = (𝐹𝐴) ↔ (𝐹𝐵) = (𝐹𝐴)))
138135, 137syl5ibrcom 237 . . . . . . . . . . 11 (𝜑 → (𝑢 = 𝐵 → (𝐹𝑢) = (𝐹𝐴)))
139133, 138jaod 838 . . . . . . . . . 10 (𝜑 → ((𝑢 = 𝐴𝑢 = 𝐵) → (𝐹𝑢) = (𝐹𝐴)))
140131, 139syl5bi 232 . . . . . . . . 9 (𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴)))
141 eleq1w 2833 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝑢 ∈ {𝐴, 𝐵} ↔ 𝑣 ∈ {𝐴, 𝐵}))
14294eqeq1d 2773 . . . . . . . . . . . 12 (𝑢 = 𝑣 → ((𝐹𝑢) = (𝐹𝐴) ↔ (𝐹𝑣) = (𝐹𝐴)))
143141, 142imbi12d 333 . . . . . . . . . . 11 (𝑢 = 𝑣 → ((𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴)) ↔ (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴))))
144143imbi2d 329 . . . . . . . . . 10 (𝑢 = 𝑣 → ((𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴))) ↔ (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴)))))
145144, 140chvarv 2425 . . . . . . . . 9 (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴)))
146140, 145anim12d 588 . . . . . . . 8 (𝜑 → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))))
147146ad2antrr 697 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))))
1481rexrd 10291 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ*)
1492rexrd 10291 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
150 lbicc2 12495 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
151148, 149, 4, 150syl3anc 1476 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ (𝐴[,]𝐵))
15231, 151ffvelrnd 6503 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝐴) ∈ ℝ)
153152ad2antrr 697 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝐴) ∈ ℝ)
15487, 153letri3d 10381 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦))))
155 breq2 4790 . . . . . . . . . . . . . . 15 ((𝐹𝑢) = (𝐹𝐴) → ((𝐹𝑦) ≤ (𝐹𝑢) ↔ (𝐹𝑦) ≤ (𝐹𝐴)))
156 breq1 4789 . . . . . . . . . . . . . . 15 ((𝐹𝑣) = (𝐹𝐴) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ (𝐹𝐴) ≤ (𝐹𝑦)))
157155, 156bi2anan9 612 . . . . . . . . . . . . . 14 (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦))))
158157bibi2d 331 . . . . . . . . . . . . 13 (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → (((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) ↔ ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦)))))
159154, 158syl5ibrcom 237 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)))))
160159impancom 439 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)))))
161160imp 393 . . . . . . . . . 10 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))))
162161ralbidva 3134 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))))
163 ffn 6185 . . . . . . . . . . . . . 14 (𝐹:(𝐴[,]𝐵)⟶ℝ → 𝐹 Fn (𝐴[,]𝐵))
16431, 163syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (𝐴[,]𝐵))
165 fnconstg 6233 . . . . . . . . . . . . . 14 ((𝐹𝐴) ∈ ℝ → ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵))
166152, 165syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵))
167 eqfnfv 6454 . . . . . . . . . . . . 13 ((𝐹 Fn (𝐴[,]𝐵) ∧ ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵)) → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦)))
168164, 166, 167syl2anc 565 . . . . . . . . . . . 12 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦)))
169 fvex 6342 . . . . . . . . . . . . . . 15 (𝐹𝐴) ∈ V
170169fvconst2 6613 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) = (𝐹𝐴))
171170eqeq2d 2781 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) ↔ (𝐹𝑦) = (𝐹𝐴)))
172171ralbiia 3128 . . . . . . . . . . . 12 (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴))
173168, 172syl6bb 276 . . . . . . . . . . 11 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴)))
174 fconstmpt 5303 . . . . . . . . . . . . . . . . . . . 20 ((𝐴[,]𝐵) × {(𝐹𝐴)}) = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))
175174eqeq2i 2783 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴)))
176175biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴)))
177176oveq2d 6809 . . . . . . . . . . . . . . . . 17 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))))
178152recnd 10270 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹𝐴) ∈ ℂ)
179178adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ ℝ) → (𝐹𝐴) ∈ ℂ)
180 0cnd 10235 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ ℝ) → 0 ∈ ℂ)
18160, 178dvmptc 23941 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑢 ∈ ℝ ↦ (𝐹𝐴))) = (𝑢 ∈ ℝ ↦ 0))
18260, 179, 180, 181, 49, 55, 54, 57dvmptres2 23945 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0))
183177, 182sylan9eqr 2827 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0))
184183fveq1d 6334 . . . . . . . . . . . . . . 15 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ((ℝ D 𝐹)‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥))
185 eqidd 2772 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 0 = 0)
186 eqid 2771 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (𝐴(,)𝐵) ↦ 0) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0)
187 c0ex 10236 . . . . . . . . . . . . . . . 16 0 ∈ V
188185, 186, 187fvmpt 6424 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥) = 0)
189184, 188sylan9eq 2825 . . . . . . . . . . . . . 14 (((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) = 0)
190189ralrimiva 3115 . . . . . . . . . . . . 13 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
191 ioon0 12406 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵))
192148, 149, 191syl2anc 565 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵))
1933, 192mpbird 247 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
194 r19.2z 4201 . . . . . . . . . . . . . 14 (((𝐴(,)𝐵) ≠ ∅ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
195193, 194sylan 561 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
196190, 195syldan 571 . . . . . . . . . . . 12 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
197196ex 397 . . . . . . . . . . 11 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
198173, 197sylbird 250 . . . . . . . . . 10 (𝜑 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
199198ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
200162, 199sylbird 250 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
201200impancom 439 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
202147, 201syld 47 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
20326, 129, 202ecased 1021 . . . . 5 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
204203ex 397 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
2059, 204syl5bir 233 . . 3 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → ((∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
206205rexlimdvva 3186 . 2 (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
2078, 206mpd 15 1 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 826   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  wss 3723  c0 4063  {csn 4316  {cpr 4318   class class class wbr 4786  cmpt 4863   × cxp 5247  dom cdm 5249  ran crn 5250   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  cc 10136  cr 10137  0cc0 10138  *cxr 10275   < clt 10276  cle 10277  -cneg 10469  (,)cioo 12380  [,]cicc 12383  TopOpenctopn 16290  topGenctg 16306  fldccnfld 19961  intcnt 21042  cnccncf 22899   D cdv 23847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17957  df-cmn 18402  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-cmp 21411  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-xms 22345  df-ms 22346  df-tms 22347  df-cncf 22901  df-limc 23850  df-dv 23851
This theorem is referenced by:  cmvth  23974  lhop1lem  23996
  Copyright terms: Public domain W3C validator