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

Theorem dvlipcn 25358
Description: A complex function with derivative bounded by 𝑀 on an open ball is 𝑀-Lipschitz continuous. (Contributed by Mario Carneiro, 18-Mar-2015.)
Hypotheses
Ref Expression
dvlipcn.x (𝜑𝑋 ⊆ ℂ)
dvlipcn.f (𝜑𝐹:𝑋⟶ℂ)
dvlipcn.a (𝜑𝐴 ∈ ℂ)
dvlipcn.r (𝜑𝑅 ∈ ℝ*)
dvlipcn.b 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
dvlipcn.d (𝜑𝐵 ⊆ dom (ℂ D 𝐹))
dvlipcn.m (𝜑𝑀 ∈ ℝ)
dvlipcn.l ((𝜑𝑥𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
Assertion
Ref Expression
dvlipcn ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (abs‘((𝐹𝑌) − (𝐹𝑍))) ≤ (𝑀 · (abs‘(𝑌𝑍))))
Distinct variable groups:   𝑥,𝐵   𝑥,𝐹   𝑥,𝑀   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝑅(𝑥)   𝑋(𝑥)   𝑌(𝑥)   𝑍(𝑥)

Proof of Theorem dvlipcn
Dummy variables 𝑡 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1elunit 13387 . . 3 1 ∈ (0[,]1)
2 0elunit 13386 . . 3 0 ∈ (0[,]1)
3 0red 11158 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 0 ∈ ℝ)
4 1red 11156 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 1 ∈ ℝ)
5 dvlipcn.d . . . . . . . . . . . . . 14 (𝜑𝐵 ⊆ dom (ℂ D 𝐹))
6 ssidd 3967 . . . . . . . . . . . . . . 15 (𝜑 → ℂ ⊆ ℂ)
7 dvlipcn.f . . . . . . . . . . . . . . 15 (𝜑𝐹:𝑋⟶ℂ)
8 dvlipcn.x . . . . . . . . . . . . . . 15 (𝜑𝑋 ⊆ ℂ)
96, 7, 8dvbss 25265 . . . . . . . . . . . . . 14 (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑋)
105, 9sstrd 3954 . . . . . . . . . . . . 13 (𝜑𝐵𝑋)
1110, 8sstrd 3954 . . . . . . . . . . . 12 (𝜑𝐵 ⊆ ℂ)
1211adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝐵 ⊆ ℂ)
13 simprl 769 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝑌𝐵)
1412, 13sseldd 3945 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝑌 ∈ ℂ)
1514adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌 ∈ ℂ)
16 unitssre 13416 . . . . . . . . . . 11 (0[,]1) ⊆ ℝ
17 ax-resscn 11108 . . . . . . . . . . 11 ℝ ⊆ ℂ
1816, 17sstri 3953 . . . . . . . . . 10 (0[,]1) ⊆ ℂ
19 simpr 485 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ (0[,]1))
2018, 19sselid 3942 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑡 ∈ ℂ)
2115, 20mulcomd 11176 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑌 · 𝑡) = (𝑡 · 𝑌))
22 simprr 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝑍𝐵)
2312, 22sseldd 3945 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝑍 ∈ ℂ)
2423adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍 ∈ ℂ)
25 iirev 24292 . . . . . . . . . . 11 (𝑡 ∈ (0[,]1) → (1 − 𝑡) ∈ (0[,]1))
2625adantl 482 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ (0[,]1))
2718, 26sselid 3942 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (1 − 𝑡) ∈ ℂ)
2824, 27mulcomd 11176 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝑍 · (1 − 𝑡)) = ((1 − 𝑡) · 𝑍))
2921, 28oveq12d 7375 . . . . . . 7 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)))
30 dvlipcn.a . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3130ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐴 ∈ ℂ)
32 dvlipcn.r . . . . . . . . 9 (𝜑𝑅 ∈ ℝ*)
3332ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑅 ∈ ℝ*)
3413adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑌𝐵)
3522adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝑍𝐵)
36 dvlipcn.b . . . . . . . . 9 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)
3736blcvx 24161 . . . . . . . 8 (((𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ*) ∧ (𝑌𝐵𝑍𝐵𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
3831, 33, 34, 35, 19, 37syl23anc 1377 . . . . . . 7 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑌) + ((1 − 𝑡) · 𝑍)) ∈ 𝐵)
3929, 38eqeltrd 2838 . . . . . 6 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
40 eqidd 2737 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
417, 10fssresd 6709 . . . . . . . . 9 (𝜑 → (𝐹𝐵):𝐵⟶ℂ)
4241feqmptd 6910 . . . . . . . 8 (𝜑 → (𝐹𝐵) = (𝑧𝐵 ↦ ((𝐹𝐵)‘𝑧)))
43 fvres 6861 . . . . . . . . 9 (𝑧𝐵 → ((𝐹𝐵)‘𝑧) = (𝐹𝑧))
4443mpteq2ia 5208 . . . . . . . 8 (𝑧𝐵 ↦ ((𝐹𝐵)‘𝑧)) = (𝑧𝐵 ↦ (𝐹𝑧))
4542, 44eqtrdi 2792 . . . . . . 7 (𝜑 → (𝐹𝐵) = (𝑧𝐵 ↦ (𝐹𝑧)))
4645adantr 481 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝐹𝐵) = (𝑧𝐵 ↦ (𝐹𝑧)))
47 fveq2 6842 . . . . . 6 (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (𝐹𝑧) = (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
4839, 40, 46, 47fmptco 7075 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝐹𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
4939fmpttd 7063 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵)
50 eqid 2736 . . . . . . . . 9 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5150addcn 24228 . . . . . . . . . 10 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
5251a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
53 ssid 3966 . . . . . . . . . . . 12 ℂ ⊆ ℂ
54 cncfmptc 24275 . . . . . . . . . . . 12 ((𝑌 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
5518, 53, 54mp3an23 1453 . . . . . . . . . . 11 (𝑌 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
5614, 55syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑌) ∈ ((0[,]1)–cn→ℂ))
57 cncfmptid 24276 . . . . . . . . . . . 12 (((0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
5818, 53, 57mp2an 690 . . . . . . . . . . 11 (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ)
5958a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((0[,]1)–cn→ℂ))
6056, 59mulcncf 24810 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑌 · 𝑡)) ∈ ((0[,]1)–cn→ℂ))
61 cncfmptc 24275 . . . . . . . . . . . 12 ((𝑍 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
6218, 53, 61mp3an23 1453 . . . . . . . . . . 11 (𝑍 ∈ ℂ → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
6323, 62syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ 𝑍) ∈ ((0[,]1)–cn→ℂ))
6450subcn 24229 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
6564a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
66 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
67 cncfmptc 24275 . . . . . . . . . . . . 13 ((1 ∈ ℂ ∧ (0[,]1) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
6866, 18, 53, 67mp3an 1461 . . . . . . . . . . . 12 (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ)
6968a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ 1) ∈ ((0[,]1)–cn→ℂ))
7050, 65, 69, 59cncfmpt2f 24278 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((0[,]1)–cn→ℂ))
7163, 70mulcncf 24810 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝑍 · (1 − 𝑡))) ∈ ((0[,]1)–cn→ℂ))
7250, 52, 60, 71cncfmpt2f 24278 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ))
73 cncfcdm 24261 . . . . . . . 8 ((𝐵 ⊆ ℂ ∧ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn→ℂ)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
7412, 72, 73syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn𝐵) ↔ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))):(0[,]1)⟶𝐵))
7549, 74mpbird 256 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ((0[,]1)–cn𝐵))
76 ssidd 3967 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ℂ ⊆ ℂ)
7741adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝐹𝐵):𝐵⟶ℂ)
7850cnfldtopon 24146 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
7978toponrestid 22270 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
8050, 79dvres 25275 . . . . . . . . . . . 12 (((ℂ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
816, 7, 8, 11, 80syl22anc 837 . . . . . . . . . . 11 (𝜑 → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
8250cnfldtop 24147 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ Top
83 cnxmet 24136 . . . . . . . . . . . . . . 15 (abs ∘ − ) ∈ (∞Met‘ℂ)
8450cnfldtopn 24145 . . . . . . . . . . . . . . . 16 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
8584blopn 23856 . . . . . . . . . . . . . . 15 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂfld))
8683, 30, 32, 85mp3an2i 1466 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂfld))
8736, 86eqeltrid 2842 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (TopOpen‘ℂfld))
88 isopn3i 22433 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ Top ∧ 𝐵 ∈ (TopOpen‘ℂfld)) → ((int‘(TopOpen‘ℂfld))‘𝐵) = 𝐵)
8982, 87, 88sylancr 587 . . . . . . . . . . . 12 (𝜑 → ((int‘(TopOpen‘ℂfld))‘𝐵) = 𝐵)
9089reseq2d 5937 . . . . . . . . . . 11 (𝜑 → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
9181, 90eqtrd 2776 . . . . . . . . . 10 (𝜑 → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
9291dmeqd 5861 . . . . . . . . 9 (𝜑 → dom (ℂ D (𝐹𝐵)) = dom ((ℂ D 𝐹) ↾ 𝐵))
93 dmres 5959 . . . . . . . . . 10 dom ((ℂ D 𝐹) ↾ 𝐵) = (𝐵 ∩ dom (ℂ D 𝐹))
94 df-ss 3927 . . . . . . . . . . 11 (𝐵 ⊆ dom (ℂ D 𝐹) ↔ (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
955, 94sylib 217 . . . . . . . . . 10 (𝜑 → (𝐵 ∩ dom (ℂ D 𝐹)) = 𝐵)
9693, 95eqtrid 2788 . . . . . . . . 9 (𝜑 → dom ((ℂ D 𝐹) ↾ 𝐵) = 𝐵)
9792, 96eqtrd 2776 . . . . . . . 8 (𝜑 → dom (ℂ D (𝐹𝐵)) = 𝐵)
9897adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → dom (ℂ D (𝐹𝐵)) = 𝐵)
99 dvcn 25285 . . . . . . 7 (((ℂ ⊆ ℂ ∧ (𝐹𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℂ) ∧ dom (ℂ D (𝐹𝐵)) = 𝐵) → (𝐹𝐵) ∈ (𝐵cn→ℂ))
10076, 77, 12, 98, 99syl31anc 1373 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝐹𝐵) ∈ (𝐵cn→ℂ))
10175, 100cncfco 24270 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝐹𝐵) ∘ (𝑡 ∈ (0[,]1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
10248, 101eqeltrrd 2839 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ((0[,]1)–cn→ℂ))
10317a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ℝ ⊆ ℂ)
10416a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (0[,]1) ⊆ ℝ)
1057ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐹:𝑋⟶ℂ)
10610ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → 𝐵𝑋)
107106, 39sseldd 3945 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝑋)
108105, 107ffvelcdmd 7036 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0[,]1)) → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
10950tgioo2 24166 . . . . . . . 8 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
110 1re 11155 . . . . . . . . 9 1 ∈ ℝ
111 iccntr 24184 . . . . . . . . 9 ((0 ∈ ℝ ∧ 1 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
1123, 110, 111sylancl 586 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((int‘(topGen‘ran (,)))‘(0[,]1)) = (0(,)1))
113103, 104, 108, 109, 50, 112dvmptntr 25335 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))))
114 reelprrecn 11143 . . . . . . . . 9 ℝ ∈ {ℝ, ℂ}
115114a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ℝ ∈ {ℝ, ℂ})
116 cnelprrecn 11144 . . . . . . . . 9 ℂ ∈ {ℝ, ℂ}
117116a1i 11 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ℂ ∈ {ℝ, ℂ})
118 ioossicc 13350 . . . . . . . . . 10 (0(,)1) ⊆ (0[,]1)
119118sseli 3940 . . . . . . . . 9 (𝑡 ∈ (0(,)1) → 𝑡 ∈ (0[,]1))
120119, 39sylan2 593 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ 𝐵)
12114, 23subcld 11512 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑌𝑍) ∈ ℂ)
122121adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌𝑍) ∈ ℂ)
12310adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝐵𝑋)
124123sselda 3944 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑧𝐵) → 𝑧𝑋)
1257adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝐹:𝑋⟶ℂ)
126125ffvelcdmda 7035 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑧𝑋) → (𝐹𝑧) ∈ ℂ)
127124, 126syldan 591 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑧𝐵) → (𝐹𝑧) ∈ ℂ)
128 fvexd 6857 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑧𝐵) → ((ℂ D 𝐹)‘𝑧) ∈ V)
12914adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑌 ∈ ℂ)
130119, 20sylan2 593 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
131129, 130mulcld 11175 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑌 · 𝑡) ∈ ℂ)
132 1red 11156 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℝ)
133 simpr 485 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℝ)
134133recnd 11183 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ ℝ) → 𝑡 ∈ ℂ)
135 1red 11156 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℝ)
136115dvmptid 25321 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 𝑡)) = (𝑡 ∈ ℝ ↦ 1))
137 ioossre 13325 . . . . . . . . . . . . . 14 (0(,)1) ⊆ ℝ
138137a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (0(,)1) ⊆ ℝ)
139 iooretop 24129 . . . . . . . . . . . . . 14 (0(,)1) ∈ (topGen‘ran (,))
140139a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (0(,)1) ∈ (topGen‘ran (,)))
141115, 134, 135, 136, 138, 109, 50, 140dvmptres 25327 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 𝑡)) = (𝑡 ∈ (0(,)1) ↦ 1))
142115, 130, 132, 141, 14dvmptcmul 25328 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)))
14314mulid1d 11172 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑌 · 1) = 𝑌)
144143mpteq2dv 5207 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 · 1)) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
145142, 144eqtrd 2776 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑌 · 𝑡))) = (𝑡 ∈ (0(,)1) ↦ 𝑌))
14623adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑍 ∈ ℂ)
147119, 27sylan2 593 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
148146, 147mulcld 11175 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (𝑍 · (1 − 𝑡)) ∈ ℂ)
149 negex 11399 . . . . . . . . . . 11 -𝑍 ∈ V
150149a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -𝑍 ∈ V)
151 negex 11399 . . . . . . . . . . . . 13 -1 ∈ V
152151a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → -1 ∈ V)
153 1cnd 11150 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 1 ∈ ℂ)
154 0red 11158 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ∈ ℝ)
155 1cnd 11150 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ ℝ) → 1 ∈ ℂ)
156 0red 11158 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ ℝ) → 0 ∈ ℝ)
157 1cnd 11150 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 1 ∈ ℂ)
158115, 157dvmptc 25322 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ ℝ ↦ 1)) = (𝑡 ∈ ℝ ↦ 0))
159115, 155, 156, 158, 138, 109, 50, 140dvmptres 25327 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ 1)) = (𝑡 ∈ (0(,)1) ↦ 0))
160115, 153, 154, 159, 130, 132, 141dvmptsub 25331 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ (0 − 1)))
161 df-neg 11388 . . . . . . . . . . . . . 14 -1 = (0 − 1)
162161mpteq2i 5210 . . . . . . . . . . . . 13 (𝑡 ∈ (0(,)1) ↦ -1) = (𝑡 ∈ (0(,)1) ↦ (0 − 1))
163160, 162eqtr4di 2794 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (1 − 𝑡))) = (𝑡 ∈ (0(,)1) ↦ -1))
164115, 147, 152, 163, 23dvmptcmul 25328 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)))
165 neg1cn 12267 . . . . . . . . . . . . . 14 -1 ∈ ℂ
166 mulcom 11137 . . . . . . . . . . . . . 14 ((𝑍 ∈ ℂ ∧ -1 ∈ ℂ) → (𝑍 · -1) = (-1 · 𝑍))
16723, 165, 166sylancl 586 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑍 · -1) = (-1 · 𝑍))
16823mulm1d 11607 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (-1 · 𝑍) = -𝑍)
169167, 168eqtrd 2776 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑍 · -1) = -𝑍)
170169mpteq2dv 5207 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑍 · -1)) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
171164, 170eqtrd 2776 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝑍 · (1 − 𝑡)))) = (𝑡 ∈ (0(,)1) ↦ -𝑍))
172115, 131, 129, 145, 148, 150, 171dvmptadd 25324 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)))
17314, 23negsubd 11518 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑌 + -𝑍) = (𝑌𝑍))
174173mpteq2dv 5207 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑡 ∈ (0(,)1) ↦ (𝑌 + -𝑍)) = (𝑡 ∈ (0(,)1) ↦ (𝑌𝑍)))
175172, 174eqtrd 2776 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0(,)1) ↦ (𝑌𝑍)))
1768adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝑋 ⊆ ℂ)
17776, 125, 176, 12, 80syl22anc 837 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
17889adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((int‘(TopOpen‘ℂfld))‘𝐵) = 𝐵)
179178reseq2d 5937 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
180177, 179eqtrd 2776 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ 𝐵))
18146oveq2d 7373 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℂ D (𝐹𝐵)) = (ℂ D (𝑧𝐵 ↦ (𝐹𝑧))))
182 dvfcn 25272 . . . . . . . . . . . . 13 (ℂ D (𝐹𝐵)):dom (ℂ D (𝐹𝐵))⟶ℂ
18398feq2d 6654 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℂ D (𝐹𝐵)):dom (ℂ D (𝐹𝐵))⟶ℂ ↔ (ℂ D (𝐹𝐵)):𝐵⟶ℂ))
184182, 183mpbii 232 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℂ D (𝐹𝐵)):𝐵⟶ℂ)
185180feq1d 6653 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℂ D (𝐹𝐵)):𝐵⟶ℂ ↔ ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ))
186184, 185mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℂ D 𝐹) ↾ 𝐵):𝐵⟶ℂ)
187186feqmptd 6910 . . . . . . . . . 10 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)))
188 fvres 6861 . . . . . . . . . . 11 (𝑧𝐵 → (((ℂ D 𝐹) ↾ 𝐵)‘𝑧) = ((ℂ D 𝐹)‘𝑧))
189188mpteq2ia 5208 . . . . . . . . . 10 (𝑧𝐵 ↦ (((ℂ D 𝐹) ↾ 𝐵)‘𝑧)) = (𝑧𝐵 ↦ ((ℂ D 𝐹)‘𝑧))
190187, 189eqtrdi 2792 . . . . . . . . 9 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℂ D 𝐹) ↾ 𝐵) = (𝑧𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
191180, 181, 1903eqtr3d 2784 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℂ D (𝑧𝐵 ↦ (𝐹𝑧))) = (𝑧𝐵 ↦ ((ℂ D 𝐹)‘𝑧)))
192 fveq2 6842 . . . . . . . 8 (𝑧 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((ℂ D 𝐹)‘𝑧) = ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
193115, 117, 120, 122, 127, 128, 175, 191, 47, 192dvmptco 25336 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0(,)1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))))
194113, 193eqtrd 2776 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))))
195194dmeqd 5861 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))))
196 ovex 7390 . . . . . . 7 (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)) ∈ V
197196rgenw 3068 . . . . . 6 𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)) ∈ V
198 dmmptg 6194 . . . . . 6 (∀𝑡 ∈ (0(,)1)(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)) ∈ V → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))) = (0(,)1))
199197, 198mp1i 13 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → dom (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))) = (0(,)1))
200195, 199eqtrd 2776 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → dom (ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))) = (0(,)1))
201 dvlipcn.m . . . . . 6 (𝜑𝑀 ∈ ℝ)
202201adantr 481 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → 𝑀 ∈ ℝ)
203121abscld 15321 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (abs‘(𝑌𝑍)) ∈ ℝ)
204202, 203remulcld 11185 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑀 · (abs‘(𝑌𝑍))) ∈ ℝ)
205194fveq1d 6844 . . . . . . . . . . 11 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))‘𝑡))
206 eqid 2736 . . . . . . . . . . . . 13 (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))) = (𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))
207206fvmpt2 6959 . . . . . . . . . . . 12 ((𝑡 ∈ (0(,)1) ∧ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)) ∈ V) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))
208196, 207mpan2 689 . . . . . . . . . . 11 (𝑡 ∈ (0(,)1) → ((𝑡 ∈ (0(,)1) ↦ (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))
209205, 208sylan9eq 2796 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡) = (((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍)))
210209fveq2d 6846 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))))
211 dvfcn 25272 . . . . . . . . . . 11 (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
2125ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝐵 ⊆ dom (ℂ D 𝐹))
213212, 120sseldd 3945 . . . . . . . . . . 11 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹))
214 ffvelcdm 7032 . . . . . . . . . . 11 (((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ∧ ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) ∈ dom (ℂ D 𝐹)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
215211, 213, 214sylancr 587 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) ∈ ℂ)
216215, 122absmuld 15339 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) · (𝑌𝑍))) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌𝑍))))
217210, 216eqtrd 2776 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌𝑍))))
218215abscld 15321 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ∈ ℝ)
219201ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 𝑀 ∈ ℝ)
220122abscld 15321 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘(𝑌𝑍)) ∈ ℝ)
221122absge0d 15329 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → 0 ≤ (abs‘(𝑌𝑍)))
222 2fveq3 6847 . . . . . . . . . . 11 (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → (abs‘((ℂ D 𝐹)‘𝑦)) = (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
223222breq1d 5115 . . . . . . . . . 10 (𝑦 = ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) → ((abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀))
224 dvlipcn.l . . . . . . . . . . . . 13 ((𝜑𝑥𝐵) → (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
225224ralrimiva 3143 . . . . . . . . . . . 12 (𝜑 → ∀𝑥𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)
226 2fveq3 6847 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (abs‘((ℂ D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑦)))
227226breq1d 5115 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀))
228227cbvralvw 3225 . . . . . . . . . . . 12 (∀𝑥𝐵 (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀 ↔ ∀𝑦𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
229225, 228sylib 217 . . . . . . . . . . 11 (𝜑 → ∀𝑦𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
230229ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ∀𝑦𝐵 (abs‘((ℂ D 𝐹)‘𝑦)) ≤ 𝑀)
231223, 230, 120rspcdva 3582 . . . . . . . . 9 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) ≤ 𝑀)
232218, 219, 220, 221, 231lemul1ad 12094 . . . . . . . 8 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → ((abs‘((ℂ D 𝐹)‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) · (abs‘(𝑌𝑍))) ≤ (𝑀 · (abs‘(𝑌𝑍))))
233217, 232eqbrtrd 5127 . . . . . . 7 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑡 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌𝑍))))
234233ralrimiva 3143 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌𝑍))))
235 nfv 1917 . . . . . . 7 𝑧(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌𝑍)))
236 nfcv 2907 . . . . . . . . 9 𝑡abs
237 nfcv 2907 . . . . . . . . . . 11 𝑡
238 nfcv 2907 . . . . . . . . . . 11 𝑡 D
239 nfmpt1 5213 . . . . . . . . . . 11 𝑡(𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
240237, 238, 239nfov 7387 . . . . . . . . . 10 𝑡(ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))
241 nfcv 2907 . . . . . . . . . 10 𝑡𝑧
242240, 241nffv 6852 . . . . . . . . 9 𝑡((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)
243236, 242nffv 6852 . . . . . . . 8 𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧))
244 nfcv 2907 . . . . . . . 8 𝑡
245 nfcv 2907 . . . . . . . 8 𝑡(𝑀 · (abs‘(𝑌𝑍)))
246243, 244, 245nfbr 5152 . . . . . . 7 𝑡(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌𝑍)))
247 2fveq3 6847 . . . . . . . 8 (𝑡 = 𝑧 → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) = (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)))
248247breq1d 5115 . . . . . . 7 (𝑡 = 𝑧 → ((abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌𝑍))) ↔ (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌𝑍)))))
249235, 246, 248cbvralw 3289 . . . . . 6 (∀𝑡 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑡)) ≤ (𝑀 · (abs‘(𝑌𝑍))) ↔ ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌𝑍))))
250234, 249sylib 217 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ∀𝑧 ∈ (0(,)1)(abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌𝑍))))
251250r19.21bi 3234 . . . 4 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ 𝑧 ∈ (0(,)1)) → (abs‘((ℝ D (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))))‘𝑧)) ≤ (𝑀 · (abs‘(𝑌𝑍))))
2523, 4, 102, 200, 204, 251dvlip 25357 . . 3 (((𝜑 ∧ (𝑌𝐵𝑍𝐵)) ∧ (1 ∈ (0[,]1) ∧ 0 ∈ (0[,]1))) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌𝑍))) · (abs‘(1 − 0))))
2531, 2, 252mpanr12 703 . 2 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) ≤ ((𝑀 · (abs‘(𝑌𝑍))) · (abs‘(1 − 0))))
254 oveq2 7365 . . . . . . . . 9 (𝑡 = 1 → (𝑌 · 𝑡) = (𝑌 · 1))
255 oveq2 7365 . . . . . . . . . . 11 (𝑡 = 1 → (1 − 𝑡) = (1 − 1))
256 1m1e0 12225 . . . . . . . . . . 11 (1 − 1) = 0
257255, 256eqtrdi 2792 . . . . . . . . . 10 (𝑡 = 1 → (1 − 𝑡) = 0)
258257oveq2d 7373 . . . . . . . . 9 (𝑡 = 1 → (𝑍 · (1 − 𝑡)) = (𝑍 · 0))
259254, 258oveq12d 7375 . . . . . . . 8 (𝑡 = 1 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 1) + (𝑍 · 0)))
260259fveq2d 6846 . . . . . . 7 (𝑡 = 1 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
261 eqid 2736 . . . . . . 7 (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))))) = (𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))
262 fvex 6855 . . . . . . 7 (𝐹‘((𝑌 · 1) + (𝑍 · 0))) ∈ V
263260, 261, 262fvmpt 6948 . . . . . 6 (1 ∈ (0[,]1) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘((𝑌 · 1) + (𝑍 · 0))))
2641, 263ax-mp 5 . . . . 5 ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹‘((𝑌 · 1) + (𝑍 · 0)))
26523mul01d 11354 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑍 · 0) = 0)
266143, 265oveq12d 7375 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = (𝑌 + 0))
26714addid1d 11355 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑌 + 0) = 𝑌)
268266, 267eqtrd 2776 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑌 · 1) + (𝑍 · 0)) = 𝑌)
269268fveq2d 6846 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝐹‘((𝑌 · 1) + (𝑍 · 0))) = (𝐹𝑌))
270264, 269eqtrid 2788 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) = (𝐹𝑌))
271 oveq2 7365 . . . . . . . . 9 (𝑡 = 0 → (𝑌 · 𝑡) = (𝑌 · 0))
272 oveq2 7365 . . . . . . . . . . 11 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
273 1m0e1 12274 . . . . . . . . . . 11 (1 − 0) = 1
274272, 273eqtrdi 2792 . . . . . . . . . 10 (𝑡 = 0 → (1 − 𝑡) = 1)
275274oveq2d 7373 . . . . . . . . 9 (𝑡 = 0 → (𝑍 · (1 − 𝑡)) = (𝑍 · 1))
276271, 275oveq12d 7375 . . . . . . . 8 (𝑡 = 0 → ((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡))) = ((𝑌 · 0) + (𝑍 · 1)))
277276fveq2d 6846 . . . . . . 7 (𝑡 = 0 → (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
278 fvex 6855 . . . . . . 7 (𝐹‘((𝑌 · 0) + (𝑍 · 1))) ∈ V
279277, 261, 278fvmpt 6948 . . . . . 6 (0 ∈ (0[,]1) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘((𝑌 · 0) + (𝑍 · 1))))
2802, 279ax-mp 5 . . . . 5 ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹‘((𝑌 · 0) + (𝑍 · 1)))
28114mul01d 11354 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑌 · 0) = 0)
28223mulid1d 11172 . . . . . . . 8 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑍 · 1) = 𝑍)
283281, 282oveq12d 7375 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = (0 + 𝑍))
28423addid2d 11356 . . . . . . 7 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (0 + 𝑍) = 𝑍)
285283, 284eqtrd 2776 . . . . . 6 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑌 · 0) + (𝑍 · 1)) = 𝑍)
286285fveq2d 6846 . . . . 5 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝐹‘((𝑌 · 0) + (𝑍 · 1))) = (𝐹𝑍))
287280, 286eqtrid 2788 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0) = (𝐹𝑍))
288270, 287oveq12d 7375 . . 3 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0)) = ((𝐹𝑌) − (𝐹𝑍)))
289288fveq2d 6846 . 2 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (abs‘(((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘1) − ((𝑡 ∈ (0[,]1) ↦ (𝐹‘((𝑌 · 𝑡) + (𝑍 · (1 − 𝑡)))))‘0))) = (abs‘((𝐹𝑌) − (𝐹𝑍))))
290273fveq2i 6845 . . . . 5 (abs‘(1 − 0)) = (abs‘1)
291 abs1 15182 . . . . 5 (abs‘1) = 1
292290, 291eqtri 2764 . . . 4 (abs‘(1 − 0)) = 1
293292oveq2i 7368 . . 3 ((𝑀 · (abs‘(𝑌𝑍))) · (abs‘(1 − 0))) = ((𝑀 · (abs‘(𝑌𝑍))) · 1)
294204recnd 11183 . . . 4 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (𝑀 · (abs‘(𝑌𝑍))) ∈ ℂ)
295294mulid1d 11172 . . 3 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑀 · (abs‘(𝑌𝑍))) · 1) = (𝑀 · (abs‘(𝑌𝑍))))
296293, 295eqtrid 2788 . 2 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → ((𝑀 · (abs‘(𝑌𝑍))) · (abs‘(1 − 0))) = (𝑀 · (abs‘(𝑌𝑍))))
297253, 289, 2963brtr3d 5136 1 ((𝜑 ∧ (𝑌𝐵𝑍𝐵)) → (abs‘((𝐹𝑌) − (𝐹𝑍))) ≤ (𝑀 · (abs‘(𝑌𝑍))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  Vcvv 3445  cin 3909  wss 3910  {cpr 4588   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  cres 5635  ccom 5637  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188  cle 11190  cmin 11385  -cneg 11386  (,)cioo 13264  [,]cicc 13267  abscabs 15119  TopOpenctopn 17303  topGenctg 17319  ∞Metcxmet 20781  ballcbl 20783  fldccnfld 20796  Topctop 22242  intcnt 22368   Cn ccn 22575   ×t ctx 22911  cnccncf 24239   D cdv 25227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-limc 25230  df-dv 25231
This theorem is referenced by:  dvlip2  25359  dv11cn  25365
  Copyright terms: Public domain W3C validator