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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
26 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ )
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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ )
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 biimpi ⊢ ( 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) → 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) )
62 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑋 ∈ Fin )
63 simpll ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝜑 )
64 59 biimpri ⊢ ( 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
65 64 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
66 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
67 63 65 66 53 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
68 50 sqge0d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
69 63 65 66 68 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
70 62 67 69 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
71 38 61 70 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) )
72 54 71 resqrtcld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
73 33 72 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) ∈ ℝ )
74 26 25 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
75 74 resqcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
76 2 75 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
77 74 sqge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
78 2 75 77 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
79 76 78 resqrtcld ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
81 7 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝐸 ∈ ℝ )
83 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → 𝑋 ≠ ∅ )
84 75 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
85 38 26 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ )
86 38 25 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
87 85 86 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
88 25 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ* )
89 42 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ* )
90 2rp ⊢ 2 ∈ ℝ+
91 90 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
92 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
93 2 92 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
94 3 93 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
95 94 nnred ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ )
96 94 nngt0d ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑋 ) )
97 95 96 elrpd ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ+ )
98 97 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℝ+ )
99 91 98 rpmulcld ⊢ ( 𝜑 → ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ+ )
100 7 99 rpdivcld ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ+ )
101 100 rpred ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
103 42 102 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
104 103 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
105 iooltub ⊢ ( ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( 𝐶 ‘ 𝑖 ) < ( 𝑌 ‘ 𝑖 ) )
106 104 89 8 105 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) < ( 𝑌 ‘ 𝑖 ) )
107 25 42 106 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ≤ ( 𝑌 ‘ 𝑖 ) )
108 42 102 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
109 108 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
110 ioogtlb ⊢ ( ( ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝑌 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
111 89 109 9 110 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
112 88 27 89 107 111 elicod ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
113 38 112 sylan ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
114 icodiamlt ⊢ ( ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℝ ) ∧ ( ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ∧ ( 𝑓 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ) → ( abs ‘ ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ) < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
115 86 85 113 48 114 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ) < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
116 0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ∈ ℝ )
117 25 42 26 107 111 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
118 25 26 posdifd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐶 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) ↔ 0 < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
119 117 118 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 < ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
120 116 74 119 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
121 74 120 absidd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) = ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) )
122 121 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
123 122 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) = ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
124 115 123 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ) < ( abs ‘ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) )
125 50 87 124 abslt2sqd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
126 63 65 66 125 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
127 62 83 67 84 126 fsumlt ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑗 ∈ 𝑋 ( ( 𝐶 ‘ 𝑗 ) [,) ( 𝐷 ‘ 𝑗 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
128 38 61 127 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
129 38 76 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
130 38 78 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) )
131 54 71 129 130 sqrtltd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ↔ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
132 128 131 mpbid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝑓 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) )
133 33 132 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) )
134 81 98 rerpdivcld ⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ )
135 134 resqcld ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℝ )
136 135 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℝ )
137 26 25 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) )
138 108 103 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ) )
139 137 138 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) ∧ ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ) ) )
140 iooltub ⊢ ( ( ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
141 89 109 9 140 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
142 ioogtlb ⊢ ( ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) )
143 104 89 8 142 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) )
144 141 143 jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) ) )
145 lt2sub ⊢ ( ( ( ( 𝐷 ‘ 𝑖 ) ∈ ℝ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℝ ) ∧ ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ ) ) → ( ( ( 𝐷 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∧ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝐶 ‘ 𝑖 ) ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
146 139 144 145 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
147 42 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℂ )
148 102 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℂ )
149 147 148 148 pnncand ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) = ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
150 81 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
151 98 rpcnd ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℂ )
152 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
153 98 rpne0d ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ≠ 0 )
154 91 rpne0d ⊢ ( 𝜑 → 2 ≠ 0 )
155 150 151 152 153 154 divdiv3d ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) = ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) )
156 155 eqcomd ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) = ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) )
157 156 156 oveq12d ⊢ ( 𝜑 → ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) + ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) ) )
158 150 151 153 divcld ⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℂ )
159 158 2halvesd ⊢ ( 𝜑 → ( ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) + ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) / 2 ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
160 157 159 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
161 160 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
162 149 161 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) − ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
163 146 162 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
164 134 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ )
165 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
166 98 rpred ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℝ )
167 7 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
168 98 rpgt0d ⊢ ( 𝜑 → 0 < ( √ ‘ ( ♯ ‘ 𝑋 ) ) )
169 81 166 167 168 divgt0d ⊢ ( 𝜑 → 0 < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
170 165 134 169 ltled ⊢ ( 𝜑 → 0 ≤ ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
171 170 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) )
172 lt2sq ⊢ ( ( ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↔ ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
173 74 120 164 171 172 syl22anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↔ ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
174 163 173 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
175 2 3 75 136 174 fsumlt ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
176 2 136 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℝ )
177 164 sqge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 0 ≤ ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
178 2 136 177 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) )
179 76 78 176 178 sqrtltd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) < Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ↔ ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) ) )
180 175 179 mpbid ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
181 135 recnd ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℂ )
182 fsumconst ⊢ ( ( 𝑋 ∈ Fin ∧ ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ∈ ℂ ) → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
183 2 181 182 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) )
184 sqdiv ⊢ ( ( 𝐸 ∈ ℂ ∧ ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℂ ∧ ( √ ‘ ( ♯ ‘ 𝑋 ) ) ≠ 0 ) → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) / ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) ) )
185 150 151 153 184 syl3anc ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) / ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) ) )
186 95 recnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℂ )
187 sqrtth ⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℂ → ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) = ( ♯ ‘ 𝑋 ) )
188 186 187 syl ⊢ ( 𝜑 → ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) = ( ♯ ‘ 𝑋 ) )
189 188 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 ↑ 2 ) / ( ( √ ‘ ( ♯ ‘ 𝑋 ) ) ↑ 2 ) ) = ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) )
190 185 189 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) )
191 190 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) = ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) ) )
192 150 sqcld ⊢ ( 𝜑 → ( 𝐸 ↑ 2 ) ∈ ℂ )
193 165 96 gtned ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ≠ 0 )
194 192 186 193 divcan2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) · ( ( 𝐸 ↑ 2 ) / ( ♯ ‘ 𝑋 ) ) ) = ( 𝐸 ↑ 2 ) )
195 183 191 194 3eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) = ( 𝐸 ↑ 2 ) )
196 195 fveq2d ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) = ( √ ‘ ( 𝐸 ↑ 2 ) ) )
197 165 81 167 ltled ⊢ ( 𝜑 → 0 ≤ 𝐸 )
198 sqrtsq ⊢ ( ( 𝐸 ∈ ℝ ∧ 0 ≤ 𝐸 ) → ( √ ‘ ( 𝐸 ↑ 2 ) ) = 𝐸 )
199 81 197 198 syl2anc ⊢ ( 𝜑 → ( √ ‘ ( 𝐸 ↑ 2 ) ) = 𝐸 )
200 eqidd ⊢ ( 𝜑 → 𝐸 = 𝐸 )
201 196 199 200 3eqtrd ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ↑ 2 ) ) = 𝐸 )
202 180 201 breqtrd ⊢ ( 𝜑 → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < 𝐸 )
203 202 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( √ ‘ Σ 𝑖 ∈ 𝑋 ( ( ( 𝐷 ‘ 𝑖 ) − ( 𝐶 ‘ 𝑖 ) ) ↑ 2 ) ) < 𝐸 )
204 73 80 82 133 203 lttrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < 𝐸 )
205 eqid ⊢ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) = ( dist ‘ ( ℝ^ ‘ 𝑋 ) )
206 205 rrxmetfi ⊢ ( 𝑋 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) )
207 metxmet ⊢ ( ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( Met ‘ ( ℝ ↑m 𝑋 ) ) → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
208 2 206 207 3syl ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
209 208 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) )
210 82 rexrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝐸 ∈ ℝ* )
211 31 11 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( ℝ ↑m 𝑋 ) )
212 elbl2 ⊢ ( ( ( ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ∈ ( ∞Met ‘ ( ℝ ↑m 𝑋 ) ) ∧ 𝐸 ∈ ℝ* ) ∧ ( 𝑌 ∈ ( ℝ ↑m 𝑋 ) ∧ 𝑓 ∈ ( ℝ ↑m 𝑋 ) ) ) → ( 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < 𝐸 ) )
213 209 210 24 211 212 syl22anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → ( 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ ( 𝑌 ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) 𝑓 ) < 𝐸 ) )
214 204 213 mpbird ⊢ ( ( 𝜑 ∧ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) → 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
215 214 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
216 dfss3 ⊢ ( X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ↔ ∀ 𝑓 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) 𝑓 ∈ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
217 215 216 sylibr ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )