Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoiqssbllem2 Structured version   Visualization version   GIF version

Theorem hoiqssbllem2 43277
 Description: The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
hoiqssbllem2.i 𝑖𝜑
hoiqssbllem2.x (𝜑𝑋 ∈ Fin)
hoiqssbllem2.n (𝜑𝑋 ≠ ∅)
hoiqssbllem2.y (𝜑𝑌 ∈ (ℝ ↑m 𝑋))
hoiqssbllem2.c (𝜑𝐶:𝑋⟶ℝ)
hoiqssbllem2.d (𝜑𝐷:𝑋⟶ℝ)
hoiqssbllem2.e (𝜑𝐸 ∈ ℝ+)
hoiqssbllem2.l ((𝜑𝑖𝑋) → (𝐶𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
hoiqssbllem2.r ((𝜑𝑖𝑋) → (𝐷𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
Assertion
Ref Expression
hoiqssbllem2 (𝜑X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
Distinct variable groups:   𝐶,𝑖   𝐷,𝑖   𝑖,𝐸   𝑖,𝑋   𝑖,𝑌   𝜑,𝑖

Proof of Theorem hoiqssbllem2
Dummy variables 𝑓 𝑔 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoiqssbllem2.x . . . . . . . . 9 (𝜑𝑋 ∈ Fin)
2 eqid 2798 . . . . . . . . . 10 (ℝ^‘𝑋) = (ℝ^‘𝑋)
3 eqid 2798 . . . . . . . . . 10 (ℝ ↑m 𝑋) = (ℝ ↑m 𝑋)
42, 3rrxdsfi 24022 . . . . . . . . 9 (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑m 𝑋), ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑖𝑋 (((𝑔𝑖) − (𝑖))↑2))))
51, 4syl 17 . . . . . . . 8 (𝜑 → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑m 𝑋), ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑖𝑋 (((𝑔𝑖) − (𝑖))↑2))))
65adantr 484 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑m 𝑋), ∈ (ℝ ↑m 𝑋) ↦ (√‘Σ𝑖𝑋 (((𝑔𝑖) − (𝑖))↑2))))
7 fveq1 6644 . . . . . . . . . . . . 13 (𝑔 = 𝑌 → (𝑔𝑖) = (𝑌𝑖))
87adantr 484 . . . . . . . . . . . 12 ((𝑔 = 𝑌 = 𝑓) → (𝑔𝑖) = (𝑌𝑖))
9 fveq1 6644 . . . . . . . . . . . . 13 ( = 𝑓 → (𝑖) = (𝑓𝑖))
109adantl 485 . . . . . . . . . . . 12 ((𝑔 = 𝑌 = 𝑓) → (𝑖) = (𝑓𝑖))
118, 10oveq12d 7153 . . . . . . . . . . 11 ((𝑔 = 𝑌 = 𝑓) → ((𝑔𝑖) − (𝑖)) = ((𝑌𝑖) − (𝑓𝑖)))
1211oveq1d 7150 . . . . . . . . . 10 ((𝑔 = 𝑌 = 𝑓) → (((𝑔𝑖) − (𝑖))↑2) = (((𝑌𝑖) − (𝑓𝑖))↑2))
1312sumeq2sdv 15055 . . . . . . . . 9 ((𝑔 = 𝑌 = 𝑓) → Σ𝑖𝑋 (((𝑔𝑖) − (𝑖))↑2) = Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2))
1413fveq2d 6649 . . . . . . . 8 ((𝑔 = 𝑌 = 𝑓) → (√‘Σ𝑖𝑋 (((𝑔𝑖) − (𝑖))↑2)) = (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)))
1514adantl 485 . . . . . . 7 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ (𝑔 = 𝑌 = 𝑓)) → (√‘Σ𝑖𝑋 (((𝑔𝑖) − (𝑖))↑2)) = (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)))
16 hoiqssbllem2.y . . . . . . . 8 (𝜑𝑌 ∈ (ℝ ↑m 𝑋))
1716adantr 484 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑌 ∈ (ℝ ↑m 𝑋))
18 hoiqssbllem2.i . . . . . . . . . 10 𝑖𝜑
19 hoiqssbllem2.c . . . . . . . . . . 11 (𝜑𝐶:𝑋⟶ℝ)
2019ffvelrnda 6828 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝐶𝑖) ∈ ℝ)
21 hoiqssbllem2.d . . . . . . . . . . . 12 (𝜑𝐷:𝑋⟶ℝ)
2221ffvelrnda 6828 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐷𝑖) ∈ ℝ)
2322rexrd 10682 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝐷𝑖) ∈ ℝ*)
2418, 20, 23hoissrrn2 43232 . . . . . . . . 9 (𝜑X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ (ℝ ↑m 𝑋))
2524adantr 484 . . . . . . . 8 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ (ℝ ↑m 𝑋))
26 simpr 488 . . . . . . . 8 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)))
2725, 26sseldd 3916 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑓 ∈ (ℝ ↑m 𝑋))
28 fvexd 6660 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)) ∈ V)
296, 15, 17, 27, 28ovmpod 7282 . . . . . 6 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) = (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)))
30 nfcv 2955 . . . . . . . . . 10 𝑖𝑓
31 nfixp1 8467 . . . . . . . . . 10 𝑖X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))
3230, 31nfel 2969 . . . . . . . . 9 𝑖 𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))
3318, 32nfan 1900 . . . . . . . 8 𝑖(𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)))
34 simpl 486 . . . . . . . . 9 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝜑)
3534, 1syl 17 . . . . . . . 8 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑋 ∈ Fin)
36 elmapi 8413 . . . . . . . . . . . . 13 (𝑌 ∈ (ℝ ↑m 𝑋) → 𝑌:𝑋⟶ℝ)
3716, 36syl 17 . . . . . . . . . . . 12 (𝜑𝑌:𝑋⟶ℝ)
3837ffvelrnda 6828 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝑌𝑖) ∈ ℝ)
3934, 38sylan 583 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (𝑌𝑖) ∈ ℝ)
40 icossre 12808 . . . . . . . . . . . . 13 (((𝐶𝑖) ∈ ℝ ∧ (𝐷𝑖) ∈ ℝ*) → ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ ℝ)
4120, 23, 40syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ ℝ)
4241adantlr 714 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ ℝ)
43 fvixp2 41842 . . . . . . . . . . . 12 ((𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐶𝑖)[,)(𝐷𝑖)))
4443adantll 713 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐶𝑖)[,)(𝐷𝑖)))
4542, 44sseldd 3916 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
4639, 45resubcld 11059 . . . . . . . . 9 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → ((𝑌𝑖) − (𝑓𝑖)) ∈ ℝ)
47 2nn0 11904 . . . . . . . . . 10 2 ∈ ℕ0
4847a1i 11 . . . . . . . . 9 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → 2 ∈ ℕ0)
4946, 48reexpcld 13525 . . . . . . . 8 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (((𝑌𝑖) − (𝑓𝑖))↑2) ∈ ℝ)
5033, 35, 49fsumreclf 42233 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2) ∈ ℝ)
51 fveq2 6645 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝐶𝑖) = (𝐶𝑗))
52 fveq2 6645 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝐷𝑖) = (𝐷𝑗))
5351, 52oveq12d 7153 . . . . . . . . . . . 12 (𝑖 = 𝑗 → ((𝐶𝑖)[,)(𝐷𝑖)) = ((𝐶𝑗)[,)(𝐷𝑗)))
5453cbvixpv 8464 . . . . . . . . . . 11 X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) = X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))
5554eleq2i 2881 . . . . . . . . . 10 (𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ↔ 𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗)))
5655biimpi 219 . . . . . . . . 9 (𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) → 𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗)))
5756adantl 485 . . . . . . . 8 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗)))
581adantr 484 . . . . . . . . 9 ((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) → 𝑋 ∈ Fin)
59 simpll 766 . . . . . . . . . 10 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → 𝜑)
6055biimpri 231 . . . . . . . . . . 11 (𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗)) → 𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)))
6160ad2antlr 726 . . . . . . . . . 10 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → 𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)))
62 simpr 488 . . . . . . . . . 10 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → 𝑖𝑋)
6359, 61, 62, 49syl21anc 836 . . . . . . . . 9 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → (((𝑌𝑖) − (𝑓𝑖))↑2) ∈ ℝ)
6446sqge0d 13610 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → 0 ≤ (((𝑌𝑖) − (𝑓𝑖))↑2))
6559, 61, 62, 64syl21anc 836 . . . . . . . . 9 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → 0 ≤ (((𝑌𝑖) − (𝑓𝑖))↑2))
6658, 63, 65fsumge0 15144 . . . . . . . 8 ((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) → 0 ≤ Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2))
6734, 57, 66syl2anc 587 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 0 ≤ Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2))
6850, 67resqrtcld 14771 . . . . . 6 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)) ∈ ℝ)
6929, 68eqeltrd 2890 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) ∈ ℝ)
7022, 20resubcld 11059 . . . . . . . . 9 ((𝜑𝑖𝑋) → ((𝐷𝑖) − (𝐶𝑖)) ∈ ℝ)
7170resqcld 13609 . . . . . . . 8 ((𝜑𝑖𝑋) → (((𝐷𝑖) − (𝐶𝑖))↑2) ∈ ℝ)
721, 71fsumrecl 15085 . . . . . . 7 (𝜑 → Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2) ∈ ℝ)
7370sqge0d 13610 . . . . . . . 8 ((𝜑𝑖𝑋) → 0 ≤ (((𝐷𝑖) − (𝐶𝑖))↑2))
741, 71, 73fsumge0 15144 . . . . . . 7 (𝜑 → 0 ≤ Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2))
7572, 74resqrtcld 14771 . . . . . 6 (𝜑 → (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)) ∈ ℝ)
7675adantr 484 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)) ∈ ℝ)
77 hoiqssbllem2.e . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
7877rpred 12421 . . . . . 6 (𝜑𝐸 ∈ ℝ)
7978adantr 484 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝐸 ∈ ℝ)
80 hoiqssbllem2.n . . . . . . . . . 10 (𝜑𝑋 ≠ ∅)
8180adantr 484 . . . . . . . . 9 ((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) → 𝑋 ≠ ∅)
8271adantlr 714 . . . . . . . . 9 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → (((𝐷𝑖) − (𝐶𝑖))↑2) ∈ ℝ)
8334, 22sylan 583 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (𝐷𝑖) ∈ ℝ)
8434, 20sylan 583 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (𝐶𝑖) ∈ ℝ)
8583, 84resubcld 11059 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → ((𝐷𝑖) − (𝐶𝑖)) ∈ ℝ)
8620rexrd 10682 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝐶𝑖) ∈ ℝ*)
8738rexrd 10682 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝑌𝑖) ∈ ℝ*)
88 2rp 12384 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℝ+
8988a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 2 ∈ ℝ+)
90 hashnncl 13725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
911, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
9280, 91mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (♯‘𝑋) ∈ ℕ)
9392nnred 11642 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (♯‘𝑋) ∈ ℝ)
9492nngt0d 11676 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 0 < (♯‘𝑋))
9593, 94elrpd 12418 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (♯‘𝑋) ∈ ℝ+)
9695rpsqrtcld 14765 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ+)
9789, 96rpmulcld 12437 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (2 · (√‘(♯‘𝑋))) ∈ ℝ+)
9877, 97rpdivcld 12438 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ+)
9998rpred 12421 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
10099adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
10138, 100resubcld 11059 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖𝑋) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
102101rexrd 10682 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ*)
103 hoiqssbllem2.l . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋) → (𝐶𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
104 iooltub 42162 . . . . . . . . . . . . . . . . 17 ((((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ* ∧ (𝑌𝑖) ∈ ℝ* ∧ (𝐶𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) → (𝐶𝑖) < (𝑌𝑖))
105102, 87, 103, 104syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → (𝐶𝑖) < (𝑌𝑖))
10620, 38, 105ltled 10779 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝐶𝑖) ≤ (𝑌𝑖))
10738, 100readdcld 10661 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋) → ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
108107rexrd 10682 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ*)
109 hoiqssbllem2.r . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → (𝐷𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
110 ioogtlb 42147 . . . . . . . . . . . . . . . 16 (((𝑌𝑖) ∈ ℝ* ∧ ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ* ∧ (𝐷𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝑌𝑖) < (𝐷𝑖))
11187, 108, 109, 110syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝑌𝑖) < (𝐷𝑖))
11286, 23, 87, 106, 111elicod 12777 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝑌𝑖) ∈ ((𝐶𝑖)[,)(𝐷𝑖)))
11334, 112sylan 583 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (𝑌𝑖) ∈ ((𝐶𝑖)[,)(𝐷𝑖)))
114 icodiamlt 14789 . . . . . . . . . . . . 13 ((((𝐶𝑖) ∈ ℝ ∧ (𝐷𝑖) ∈ ℝ) ∧ ((𝑌𝑖) ∈ ((𝐶𝑖)[,)(𝐷𝑖)) ∧ (𝑓𝑖) ∈ ((𝐶𝑖)[,)(𝐷𝑖)))) → (abs‘((𝑌𝑖) − (𝑓𝑖))) < ((𝐷𝑖) − (𝐶𝑖)))
11584, 83, 113, 44, 114syl22anc 837 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (abs‘((𝑌𝑖) − (𝑓𝑖))) < ((𝐷𝑖) − (𝐶𝑖)))
116 0red 10635 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → 0 ∈ ℝ)
11720, 38, 22, 106, 111lelttrd 10789 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋) → (𝐶𝑖) < (𝐷𝑖))
11820, 22posdifd 11218 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖𝑋) → ((𝐶𝑖) < (𝐷𝑖) ↔ 0 < ((𝐷𝑖) − (𝐶𝑖))))
119117, 118mpbid 235 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → 0 < ((𝐷𝑖) − (𝐶𝑖)))
120116, 70, 119ltled 10779 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 0 ≤ ((𝐷𝑖) − (𝐶𝑖)))
12170, 120absidd 14776 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (abs‘((𝐷𝑖) − (𝐶𝑖))) = ((𝐷𝑖) − (𝐶𝑖)))
122121eqcomd 2804 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐷𝑖) − (𝐶𝑖)) = (abs‘((𝐷𝑖) − (𝐶𝑖))))
123122adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → ((𝐷𝑖) − (𝐶𝑖)) = (abs‘((𝐷𝑖) − (𝐶𝑖))))
124115, 123breqtrd 5056 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (abs‘((𝑌𝑖) − (𝑓𝑖))) < (abs‘((𝐷𝑖) − (𝐶𝑖))))
12546, 85, 124abslt2sqd 42007 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) ∧ 𝑖𝑋) → (((𝑌𝑖) − (𝑓𝑖))↑2) < (((𝐷𝑖) − (𝐶𝑖))↑2))
12659, 61, 62, 125syl21anc 836 . . . . . . . . 9 (((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) ∧ 𝑖𝑋) → (((𝑌𝑖) − (𝑓𝑖))↑2) < (((𝐷𝑖) − (𝐶𝑖))↑2))
12758, 81, 63, 82, 126fsumlt 15149 . . . . . . . 8 ((𝜑𝑓X𝑗𝑋 ((𝐶𝑗)[,)(𝐷𝑗))) → Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2) < Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2))
12834, 57, 127syl2anc 587 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2) < Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2))
12934, 72syl 17 . . . . . . . 8 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2) ∈ ℝ)
13034, 74syl 17 . . . . . . . 8 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 0 ≤ Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2))
13150, 67, 129, 130sqrtltd 14781 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2) < Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2) ↔ (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)) < (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2))))
132128, 131mpbid 235 . . . . . 6 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (√‘Σ𝑖𝑋 (((𝑌𝑖) − (𝑓𝑖))↑2)) < (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)))
13329, 132eqbrtrd 5052 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)))
13478, 96rerpdivcld 12452 . . . . . . . . . . 11 (𝜑 → (𝐸 / (√‘(♯‘𝑋))) ∈ ℝ)
135134resqcld 13609 . . . . . . . . . 10 (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
136135adantr 484 . . . . . . . . 9 ((𝜑𝑖𝑋) → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
13722, 20jca 515 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝐷𝑖) ∈ ℝ ∧ (𝐶𝑖) ∈ ℝ))
138107, 101jca 515 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ))
139137, 138jca 515 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (((𝐷𝑖) ∈ ℝ ∧ (𝐶𝑖) ∈ ℝ) ∧ (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)))
140 iooltub 42162 . . . . . . . . . . . . . 14 (((𝑌𝑖) ∈ ℝ* ∧ ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ* ∧ (𝐷𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝐷𝑖) < ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
14187, 108, 109, 140syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐷𝑖) < ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
142 ioogtlb 42147 . . . . . . . . . . . . . 14 ((((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ* ∧ (𝑌𝑖) ∈ ℝ* ∧ (𝐶𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶𝑖))
143102, 87, 103, 142syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶𝑖))
144141, 143jca 515 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐷𝑖) < ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∧ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶𝑖)))
145 lt2sub 11129 . . . . . . . . . . . 12 ((((𝐷𝑖) ∈ ℝ ∧ (𝐶𝑖) ∈ ℝ) ∧ (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)) → (((𝐷𝑖) < ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∧ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶𝑖)) → ((𝐷𝑖) − (𝐶𝑖)) < (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))))))
146139, 144, 145sylc 65 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝐷𝑖) − (𝐶𝑖)) < (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))))
14738recnd 10660 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝑌𝑖) ∈ ℂ)
148100recnd 10660 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℂ)
149147, 148, 148pnncand 11027 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))) = ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
15078recnd 10660 . . . . . . . . . . . . . . . . 17 (𝜑𝐸 ∈ ℂ)
15196rpcnd 12423 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(♯‘𝑋)) ∈ ℂ)
152 2cnd 11705 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ∈ ℂ)
15396rpne0d 12426 . . . . . . . . . . . . . . . . 17 (𝜑 → (√‘(♯‘𝑋)) ≠ 0)
15489rpne0d 12426 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 ≠ 0)
155150, 151, 152, 153, 154divdiv3d 42006 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐸 / (√‘(♯‘𝑋))) / 2) = (𝐸 / (2 · (√‘(♯‘𝑋)))))
156155eqcomd 2804 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) = ((𝐸 / (√‘(♯‘𝑋))) / 2))
157156, 156oveq12d 7153 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (((𝐸 / (√‘(♯‘𝑋))) / 2) + ((𝐸 / (√‘(♯‘𝑋))) / 2)))
158150, 151, 153divcld 11407 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸 / (√‘(♯‘𝑋))) ∈ ℂ)
1591582halvesd 11873 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸 / (√‘(♯‘𝑋))) / 2) + ((𝐸 / (√‘(♯‘𝑋))) / 2)) = (𝐸 / (√‘(♯‘𝑋))))
160157, 159eqtrd 2833 . . . . . . . . . . . . 13 (𝜑 → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (𝐸 / (√‘(♯‘𝑋))))
161160adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (𝐸 / (√‘(♯‘𝑋))))
162149, 161eqtrd 2833 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))) = (𝐸 / (√‘(♯‘𝑋))))
163146, 162breqtrd 5056 . . . . . . . . . 10 ((𝜑𝑖𝑋) → ((𝐷𝑖) − (𝐶𝑖)) < (𝐸 / (√‘(♯‘𝑋))))
164134adantr 484 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐸 / (√‘(♯‘𝑋))) ∈ ℝ)
165 0red 10635 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
16696rpred 12421 . . . . . . . . . . . . . 14 (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ)
16777rpgt0d 12424 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝐸)
16896rpgt0d 12424 . . . . . . . . . . . . . 14 (𝜑 → 0 < (√‘(♯‘𝑋)))
16978, 166, 167, 168divgt0d 11566 . . . . . . . . . . . . 13 (𝜑 → 0 < (𝐸 / (√‘(♯‘𝑋))))
170165, 134, 169ltled 10779 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝐸 / (√‘(♯‘𝑋))))
171170adantr 484 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → 0 ≤ (𝐸 / (√‘(♯‘𝑋))))
172 lt2sq 13496 . . . . . . . . . . 11 (((((𝐷𝑖) − (𝐶𝑖)) ∈ ℝ ∧ 0 ≤ ((𝐷𝑖) − (𝐶𝑖))) ∧ ((𝐸 / (√‘(♯‘𝑋))) ∈ ℝ ∧ 0 ≤ (𝐸 / (√‘(♯‘𝑋))))) → (((𝐷𝑖) − (𝐶𝑖)) < (𝐸 / (√‘(♯‘𝑋))) ↔ (((𝐷𝑖) − (𝐶𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2)))
17370, 120, 164, 171, 172syl22anc 837 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (((𝐷𝑖) − (𝐶𝑖)) < (𝐸 / (√‘(♯‘𝑋))) ↔ (((𝐷𝑖) − (𝐶𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2)))
174163, 173mpbid 235 . . . . . . . . 9 ((𝜑𝑖𝑋) → (((𝐷𝑖) − (𝐶𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2))
1751, 80, 71, 136, 174fsumlt 15149 . . . . . . . 8 (𝜑 → Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2) < Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))
1761, 136fsumrecl 15085 . . . . . . . . 9 (𝜑 → Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
177164sqge0d 13610 . . . . . . . . . 10 ((𝜑𝑖𝑋) → 0 ≤ ((𝐸 / (√‘(♯‘𝑋)))↑2))
1781, 136, 177fsumge0 15144 . . . . . . . . 9 (𝜑 → 0 ≤ Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))
17972, 74, 176, 178sqrtltd 14781 . . . . . . . 8 (𝜑 → (Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2) < Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) ↔ (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)) < (√‘Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))))
180175, 179mpbid 235 . . . . . . 7 (𝜑 → (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)) < (√‘Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)))
181135recnd 10660 . . . . . . . . . . 11 (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℂ)
182 fsumconst 15139 . . . . . . . . . . 11 ((𝑋 ∈ Fin ∧ ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℂ) → Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)))
1831, 181, 182syl2anc 587 . . . . . . . . . 10 (𝜑 → Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)))
184 sqdiv 13485 . . . . . . . . . . . . 13 ((𝐸 ∈ ℂ ∧ (√‘(♯‘𝑋)) ∈ ℂ ∧ (√‘(♯‘𝑋)) ≠ 0) → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)))
185150, 151, 153, 184syl3anc 1368 . . . . . . . . . . . 12 (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)))
18693recnd 10660 . . . . . . . . . . . . . 14 (𝜑 → (♯‘𝑋) ∈ ℂ)
187 sqrtth 14718 . . . . . . . . . . . . . 14 ((♯‘𝑋) ∈ ℂ → ((√‘(♯‘𝑋))↑2) = (♯‘𝑋))
188186, 187syl 17 . . . . . . . . . . . . 13 (𝜑 → ((√‘(♯‘𝑋))↑2) = (♯‘𝑋))
189188oveq2d 7151 . . . . . . . . . . . 12 (𝜑 → ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)) = ((𝐸↑2) / (♯‘𝑋)))
190185, 189eqtrd 2833 . . . . . . . . . . 11 (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / (♯‘𝑋)))
191190oveq2d 7151 . . . . . . . . . 10 (𝜑 → ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)) = ((♯‘𝑋) · ((𝐸↑2) / (♯‘𝑋))))
192150sqcld 13506 . . . . . . . . . . 11 (𝜑 → (𝐸↑2) ∈ ℂ)
193165, 94gtned 10766 . . . . . . . . . . 11 (𝜑 → (♯‘𝑋) ≠ 0)
194192, 186, 193divcan2d 11409 . . . . . . . . . 10 (𝜑 → ((♯‘𝑋) · ((𝐸↑2) / (♯‘𝑋))) = (𝐸↑2))
195183, 191, 1943eqtrd 2837 . . . . . . . . 9 (𝜑 → Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = (𝐸↑2))
196195fveq2d 6649 . . . . . . . 8 (𝜑 → (√‘Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)) = (√‘(𝐸↑2)))
197165, 78, 167ltled 10779 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
198 sqrtsq 14623 . . . . . . . . 9 ((𝐸 ∈ ℝ ∧ 0 ≤ 𝐸) → (√‘(𝐸↑2)) = 𝐸)
19978, 197, 198syl2anc 587 . . . . . . . 8 (𝜑 → (√‘(𝐸↑2)) = 𝐸)
200 eqidd 2799 . . . . . . . 8 (𝜑𝐸 = 𝐸)
201196, 199, 2003eqtrd 2837 . . . . . . 7 (𝜑 → (√‘Σ𝑖𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)) = 𝐸)
202180, 201breqtrd 5056 . . . . . 6 (𝜑 → (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)) < 𝐸)
203202adantr 484 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (√‘Σ𝑖𝑋 (((𝐷𝑖) − (𝐶𝑖))↑2)) < 𝐸)
20469, 76, 79, 133, 203lttrd 10792 . . . 4 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸)
205 eqid 2798 . . . . . . . 8 (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
206205rrxmetfi 24023 . . . . . . 7 (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑m 𝑋)))
207 metxmet 22948 . . . . . . 7 ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑m 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑m 𝑋)))
2081, 206, 2073syl 18 . . . . . 6 (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑m 𝑋)))
209208adantr 484 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑m 𝑋)))
21079rexrd 10682 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝐸 ∈ ℝ*)
21127, 3eleqtrdi 2900 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑓 ∈ (ℝ ↑m 𝑋))
212 elbl2 23004 . . . . 5 ((((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑m 𝑋)) ∧ 𝐸 ∈ ℝ*) ∧ (𝑌 ∈ (ℝ ↑m 𝑋) ∧ 𝑓 ∈ (ℝ ↑m 𝑋))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸))
213209, 210, 17, 211, 212syl22anc 837 . . . 4 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸))
214204, 213mpbird 260 . . 3 ((𝜑𝑓X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))) → 𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
215214ralrimiva 3149 . 2 (𝜑 → ∀𝑓X 𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
216 dfss3 3903 . 2 (X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ ∀𝑓X 𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
217215, 216sylibr 237 1 (𝜑X𝑖𝑋 ((𝐶𝑖)[,)(𝐷𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  Vcvv 3441   ⊆ wss 3881  ∅c0 4243   class class class wbr 5030  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∈ cmpo 7137   ↑m cmap 8391  Xcixp 8446  Fincfn 8494  ℂcc 10526  ℝcr 10527  0cc0 10528   + caddc 10531   · cmul 10533  ℝ*cxr 10665   < clt 10666   ≤ cle 10667   − cmin 10861   / cdiv 11288  ℕcn 11627  2c2 11682  ℕ0cn0 11887  ℝ+crp 12379  (,)cioo 12728  [,)cico 12730  ↑cexp 13427  ♯chash 13688  √csqrt 14586  abscabs 14587  Σcsu 15036  distcds 16568  ∞Metcxmet 20079  Metcmet 20080  ballcbl 20081  ℝ^crrx 23994 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606  ax-addf 10607  ax-mulf 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7390  df-om 7563  df-1st 7673  df-2nd 7674  df-supp 7816  df-tpos 7877  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-map 8393  df-ixp 8447  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-fsupp 8820  df-sup 8892  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-4 11692  df-5 11693  df-6 11694  df-7 11695  df-8 11696  df-9 11697  df-n0 11888  df-z 11972  df-dec 12089  df-uz 12234  df-rp 12380  df-xadd 12498  df-ioo 12732  df-ico 12734  df-fz 12888  df-fzo 13031  df-seq 13367  df-exp 13428  df-hash 13689  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-sum 15037  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-starv 16574  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-hom 16583  df-cco 16584  df-0g 16709  df-gsum 16710  df-prds 16715  df-pws 16717  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-mhm 17950  df-grp 18100  df-minusg 18101  df-sbg 18102  df-subg 18271  df-ghm 18351  df-cntz 18442  df-cmn 18903  df-abl 18904  df-mgp 19236  df-ur 19248  df-ring 19295  df-cring 19296  df-oppr 19372  df-dvdsr 19390  df-unit 19391  df-invr 19421  df-dvr 19432  df-rnghom 19466  df-drng 19500  df-field 19501  df-subrg 19529  df-staf 19612  df-srng 19613  df-lmod 19632  df-lss 19700  df-sra 19940  df-rgmod 19941  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-cnfld 20095  df-refld 20298  df-dsmm 20425  df-frlm 20440  df-nm 23196  df-tng 23198  df-tcph 23781  df-rrx 23996 This theorem is referenced by:  hoiqssbllem3  43278
 Copyright terms: Public domain W3C validator