Metamath Proof Explorer

Theorem dvlip2

Description: Combine the results of dvlip and dvlipcn into one. (Contributed by Mario Carneiro, 18-Mar-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses dvlip2.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvlip2.j ⊢ 𝐽 = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
dvlip2.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvlip2.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvlip2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
dvlip2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
dvlip2.b ⊢ 𝐵 = ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 )
dvlip2.d ⊢ ( 𝜑 → 𝐵 ⊆ dom ( 𝑆 D 𝐹 ) )
dvlip2.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
dvlip2.l ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
Assertion dvlip2 ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvlip2.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvlip2.j ⊢ 𝐽 = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
3 dvlip2.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
4 dvlip2.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
5 dvlip2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
6 dvlip2.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
7 dvlip2.b ⊢ 𝐵 = ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 )
8 dvlip2.d ⊢ ( 𝜑 → 𝐵 ⊆ dom ( 𝑆 D 𝐹 ) )
9 dvlip2.m ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
10 dvlip2.l ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
11 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
12 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
13 1 12 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
14 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
15 11 13 14 sylancr ⊢ ( 𝜑 → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
16 2 15 eqeltrid ⊢ ( 𝜑 → 𝐽 ∈ ( ∞Met ‘ 𝑆 ) )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐽 ∈ ( ∞Met ‘ 𝑆 ) )
18 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐴 ∈ 𝑆 )
19 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑍 ∈ 𝐵 )
20 19 7 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑍 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) )
21 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑅 ∈ ℝ* )
22 elbl ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ* ) → ( 𝑍 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ↔ ( 𝑍 ∈ 𝑆 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑅 ) ) )
23 17 18 21 22 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑍 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ↔ ( 𝑍 ∈ 𝑆 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑅 ) ) )
24 20 23 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑍 ∈ 𝑆 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑅 ) )
25 24 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑍 ∈ 𝑆 )
26 xmetcl ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐴 𝐽 𝑍 ) ∈ ℝ* )
27 17 18 25 26 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑍 ) ∈ ℝ* )
28 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑌 ∈ 𝐵 )
29 28 7 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑌 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) )
30 elbl ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ* ) → ( 𝑌 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ↔ ( 𝑌 ∈ 𝑆 ∧ ( 𝐴 𝐽 𝑌 ) < 𝑅 ) ) )
31 17 18 21 30 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑌 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ↔ ( 𝑌 ∈ 𝑆 ∧ ( 𝐴 𝐽 𝑌 ) < 𝑅 ) ) )
32 29 31 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑌 ∈ 𝑆 ∧ ( 𝐴 𝐽 𝑌 ) < 𝑅 ) )
33 32 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑌 ∈ 𝑆 )
34 xmetcl ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝐴 𝐽 𝑌 ) ∈ ℝ* )
35 17 18 33 34 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑌 ) ∈ ℝ* )
36 27 35 ifcld ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) ∈ ℝ* )
37 24 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑍 ) < 𝑅 )
38 32 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑌 ) < 𝑅 )
39 breq1 ⊢ ( ( 𝐴 𝐽 𝑍 ) = if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) → ( ( 𝐴 𝐽 𝑍 ) < 𝑅 ↔ if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑅 ) )
40 breq1 ⊢ ( ( 𝐴 𝐽 𝑌 ) = if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) → ( ( 𝐴 𝐽 𝑌 ) < 𝑅 ↔ if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑅 ) )
41 39 40 ifboth ⊢ ( ( ( 𝐴 𝐽 𝑍 ) < 𝑅 ∧ ( 𝐴 𝐽 𝑌 ) < 𝑅 ) → if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑅 )
42 37 38 41 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑅 )
43 qbtwnxr ⊢ ( ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑅 ) → ∃ 𝑟 ∈ ℚ ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ∧ 𝑟 < 𝑅 ) )
44 36 21 42 43 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ∃ 𝑟 ∈ ℚ ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ∧ 𝑟 < 𝑅 ) )
45 qre ⊢ ( 𝑟 ∈ ℚ → 𝑟 ∈ ℝ )
46 rexr ⊢ ( 𝑟 ∈ ℝ → 𝑟 ∈ ℝ* )
47 xrmaxlt ⊢ ( ( ( 𝐴 𝐽 𝑌 ) ∈ ℝ* ∧ ( 𝐴 𝐽 𝑍 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ* ) → ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ↔ ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ) )
48 35 27 46 47 syl2an3an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) → ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ↔ ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ) )
49 ioossicc ⊢ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ⊆ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) )
50 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑆 = ℝ )
51 33 50 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑌 ∈ ℝ )
52 51 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑌 ∈ ℝ )
53 xmetsym ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝐴 𝐽 𝑌 ) = ( 𝑌 𝐽 𝐴 ) )
54 17 18 33 53 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑌 ) = ( 𝑌 𝐽 𝐴 ) )
55 50 sqxpeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑆 × 𝑆 ) = ( ℝ × ℝ ) )
56 55 reseq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
57 2 56 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐽 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
58 57 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑌 𝐽 𝐴 ) = ( 𝑌 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) )
59 18 50 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐴 ∈ ℝ )
60 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
61 60 remetdval ⊢ ( ( 𝑌 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑌 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) = ( abs ‘ ( 𝑌 − 𝐴 ) ) )
62 51 59 61 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑌 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) = ( abs ‘ ( 𝑌 − 𝐴 ) ) )
63 54 58 62 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑌 ) = ( abs ‘ ( 𝑌 − 𝐴 ) ) )
64 63 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 𝐽 𝑌 ) = ( abs ‘ ( 𝑌 − 𝐴 ) ) )
65 simprll ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 𝐽 𝑌 ) < 𝑟 )
66 64 65 eqbrtrrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( abs ‘ ( 𝑌 − 𝐴 ) ) < 𝑟 )
67 59 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝐴 ∈ ℝ )
68 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑟 ∈ ℝ )
69 52 67 68 absdifltd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( abs ‘ ( 𝑌 − 𝐴 ) ) < 𝑟 ↔ ( ( 𝐴 − 𝑟 ) < 𝑌 ∧ 𝑌 < ( 𝐴 + 𝑟 ) ) ) )
70 66 69 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) < 𝑌 ∧ 𝑌 < ( 𝐴 + 𝑟 ) ) )
71 70 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 − 𝑟 ) < 𝑌 )
72 70 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑌 < ( 𝐴 + 𝑟 ) )
73 67 68 resubcld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 − 𝑟 ) ∈ ℝ )
74 73 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 − 𝑟 ) ∈ ℝ* )
75 67 68 readdcld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 + 𝑟 ) ∈ ℝ )
76 75 rexrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 + 𝑟 ) ∈ ℝ* )
77 elioo2 ⊢ ( ( ( 𝐴 − 𝑟 ) ∈ ℝ* ∧ ( 𝐴 + 𝑟 ) ∈ ℝ* ) → ( 𝑌 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ↔ ( 𝑌 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) < 𝑌 ∧ 𝑌 < ( 𝐴 + 𝑟 ) ) ) )
78 74 76 77 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝑌 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ↔ ( 𝑌 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) < 𝑌 ∧ 𝑌 < ( 𝐴 + 𝑟 ) ) ) )
79 52 71 72 78 mpbir3and ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑌 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
80 49 79 sseldi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑌 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) )
81 80 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) )
82 25 50 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑍 ∈ ℝ )
83 82 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑍 ∈ ℝ )
84 xmetsym ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐴 𝐽 𝑍 ) = ( 𝑍 𝐽 𝐴 ) )
85 17 18 25 84 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑍 ) = ( 𝑍 𝐽 𝐴 ) )
86 57 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑍 𝐽 𝐴 ) = ( 𝑍 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) )
87 60 remetdval ⊢ ( ( 𝑍 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑍 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) = ( abs ‘ ( 𝑍 − 𝐴 ) ) )
88 82 59 87 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑍 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) = ( abs ‘ ( 𝑍 − 𝐴 ) ) )
89 85 86 88 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 𝐽 𝑍 ) = ( abs ‘ ( 𝑍 − 𝐴 ) ) )
90 89 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 𝐽 𝑍 ) = ( abs ‘ ( 𝑍 − 𝐴 ) ) )
91 simprlr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 𝐽 𝑍 ) < 𝑟 )
92 90 91 eqbrtrrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( abs ‘ ( 𝑍 − 𝐴 ) ) < 𝑟 )
93 83 67 68 absdifltd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( abs ‘ ( 𝑍 − 𝐴 ) ) < 𝑟 ↔ ( ( 𝐴 − 𝑟 ) < 𝑍 ∧ 𝑍 < ( 𝐴 + 𝑟 ) ) ) )
94 92 93 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) < 𝑍 ∧ 𝑍 < ( 𝐴 + 𝑟 ) ) )
95 94 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐴 − 𝑟 ) < 𝑍 )
96 94 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑍 < ( 𝐴 + 𝑟 ) )
97 elioo2 ⊢ ( ( ( 𝐴 − 𝑟 ) ∈ ℝ* ∧ ( 𝐴 + 𝑟 ) ∈ ℝ* ) → ( 𝑍 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ↔ ( 𝑍 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) < 𝑍 ∧ 𝑍 < ( 𝐴 + 𝑟 ) ) ) )
98 74 76 97 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝑍 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ↔ ( 𝑍 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) < 𝑍 ∧ 𝑍 < ( 𝐴 + 𝑟 ) ) ) )
99 83 95 96 98 mpbir3and ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑍 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
100 49 99 sseldi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑍 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) )
101 100 fvresd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑍 ) = ( 𝐹 ‘ 𝑍 ) )
102 81 101 oveq12d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑍 ) ) = ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) )
103 102 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑍 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) )
104 17 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝐽 ∈ ( ∞Met ‘ 𝑆 ) )
105 elicc2 ⊢ ( ( ( 𝐴 − 𝑟 ) ∈ ℝ ∧ ( 𝐴 + 𝑟 ) ∈ ℝ ) → ( 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐴 + 𝑟 ) ) ) )
106 73 75 105 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐴 + 𝑟 ) ) ) )
107 106 biimpa ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝐴 − 𝑟 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐴 + 𝑟 ) ) )
108 107 simp1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑥 ∈ ℝ )
109 50 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑆 = ℝ )
110 108 109 eleqtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑥 ∈ 𝑆 )
111 18 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝐴 ∈ 𝑆 )
112 xmetcl ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑥 𝐽 𝐴 ) ∈ ℝ* )
113 104 110 111 112 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 𝐽 𝐴 ) ∈ ℝ* )
114 68 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑟 ∈ ℝ )
115 114 rexrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑟 ∈ ℝ* )
116 21 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑅 ∈ ℝ* )
117 57 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝐽 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
118 117 oveqd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 𝐽 𝐴 ) = ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) )
119 67 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝐴 ∈ ℝ )
120 60 remetdval ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) = ( abs ‘ ( 𝑥 − 𝐴 ) ) )
121 108 119 120 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) 𝐴 ) = ( abs ‘ ( 𝑥 − 𝐴 ) ) )
122 118 121 eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 𝐽 𝐴 ) = ( abs ‘ ( 𝑥 − 𝐴 ) ) )
123 107 simp2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝐴 − 𝑟 ) ≤ 𝑥 )
124 107 simp3d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑥 ≤ ( 𝐴 + 𝑟 ) )
125 108 119 114 absdifled ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( ( abs ‘ ( 𝑥 − 𝐴 ) ) ≤ 𝑟 ↔ ( ( 𝐴 − 𝑟 ) ≤ 𝑥 ∧ 𝑥 ≤ ( 𝐴 + 𝑟 ) ) ) )
126 123 124 125 mpbir2and ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( abs ‘ ( 𝑥 − 𝐴 ) ) ≤ 𝑟 )
127 122 126 eqbrtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 𝐽 𝐴 ) ≤ 𝑟 )
128 simplrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑟 < 𝑅 )
129 113 115 116 127 128 xrlelttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 𝐽 𝐴 ) < 𝑅 )
130 elbl3 ⊢ ( ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑥 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ↔ ( 𝑥 𝐽 𝐴 ) < 𝑅 ) )
131 104 116 111 110 130 syl22anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( 𝑥 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ↔ ( 𝑥 𝐽 𝐴 ) < 𝑅 ) )
132 129 131 mpbird ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → 𝑥 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) )
133 132 ex ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝑥 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) → 𝑥 ∈ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ) )
134 133 ssrdv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ⊆ ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) )
135 134 7 sseqtrrdi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ⊆ 𝐵 )
136 135 resabs1d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐹 ↾ 𝐵 ) ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) = ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) )
137 ax-resscn ⊢ ℝ ⊆ ℂ
138 137 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ℝ ⊆ ℂ )
139 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝐹 : 𝑋 ⟶ ℂ )
140 13 4 3 dvbss ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝑋 )
141 8 140 sstrd ⊢ ( 𝜑 → 𝐵 ⊆ 𝑋 )
142 141 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝐵 ⊆ 𝑋 )
143 139 142 fssresd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℂ )
144 blssm ⊢ ( ( 𝐽 ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ* ) → ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ⊆ 𝑆 )
145 17 18 21 144 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) ⊆ 𝑆 )
146 7 145 eqsstrid ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐵 ⊆ 𝑆 )
147 146 50 sseqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐵 ⊆ ℝ )
148 147 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝐵 ⊆ ℝ )
149 137 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ℝ ⊆ ℂ )
150 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐹 : 𝑋 ⟶ ℂ )
151 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑋 ⊆ 𝑆 )
152 151 50 sseqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝑋 ⊆ ℝ )
153 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
154 153 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
155 153 154 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ) ∧ ( 𝑋 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐵 ) ) )
156 149 150 152 147 155 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐵 ) ) )
157 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
158 57 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ball ‘ 𝐽 ) = ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) )
159 158 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) = ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑅 ) )
160 7 159 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐵 = ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑅 ) )
161 57 17 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ 𝑆 ) )
162 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
163 60 162 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
164 163 blopn ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ∧ 𝑅 ∈ ℝ* ) → ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑅 ) ∈ ( topGen ‘ ran (,) ) )
165 161 18 21 164 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐴 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑅 ) ∈ ( topGen ‘ ran (,) ) )
166 160 165 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐵 ∈ ( topGen ‘ ran (,) ) )
167 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐵 ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐵 ) = 𝐵 )
168 157 166 167 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐵 ) = 𝐵 )
169 168 reseq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ 𝐵 ) ) = ( ( ℝ D 𝐹 ) ↾ 𝐵 ) )
170 156 169 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = ( ( ℝ D 𝐹 ) ↾ 𝐵 ) )
171 170 dmeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = dom ( ( ℝ D 𝐹 ) ↾ 𝐵 ) )
172 dmres ⊢ dom ( ( ℝ D 𝐹 ) ↾ 𝐵 ) = ( 𝐵 ∩ dom ( ℝ D 𝐹 ) )
173 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐵 ⊆ dom ( 𝑆 D 𝐹 ) )
174 50 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝑆 D 𝐹 ) = ( ℝ D 𝐹 ) )
175 174 dmeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → dom ( 𝑆 D 𝐹 ) = dom ( ℝ D 𝐹 ) )
176 173 175 sseqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → 𝐵 ⊆ dom ( ℝ D 𝐹 ) )
177 df-ss ⊢ ( 𝐵 ⊆ dom ( ℝ D 𝐹 ) ↔ ( 𝐵 ∩ dom ( ℝ D 𝐹 ) ) = 𝐵 )
178 176 177 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( 𝐵 ∩ dom ( ℝ D 𝐹 ) ) = 𝐵 )
179 172 178 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → dom ( ( ℝ D 𝐹 ) ↾ 𝐵 ) = 𝐵 )
180 171 179 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = 𝐵 )
181 180 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = 𝐵 )
182 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℂ ∧ 𝐵 ⊆ ℝ ) ∧ dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = 𝐵 ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐵 –cn→ ℂ ) )
183 138 143 148 181 182 syl31anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐵 –cn→ ℂ ) )
184 rescncf ⊢ ( ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐵 –cn→ ℂ ) → ( ( 𝐹 ↾ 𝐵 ) ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ∈ ( ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) –cn→ ℂ ) ) )
185 135 183 184 sylc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐹 ↾ 𝐵 ) ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ∈ ( ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) –cn→ ℂ ) )
186 136 185 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ∈ ( ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) –cn→ ℂ ) )
187 135 148 sstrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ⊆ ℝ )
188 153 154 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℂ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ⊆ ℝ ) ) → ( ℝ D ( ( 𝐹 ↾ 𝐵 ) ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) )
189 138 143 148 187 188 syl22anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ℝ D ( ( 𝐹 ↾ 𝐵 ) ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) )
190 136 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ℝ D ( ( 𝐹 ↾ 𝐵 ) ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) )
191 iccntr ⊢ ( ( ( 𝐴 − 𝑟 ) ∈ ℝ ∧ ( 𝐴 + 𝑟 ) ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) = ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
192 73 75 191 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) = ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
193 192 reseq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) )
194 189 190 193 3eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) )
195 194 dmeqd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = dom ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) )
196 dmres ⊢ dom ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) = ( ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ∩ dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) )
197 49 135 sstrid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ⊆ 𝐵 )
198 197 181 sseqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ⊆ dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) )
199 df-ss ⊢ ( ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ⊆ dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↔ ( ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ∩ dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ) = ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
200 198 199 sylib ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ∩ dom ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ) = ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
201 196 200 syl5eq ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → dom ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) = ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
202 195 201 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) = ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) )
203 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝑀 ∈ ℝ )
204 194 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) ‘ 𝑥 ) = ( ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) ‘ 𝑥 ) )
205 fvres ⊢ ( 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) → ( ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ↾ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) ‘ 𝑥 ) = ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑥 ) )
206 204 205 sylan9eq ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) ‘ 𝑥 ) = ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑥 ) )
207 174 reseq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) = ( ( ℝ D 𝐹 ) ↾ 𝐵 ) )
208 170 207 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ℝ D ( 𝐹 ↾ 𝐵 ) ) = ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) )
209 208 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) ‘ 𝑥 ) )
210 209 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( ( ℝ D ( 𝐹 ↾ 𝐵 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) ‘ 𝑥 ) )
211 197 sselda ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → 𝑥 ∈ 𝐵 )
212 211 fvresd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( ( ( 𝑆 D 𝐹 ) ↾ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
213 206 210 212 3eqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
214 213 fveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) ‘ 𝑥 ) ) = ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
215 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → 𝜑 )
216 215 211 10 syl2an2r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
217 214 216 eqbrtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ 𝑥 ∈ ( ( 𝐴 − 𝑟 ) (,) ( 𝐴 + 𝑟 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) ‘ 𝑥 ) ) ≤ 𝑀 )
218 73 75 186 202 203 217 dvlip ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) ∧ ( 𝑌 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ∧ 𝑍 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
219 218 ex ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( ( 𝑌 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ∧ 𝑍 ∈ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) ) )
220 80 100 219 mp2and ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( abs ‘ ( ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑌 ) − ( ( 𝐹 ↾ ( ( 𝐴 − 𝑟 ) [,] ( 𝐴 + 𝑟 ) ) ) ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
221 103 220 eqbrtrrd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) ∧ ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) ∧ 𝑟 < 𝑅 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
222 221 exp32 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) → ( ( ( 𝐴 𝐽 𝑌 ) < 𝑟 ∧ ( 𝐴 𝐽 𝑍 ) < 𝑟 ) → ( 𝑟 < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) ) ) )
223 48 222 sylbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) → ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 → ( 𝑟 < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) ) ) )
224 223 impd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℝ ) → ( ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ∧ 𝑟 < 𝑅 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) ) )
225 45 224 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) ∧ 𝑟 ∈ ℚ ) → ( ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ∧ 𝑟 < 𝑅 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) ) )
226 225 rexlimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( ∃ 𝑟 ∈ ℚ ( if ( ( 𝐴 𝐽 𝑌 ) ≤ ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑍 ) , ( 𝐴 𝐽 𝑌 ) ) < 𝑟 ∧ 𝑟 < 𝑅 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) ) )
227 44 226 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℝ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
228 simpr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝑆 = ℂ )
229 228 sqxpeqd ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑆 × 𝑆 ) = ( ℂ × ℂ ) )
230 229 reseq2d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) )
231 absf ⊢ abs : ℂ ⟶ ℝ
232 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
233 fco ⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
234 231 232 233 mp2an ⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
235 ffn ⊢ ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
236 fnresdm ⊢ ( ( abs ∘ − ) Fn ( ℂ × ℂ ) → ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − ) )
237 234 235 236 mp2b ⊢ ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − )
238 230 237 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( abs ∘ − ) )
239 2 238 syl5eq ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝐽 = ( abs ∘ − ) )
240 239 fveq2d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( ball ‘ 𝐽 ) = ( ball ‘ ( abs ∘ − ) ) )
241 240 oveqd ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝐴 ( ball ‘ 𝐽 ) 𝑅 ) = ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
242 7 241 syl5eq ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝐵 = ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
243 242 eleq2d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑌 ∈ 𝐵 ↔ 𝑌 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
244 242 eleq2d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑍 ∈ 𝐵 ↔ 𝑍 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
245 243 244 anbi12d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ↔ ( 𝑌 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∧ 𝑍 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ) )
246 245 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑆 = ℂ ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∧ 𝑍 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
247 3 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝑋 ⊆ 𝑆 )
248 247 228 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝑋 ⊆ ℂ )
249 4 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝐹 : 𝑋 ⟶ ℂ )
250 5 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝐴 ∈ 𝑆 )
251 250 228 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝐴 ∈ ℂ )
252 6 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝑅 ∈ ℝ* )
253 eqid ⊢ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) = ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
254 8 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝐵 ⊆ dom ( 𝑆 D 𝐹 ) )
255 228 oveq1d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑆 D 𝐹 ) = ( ℂ D 𝐹 ) )
256 255 dmeqd ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → dom ( 𝑆 D 𝐹 ) = dom ( ℂ D 𝐹 ) )
257 254 242 256 3sstr3d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ⊆ dom ( ℂ D 𝐹 ) )
258 9 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → 𝑀 ∈ ℝ )
259 10 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 ) )
260 259 adantr ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑥 ∈ 𝐵 → ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 ) )
261 242 eleq2d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) )
262 255 fveq1d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) = ( ( ℂ D 𝐹 ) ‘ 𝑥 ) )
263 262 fveq2d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) = ( abs ‘ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) )
264 263 breq1d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( ( abs ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 ↔ ( abs ‘ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 ) )
265 260 261 264 3imtr3d ⊢ ( ( 𝜑 ∧ 𝑆 = ℂ ) → ( 𝑥 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) → ( abs ‘ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 ) )
266 265 imp ⊢ ( ( ( 𝜑 ∧ 𝑆 = ℂ ) ∧ 𝑥 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) → ( abs ‘ ( ( ℂ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑀 )
267 248 249 251 252 253 257 258 266 dvlipcn ⊢ ( ( ( 𝜑 ∧ 𝑆 = ℂ ) ∧ ( 𝑌 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∧ 𝑍 ∈ ( 𝐴 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
268 246 267 syldan ⊢ ( ( ( 𝜑 ∧ 𝑆 = ℂ ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
269 268 an32s ⊢ ( ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑆 = ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )
270 elpri ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
271 1 270 syl ⊢ ( 𝜑 → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
272 271 adantr ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
273 227 269 272 mpjaodan ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑌 ) − ( 𝐹 ‘ 𝑍 ) ) ) ≤ ( 𝑀 · ( abs ‘ ( 𝑌 − 𝑍 ) ) ) )