| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | rolle.a | . . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 2 |  | rolle.b | . . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 3 |  | rolle.lt | . . . . 5
⊢ (𝜑 → 𝐴 < 𝐵) | 
| 4 | 1, 2, 3 | ltled 11409 | . . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 5 |  | rolle.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 6 | 1, 2, 4, 5 | evthicc 25494 | . . 3
⊢ (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦))) | 
| 7 |  | reeanv 3229 | . . 3
⊢
(∃𝑢 ∈
(𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦)) ↔ (∃𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∃𝑣 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦))) | 
| 8 | 6, 7 | sylibr 234 | . 2
⊢ (𝜑 → ∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦))) | 
| 9 |  | r19.26 3111 | . . . 4
⊢
(∀𝑦 ∈
(𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦))) | 
| 10 | 1 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ) | 
| 11 | 2 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ) | 
| 12 | 3 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵) | 
| 13 | 5 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 14 |  | rolle.d | . . . . . . . . 9
⊢ (𝜑 → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) | 
| 15 | 14 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → dom (ℝ D 𝐹) = (𝐴(,)𝐵)) | 
| 16 |  | simpl 482 | . . . . . . . . . . 11
⊢ (((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → (𝐹‘𝑦) ≤ (𝐹‘𝑢)) | 
| 17 | 16 | ralimi 3083 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
(𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢)) | 
| 18 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡)) | 
| 19 | 18 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑡 → ((𝐹‘𝑦) ≤ (𝐹‘𝑢) ↔ (𝐹‘𝑡) ≤ (𝐹‘𝑢))) | 
| 20 | 19 | cbvralvw 3237 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
(𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹‘𝑡) ≤ (𝐹‘𝑢)) | 
| 21 | 17, 20 | sylib 218 | . . . . . . . . 9
⊢
(∀𝑦 ∈
(𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹‘𝑡) ≤ (𝐹‘𝑢)) | 
| 22 | 21 | ad2antrl 728 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)(𝐹‘𝑡) ≤ (𝐹‘𝑢)) | 
| 23 |  | simplrl 777 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → 𝑢 ∈ (𝐴[,]𝐵)) | 
| 24 |  | simprr 773 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ¬ 𝑢 ∈ {𝐴, 𝐵}) | 
| 25 | 10, 11, 12, 13, 15, 22, 23, 24 | rollelem 26027 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑢 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | 
| 26 | 25 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → (¬ 𝑢 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 27 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 ∈ ℝ) | 
| 28 | 2 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐵 ∈ ℝ) | 
| 29 | 3 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝐴 < 𝐵) | 
| 30 |  | cncff 24919 | . . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℝ) → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 31 | 5, 30 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 32 | 31 | ffvelcdmda 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑢) ∈ ℝ) | 
| 33 | 32 | renegcld 11690 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹‘𝑢) ∈ ℝ) | 
| 34 | 33 | fmpttd 7135 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)):(𝐴[,]𝐵)⟶ℝ) | 
| 35 |  | ax-resscn 11212 | . . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ | 
| 36 |  | ssid 4006 | . . . . . . . . . . . . . . 15
⊢ ℂ
⊆ ℂ | 
| 37 |  | cncfss 24925 | . . . . . . . . . . . . . . 15
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ)) | 
| 38 | 35, 36, 37 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ ((𝐴[,]𝐵)–cn→ℝ) ⊆ ((𝐴[,]𝐵)–cn→ℂ) | 
| 39 | 38, 5 | sselid 3981 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) = (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) | 
| 41 | 40 | negfcncf 24950 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) | 
| 42 | 39, 41 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) | 
| 43 |  | cncfcdm 24924 | . . . . . . . . . . . 12
⊢ ((ℝ
⊆ ℂ ∧ (𝑢
∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)):(𝐴[,]𝐵)⟶ℝ)) | 
| 44 | 35, 42, 43 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ) ↔ (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)):(𝐴[,]𝐵)⟶ℝ)) | 
| 45 | 34, 44 | mpbird 257 | . . . . . . . . . 10
⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 46 | 45 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)) ∈ ((𝐴[,]𝐵)–cn→ℝ)) | 
| 47 | 35 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 48 |  | iccssre 13469 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 49 | 1, 2, 48 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | 
| 50 |  | fss 6752 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(𝐴[,]𝐵)⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 51 | 31, 35, 50 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) | 
| 52 | 51 | ffvelcdmda 7104 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑢) ∈ ℂ) | 
| 53 | 52 | negcld 11607 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → -(𝐹‘𝑢) ∈ ℂ) | 
| 54 |  | tgioo4 24826 | . . . . . . . . . . . . . 14
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 55 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 56 |  | iccntr 24843 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 57 | 1, 2, 56 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 58 | 47, 49, 53, 54, 55, 57 | dvmptntr 26009 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑢)))) | 
| 59 |  | reelprrecn 11247 | . . . . . . . . . . . . . . 15
⊢ ℝ
∈ {ℝ, ℂ} | 
| 60 | 59 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) | 
| 61 |  | ioossicc 13473 | . . . . . . . . . . . . . . . 16
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) | 
| 62 | 61 | sseli 3979 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ (𝐴(,)𝐵) → 𝑢 ∈ (𝐴[,]𝐵)) | 
| 63 | 62, 52 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑢) ∈ ℂ) | 
| 64 |  | fvexd 6921 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑢) ∈ V) | 
| 65 | 31 | feqmptd 6977 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑢))) | 
| 66 | 65 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑢)))) | 
| 67 |  | dvf 25942 | . . . . . . . . . . . . . . . . 17
⊢ (ℝ
D 𝐹):dom (ℝ D 𝐹)⟶ℂ | 
| 68 | 14 | feq2d 6722 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ ↔ (ℝ
D 𝐹):(𝐴(,)𝐵)⟶ℂ)) | 
| 69 | 67, 68 | mpbii 233 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) | 
| 70 | 69 | feqmptd 6977 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢))) | 
| 71 | 47, 49, 52, 54, 55, 57 | dvmptntr 26009 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑢))) = (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑢)))) | 
| 72 | 66, 70, 71 | 3eqtr3rd 2786 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑢))) | 
| 73 | 60, 63, 64, 72 | dvmptneg 26004 | . . . . . . . . . . . . 13
⊢ (𝜑 → (ℝ D (𝑢 ∈ (𝐴(,)𝐵) ↦ -(𝐹‘𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))) | 
| 74 | 58, 73 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))) | 
| 75 | 74 | dmeqd 5916 | . . . . . . . . . . 11
⊢ (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))) = dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))) | 
| 76 |  | dmmptg 6262 | . . . . . . . . . . . 12
⊢
(∀𝑢 ∈
(𝐴(,)𝐵)-((ℝ D 𝐹)‘𝑢) ∈ V → dom (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵)) | 
| 77 |  | negex 11506 | . . . . . . . . . . . . 13
⊢
-((ℝ D 𝐹)‘𝑢) ∈ V | 
| 78 | 77 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ (𝐴(,)𝐵) → -((ℝ D 𝐹)‘𝑢) ∈ V) | 
| 79 | 76, 78 | mprg 3067 | . . . . . . . . . . 11
⊢ dom
(𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝐴(,)𝐵) | 
| 80 | 75, 79 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝜑 → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))) = (𝐴(,)𝐵)) | 
| 81 | 80 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → dom (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))) = (𝐴(,)𝐵)) | 
| 82 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → (𝐹‘𝑣) ≤ (𝐹‘𝑦)) | 
| 83 | 31 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 84 |  | simplrr 778 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → 𝑣 ∈ (𝐴[,]𝐵)) | 
| 85 | 83, 84 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑣) ∈ ℝ) | 
| 86 | 31 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → 𝐹:(𝐴[,]𝐵)⟶ℝ) | 
| 87 | 86 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑦) ∈ ℝ) | 
| 88 | 85, 87 | lenegd 11842 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹‘𝑣) ≤ (𝐹‘𝑦) ↔ -(𝐹‘𝑦) ≤ -(𝐹‘𝑣))) | 
| 89 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑦 → (𝐹‘𝑢) = (𝐹‘𝑦)) | 
| 90 | 89 | negeqd 11502 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑦 → -(𝐹‘𝑢) = -(𝐹‘𝑦)) | 
| 91 |  | negex 11506 | . . . . . . . . . . . . . . . . . 18
⊢ -(𝐹‘𝑦) ∈ V | 
| 92 | 90, 40, 91 | fvmpt 7016 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) = -(𝐹‘𝑦)) | 
| 93 | 92 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) = -(𝐹‘𝑦)) | 
| 94 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑣 → (𝐹‘𝑢) = (𝐹‘𝑣)) | 
| 95 | 94 | negeqd 11502 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑣 → -(𝐹‘𝑢) = -(𝐹‘𝑣)) | 
| 96 |  | negex 11506 | . . . . . . . . . . . . . . . . . 18
⊢ -(𝐹‘𝑣) ∈ V | 
| 97 | 95, 40, 96 | fvmpt 7016 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ (𝐴[,]𝐵) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣) = -(𝐹‘𝑣)) | 
| 98 | 84, 97 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣) = -(𝐹‘𝑣)) | 
| 99 | 93, 98 | breq12d 5156 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣) ↔ -(𝐹‘𝑦) ≤ -(𝐹‘𝑣))) | 
| 100 | 88, 99 | bitr4d 282 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹‘𝑣) ≤ (𝐹‘𝑦) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣))) | 
| 101 | 82, 100 | imbitrid 244 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣))) | 
| 102 | 101 | ralimdva 3167 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣))) | 
| 103 | 102 | imp 406 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → ∀𝑦 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣)) | 
| 104 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑡 → ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) = ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑡)) | 
| 105 | 104 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑡 → (((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣) ↔ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣))) | 
| 106 | 105 | cbvralvw 3237 | . . . . . . . . . . 11
⊢
(∀𝑦 ∈
(𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑦) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣) ↔ ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣)) | 
| 107 | 103, 106 | sylib 218 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣)) | 
| 108 | 107 | adantrr 717 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∀𝑡 ∈ (𝐴[,]𝐵)((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑡) ≤ ((𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢))‘𝑣)) | 
| 109 |  | simplrr 778 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → 𝑣 ∈ (𝐴[,]𝐵)) | 
| 110 |  | simprr 773 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ¬ 𝑣 ∈ {𝐴, 𝐵}) | 
| 111 | 27, 28, 29, 46, 81, 108, 109, 110 | rollelem 26027 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = 0) | 
| 112 | 74 | fveq1d 6908 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥)) | 
| 113 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → ((ℝ D 𝐹)‘𝑢) = ((ℝ D 𝐹)‘𝑥)) | 
| 114 | 113 | negeqd 11502 | . . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑥 → -((ℝ D 𝐹)‘𝑢) = -((ℝ D 𝐹)‘𝑥)) | 
| 115 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) = (𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢)) | 
| 116 |  | negex 11506 | . . . . . . . . . . . . . 14
⊢
-((ℝ D 𝐹)‘𝑥) ∈ V | 
| 117 | 114, 115,
116 | fvmpt 7016 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ -((ℝ D 𝐹)‘𝑢))‘𝑥) = -((ℝ D 𝐹)‘𝑥)) | 
| 118 | 112, 117 | sylan9eq 2797 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = -((ℝ D 𝐹)‘𝑥)) | 
| 119 | 118 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0)) | 
| 120 | 14 | eleq2d 2827 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ dom (ℝ D 𝐹) ↔ 𝑥 ∈ (𝐴(,)𝐵))) | 
| 121 | 120 | biimpar 477 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ dom (ℝ D 𝐹)) | 
| 122 | 67 | ffvelcdmi 7103 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) | 
| 123 | 121, 122 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) | 
| 124 | 123 | negeq0d 11612 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) = 0 ↔ -((ℝ D 𝐹)‘𝑥) = 0)) | 
| 125 | 119, 124 | bitr4d 282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = 0 ↔ ((ℝ D 𝐹)‘𝑥) = 0)) | 
| 126 | 125 | rexbidva 3177 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 127 | 126 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → (∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ -(𝐹‘𝑢)))‘𝑥) = 0 ↔ ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 128 | 111, 127 | mpbid 232 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ∧ ¬ 𝑣 ∈ {𝐴, 𝐵})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | 
| 129 | 128 | expr 456 | . . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → (¬ 𝑣 ∈ {𝐴, 𝐵} → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 130 |  | vex 3484 | . . . . . . . . . . 11
⊢ 𝑢 ∈ V | 
| 131 | 130 | elpr 4650 | . . . . . . . . . 10
⊢ (𝑢 ∈ {𝐴, 𝐵} ↔ (𝑢 = 𝐴 ∨ 𝑢 = 𝐵)) | 
| 132 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝐴 → (𝐹‘𝑢) = (𝐹‘𝐴)) | 
| 133 | 132 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑢 = 𝐴 → (𝐹‘𝑢) = (𝐹‘𝐴))) | 
| 134 |  | rolle.e | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵)) | 
| 135 | 134 | eqcomd 2743 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘𝐵) = (𝐹‘𝐴)) | 
| 136 |  | fveqeq2 6915 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝐵 → ((𝐹‘𝑢) = (𝐹‘𝐴) ↔ (𝐹‘𝐵) = (𝐹‘𝐴))) | 
| 137 | 135, 136 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑢 = 𝐵 → (𝐹‘𝑢) = (𝐹‘𝐴))) | 
| 138 | 133, 137 | jaod 860 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑢 = 𝐴 ∨ 𝑢 = 𝐵) → (𝐹‘𝑢) = (𝐹‘𝐴))) | 
| 139 | 131, 138 | biimtrid 242 | . . . . . . . . 9
⊢ (𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹‘𝑢) = (𝐹‘𝐴))) | 
| 140 |  | eleq1w 2824 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → (𝑢 ∈ {𝐴, 𝐵} ↔ 𝑣 ∈ {𝐴, 𝐵})) | 
| 141 |  | fveqeq2 6915 | . . . . . . . . . . . 12
⊢ (𝑢 = 𝑣 → ((𝐹‘𝑢) = (𝐹‘𝐴) ↔ (𝐹‘𝑣) = (𝐹‘𝐴))) | 
| 142 | 140, 141 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑢 = 𝑣 → ((𝑢 ∈ {𝐴, 𝐵} → (𝐹‘𝑢) = (𝐹‘𝐴)) ↔ (𝑣 ∈ {𝐴, 𝐵} → (𝐹‘𝑣) = (𝐹‘𝐴)))) | 
| 143 | 142 | imbi2d 340 | . . . . . . . . . 10
⊢ (𝑢 = 𝑣 → ((𝜑 → (𝑢 ∈ {𝐴, 𝐵} → (𝐹‘𝑢) = (𝐹‘𝐴))) ↔ (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹‘𝑣) = (𝐹‘𝐴))))) | 
| 144 | 143, 139 | chvarvv 1998 | . . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ {𝐴, 𝐵} → (𝐹‘𝑣) = (𝐹‘𝐴))) | 
| 145 | 139, 144 | anim12d 609 | . . . . . . . 8
⊢ (𝜑 → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴)))) | 
| 146 | 145 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴)))) | 
| 147 | 1 | rexrd 11311 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 148 | 2 | rexrd 11311 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 149 |  | lbicc2 13504 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 150 | 147, 148,
4, 149 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 151 | 31, 150 | ffvelcdmd 7105 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) | 
| 152 | 151 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘𝐴) ∈ ℝ) | 
| 153 | 87, 152 | letri3d 11403 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹‘𝑦) = (𝐹‘𝐴) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝐴) ∧ (𝐹‘𝐴) ≤ (𝐹‘𝑦)))) | 
| 154 |  | breq2 5147 | . . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑢) = (𝐹‘𝐴) → ((𝐹‘𝑦) ≤ (𝐹‘𝑢) ↔ (𝐹‘𝑦) ≤ (𝐹‘𝐴))) | 
| 155 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑣) = (𝐹‘𝐴) → ((𝐹‘𝑣) ≤ (𝐹‘𝑦) ↔ (𝐹‘𝐴) ≤ (𝐹‘𝑦))) | 
| 156 | 154, 155 | bi2anan9 638 | . . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴)) → (((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝐴) ∧ (𝐹‘𝐴) ≤ (𝐹‘𝑦)))) | 
| 157 | 156 | bibi2d 342 | . . . . . . . . . . . . 13
⊢ (((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴)) → (((𝐹‘𝑦) = (𝐹‘𝐴) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) ↔ ((𝐹‘𝑦) = (𝐹‘𝐴) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝐴) ∧ (𝐹‘𝐴) ≤ (𝐹‘𝑦))))) | 
| 158 | 153, 157 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴)) → ((𝐹‘𝑦) = (𝐹‘𝐴) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))))) | 
| 159 | 158 | impancom 451 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴))) → (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹‘𝑦) = (𝐹‘𝐴) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))))) | 
| 160 | 159 | imp 406 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴))) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((𝐹‘𝑦) = (𝐹‘𝐴) ↔ ((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)))) | 
| 161 | 160 | ralbidva 3176 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (𝐹‘𝐴) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)))) | 
| 162 | 31 | ffnd 6737 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn (𝐴[,]𝐵)) | 
| 163 |  | fnconstg 6796 | . . . . . . . . . . . . . 14
⊢ ((𝐹‘𝐴) ∈ ℝ → ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) Fn (𝐴[,]𝐵)) | 
| 164 | 151, 163 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) Fn (𝐴[,]𝐵)) | 
| 165 |  | eqfnfv 7051 | . . . . . . . . . . . . 13
⊢ ((𝐹 Fn (𝐴[,]𝐵) ∧ ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) Fn (𝐴[,]𝐵)) → (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (((𝐴[,]𝐵) × {(𝐹‘𝐴)})‘𝑦))) | 
| 166 | 162, 164,
165 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (((𝐴[,]𝐵) × {(𝐹‘𝐴)})‘𝑦))) | 
| 167 |  | fvex 6919 | . . . . . . . . . . . . . . 15
⊢ (𝐹‘𝐴) ∈ V | 
| 168 | 167 | fvconst2 7224 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {(𝐹‘𝐴)})‘𝑦) = (𝐹‘𝐴)) | 
| 169 | 168 | eqeq2d 2748 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝐴[,]𝐵) → ((𝐹‘𝑦) = (((𝐴[,]𝐵) × {(𝐹‘𝐴)})‘𝑦) ↔ (𝐹‘𝑦) = (𝐹‘𝐴))) | 
| 170 | 169 | ralbiia 3091 | . . . . . . . . . . . 12
⊢
(∀𝑦 ∈
(𝐴[,]𝐵)(𝐹‘𝑦) = (((𝐴[,]𝐵) × {(𝐹‘𝐴)})‘𝑦) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (𝐹‘𝐴)) | 
| 171 | 166, 170 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (𝐹‘𝐴))) | 
| 172 |  | ioon0 13413 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵)) | 
| 173 | 147, 148,
172 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴(,)𝐵) ≠ ∅ ↔ 𝐴 < 𝐵)) | 
| 174 | 3, 173 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(,)𝐵) ≠ ∅) | 
| 175 |  | fconstmpt 5747 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝐴)) | 
| 176 | 175 | eqeq2i 2750 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) ↔ 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝐴))) | 
| 177 | 176 | biimpi 216 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) → 𝐹 = (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝐴))) | 
| 178 | 177 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) → (ℝ D 𝐹) = (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝐴)))) | 
| 179 | 151 | recnd 11289 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) | 
| 180 | 179 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ ℝ) → (𝐹‘𝐴) ∈ ℂ) | 
| 181 |  | 0cnd 11254 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ ℝ) → 0 ∈
ℂ) | 
| 182 | 60, 179 | dvmptc 25996 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℝ D (𝑢 ∈ ℝ ↦ (𝐹‘𝐴))) = (𝑢 ∈ ℝ ↦ 0)) | 
| 183 | 60, 180, 181, 182, 49, 54, 55, 57 | dvmptres2 26000 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℝ D (𝑢 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝐴))) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0)) | 
| 184 | 178, 183 | sylan9eqr 2799 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)})) → (ℝ D 𝐹) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0)) | 
| 185 | 184 | fveq1d 6908 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)})) → ((ℝ D 𝐹)‘𝑥) = ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥)) | 
| 186 |  | eqidd 2738 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → 0 = 0) | 
| 187 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ (𝐴(,)𝐵) ↦ 0) = (𝑢 ∈ (𝐴(,)𝐵) ↦ 0) | 
| 188 |  | c0ex 11255 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
V | 
| 189 | 186, 187,
188 | fvmpt 7016 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴(,)𝐵) → ((𝑢 ∈ (𝐴(,)𝐵) ↦ 0)‘𝑥) = 0) | 
| 190 | 185, 189 | sylan9eq 2797 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)})) ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) = 0) | 
| 191 | 190 | ralrimiva 3146 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)})) → ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | 
| 192 |  | r19.2z 4495 | . . . . . . . . . . . . 13
⊢ (((𝐴(,)𝐵) ≠ ∅ ∧ ∀𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | 
| 193 | 174, 191,
192 | syl2an2r 685 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)})) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | 
| 194 | 193 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹 = ((𝐴[,]𝐵) × {(𝐹‘𝐴)}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 195 | 171, 194 | sylbird 260 | . . . . . . . . . 10
⊢ (𝜑 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (𝐹‘𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 196 | 195 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) = (𝐹‘𝐴) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 197 | 161, 196 | sylbird 260 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 198 | 197 | impancom 451 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → (((𝐹‘𝑢) = (𝐹‘𝐴) ∧ (𝐹‘𝑣) = (𝐹‘𝐴)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 199 | 146, 198 | syld 47 | . . . . . 6
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → ((𝑢 ∈ {𝐴, 𝐵} ∧ 𝑣 ∈ {𝐴, 𝐵}) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 200 | 26, 129, 199 | ecased 1036 | . . . . 5
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦))) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) | 
| 201 | 200 | ex 412 | . . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → (∀𝑦 ∈ (𝐴[,]𝐵)((𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ (𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 202 | 9, 201 | biimtrrid 243 | . . 3
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑣 ∈ (𝐴[,]𝐵))) → ((∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 203 | 202 | rexlimdvva 3213 | . 2
⊢ (𝜑 → (∃𝑢 ∈ (𝐴[,]𝐵)∃𝑣 ∈ (𝐴[,]𝐵)(∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑦) ≤ (𝐹‘𝑢) ∧ ∀𝑦 ∈ (𝐴[,]𝐵)(𝐹‘𝑣) ≤ (𝐹‘𝑦)) → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0)) | 
| 204 | 8, 203 | mpd 15 | 1
⊢ (𝜑 → ∃𝑥 ∈ (𝐴(,)𝐵)((ℝ D 𝐹)‘𝑥) = 0) |