Metamath Proof Explorer

Theorem rolle

Description: Rolle's theorem. If F is a real continuous function on [ A , B ] which is differentiable on ( A , B ) , and F ( A ) = F ( B ) , then there is some x e. ( A , B ) such that ( RR _D F )x = 0 . (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses rolle.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
rolle.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
rolle.lt ⊢ ( 𝜑 → 𝐴 < 𝐵 )
rolle.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
rolle.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
rolle.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
Assertion rolle ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )

Proof

Step Hyp Ref Expression
1 rolle.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 rolle.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 rolle.lt ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 rolle.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
5 rolle.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
6 rolle.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
7 1 2 3 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
8 1 2 7 4 evthicc ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∃ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
9 reeanv ⊢ ( ∃ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ∃ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∃ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
10 8 9 sylibr ⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
11 r19.26 ⊢ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
12 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → 𝐴 ∈ ℝ )
13 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → 𝐵 ∈ ℝ )
14 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → 𝐴 < 𝐵 )
15 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
16 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
17 simpl ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) )
18 17 ralimi ⊢ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) )
19 fveq2 ⊢ ( 𝑦 = 𝑡 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑡 ) )
20 19 breq1d ⊢ ( 𝑦 = 𝑡 → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑢 ) ) )
21 20 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ↔ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑢 ) )
22 18 21 sylib ⊢ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑢 ) )
23 22 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑡 ) ≤ ( 𝐹 ‘ 𝑢 ) )
24 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → 𝑢 ∈ ( 𝐴 [,] 𝐵 ) )
25 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → ¬ 𝑢 ∈ { 𝐴 , 𝐵 } )
26 12 13 14 15 16 23 24 25 rollelem ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑢 ∈ { 𝐴 , 𝐵 } ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
27 26 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( ¬ 𝑢 ∈ { 𝐴 , 𝐵 } → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
28 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → 𝐴 ∈ ℝ )
29 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → 𝐵 ∈ ℝ )
30 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → 𝐴 < 𝐵 )
31 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
32 4 31 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
33 32 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ℝ )
34 33 renegcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → - ( 𝐹 ‘ 𝑢 ) ∈ ℝ )
35 34 fmpttd ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
36 ax-resscn ⊢ ℝ ⊆ ℂ
37 ssid ⊢ ℂ ⊆ ℂ
38 cncfss ⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
39 36 37 38 mp2an ⊢ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ )
40 39 4 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
41 eqid ⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) = ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) )
42 41 negfcncf ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
43 40 42 syl ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
44 cncfcdm ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ↔ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ) )
45 36 43 44 sylancr ⊢ ( 𝜑 → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) ↔ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ) )
46 35 45 mpbird ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
48 36 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
49 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
50 1 2 49 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
51 fss ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
52 32 36 51 sylancl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
53 52 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
54 53 negcld ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ) → - ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
55 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
56 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
57 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
58 1 2 57 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
59 48 50 54 55 56 58 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) = ( ℝ D ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) )
60 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
61 60 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
62 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
63 62 sseli ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) → 𝑢 ∈ ( 𝐴 [,] 𝐵 ) )
64 63 53 sylan2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
65 fvexd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ∈ V )
66 32 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑢 ) ) )
67 66 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑢 ) ) ) )
68 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
69 5 feq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ↔ ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ ) )
70 68 69 mpbii ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
71 70 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) )
72 48 50 53 55 56 58 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑢 ) ) ) = ( ℝ D ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑢 ) ) ) )
73 67 71 72 3eqtr3rd ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑢 ) ) ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) )
74 61 64 65 73 dvmptneg ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) )
75 59 74 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) )
76 75 dmeqd ⊢ ( 𝜑 → dom ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) = dom ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) )
77 dmmptg ⊢ ( ∀ 𝑢 ∈ ( 𝐴 (,) 𝐵 ) - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ∈ V → dom ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) = ( 𝐴 (,) 𝐵 ) )
78 negex ⊢ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ∈ V
79 78 a1i ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) → - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ∈ V )
80 77 79 mprg ⊢ dom ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) = ( 𝐴 (,) 𝐵 )
81 76 80 eqtrdi ⊢ ( 𝜑 → dom ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) = ( 𝐴 (,) 𝐵 ) )
82 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → dom ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) = ( 𝐴 (,) 𝐵 ) )
83 simpr ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) )
84 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
85 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑣 ∈ ( 𝐴 [,] 𝐵 ) )
86 84 85 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑣 ) ∈ ℝ )
87 32 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
88 87 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
89 86 88 lenegd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑣 ) ) )
90 fveq2 ⊢ ( 𝑢 = 𝑦 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑦 ) )
91 90 negeqd ⊢ ( 𝑢 = 𝑦 → - ( 𝐹 ‘ 𝑢 ) = - ( 𝐹 ‘ 𝑦 ) )
92 negex ⊢ - ( 𝐹 ‘ 𝑦 ) ∈ V
93 91 41 92 fvmpt ⊢ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑦 ) )
94 93 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑦 ) )
95 fveq2 ⊢ ( 𝑢 = 𝑣 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑣 ) )
96 95 negeqd ⊢ ( 𝑢 = 𝑣 → - ( 𝐹 ‘ 𝑢 ) = - ( 𝐹 ‘ 𝑣 ) )
97 negex ⊢ - ( 𝐹 ‘ 𝑣 ) ∈ V
98 96 41 97 fvmpt ⊢ ( 𝑣 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 ) )
99 85 98 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) = - ( 𝐹 ‘ 𝑣 ) )
100 94 99 breq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ↔ - ( 𝐹 ‘ 𝑦 ) ≤ - ( 𝐹 ‘ 𝑣 ) ) )
101 89 100 bitr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
102 83 101 imbitrid ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
103 102 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
104 103 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) )
105 fveq2 ⊢ ( 𝑦 = 𝑡 → ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) = ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑡 ) )
106 105 breq1d ⊢ ( 𝑦 = 𝑡 → ( ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ↔ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ) )
107 106 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑦 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) ↔ ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) )
108 104 107 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) )
109 108 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → ∀ 𝑡 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ‘ 𝑣 ) )
110 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → 𝑣 ∈ ( 𝐴 [,] 𝐵 ) )
111 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → ¬ 𝑣 ∈ { 𝐴 , 𝐵 } )
112 28 29 30 47 82 109 110 111 rollelem ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = 0 )
113 75 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = ( ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) ‘ 𝑥 ) )
114 fveq2 ⊢ ( 𝑢 = 𝑥 → ( ( ℝ D 𝐹 ) ‘ 𝑢 ) = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
115 114 negeqd ⊢ ( 𝑢 = 𝑥 → - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
116 eqid ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) )
117 negex ⊢ - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ V
118 115 116 117 fvmpt ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ - ( ( ℝ D 𝐹 ) ‘ 𝑢 ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
119 113 118 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) )
120 119 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = 0 ↔ - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
121 5 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom ( ℝ D 𝐹 ) ↔ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) )
122 121 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ dom ( ℝ D 𝐹 ) )
123 68 ffvelcdmi ⊢ ( 𝑥 ∈ dom ( ℝ D 𝐹 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
124 122 123 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
125 124 negeq0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ↔ - ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
126 120 125 bitr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = 0 ↔ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
127 126 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = 0 ↔ ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
128 127 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → ( ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ - ( 𝐹 ‘ 𝑢 ) ) ) ‘ 𝑥 ) = 0 ↔ ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
129 112 128 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ∧ ¬ 𝑣 ∈ { 𝐴 , 𝐵 } ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
130 129 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( ¬ 𝑣 ∈ { 𝐴 , 𝐵 } → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
131 vex ⊢ 𝑢 ∈ V
132 131 elpr ⊢ ( 𝑢 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑢 = 𝐴 ∨ 𝑢 = 𝐵 ) )
133 fveq2 ⊢ ( 𝑢 = 𝐴 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) )
134 133 a1i ⊢ ( 𝜑 → ( 𝑢 = 𝐴 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ) )
135 6 eqcomd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) )
136 fveqeq2 ⊢ ( 𝑢 = 𝐵 → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ) )
137 135 136 syl5ibrcom ⊢ ( 𝜑 → ( 𝑢 = 𝐵 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ) )
138 134 137 jaod ⊢ ( 𝜑 → ( ( 𝑢 = 𝐴 ∨ 𝑢 = 𝐵 ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ) )
139 132 138 biimtrid ⊢ ( 𝜑 → ( 𝑢 ∈ { 𝐴 , 𝐵 } → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ) )
140 eleq1w ⊢ ( 𝑢 = 𝑣 → ( 𝑢 ∈ { 𝐴 , 𝐵 } ↔ 𝑣 ∈ { 𝐴 , 𝐵 } ) )
141 fveqeq2 ⊢ ( 𝑢 = 𝑣 → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) )
142 140 141 imbi12d ⊢ ( 𝑢 = 𝑣 → ( ( 𝑢 ∈ { 𝐴 , 𝐵 } → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ) ↔ ( 𝑣 ∈ { 𝐴 , 𝐵 } → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) )
143 142 imbi2d ⊢ ( 𝑢 = 𝑣 → ( ( 𝜑 → ( 𝑢 ∈ { 𝐴 , 𝐵 } → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ) ) ↔ ( 𝜑 → ( 𝑣 ∈ { 𝐴 , 𝐵 } → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) ) )
144 143 139 chvarvv ⊢ ( 𝜑 → ( 𝑣 ∈ { 𝐴 , 𝐵 } → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) )
145 139 144 anim12d ⊢ ( 𝜑 → ( ( 𝑢 ∈ { 𝐴 , 𝐵 } ∧ 𝑣 ∈ { 𝐴 , 𝐵 } ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) )
146 145 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑢 ∈ { 𝐴 , 𝐵 } ∧ 𝑣 ∈ { 𝐴 , 𝐵 } ) → ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) )
147 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
148 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
149 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
150 147 148 7 149 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
151 32 150 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
152 151 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
153 88 152 letri3d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
154 breq2 ⊢ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝐴 ) ) )
155 breq1 ⊢ ( ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
156 154 155 bi2anan9 ⊢ ( ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
157 156 bibi2d ⊢ ( ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ) )
158 153 157 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ) )
159 158 impancom ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) ) )
160 159 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
161 160 ralbidva ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
162 32 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 [,] 𝐵 ) )
163 fnconstg ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ → ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) Fn ( 𝐴 [,] 𝐵 ) )
164 151 163 syl ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) Fn ( 𝐴 [,] 𝐵 ) )
165 eqfnfv ⊢ ( ( 𝐹 Fn ( 𝐴 [,] 𝐵 ) ∧ ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) Fn ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑦 ) ) )
166 162 164 165 syl2anc ⊢ ( 𝜑 → ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑦 ) ) )
167 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
168 167 fvconst2 ⊢ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
169 168 eqeq2d ⊢ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝐹 ‘ 𝑦 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ) )
170 169 ralbiia ⊢ ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
171 166 170 bitrdi ⊢ ( 𝜑 → ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) ) )
172 ioon0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ 𝐴 < 𝐵 ) )
173 147 148 172 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ↔ 𝐴 < 𝐵 ) )
174 3 173 mpbird ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
175 fconstmpt ⊢ ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) = ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝐴 ) )
176 175 eqeq2i ⊢ ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ↔ 𝐹 = ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝐴 ) ) )
177 176 biimpi ⊢ ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) → 𝐹 = ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝐴 ) ) )
178 177 oveq2d ⊢ ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝐴 ) ) ) )
179 151 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
181 0cnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℝ ) → 0 ∈ ℂ )
182 61 179 dvmptc ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ℝ ↦ ( 𝐹 ‘ 𝐴 ) ) ) = ( 𝑢 ∈ ℝ ↦ 0 ) )
183 61 180 181 182 50 55 56 58 dvmptres2 ⊢ ( 𝜑 → ( ℝ D ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝐴 ) ) ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
184 178 183 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ) → ( ℝ D 𝐹 ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
185 184 fveq1d ⊢ ( ( 𝜑 ∧ 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = ( ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) ‘ 𝑥 ) )
186 eqidd ⊢ ( 𝑢 = 𝑥 → 0 = 0 )
187 eqid ⊢ ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) = ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 )
188 c0ex ⊢ 0 ∈ V
189 186 187 188 fvmpt ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → ( ( 𝑢 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) ‘ 𝑥 ) = 0 )
190 185 189 sylan9eq ⊢ ( ( ( 𝜑 ∧ 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
191 190 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ) → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
192 r19.2z ⊢ ( ( ( 𝐴 (,) 𝐵 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
193 174 191 192 syl2an2r ⊢ ( ( 𝜑 ∧ 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
194 193 ex ⊢ ( 𝜑 → ( 𝐹 = ( ( 𝐴 [,] 𝐵 ) × { ( 𝐹 ‘ 𝐴 ) } ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
195 171 194 sylbird ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
196 195 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
197 161 196 sylbird ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
198 197 impancom ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( ( ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
199 146 198 syld ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑢 ∈ { 𝐴 , 𝐵 } ∧ 𝑣 ∈ { 𝐴 , 𝐵 } ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
200 27 130 199 ecased ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )
201 200 ex ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
202 11 201 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
203 202 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑣 ∈ ( 𝐴 [,] 𝐵 ) ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑣 ) ≤ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 ) )
204 10 203 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑥 ) = 0 )