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

Theorem rolle 23664
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 10132 . . . 4 (𝜑𝐴𝐵)
5 rolle.f . . . 4 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
61, 2, 4, 5evthicc 23141 . . 3 (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
7 reeanv 3097 . . 3 (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) ↔ (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
86, 7sylibr 224 . 2 (𝜑 → ∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
9 r19.26 3057 . . . 4 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)))
101ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ)
112ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ)
123ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵)
135ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ))
14 rolle.d . . . . . . . . 9 (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
1514ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → dom (ℝ D 𝐹) = (𝐴(,)𝐵))
16 simpl 473 . . . . . . . . . . 11 (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → (𝐹𝑦) ≤ (𝐹𝑢))
1716ralimi 2947 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢))
18 fveq2 6150 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (𝐹𝑦) = (𝐹𝑡))
1918breq1d 4625 . . . . . . . . . . 11 (𝑦 = 𝑡 → ((𝐹𝑦) ≤ (𝐹𝑢) ↔ (𝐹𝑡) ≤ (𝐹𝑢)))
2019cbvralv 3159 . . . . . . . . . 10 (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
2117, 20sylib 208 . . . . . . . . 9 (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
2221ad2antrl 763 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹𝑡) ≤ (𝐹𝑢))
23 simplrl 799 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝑢 ∈ (𝐴[,]𝐵))
24 simprr 795 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ¬ 𝑢 ∈ {𝐴, 𝐵})
2510, 11, 12, 13, 15, 22, 23, 24rollelem 23663 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
2625expr 642 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (¬ 𝑢 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
271ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ)
282ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ)
293ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵)
30 cncff 22609 . . . . . . . . . . . . . . 15 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
315, 30syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹:(𝐴[,]𝐵)⟶ℝ)
3231ffvelrnda 6317 . . . . . . . . . . . . 13 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐹𝑢) ∈ ℝ)
3332renegcld 10404 . . . . . . . . . . . 12 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹𝑢) ∈ ℝ)
34 eqid 2621 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) = (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))
3533, 34fmptd 6343 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ)
36 ax-resscn 9940 . . . . . . . . . . . 12 ℝ ⊆ ℂ
37 ssid 3605 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
38 cncfss 22615 . . . . . . . . . . . . . . 15 ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ))
3936, 37, 38mp2an 707 . . . . . . . . . . . . . 14 ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)
4039, 5sseldi 3582 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
4134negfcncf 22635 . . . . . . . . . . . . 13 (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
4240, 41syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
43 cncffvrn 22614 . . . . . . . . . . . 12 ((ℝ ⊆ ℂ ∧ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ))
4436, 42, 43sylancr 694 . . . . . . . . . . 11 (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)):(𝐴[,]𝐵)⟶ℝ))
4535, 44mpbird 247 . . . . . . . . . 10 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4645ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ))
4736a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ⊆ ℂ)
48 iccssre 12200 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
491, 2, 48syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
50 fss 6015 . . . . . . . . . . . . . . . . 17 ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆ ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
5131, 36, 50sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝐴[,]𝐵)⟶ℂ)
5251ffvelrnda 6317 . . . . . . . . . . . . . . 15 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐹𝑢) ∈ ℂ)
5352negcld 10326 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹𝑢) ∈ ℂ)
54 eqid 2621 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5554tgioo2 22519 . . . . . . . . . . . . . 14 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
56 iccntr 22537 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
571, 2, 56syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
5847, 49, 53, 55, 54, 57dvmptntr 23647 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹𝑢))))
59 reelprrecn 9975 . . . . . . . . . . . . . . 15 ℝ ∈ {ℝ, ℂ}
6059a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ℝ ∈ {ℝ, ℂ})
61 ioossicc 12204 . . . . . . . . . . . . . . . 16 (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
6261sseli 3580 . . . . . . . . . . . . . . 15 (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ (𝐴[,]𝐵))
6362, 52sylan2 491 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴(,)𝐵)) → (𝐹𝑢) ∈ ℂ)
64 fvex 6160 . . . . . . . . . . . . . . 15 ((ℝ D 𝐹)‘𝑢) ∈ V
6564a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑢 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑢) ∈ V)
6631feqmptd 6208 . . . . . . . . . . . . . . . 16 (𝜑𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢)))
6766oveq2d 6623 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢))))
68 dvf 23584 . . . . . . . . . . . . . . . . 17 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
6914feq2d 5990 . . . . . . . . . . . . . . . . 17 (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ))
7068, 69mpbii 223 . . . . . . . . . . . . . . . 16 (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ)
7170feqmptd 6208 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢)))
7247, 49, 52, 55, 54, 57dvmptntr 23647 . . . . . . . . . . . . . . 15 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑢))))
7367, 71, 723eqtr3rd 2664 . . . . . . . . . . . . . 14 (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢)))
7460, 63, 65, 73dvmptneg 23642 . . . . . . . . . . . . 13 (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
7558, 74eqtrd 2655 . . . . . . . . . . . 12 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
7675dmeqd 5288 . . . . . . . . . . 11 (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)))
77 dmmptg 5593 . . . . . . . . . . . 12 (∀𝑢 ∈ (𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑢) ∈ V → dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵))
78 negex 10226 . . . . . . . . . . . . 13 -((ℝ D 𝐹)‘𝑢) ∈ V
7978a1i 11 . . . . . . . . . . . 12 (𝑢 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑢) ∈ V)
8077, 79mprg 2921 . . . . . . . . . . 11 dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵)
8176, 80syl6eq 2671 . . . . . . . . . 10 (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝐴(,)𝐵))
8281ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))) = (𝐴(,)𝐵))
83 simpr 477 . . . . . . . . . . . . . 14 (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → (𝐹𝑣) ≤ (𝐹𝑦))
8431ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
85 simplrr 800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑣 ∈ (𝐴[,]𝐵))
8684, 85ffvelrnd 6318 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑣) ∈ ℝ)
8731adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → 𝐹:(𝐴[,]𝐵)⟶ℝ)
8887ffvelrnda 6317 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝑦) ∈ ℝ)
8986, 88lenegd 10553 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ -(𝐹𝑦) ≤ -(𝐹𝑣)))
90 fveq2 6150 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑦 → (𝐹𝑢) = (𝐹𝑦))
9190negeqd 10222 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑦 → -(𝐹𝑢) = -(𝐹𝑦))
92 negex 10226 . . . . . . . . . . . . . . . . . 18 -(𝐹𝑦) ∈ V
9391, 34, 92fvmpt 6241 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = -(𝐹𝑦))
9493adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = -(𝐹𝑦))
95 fveq2 6150 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑣 → (𝐹𝑢) = (𝐹𝑣))
9695negeqd 10222 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑣 → -(𝐹𝑢) = -(𝐹𝑣))
97 negex 10226 . . . . . . . . . . . . . . . . . 18 -(𝐹𝑣) ∈ V
9896, 34, 97fvmpt 6241 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) = -(𝐹𝑣))
9985, 98syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) = -(𝐹𝑣))
10094, 99breq12d 4628 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ -(𝐹𝑦) ≤ -(𝐹𝑣)))
10189, 100bitr4d 271 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
10283, 101syl5ib 234 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
103102ralimdva 2956 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
104103imp 445 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
105 fveq2 6150 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) = ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡))
106105breq1d 4625 . . . . . . . . . . . 12 (𝑦 = 𝑡 → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣)))
107106cbvralv 3159 . . . . . . . . . . 11 (∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
108104, 107sylib 208 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
109108adantrr 752 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢))‘𝑣))
110 simplrr 800 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝑣 ∈ (𝐴[,]𝐵))
111 simprr 795 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ¬ 𝑣 ∈ {𝐴, 𝐵})
11227, 28, 29, 46, 82, 109, 110, 111rollelem 23663 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0)
11375fveq1d 6152 . . . . . . . . . . . . 13 (𝜑 → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥))
114 fveq2 6150 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ((ℝ D 𝐹)‘𝑢) = ((ℝ D 𝐹)‘𝑥))
115114negeqd 10222 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → -((ℝ D 𝐹)‘𝑢) = -((ℝ D 𝐹)‘𝑥))
116 eqid 2621 . . . . . . . . . . . . . 14 (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))
117 negex 10226 . . . . . . . . . . . . . 14 -((ℝ D 𝐹)‘𝑥) ∈ V
118115, 116, 117fvmpt 6241 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥) = -((ℝ D 𝐹)‘𝑥))
119113, 118sylan9eq 2675 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = -((ℝ D 𝐹)‘𝑥))
120119eqeq1d 2623 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0))
12114eleq2d 2684 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ dom (ℝ D 𝐹) ↔ 𝑥 ∈ (𝐴(,)𝐵)))
122121biimpar 502 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ dom (ℝ D 𝐹))
12368ffvelrni 6316 . . . . . . . . . . . . 13 (𝑥 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
124122, 123syl 17 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ)
125124negeq0d 10331 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0))
126120, 125bitr4d 271 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ((ℝ D 𝐹)‘𝑥) = 0))
127126rexbidva 3042 . . . . . . . . 9 (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
128127ad2antrr 761 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
129112, 128mpbid 222 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
130129expr 642 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (¬ 𝑣 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
131 vex 3189 . . . . . . . . . . 11 𝑢 ∈ V
132131elpr 4171 . . . . . . . . . 10 (𝑢 ∈ {𝐴, 𝐵} ↔ (𝑢 = 𝐴𝑢 = 𝐵))
133 fveq2 6150 . . . . . . . . . . . 12 (𝑢 = 𝐴 → (𝐹𝑢) = (𝐹𝐴))
134133a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑢 = 𝐴 → (𝐹𝑢) = (𝐹𝐴)))
135 rolle.e . . . . . . . . . . . . 13 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
136135eqcomd 2627 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐵) = (𝐹𝐴))
137 fveq2 6150 . . . . . . . . . . . . 13 (𝑢 = 𝐵 → (𝐹𝑢) = (𝐹𝐵))
138137eqeq1d 2623 . . . . . . . . . . . 12 (𝑢 = 𝐵 → ((𝐹𝑢) = (𝐹𝐴) ↔ (𝐹𝐵) = (𝐹𝐴)))
139136, 138syl5ibrcom 237 . . . . . . . . . . 11 (𝜑 → (𝑢 = 𝐵 → (𝐹𝑢) = (𝐹𝐴)))
140134, 139jaod 395 . . . . . . . . . 10 (𝜑 → ((𝑢 = 𝐴𝑢 = 𝐵) → (𝐹𝑢) = (𝐹𝐴)))
141132, 140syl5bi 232 . . . . . . . . 9 (𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴)))
142 eleq1 2686 . . . . . . . . . . . 12 (𝑢 = 𝑣 → (𝑢 ∈ {𝐴, 𝐵} ↔ 𝑣 ∈ {𝐴, 𝐵}))
14395eqeq1d 2623 . . . . . . . . . . . 12 (𝑢 = 𝑣 → ((𝐹𝑢) = (𝐹𝐴) ↔ (𝐹𝑣) = (𝐹𝐴)))
144142, 143imbi12d 334 . . . . . . . . . . 11 (𝑢 = 𝑣 → ((𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴)) ↔ (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴))))
145144imbi2d 330 . . . . . . . . . 10 (𝑢 = 𝑣 → ((𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹𝑢) = (𝐹𝐴))) ↔ (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴)))))
146145, 141chvarv 2262 . . . . . . . . 9 (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹𝑣) = (𝐹𝐴)))
147141, 146anim12d 585 . . . . . . . 8 (𝜑 → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))))
148147ad2antrr 761 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))))
1491rexrd 10036 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℝ*)
1502rexrd 10036 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ*)
151 lbicc2 12233 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
152149, 150, 4, 151syl3anc 1323 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ (𝐴[,]𝐵))
15331, 152ffvelrnd 6318 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝐴) ∈ ℝ)
154153ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹𝐴) ∈ ℝ)
15588, 154letri3d 10126 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦))))
156 breq2 4619 . . . . . . . . . . . . . . 15 ((𝐹𝑢) = (𝐹𝐴) → ((𝐹𝑦) ≤ (𝐹𝑢) ↔ (𝐹𝑦) ≤ (𝐹𝐴)))
157 breq1 4618 . . . . . . . . . . . . . . 15 ((𝐹𝑣) = (𝐹𝐴) → ((𝐹𝑣) ≤ (𝐹𝑦) ↔ (𝐹𝐴) ≤ (𝐹𝑦)))
158156, 157bi2anan9 916 . . . . . . . . . . . . . 14 (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → (((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦))))
159158bibi2d 332 . . . . . . . . . . . . 13 (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → (((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) ↔ ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝐴) ∧ (𝐹𝐴) ≤ (𝐹𝑦)))))
160155, 159syl5ibrcom 237 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)))))
161160impancom 456 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)))))
162161imp 445 . . . . . . . . . 10 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹𝑦) = (𝐹𝐴) ↔ ((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))))
163162ralbidva 2979 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))))
164 ffn 6004 . . . . . . . . . . . . . 14 (𝐹:(𝐴[,]𝐵)⟶ℝ → 𝐹 Fn (𝐴[,]𝐵))
16531, 164syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (𝐴[,]𝐵))
166 fnconstg 6052 . . . . . . . . . . . . . 14 ((𝐹𝐴) ∈ ℝ → ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵))
167153, 166syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵))
168 eqfnfv 6269 . . . . . . . . . . . . 13 ((𝐹 Fn (𝐴[,]𝐵) ∧ ((𝐴[,]𝐵) × {(𝐹𝐴)}) Fn (𝐴[,]𝐵)) → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦)))
169165, 167, 168syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦)))
170 fvex 6160 . . . . . . . . . . . . . . 15 (𝐹𝐴) ∈ V
171170fvconst2 6426 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) = (𝐹𝐴))
172171eqeq2d 2631 . . . . . . . . . . . . 13 (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) ↔ (𝐹𝑦) = (𝐹𝐴)))
173172ralbiia 2973 . . . . . . . . . . . 12 (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (((𝐴[,]𝐵) × {(𝐹𝐴)})‘𝑦) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴))
174169, 173syl6bb 276 . . . . . . . . . . 11 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴)))
175 fconstmpt 5125 . . . . . . . . . . . . . . . . . . . 20 ((𝐴[,]𝐵) × {(𝐹𝐴)}) = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))
176175eqeq2i 2633 . . . . . . . . . . . . . . . . . . 19 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) ↔ 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴)))
177176biimpi 206 . . . . . . . . . . . . . . . . . 18 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴)))
178177oveq2d 6623 . . . . . . . . . . . . . . . . 17 (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))))
179153recnd 10015 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹𝐴) ∈ ℂ)
180179adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ ℝ) → (𝐹𝐴) ∈ ℂ)
181 0cnd 9980 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑢 ∈ ℝ) → 0 ∈ ℂ)
18260, 179dvmptc 23634 . . . . . . . . . . . . . . . . . 18 (𝜑 → (ℝ D (𝑢 ∈ ℝ ↦ (𝐹𝐴))) = (𝑢 ∈ ℝ ↦ 0))
18360, 180, 181, 182, 49, 55, 54, 57dvmptres2 23638 . . . . . . . . . . . . . . . . 17 (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐴))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0))
184178, 183sylan9eqr 2677 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0))
185184fveq1d 6152 . . . . . . . . . . . . . . 15 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ((ℝ D 𝐹)‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥))
186 eqidd 2622 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 0 = 0)
187 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑢 ∈ (𝐴(,)𝐵) ↦ 0) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0)
188 c0ex 9981 . . . . . . . . . . . . . . . 16 0 ∈ V
189186, 187, 188fvmpt 6241 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥) = 0)
190185, 189sylan9eq 2675 . . . . . . . . . . . . . 14 (((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) = 0)
191190ralrimiva 2960 . . . . . . . . . . . . 13 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
192 ioon0 12146 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵))
193149, 150, 192syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵))
1943, 193mpbird 247 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(,)𝐵) ≠ ∅)
195 r19.2z 4034 . . . . . . . . . . . . . 14 (((𝐴(,)𝐵) ≠ ∅ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
196194, 195sylan 488 . . . . . . . . . . . . 13 ((𝜑 ∧ ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
197191, 196syldan 487 . . . . . . . . . . . 12 ((𝜑𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
198197ex 450 . . . . . . . . . . 11 (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹𝐴)}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
199174, 198sylbird 250 . . . . . . . . . 10 (𝜑 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
200199ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) = (𝐹𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
201163, 200sylbird 250 . . . . . . . 8 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
202201impancom 456 . . . . . . 7 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → (((𝐹𝑢) = (𝐹𝐴) ∧ (𝐹𝑣) = (𝐹𝐴)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
203148, 202syld 47 . . . . . 6 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
20426, 130, 203ecased 984 . . . . 5 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦))) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
205204ex 450 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹𝑦) ≤ (𝐹𝑢) ∧ (𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
2069, 205syl5bir 233 . . 3 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → ((∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
207206rexlimdvva 3031 . 2 (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑦) ≤ (𝐹𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹𝑣) ≤ (𝐹𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0))
2088, 207mpd 15 1 (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  wss 3556  c0 3893  {csn 4150  {cpr 4152   class class class wbr 4615  cmpt 4675   × cxp 5074  dom cdm 5076  ran crn 5077   Fn wfn 5844  wf 5845  cfv 5849  (class class class)co 6607  cc 9881  cr 9882  0cc0 9883  *cxr 10020   < clt 10021  cle 10022  -cneg 10214  (,)cioo 12120  [,]cicc 12123  TopOpenctopn 16006  topGenctg 16022  fldccnfld 19668  intcnt 20734  cnccncf 22592   D cdv 23540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961  ax-addf 9962  ax-mulf 9963
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-of 6853  df-om 7016  df-1st 7116  df-2nd 7117  df-supp 7244  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-er 7690  df-map 7807  df-pm 7808  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fsupp 8223  df-fi 8264  df-sup 8295  df-inf 8296  df-oi 8362  df-card 8712  df-cda 8937  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-z 11325  df-dec 11441  df-uz 11635  df-q 11736  df-rp 11780  df-xneg 11893  df-xadd 11894  df-xmul 11895  df-ioo 12124  df-ico 12126  df-icc 12127  df-fz 12272  df-fzo 12410  df-seq 12745  df-exp 12804  df-hash 13061  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-mulr 15879  df-starv 15880  df-sca 15881  df-vsca 15882  df-ip 15883  df-tset 15884  df-ple 15885  df-ds 15888  df-unif 15889  df-hom 15890  df-cco 15891  df-rest 16007  df-topn 16008  df-0g 16026  df-gsum 16027  df-topgen 16028  df-pt 16029  df-prds 16032  df-xrs 16086  df-qtop 16091  df-imas 16092  df-xps 16094  df-mre 16170  df-mrc 16171  df-acs 16173  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-submnd 17260  df-mulg 17465  df-cntz 17674  df-cmn 18119  df-psmet 19660  df-xmet 19661  df-met 19662  df-bl 19663  df-mopn 19664  df-fbas 19665  df-fg 19666  df-cnfld 19669  df-top 20621  df-topon 20638  df-topsp 20651  df-bases 20664  df-cld 20736  df-ntr 20737  df-cls 20738  df-nei 20815  df-lp 20853  df-perf 20854  df-cn 20944  df-cnp 20945  df-haus 21032  df-cmp 21103  df-tx 21278  df-hmeo 21471  df-fil 21563  df-fm 21655  df-flim 21656  df-flf 21657  df-xms 22038  df-ms 22039  df-tms 22040  df-cncf 22594  df-limc 23543  df-dv 23544
This theorem is referenced by:  cmvth  23665  lhop1lem  23687
  Copyright terms: Public domain W3C validator