Metamath Proof Explorer

Theorem hoiqssbllem2

Description: The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoiqssbllem2.i ⊢ Ⅎ 𝑖 𝜑
hoiqssbllem2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoiqssbllem2.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
hoiqssbllem2.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
hoiqssbllem2.c ⊢ ( 𝜑 → 𝐶 : 𝑋 ⟶ ℝ )
hoiqssbllem2.d ⊢ ( 𝜑 → 𝐷 : 𝑋 ⟶ ℝ )
hoiqssbllem2.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
hoiqssbllem2.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
hoiqssbllem2.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
Assertion hoiqssbllem2 ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )

Proof

Step Hyp Ref Expression
1 hoiqssbllem2.i ⊢ Ⅎ 𝑖 𝜑
2 hoiqssbllem2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hoiqssbllem2.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
4 hoiqssbllem2.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
5 hoiqssbllem2.c ⊢ ( 𝜑 → 𝐶 : 𝑋 ⟶ ℝ )
6 hoiqssbllem2.d ⊢ ( 𝜑 → 𝐷 : 𝑋 ⟶ ℝ )
7 hoiqssbllem2.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8 hoiqssbllem2.l ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
9 hoiqssbllem2.r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
10 eqid ⊢ ( ℝ^ ‘ 𝑋 ) = ( ℝ^ ‘ 𝑋 )
11 eqid ⊢ ( ℝ ↑m 𝑋 ) = ( ℝ ↑m 𝑋 )
12 10 11 rrxdsfi ⊢ ( 𝑋 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) , ℎ ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) ) ) )
13 2 12 syl ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) , ℎ ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) ) ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( 𝑔 ∈ ( ℝ ↑m 𝑋 ) , ℎ ∈ ( ℝ ↑m 𝑋 ) ↦ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) ) ) )
15 fveq1 ⊢ ( 𝑔 = 𝑌 → ( 𝑔 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
16 15 adantr ⊢ ( ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑖 ) )
17 fveq1 ⊢ ( ℎ = 𝑓 → ( ℎ ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
18 17 adantl ⊢ ( ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) → ( ℎ ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
19 16 18 oveq12d ⊢ ( ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) → ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) = ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) )
20 19 oveq1d ⊢ ( ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) → ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
21 20 sumeq2sdv ⊢ ( ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
22 21 fveq2d ⊢ ( ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ ( 𝑔 = 𝑌 ∧ ℎ = 𝑓 ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑔 ‘ 𝑖 ) − ( ℎ ‘ 𝑖 ) ) ↑ 2 ) ) = ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) )
24 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
25 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
26 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ )
27 26 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ* )
28 1 25 27 hoissrrn2 ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( ℝ ↑m 𝑋 ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
31 29 30 sseldd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( ℝ ↑m 𝑋 ) )
32 fvexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ V )
33 14 23 24 31 32 ovmpod ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) = ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) )
34 nfcv ⊢ Ⅎ 𝑖 𝑓
35 nfixp1 ⊢ Ⅎ 𝑖 X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) )
36 34 35 nfel ⊢ Ⅎ 𝑖 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) )
37 1 36 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
38 simpl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝜑 )
39 38 2 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑋 ∈ Fin )
40 elmapi ⊢ ( 𝑌 ∈ ( ℝ ↑m 𝑋 ) → 𝑌 : 𝑋 ⟶ ℝ )
41 4 40 syl ⊢ ( 𝜑 → 𝑌 : 𝑋 ⟶ ℝ )
42 41 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ )
43 38 42 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ )
44 icossre ⊢ ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℝ* ) → ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ℝ )
45 25 27 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ℝ )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ℝ )
47 fvixp2 ⊢ ( ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
48 47 adantll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
49 46 48 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑖 ) ∈ ℝ )
50 43 49 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ∈ ℝ )
51 2nn0 ⊢ 2 ∈ ℕ0
52 51 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 2 ∈ ℕ0 )
53 50 52 reexpcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
54 37 39 53 fsumreclf ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
55 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐶 ‘ 𝑖 ) = ( 𝐶 ‘ 𝑗 ) )
56 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ 𝑗 ) )
57 55 56 oveq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
58 57 cbvixpv ⊢ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) = X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) )
59 58 eleq2i ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ↔ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
60 59 bilani ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
61 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑋 ∈ Fin )
62 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝜑 )
63 59 biimpri ⊢ ( 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
64 63 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
65 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
66 62 64 65 53 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
67 50 sqge0d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
68 62 64 65 67 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
69 61 66 68 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
70 38 60 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
71 54 70 resqrtcld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
72 33 71 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) ∈ ℝ )
73 26 25 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
74 73 resqcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
75 2 74 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
76 73 sqge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
77 2 74 76 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
78 75 77 resqrtcld ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
80 7 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝐸 ∈ ℝ )
82 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑋 ≠ ∅ )
83 74 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
84 38 26 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ )
85 38 25 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
86 84 85 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
87 25 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ* )
88 42 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ* )
89 2rp ⊢ 2 ∈ ℝ+
90 89 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
91 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
92 2 91 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
93 3 92 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
94 93 nnred ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ )
95 93 nngt0d ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑋 ) )
96 94 95 elrpd ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ+ )
97 96 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℝ+ )
98 90 97 rpmulcld ⊢ ( 𝜑 → ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ+ )
99 7 98 rpdivcld ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ+ )
100 99 rpred ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
101 100 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
102 42 101 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
103 102 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
104 iooltub ⊢ ( ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( 𝐶 ‘ 𝑖 ) < ( 𝑌 ‘ 𝑖 ) )
105 103 88 8 104 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) < ( 𝑌 ‘ 𝑖 ) )
106 25 42 105 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ≤ ( 𝑌 ‘ 𝑖 ) )
107 42 101 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
108 107 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
109 ioogtlb ⊢ ( ( ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝑌 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
110 88 108 9 109 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
111 87 27 88 106 110 elicod ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
112 38 111 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
113 icodiamlt ⊢ ( ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℝ ) ∧ ( ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) → ( abs ‘ ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ) < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
114 85 84 112 48 113 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ) < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
115 0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ∈ ℝ )
116 25 42 26 106 110 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
117 25 26 posdifd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) ↔ 0 < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
118 116 117 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
119 115 73 118 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
120 73 119 absidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
121 120 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
122 121 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
123 114 122 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ) < ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
124 50 86 123 abslt2sqd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
125 62 64 65 124 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
126 61 82 66 83 125 fsumlt ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
127 38 60 126 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
128 38 75 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
129 38 77 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
130 54 70 128 129 sqrtltd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ↔ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
131 127 130 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) )
132 33 131 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) )
133 80 97 rerpdivcld ⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ )
134 133 resqcld ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℝ )
135 134 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℝ )
136 26 25 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) )
137 107 102 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ) )
138 136 137 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) ∧ ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ) ) )
139 iooltub ⊢ ( ( ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
140 88 108 9 139 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
141 ioogtlb ⊢ ( ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) )
142 103 88 8 141 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) )
143 140 142 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) ) )
144 lt2sub ⊢ ( ( ( ( 𝐷 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) ∧ ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ) ) → ( ( ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
145 138 143 144 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
146 42 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℂ )
147 101 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℂ )
148 146 147 147 pnncand ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) = ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
149 80 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
150 97 rpcnd ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℂ )
151 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
152 97 rpne0d ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ≠ 0 )
153 90 rpne0d ⊢ ( 𝜑 → 2 ≠ 0 )
154 149 150 151 152 153 divdiv3d ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) = ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) )
155 154 eqcomd ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) = ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) )
156 155 155 oveq12d ⊢ ( 𝜑 → ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) + ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) ) )
157 149 150 152 divcld ⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℂ )
158 157 2halvesd ⊢ ( 𝜑 → ( ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) + ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
159 156 158 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
161 148 160 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
162 145 161 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
163 133 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ )
164 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
165 97 rpred ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℝ )
166 7 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
167 97 rpgt0d ⊢ ( 𝜑 → 0 < ( √ ‘ ( ♯ ‘ 𝑋 ) ) )
168 80 165 166 167 divgt0d ⊢ ( 𝜑 → 0 < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
169 164 133 168 ltled ⊢ ( 𝜑 → 0 ≤ ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
170 169 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
171 lt2sq ⊢ ( ( ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↔ ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
172 73 119 163 170 171 syl22anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↔ ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
173 162 172 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
174 2 3 74 135 173 fsumlt ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
175 2 135 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℝ )
176 163 sqge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
177 2 135 176 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
178 75 77 175 177 sqrtltd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ↔ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) ) )
179 174 178 mpbid ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
180 134 recnd ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℂ )
181 fsumconst ⊢ ( ( 𝑋 ∈ Fin ∧ ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℂ ) → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
182 2 180 181 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
183 sqdiv ⊢ ( ( 𝐸 ∈ ℂ ∧ ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℂ ∧ ( √ ‘ ( ♯ ‘ 𝑋 ) ) ≠ 0 ) → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) / ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) ) )
184 149 150 152 183 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) / ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) ) )
185 94 recnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℂ )
186 sqrtth ⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℂ → ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) = ( ♯ ‘ 𝑋 ) )
187 185 186 syl ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) = ( ♯ ‘ 𝑋 ) )
188 187 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) / ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) )
189 184 188 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) )
190 189 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) = ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) ) )
191 149 sqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
192 164 95 gtned ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ≠ 0 )
193 191 185 192 divcan2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) ) = ( 𝐸 ↑ 2 ) )
194 182 190 193 3eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( 𝐸 ↑ 2 ) )
195 194 fveq2d ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) = ( √ ‘ ( 𝐸 ↑ 2 ) ) )
196 164 80 166 ltled ⊢ ( 𝜑 → 0 ≤ 𝐸 )
197 sqrtsq ⊢ ( ( 𝐸 ∈ ℝ ∧ 0 ≤ 𝐸 ) → ( √ ‘ ( 𝐸 ↑ 2 ) ) = 𝐸 )
198 80 196 197 syl2anc ⊢ ( 𝜑 → ( √ ‘ ( 𝐸 ↑ 2 ) ) = 𝐸 )
199 eqidd ⊢ ( 𝜑 → 𝐸 = 𝐸 )
200 195 198 199 3eqtrd ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) = 𝐸 )
201 179 200 breqtrd ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < 𝐸 )
202 201 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < 𝐸 )
203 72 79 81 132 202 lttrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < 𝐸 )
204 eqid ⊢ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( dist ‘ ( ℝ^ ‘ 𝑋 ) )
205 204 rrxmetfi ⊢ ( 𝑋 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
206 metxmet ⊢ ( ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
207 2 205 206 3syl ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
208 207 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
209 81 rexrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝐸 ∈ ℝ* )
210 31 11 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( ℝ ↑m 𝑋 ) )
211 elbl2 ⊢ ( ( ( ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) ∧ 𝐸 ∈ ℝ* ) ∧ ( 𝑌 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ) → ( 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < 𝐸 ) )
212 208 209 24 210 211 syl22anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < 𝐸 ) )
213 203 212 mpbird ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
214 213 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
215 dfss3 ⊢ ( X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
216 214 215 sylibr ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )