Step | Hyp | Ref
| Expression |
1 | | dvlip2.j |
. . . . . . . 8
⊢ 𝐽 = ((abs ∘ − )
↾ (𝑆 × 𝑆)) |
2 | | cnxmet 23917 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
3 | | dvlip2.s |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
4 | | recnprss 25049 |
. . . . . . . . . 10
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
6 | | xmetres2 23495 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑆
× 𝑆)) ∈
(∞Met‘𝑆)) |
7 | 2, 5, 6 | sylancr 586 |
. . . . . . . 8
⊢ (𝜑 → ((abs ∘ − )
↾ (𝑆 × 𝑆)) ∈
(∞Met‘𝑆)) |
8 | 1, 7 | eqeltrid 2844 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (∞Met‘𝑆)) |
9 | 8 | ad2antrr 722 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐽 ∈ (∞Met‘𝑆)) |
10 | | dvlip2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
11 | 10 | ad2antrr 722 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐴 ∈ 𝑆) |
12 | | simplrr 774 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ 𝐵) |
13 | | dvlip2.b |
. . . . . . . . 9
⊢ 𝐵 = (𝐴(ball‘𝐽)𝑅) |
14 | 12, 13 | eleqtrdi 2850 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ (𝐴(ball‘𝐽)𝑅)) |
15 | | dvlip2.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
16 | 15 | ad2antrr 722 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑅 ∈
ℝ*) |
17 | | elbl 23522 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ*) → (𝑍 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑍 ∈ 𝑆 ∧ (𝐴𝐽𝑍) < 𝑅))) |
18 | 9, 11, 16, 17 | syl3anc 1369 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑍 ∈ 𝑆 ∧ (𝐴𝐽𝑍) < 𝑅))) |
19 | 14, 18 | mpbid 231 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍 ∈ 𝑆 ∧ (𝐴𝐽𝑍) < 𝑅)) |
20 | 19 | simpld 494 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ 𝑆) |
21 | | xmetcl 23465 |
. . . . . 6
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆) → (𝐴𝐽𝑍) ∈
ℝ*) |
22 | 9, 11, 20, 21 | syl3anc 1369 |
. . . . 5
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) ∈
ℝ*) |
23 | | simplrl 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ 𝐵) |
24 | 23, 13 | eleqtrdi 2850 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ (𝐴(ball‘𝐽)𝑅)) |
25 | | elbl 23522 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ*) → (𝑌 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑌 ∈ 𝑆 ∧ (𝐴𝐽𝑌) < 𝑅))) |
26 | 9, 11, 16, 25 | syl3anc 1369 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑌 ∈ 𝑆 ∧ (𝐴𝐽𝑌) < 𝑅))) |
27 | 24, 26 | mpbid 231 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌 ∈ 𝑆 ∧ (𝐴𝐽𝑌) < 𝑅)) |
28 | 27 | simpld 494 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ 𝑆) |
29 | | xmetcl 23465 |
. . . . . 6
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝐴𝐽𝑌) ∈
ℝ*) |
30 | 9, 11, 28, 29 | syl3anc 1369 |
. . . . 5
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) ∈
ℝ*) |
31 | 22, 30 | ifcld 4510 |
. . . 4
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) ∈
ℝ*) |
32 | 19 | simprd 495 |
. . . . 5
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) < 𝑅) |
33 | 27 | simprd 495 |
. . . . 5
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) < 𝑅) |
34 | | breq1 5081 |
. . . . . 6
⊢ ((𝐴𝐽𝑍) = if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) → ((𝐴𝐽𝑍) < 𝑅 ↔ if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅)) |
35 | | breq1 5081 |
. . . . . 6
⊢ ((𝐴𝐽𝑌) = if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) → ((𝐴𝐽𝑌) < 𝑅 ↔ if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅)) |
36 | 34, 35 | ifboth 4503 |
. . . . 5
⊢ (((𝐴𝐽𝑍) < 𝑅 ∧ (𝐴𝐽𝑌) < 𝑅) → if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅) |
37 | 32, 33, 36 | syl2anc 583 |
. . . 4
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅) |
38 | | qbtwnxr 12916 |
. . . 4
⊢
((if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) ∈ ℝ* ∧ 𝑅 ∈ ℝ*
∧ if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑅) → ∃𝑟 ∈ ℚ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅)) |
39 | 31, 16, 37, 38 | syl3anc 1369 |
. . 3
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ∃𝑟 ∈ ℚ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅)) |
40 | | qre 12675 |
. . . . 5
⊢ (𝑟 ∈ ℚ → 𝑟 ∈
ℝ) |
41 | | rexr 11005 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℝ*) |
42 | | xrmaxlt 12897 |
. . . . . . . 8
⊢ (((𝐴𝐽𝑌) ∈ ℝ* ∧ (𝐴𝐽𝑍) ∈ ℝ* ∧ 𝑟 ∈ ℝ*)
→ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ↔ ((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟))) |
43 | 30, 22, 41, 42 | syl2an3an 1420 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ↔ ((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟))) |
44 | | ioossicc 13147 |
. . . . . . . . . . . . 13
⊢ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) |
45 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑆 = ℝ) |
46 | 28, 45 | eleqtrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑌 ∈ ℝ) |
47 | 46 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 ∈ ℝ) |
48 | | xmetsym 23481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝐴𝐽𝑌) = (𝑌𝐽𝐴)) |
49 | 9, 11, 28, 48 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) = (𝑌𝐽𝐴)) |
50 | 45 | sqxpeqd 5620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑆 × 𝑆) = (ℝ ×
ℝ)) |
51 | 50 | reseq2d 5888 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((abs ∘ − )
↾ (𝑆 × 𝑆)) = ((abs ∘ − )
↾ (ℝ × ℝ))) |
52 | 1, 51 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐽 = ((abs ∘ − ) ↾ (ℝ
× ℝ))) |
53 | 52 | oveqd 7285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌𝐽𝐴) = (𝑌((abs ∘ − ) ↾ (ℝ
× ℝ))𝐴)) |
54 | 11, 45 | eleqtrd 2842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐴 ∈ ℝ) |
55 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
56 | 55 | remetdval 23933 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑌 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑌((abs ∘ − ) ↾
(ℝ × ℝ))𝐴) = (abs‘(𝑌 − 𝐴))) |
57 | 46, 54, 56 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑌((abs ∘ − ) ↾ (ℝ
× ℝ))𝐴) =
(abs‘(𝑌 − 𝐴))) |
58 | 49, 53, 57 | 3eqtrd 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑌) = (abs‘(𝑌 − 𝐴))) |
59 | 58 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑌) = (abs‘(𝑌 − 𝐴))) |
60 | | simprll 775 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑌) < 𝑟) |
61 | 59, 60 | eqbrtrrd 5102 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(𝑌 − 𝐴)) < 𝑟) |
62 | 54 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐴 ∈ ℝ) |
63 | | simplr 765 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑟 ∈ ℝ) |
64 | 47, 62, 63 | absdifltd 15126 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((abs‘(𝑌 − 𝐴)) < 𝑟 ↔ ((𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟)))) |
65 | 61, 64 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟))) |
66 | 65 | simpld 494 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) < 𝑌) |
67 | 65 | simprd 495 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 < (𝐴 + 𝑟)) |
68 | 62, 63 | resubcld 11386 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) ∈ ℝ) |
69 | 68 | rexrd 11009 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) ∈
ℝ*) |
70 | 62, 63 | readdcld 10988 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 + 𝑟) ∈ ℝ) |
71 | 70 | rexrd 11009 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 + 𝑟) ∈
ℝ*) |
72 | | elioo2 13102 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑟) ∈ ℝ* ∧ (𝐴 + 𝑟) ∈ ℝ*) → (𝑌 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑌 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟)))) |
73 | 69, 71, 72 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑌 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑌 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑌 ∧ 𝑌 < (𝐴 + 𝑟)))) |
74 | 47, 66, 67, 73 | mpbir3and 1340 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
75 | 44, 74 | sselid 3923 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) |
76 | 75 | fvresd 6788 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) = (𝐹‘𝑌)) |
77 | 20, 45 | eleqtrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑍 ∈ ℝ) |
78 | 77 | ad2antrr 722 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 ∈ ℝ) |
79 | | xmetsym 23481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆) → (𝐴𝐽𝑍) = (𝑍𝐽𝐴)) |
80 | 9, 11, 20, 79 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) = (𝑍𝐽𝐴)) |
81 | 52 | oveqd 7285 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍𝐽𝐴) = (𝑍((abs ∘ − ) ↾ (ℝ
× ℝ))𝐴)) |
82 | 55 | remetdval 23933 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑍 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑍((abs ∘ − ) ↾
(ℝ × ℝ))𝐴) = (abs‘(𝑍 − 𝐴))) |
83 | 77, 54, 82 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑍((abs ∘ − ) ↾ (ℝ
× ℝ))𝐴) =
(abs‘(𝑍 − 𝐴))) |
84 | 80, 81, 83 | 3eqtrd 2783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴𝐽𝑍) = (abs‘(𝑍 − 𝐴))) |
85 | 84 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑍) = (abs‘(𝑍 − 𝐴))) |
86 | | simprlr 776 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴𝐽𝑍) < 𝑟) |
87 | 85, 86 | eqbrtrrd 5102 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(𝑍 − 𝐴)) < 𝑟) |
88 | 78, 62, 63 | absdifltd 15126 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((abs‘(𝑍 − 𝐴)) < 𝑟 ↔ ((𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟)))) |
89 | 87, 88 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟))) |
90 | 89 | simpld 494 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐴 − 𝑟) < 𝑍) |
91 | 89 | simprd 495 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 < (𝐴 + 𝑟)) |
92 | | elioo2 13102 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑟) ∈ ℝ* ∧ (𝐴 + 𝑟) ∈ ℝ*) → (𝑍 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑍 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟)))) |
93 | 69, 71, 92 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑍 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ↔ (𝑍 ∈ ℝ ∧ (𝐴 − 𝑟) < 𝑍 ∧ 𝑍 < (𝐴 + 𝑟)))) |
94 | 78, 90, 91, 93 | mpbir3and 1340 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
95 | 44, 94 | sselid 3923 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) |
96 | 95 | fvresd 6788 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍) = (𝐹‘𝑍)) |
97 | 76, 96 | oveq12d 7286 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍)) = ((𝐹‘𝑌) − (𝐹‘𝑍))) |
98 | 97 | fveq2d 6772 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) = (abs‘((𝐹‘𝑌) − (𝐹‘𝑍)))) |
99 | 9 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐽 ∈ (∞Met‘𝑆)) |
100 | | elicc2 13126 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 − 𝑟) ∈ ℝ ∧ (𝐴 + 𝑟) ∈ ℝ) → (𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟)))) |
101 | 68, 70, 100 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ↔ (𝑥 ∈ ℝ ∧ (𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟)))) |
102 | 101 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥 ∈ ℝ ∧ (𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟))) |
103 | 102 | simp1d 1140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ∈ ℝ) |
104 | 45 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑆 = ℝ) |
105 | 103, 104 | eleqtrrd 2843 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ∈ 𝑆) |
106 | 11 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐴 ∈ 𝑆) |
107 | | xmetcl 23465 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆) → (𝑥𝐽𝐴) ∈
ℝ*) |
108 | 99, 105, 106, 107 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) ∈
ℝ*) |
109 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑟 ∈ ℝ) |
110 | 109 | rexrd 11009 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑟 ∈ ℝ*) |
111 | 16 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑅 ∈
ℝ*) |
112 | 52 | ad3antrrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐽 = ((abs ∘ − ) ↾ (ℝ
× ℝ))) |
113 | 112 | oveqd 7285 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) = (𝑥((abs ∘ − ) ↾ (ℝ
× ℝ))𝐴)) |
114 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝐴 ∈ ℝ) |
115 | 55 | remetdval 23933 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥((abs ∘ − ) ↾
(ℝ × ℝ))𝐴) = (abs‘(𝑥 − 𝐴))) |
116 | 103, 114,
115 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥((abs ∘ − ) ↾ (ℝ
× ℝ))𝐴) =
(abs‘(𝑥 − 𝐴))) |
117 | 113, 116 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) = (abs‘(𝑥 − 𝐴))) |
118 | 102 | simp2d 1141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝐴 − 𝑟) ≤ 𝑥) |
119 | 102 | simp3d 1142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ≤ (𝐴 + 𝑟)) |
120 | 103, 114,
109 | absdifled 15127 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → ((abs‘(𝑥 − 𝐴)) ≤ 𝑟 ↔ ((𝐴 − 𝑟) ≤ 𝑥 ∧ 𝑥 ≤ (𝐴 + 𝑟)))) |
121 | 118, 119,
120 | mpbir2and 709 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (abs‘(𝑥 − 𝐴)) ≤ 𝑟) |
122 | 117, 121 | eqbrtrd 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) ≤ 𝑟) |
123 | | simplrr 774 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑟 < 𝑅) |
124 | 108, 110,
111, 122, 123 | xrlelttrd 12876 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥𝐽𝐴) < 𝑅) |
125 | | elbl3 23526 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 ∈ (∞Met‘𝑆) ∧ 𝑅 ∈ ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆)) → (𝑥 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑥𝐽𝐴) < 𝑅)) |
126 | 99, 111, 106, 105, 125 | syl22anc 835 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (𝑥 ∈ (𝐴(ball‘𝐽)𝑅) ↔ (𝑥𝐽𝐴) < 𝑅)) |
127 | 124, 126 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → 𝑥 ∈ (𝐴(ball‘𝐽)𝑅)) |
128 | 127 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝑥 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) → 𝑥 ∈ (𝐴(ball‘𝐽)𝑅))) |
129 | 128 | ssrdv 3931 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ (𝐴(ball‘𝐽)𝑅)) |
130 | 129, 13 | sseqtrrdi 3976 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ 𝐵) |
131 | 130 | resabs1d 5919 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) = (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) |
132 | | ax-resscn 10912 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℂ |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ℝ ⊆
ℂ) |
134 | | dvlip2.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) |
135 | 134 | ad4antr 728 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐹:𝑋⟶ℂ) |
136 | | dvlip2.d |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆ dom (𝑆 D 𝐹)) |
137 | | dvlip2.x |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ⊆ 𝑆) |
138 | 5, 134, 137 | dvbss 25046 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom (𝑆 D 𝐹) ⊆ 𝑋) |
139 | 136, 138 | sstrd 3935 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ⊆ 𝑋) |
140 | 139 | ad4antr 728 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐵 ⊆ 𝑋) |
141 | 135, 140 | fssresd 6637 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐹 ↾ 𝐵):𝐵⟶ℂ) |
142 | | blssm 23552 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 ∈ (∞Met‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘𝐽)𝑅) ⊆ 𝑆) |
143 | 9, 11, 16, 142 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴(ball‘𝐽)𝑅) ⊆ 𝑆) |
144 | 13, 143 | eqsstrid 3973 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ 𝑆) |
145 | 144, 45 | sseqtrd 3965 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ ℝ) |
146 | 145 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝐵 ⊆ ℝ) |
147 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ℝ ⊆
ℂ) |
148 | 134 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐹:𝑋⟶ℂ) |
149 | 137 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑋 ⊆ 𝑆) |
150 | 149, 45 | sseqtrd 3965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝑋 ⊆ ℝ) |
151 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
152 | 151 | tgioo2 23947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
153 | 151, 152 | dvres 25056 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:𝑋⟶ℂ) ∧ (𝑋 ⊆ ℝ ∧ 𝐵 ⊆ ℝ)) → (ℝ D (𝐹 ↾ 𝐵)) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘𝐵))) |
154 | 147, 148,
150, 145, 153 | syl22anc 835 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ℝ D (𝐹 ↾ 𝐵)) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘𝐵))) |
155 | | retop 23906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(topGen‘ran (,)) ∈ Top |
156 | 52 | fveq2d 6772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ball‘𝐽) = (ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))) |
157 | 156 | oveqd 7285 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴(ball‘𝐽)𝑅) = (𝐴(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑅)) |
158 | 13, 157 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 = (𝐴(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑅)) |
159 | 52, 9 | eqeltrrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((abs ∘ − )
↾ (ℝ × ℝ)) ∈ (∞Met‘𝑆)) |
160 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
161 | 55, 160 | tgioo 23940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
162 | 161 | blopn 23637 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘𝑆) ∧
𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ*) → (𝐴(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑅) ∈ (topGen‘ran
(,))) |
163 | 159, 11, 16, 162 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐴(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))𝑅) ∈ (topGen‘ran
(,))) |
164 | 158, 163 | eqeltrd 2840 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ∈ (topGen‘ran
(,))) |
165 | | isopn3i 22214 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((topGen‘ran (,)) ∈ Top ∧ 𝐵 ∈ (topGen‘ran (,))) →
((int‘(topGen‘ran (,)))‘𝐵) = 𝐵) |
166 | 155, 164,
165 | sylancr 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) →
((int‘(topGen‘ran (,)))‘𝐵) = 𝐵) |
167 | 166 | reseq2d 5888 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((ℝ D 𝐹) ↾
((int‘(topGen‘ran (,)))‘𝐵)) = ((ℝ D 𝐹) ↾ 𝐵)) |
168 | 154, 167 | eqtrd 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ℝ D (𝐹 ↾ 𝐵)) = ((ℝ D 𝐹) ↾ 𝐵)) |
169 | 168 | dmeqd 5811 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom (ℝ D (𝐹 ↾ 𝐵)) = dom ((ℝ D 𝐹) ↾ 𝐵)) |
170 | | dmres 5910 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
((ℝ D 𝐹) ↾
𝐵) = (𝐵 ∩ dom (ℝ D 𝐹)) |
171 | 136 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ dom (𝑆 D 𝐹)) |
172 | 45 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝑆 D 𝐹) = (ℝ D 𝐹)) |
173 | 172 | dmeqd 5811 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom (𝑆 D 𝐹) = dom (ℝ D 𝐹)) |
174 | 171, 173 | sseqtrd 3965 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → 𝐵 ⊆ dom (ℝ D 𝐹)) |
175 | | df-ss 3908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ⊆ dom (ℝ D 𝐹) ↔ (𝐵 ∩ dom (ℝ D 𝐹)) = 𝐵) |
176 | 174, 175 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (𝐵 ∩ dom (ℝ D 𝐹)) = 𝐵) |
177 | 170, 176 | eqtrid 2791 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom ((ℝ D 𝐹) ↾ 𝐵) = 𝐵) |
178 | 169, 177 | eqtrd 2779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → dom (ℝ D (𝐹 ↾ 𝐵)) = 𝐵) |
179 | 178 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom (ℝ D (𝐹 ↾ 𝐵)) = 𝐵) |
180 | | dvcn 25066 |
. . . . . . . . . . . . . . 15
⊢
(((ℝ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ ∧ 𝐵 ⊆ ℝ) ∧ dom (ℝ D
(𝐹 ↾ 𝐵)) = 𝐵) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ)) |
181 | 133, 141,
146, 179, 180 | syl31anc 1371 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ)) |
182 | | rescncf 24041 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ 𝐵 → ((𝐹 ↾ 𝐵) ∈ (𝐵–cn→ℂ) → ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) ∈ (((𝐴 − 𝑟)[,](𝐴 + 𝑟))–cn→ℂ))) |
183 | 130, 181,
182 | sylc 65 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) ∈ (((𝐴 − 𝑟)[,](𝐴 + 𝑟))–cn→ℂ)) |
184 | 131, 183 | eqeltrrd 2841 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) ∈ (((𝐴 − 𝑟)[,](𝐴 + 𝑟))–cn→ℂ)) |
185 | 130, 146 | sstrd 3935 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ ℝ) |
186 | 151, 152 | dvres 25056 |
. . . . . . . . . . . . . . . 16
⊢
(((ℝ ⊆ ℂ ∧ (𝐹 ↾ 𝐵):𝐵⟶ℂ) ∧ (𝐵 ⊆ ℝ ∧ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ⊆ ℝ)) → (ℝ D
((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((int‘(topGen‘ran
(,)))‘((𝐴 −
𝑟)[,](𝐴 + 𝑟))))) |
187 | 133, 141,
146, 185, 186 | syl22anc 835 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (ℝ D ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((int‘(topGen‘ran
(,)))‘((𝐴 −
𝑟)[,](𝐴 + 𝑟))))) |
188 | 131 | oveq2d 7284 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (ℝ D ((𝐹 ↾ 𝐵) ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))) |
189 | | iccntr 23965 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 − 𝑟) ∈ ℝ ∧ (𝐴 + 𝑟) ∈ ℝ) →
((int‘(topGen‘ran (,)))‘((𝐴 − 𝑟)[,](𝐴 + 𝑟))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
190 | 68, 70, 189 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((int‘(topGen‘ran
(,)))‘((𝐴 −
𝑟)[,](𝐴 + 𝑟))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
191 | 190 | reseq2d 5888 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((int‘(topGen‘ran
(,)))‘((𝐴 −
𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))) |
192 | 187, 188,
191 | 3eqtr3d 2787 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))) |
193 | 192 | dmeqd 5811 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = dom ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))) |
194 | | dmres 5910 |
. . . . . . . . . . . . . 14
⊢ dom
((ℝ D (𝐹 ↾
𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) = (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ∩ dom (ℝ D (𝐹 ↾ 𝐵))) |
195 | 44, 130 | sstrid 3936 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ 𝐵) |
196 | 195, 179 | sseqtrrd 3966 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ dom (ℝ D (𝐹 ↾ 𝐵))) |
197 | | df-ss 3908 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ⊆ dom (ℝ D (𝐹 ↾ 𝐵)) ↔ (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ∩ dom (ℝ D (𝐹 ↾ 𝐵))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
198 | 196, 197 | sylib 217 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) ∩ dom (ℝ D (𝐹 ↾ 𝐵))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
199 | 194, 198 | eqtrid 2791 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom ((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
200 | 193, 199 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → dom (ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) = ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) |
201 | | dvlip2.m |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℝ) |
202 | 201 | ad4antr 728 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝑀 ∈ ℝ) |
203 | 192 | fveq1d 6770 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥) = (((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))‘𝑥)) |
204 | | fvres 6787 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)) → (((ℝ D (𝐹 ↾ 𝐵)) ↾ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟)))‘𝑥) = ((ℝ D (𝐹 ↾ 𝐵))‘𝑥)) |
205 | 203, 204 | sylan9eq 2799 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → ((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥) = ((ℝ D (𝐹 ↾ 𝐵))‘𝑥)) |
206 | 172 | reseq1d 5887 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((𝑆 D 𝐹) ↾ 𝐵) = ((ℝ D 𝐹) ↾ 𝐵)) |
207 | 168, 206 | eqtr4d 2782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (ℝ D (𝐹 ↾ 𝐵)) = ((𝑆 D 𝐹) ↾ 𝐵)) |
208 | 207 | fveq1d 6770 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → ((ℝ D (𝐹 ↾ 𝐵))‘𝑥) = (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥)) |
209 | 208 | ad3antrrr 726 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → ((ℝ D (𝐹 ↾ 𝐵))‘𝑥) = (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥)) |
210 | 195 | sselda 3925 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → 𝑥 ∈ 𝐵) |
211 | 210 | fvresd 6788 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (((𝑆 D 𝐹) ↾ 𝐵)‘𝑥) = ((𝑆 D 𝐹)‘𝑥)) |
212 | 205, 209,
211 | 3eqtrd 2783 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → ((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥) = ((𝑆 D 𝐹)‘𝑥)) |
213 | 212 | fveq2d 6772 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (abs‘((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥)) = (abs‘((𝑆 D 𝐹)‘𝑥))) |
214 | | simp-4l 779 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → 𝜑) |
215 | | dvlip2.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀) |
216 | 214, 210,
215 | syl2an2r 681 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀) |
217 | 213, 216 | eqbrtrd 5100 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ 𝑥 ∈ ((𝐴 − 𝑟)(,)(𝐴 + 𝑟))) → (abs‘((ℝ D (𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))))‘𝑥)) ≤ 𝑀) |
218 | 68, 70, 184, 200, 202, 217 | dvlip 25138 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) ∧ (𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ∧ 𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
219 | 218 | ex 412 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → ((𝑌 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)) ∧ 𝑍 ∈ ((𝐴 − 𝑟)[,](𝐴 + 𝑟))) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))) |
220 | 75, 95, 219 | mp2and 695 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘(((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑌) − ((𝐹 ↾ ((𝐴 − 𝑟)[,](𝐴 + 𝑟)))‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
221 | 98, 220 | eqbrtrrd 5102 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) ∧ (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) ∧ 𝑟 < 𝑅)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
222 | 221 | exp32 420 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (((𝐴𝐽𝑌) < 𝑟 ∧ (𝐴𝐽𝑍) < 𝑟) → (𝑟 < 𝑅 → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))) |
223 | 43, 222 | sylbid 239 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 → (𝑟 < 𝑅 → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))))) |
224 | 223 | impd 410 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℝ) → ((if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))) |
225 | 40, 224 | sylan2 592 |
. . . 4
⊢ ((((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) ∧ 𝑟 ∈ ℚ) → ((if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))) |
226 | 225 | rexlimdva 3214 |
. . 3
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (∃𝑟 ∈ ℚ (if((𝐴𝐽𝑌) ≤ (𝐴𝐽𝑍), (𝐴𝐽𝑍), (𝐴𝐽𝑌)) < 𝑟 ∧ 𝑟 < 𝑅) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍))))) |
227 | 39, 226 | mpd 15 |
. 2
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℝ) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
228 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑆 = ℂ) |
229 | 228 | sqxpeqd 5620 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑆 × 𝑆) = (ℂ ×
ℂ)) |
230 | 229 | reseq2d 5888 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((abs ∘ − )
↾ (𝑆 × 𝑆)) = ((abs ∘ − )
↾ (ℂ × ℂ))) |
231 | | absf 15030 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
232 | | subf 11206 |
. . . . . . . . . . . . . 14
⊢ −
:(ℂ × ℂ)⟶ℂ |
233 | | fco 6620 |
. . . . . . . . . . . . . 14
⊢
((abs:ℂ⟶ℝ ∧ − :(ℂ ×
ℂ)⟶ℂ) → (abs ∘ − ):(ℂ ×
ℂ)⟶ℝ) |
234 | 231, 232,
233 | mp2an 688 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ):(ℂ × ℂ)⟶ℝ |
235 | | ffn 6596 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ):(ℂ × ℂ)⟶ℝ → (abs ∘
− ) Fn (ℂ × ℂ)) |
236 | | fnresdm 6547 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) Fn (ℂ × ℂ) → ((abs ∘ − )
↾ (ℂ × ℂ)) = (abs ∘ − )) |
237 | 234, 235,
236 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (ℂ × ℂ)) = (abs ∘ −
) |
238 | 230, 237 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((abs ∘ − )
↾ (𝑆 × 𝑆)) = (abs ∘ −
)) |
239 | 1, 238 | eqtrid 2791 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐽 = (abs ∘ − )) |
240 | 239 | fveq2d 6772 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (ball‘𝐽) = (ball‘(abs ∘
− ))) |
241 | 240 | oveqd 7285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝐴(ball‘𝐽)𝑅) = (𝐴(ball‘(abs ∘ − ))𝑅)) |
242 | 13, 241 | eqtrid 2791 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐵 = (𝐴(ball‘(abs ∘ − ))𝑅)) |
243 | 242 | eleq2d 2825 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))) |
244 | 242 | eleq2d 2825 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑍 ∈ 𝐵 ↔ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))) |
245 | 243, 244 | anbi12d 630 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ↔ (𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) ∧ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)))) |
246 | 245 | biimpa 476 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) ∧ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))) |
247 | 137 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑋 ⊆ 𝑆) |
248 | 247, 228 | sseqtrd 3965 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑋 ⊆ ℂ) |
249 | 134 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐹:𝑋⟶ℂ) |
250 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐴 ∈ 𝑆) |
251 | 250, 228 | eleqtrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐴 ∈ ℂ) |
252 | 15 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑅 ∈
ℝ*) |
253 | | eqid 2739 |
. . . . 5
⊢ (𝐴(ball‘(abs ∘ −
))𝑅) = (𝐴(ball‘(abs ∘ − ))𝑅) |
254 | 136 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝐵 ⊆ dom (𝑆 D 𝐹)) |
255 | 228 | oveq1d 7283 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑆 D 𝐹) = (ℂ D 𝐹)) |
256 | 255 | dmeqd 5811 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → dom (𝑆 D 𝐹) = dom (ℂ D 𝐹)) |
257 | 254, 242,
256 | 3sstr3d 3971 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝐴(ball‘(abs ∘ − ))𝑅) ⊆ dom (ℂ D 𝐹)) |
258 | 201 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 = ℂ) → 𝑀 ∈ ℝ) |
259 | 215 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)) |
260 | 259 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑥 ∈ 𝐵 → (abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀)) |
261 | 242 | eleq2d 2825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))) |
262 | 255 | fveq1d 6770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((𝑆 D 𝐹)‘𝑥) = ((ℂ D 𝐹)‘𝑥)) |
263 | 262 | fveq2d 6772 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (abs‘((𝑆 D 𝐹)‘𝑥)) = (abs‘((ℂ D 𝐹)‘𝑥))) |
264 | 263 | breq1d 5088 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = ℂ) → ((abs‘((𝑆 D 𝐹)‘𝑥)) ≤ 𝑀 ↔ (abs‘((ℂ D 𝐹)‘𝑥)) ≤ 𝑀)) |
265 | 260, 261,
264 | 3imtr3d 292 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 = ℂ) → (𝑥 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) → (abs‘((ℂ D
𝐹)‘𝑥)) ≤ 𝑀)) |
266 | 265 | imp 406 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ 𝑥 ∈ (𝐴(ball‘(abs ∘ − ))𝑅)) → (abs‘((ℂ D
𝐹)‘𝑥)) ≤ 𝑀) |
267 | 248, 249,
251, 252, 253, 257, 258, 266 | dvlipcn 25139 |
. . . 4
⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ (𝑌 ∈ (𝐴(ball‘(abs ∘ − ))𝑅) ∧ 𝑍 ∈ (𝐴(ball‘(abs ∘ − ))𝑅))) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
268 | 246, 267 | syldan 590 |
. . 3
⊢ (((𝜑 ∧ 𝑆 = ℂ) ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
269 | 268 | an32s 648 |
. 2
⊢ (((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) ∧ 𝑆 = ℂ) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |
270 | | elpri 4588 |
. . . 4
⊢ (𝑆 ∈ {ℝ, ℂ}
→ (𝑆 = ℝ ∨
𝑆 =
ℂ)) |
271 | 3, 270 | syl 17 |
. . 3
⊢ (𝜑 → (𝑆 = ℝ ∨ 𝑆 = ℂ)) |
272 | 271 | adantr 480 |
. 2
⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑆 = ℝ ∨ 𝑆 = ℂ)) |
273 | 227, 269,
272 | mpjaodan 955 |
1
⊢ ((𝜑 ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (abs‘((𝐹‘𝑌) − (𝐹‘𝑍))) ≤ (𝑀 · (abs‘(𝑌 − 𝑍)))) |