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

Theorem hoiqssbllem2 45325
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 2732 . . . . . . . . . 10 (ℝ^β€˜π‘‹) = (ℝ^β€˜π‘‹)
3 eqid 2732 . . . . . . . . . 10 (ℝ ↑m 𝑋) = (ℝ ↑m 𝑋)
42, 3rrxdsfi 24919 . . . . . . . . 9 (𝑋 ∈ Fin β†’ (distβ€˜(ℝ^β€˜π‘‹)) = (𝑔 ∈ (ℝ ↑m 𝑋), β„Ž ∈ (ℝ ↑m 𝑋) ↦ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2))))
51, 4syl 17 . . . . . . . 8 (πœ‘ β†’ (distβ€˜(ℝ^β€˜π‘‹)) = (𝑔 ∈ (ℝ ↑m 𝑋), β„Ž ∈ (ℝ ↑m 𝑋) ↦ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2))))
65adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (distβ€˜(ℝ^β€˜π‘‹)) = (𝑔 ∈ (ℝ ↑m 𝑋), β„Ž ∈ (ℝ ↑m 𝑋) ↦ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2))))
7 fveq1 6887 . . . . . . . . . . . . 13 (𝑔 = π‘Œ β†’ (π‘”β€˜π‘–) = (π‘Œβ€˜π‘–))
87adantr 481 . . . . . . . . . . . 12 ((𝑔 = π‘Œ ∧ β„Ž = 𝑓) β†’ (π‘”β€˜π‘–) = (π‘Œβ€˜π‘–))
9 fveq1 6887 . . . . . . . . . . . . 13 (β„Ž = 𝑓 β†’ (β„Žβ€˜π‘–) = (π‘“β€˜π‘–))
109adantl 482 . . . . . . . . . . . 12 ((𝑔 = π‘Œ ∧ β„Ž = 𝑓) β†’ (β„Žβ€˜π‘–) = (π‘“β€˜π‘–))
118, 10oveq12d 7423 . . . . . . . . . . 11 ((𝑔 = π‘Œ ∧ β„Ž = 𝑓) β†’ ((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–)) = ((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–)))
1211oveq1d 7420 . . . . . . . . . 10 ((𝑔 = π‘Œ ∧ β„Ž = 𝑓) β†’ (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2) = (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2))
1312sumeq2sdv 15646 . . . . . . . . 9 ((𝑔 = π‘Œ ∧ β„Ž = 𝑓) β†’ Σ𝑖 ∈ 𝑋 (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2) = Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2))
1413fveq2d 6892 . . . . . . . 8 ((𝑔 = π‘Œ ∧ β„Ž = 𝑓) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2)) = (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)))
1514adantl 482 . . . . . . 7 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ (𝑔 = π‘Œ ∧ β„Ž = 𝑓)) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘”β€˜π‘–) βˆ’ (β„Žβ€˜π‘–))↑2)) = (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)))
16 hoiqssbllem2.y . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ (ℝ ↑m 𝑋))
1716adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ π‘Œ ∈ (ℝ ↑m 𝑋))
18 hoiqssbllem2.i . . . . . . . . . 10 β„²π‘–πœ‘
19 hoiqssbllem2.c . . . . . . . . . . 11 (πœ‘ β†’ 𝐢:π‘‹βŸΆβ„)
2019ffvelcdmda 7083 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) ∈ ℝ)
21 hoiqssbllem2.d . . . . . . . . . . . 12 (πœ‘ β†’ 𝐷:π‘‹βŸΆβ„)
2221ffvelcdmda 7083 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π·β€˜π‘–) ∈ ℝ)
2322rexrd 11260 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π·β€˜π‘–) ∈ ℝ*)
2418, 20, 23hoissrrn2 45280 . . . . . . . . 9 (πœ‘ β†’ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† (ℝ ↑m 𝑋))
2524adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† (ℝ ↑m 𝑋))
26 simpr 485 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
2725, 26sseldd 3982 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
28 fvexd 6903 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)) ∈ V)
296, 15, 17, 27, 28ovmpod 7556 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (π‘Œ(distβ€˜(ℝ^β€˜π‘‹))𝑓) = (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)))
30 nfcv 2903 . . . . . . . . . 10 Ⅎ𝑖𝑓
31 nfixp1 8908 . . . . . . . . . 10 Ⅎ𝑖X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))
3230, 31nfel 2917 . . . . . . . . 9 Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))
3318, 32nfan 1902 . . . . . . . 8 Ⅎ𝑖(πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
34 simpl 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ πœ‘)
3534, 1syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝑋 ∈ Fin)
36 elmapi 8839 . . . . . . . . . . . . 13 (π‘Œ ∈ (ℝ ↑m 𝑋) β†’ π‘Œ:π‘‹βŸΆβ„)
3716, 36syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Œ:π‘‹βŸΆβ„)
3837ffvelcdmda 7083 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) ∈ ℝ)
3934, 38sylan 580 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) ∈ ℝ)
40 icossre 13401 . . . . . . . . . . . . 13 (((πΆβ€˜π‘–) ∈ ℝ ∧ (π·β€˜π‘–) ∈ ℝ*) β†’ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† ℝ)
4120, 23, 40syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† ℝ)
4241adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† ℝ)
43 fvixp2 43883 . . . . . . . . . . . 12 ((𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
4443adantll 712 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
4542, 44sseldd 3982 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘“β€˜π‘–) ∈ ℝ)
4639, 45resubcld 11638 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–)) ∈ ℝ)
47 2nn0 12485 . . . . . . . . . 10 2 ∈ β„•0
4847a1i 11 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 2 ∈ β„•0)
4946, 48reexpcld 14124 . . . . . . . 8 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) ∈ ℝ)
5033, 35, 49fsumreclf 44278 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) ∈ ℝ)
51 fveq2 6888 . . . . . . . . . . . . 13 (𝑖 = 𝑗 β†’ (πΆβ€˜π‘–) = (πΆβ€˜π‘—))
52 fveq2 6888 . . . . . . . . . . . . 13 (𝑖 = 𝑗 β†’ (π·β€˜π‘–) = (π·β€˜π‘—))
5351, 52oveq12d 7423 . . . . . . . . . . . 12 (𝑖 = 𝑗 β†’ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) = ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
5453cbvixpv 8905 . . . . . . . . . . 11 X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) = X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))
5554eleq2i 2825 . . . . . . . . . 10 (𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
5655biimpi 215 . . . . . . . . 9 (𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) β†’ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
5756adantl 482 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)))
581adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝑋 ∈ Fin)
59 simpll 765 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ πœ‘)
6055biimpri 227 . . . . . . . . . . 11 (𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—)) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
6160ad2antlr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
62 simpr 485 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ 𝑖 ∈ 𝑋)
6359, 61, 62, 49syl21anc 836 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) ∈ ℝ)
6446sqge0d 14098 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ 0 ≀ (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2))
6559, 61, 62, 64syl21anc 836 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ 0 ≀ (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2))
6658, 63, 65fsumge0 15737 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 0 ≀ Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2))
6734, 57, 66syl2anc 584 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 0 ≀ Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2))
6850, 67resqrtcld 15360 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)) ∈ ℝ)
6929, 68eqeltrd 2833 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (π‘Œ(distβ€˜(ℝ^β€˜π‘‹))𝑓) ∈ ℝ)
7022, 20resubcld 11638 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) ∈ ℝ)
7170resqcld 14086 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) ∈ ℝ)
721, 71fsumrecl 15676 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) ∈ ℝ)
7370sqge0d 14098 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 0 ≀ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
741, 71, 73fsumge0 15737 . . . . . . 7 (πœ‘ β†’ 0 ≀ Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
7572, 74resqrtcld 15360 . . . . . 6 (πœ‘ β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)) ∈ ℝ)
7675adantr 481 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)) ∈ ℝ)
77 hoiqssbllem2.e . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ℝ+)
7877rpred 13012 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ)
7978adantr 481 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝐸 ∈ ℝ)
80 hoiqssbllem2.n . . . . . . . . . 10 (πœ‘ β†’ 𝑋 β‰  βˆ…)
8180adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ 𝑋 β‰  βˆ…)
8271adantlr 713 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) ∈ ℝ)
8334, 22sylan 580 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π·β€˜π‘–) ∈ ℝ)
8434, 20sylan 580 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) ∈ ℝ)
8583, 84resubcld 11638 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) ∈ ℝ)
8620rexrd 11260 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) ∈ ℝ*)
8738rexrd 11260 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) ∈ ℝ*)
88 2rp 12975 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℝ+
8988a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 2 ∈ ℝ+)
90 hashnncl 14322 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 ∈ Fin β†’ ((β™―β€˜π‘‹) ∈ β„• ↔ 𝑋 β‰  βˆ…))
911, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((β™―β€˜π‘‹) ∈ β„• ↔ 𝑋 β‰  βˆ…))
9280, 91mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (β™―β€˜π‘‹) ∈ β„•)
9392nnred 12223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (β™―β€˜π‘‹) ∈ ℝ)
9492nngt0d 12257 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 0 < (β™―β€˜π‘‹))
9593, 94elrpd 13009 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (β™―β€˜π‘‹) ∈ ℝ+)
9695rpsqrtcld 15354 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (βˆšβ€˜(β™―β€˜π‘‹)) ∈ ℝ+)
9789, 96rpmulcld 13028 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))) ∈ ℝ+)
9877, 97rpdivcld 13029 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) ∈ ℝ+)
9998rpred 13012 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) ∈ ℝ)
10099adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) ∈ ℝ)
10138, 100resubcld 11638 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ)
102101rexrd 11260 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ*)
103 hoiqssbllem2.l . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) ∈ (((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))(,)(π‘Œβ€˜π‘–)))
104 iooltub 44209 . . . . . . . . . . . . . . . . 17 ((((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ* ∧ (π‘Œβ€˜π‘–) ∈ ℝ* ∧ (πΆβ€˜π‘–) ∈ (((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))(,)(π‘Œβ€˜π‘–))) β†’ (πΆβ€˜π‘–) < (π‘Œβ€˜π‘–))
105102, 87, 103, 104syl3anc 1371 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) < (π‘Œβ€˜π‘–))
10620, 38, 105ltled 11358 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) ≀ (π‘Œβ€˜π‘–))
10738, 100readdcld 11239 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ)
108107rexrd 11260 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ*)
109 hoiqssbllem2.r . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π·β€˜π‘–) ∈ ((π‘Œβ€˜π‘–)(,)((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))))
110 ioogtlb 44194 . . . . . . . . . . . . . . . 16 (((π‘Œβ€˜π‘–) ∈ ℝ* ∧ ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ* ∧ (π·β€˜π‘–) ∈ ((π‘Œβ€˜π‘–)(,)((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))))) β†’ (π‘Œβ€˜π‘–) < (π·β€˜π‘–))
11187, 108, 109, 110syl3anc 1371 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) < (π·β€˜π‘–))
11286, 23, 87, 106, 111elicod 13370 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) ∈ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
11334, 112sylan 580 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) ∈ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))
114 icodiamlt 15378 . . . . . . . . . . . . 13 ((((πΆβ€˜π‘–) ∈ ℝ ∧ (π·β€˜π‘–) ∈ ℝ) ∧ ((π‘Œβ€˜π‘–) ∈ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) ∧ (π‘“β€˜π‘–) ∈ ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)))) β†’ (absβ€˜((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))) < ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)))
11584, 83, 113, 44, 114syl22anc 837 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))) < ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)))
116 0red 11213 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 0 ∈ ℝ)
11720, 38, 22, 106, 111lelttrd 11368 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (πΆβ€˜π‘–) < (π·β€˜π‘–))
11820, 22posdifd 11797 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((πΆβ€˜π‘–) < (π·β€˜π‘–) ↔ 0 < ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))))
119117, 118mpbid 231 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 0 < ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)))
120116, 70, 119ltled 11358 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 0 ≀ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)))
12170, 120absidd 15365 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))) = ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)))
122121eqcomd 2738 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) = (absβ€˜((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))))
123122adantlr 713 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) = (absβ€˜((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))))
124115, 123breqtrd 5173 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (absβ€˜((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))) < (absβ€˜((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))))
12546, 85, 124abslt2sqd 44056 . . . . . . . . . 10 (((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) < (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
12659, 61, 62, 125syl21anc 836 . . . . . . . . 9 (((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) < (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
12758, 81, 63, 82, 126fsumlt 15742 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((πΆβ€˜π‘—)[,)(π·β€˜π‘—))) β†’ Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) < Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
12834, 57, 127syl2anc 584 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) < Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
12934, 72syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) ∈ ℝ)
13034, 74syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 0 ≀ Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))
13150, 67, 129, 130sqrtltd 15370 . . . . . . 7 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (Σ𝑖 ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2) < Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) ↔ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)) < (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2))))
132128, 131mpbid 231 . . . . . 6 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π‘Œβ€˜π‘–) βˆ’ (π‘“β€˜π‘–))↑2)) < (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)))
13329, 132eqbrtrd 5169 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (π‘Œ(distβ€˜(ℝ^β€˜π‘‹))𝑓) < (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)))
13478, 96rerpdivcld 13043 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) ∈ ℝ)
135134resqcld 14086 . . . . . . . . . 10 (πœ‘ β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) ∈ ℝ)
136135adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) ∈ ℝ)
13722, 20jca 512 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) ∈ ℝ ∧ (πΆβ€˜π‘–) ∈ ℝ))
138107, 101jca 512 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ ∧ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ))
139137, 138jca 512 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π·β€˜π‘–) ∈ ℝ ∧ (πΆβ€˜π‘–) ∈ ℝ) ∧ (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ ∧ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ)))
140 iooltub 44209 . . . . . . . . . . . . . 14 (((π‘Œβ€˜π‘–) ∈ ℝ* ∧ ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ* ∧ (π·β€˜π‘–) ∈ ((π‘Œβ€˜π‘–)(,)((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))))) β†’ (π·β€˜π‘–) < ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))))
14187, 108, 109, 140syl3anc 1371 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π·β€˜π‘–) < ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))))
142 ioogtlb 44194 . . . . . . . . . . . . . 14 ((((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ* ∧ (π‘Œβ€˜π‘–) ∈ ℝ* ∧ (πΆβ€˜π‘–) ∈ (((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))(,)(π‘Œβ€˜π‘–))) β†’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) < (πΆβ€˜π‘–))
143102, 87, 103, 142syl3anc 1371 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) < (πΆβ€˜π‘–))
144141, 143jca 512 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) < ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∧ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) < (πΆβ€˜π‘–)))
145 lt2sub 11708 . . . . . . . . . . . 12 ((((π·β€˜π‘–) ∈ ℝ ∧ (πΆβ€˜π‘–) ∈ ℝ) ∧ (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ ∧ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∈ ℝ)) β†’ (((π·β€˜π‘–) < ((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) ∧ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) < (πΆβ€˜π‘–)) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) < (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) βˆ’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))))))
146139, 144, 145sylc 65 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) < (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) βˆ’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))))
14738recnd 11238 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (π‘Œβ€˜π‘–) ∈ β„‚)
148100recnd 11238 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) ∈ β„‚)
149147, 148, 148pnncand 11606 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) βˆ’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))) = ((𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))))
15078recnd 11238 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐸 ∈ β„‚)
15196rpcnd 13014 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆšβ€˜(β™―β€˜π‘‹)) ∈ β„‚)
152 2cnd 12286 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 2 ∈ β„‚)
15396rpne0d 13017 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆšβ€˜(β™―β€˜π‘‹)) β‰  0)
15489rpne0d 13017 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 2 β‰  0)
155150, 151, 152, 153, 154divdiv3d 44055 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) / 2) = (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))
156155eqcomd 2738 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) = ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) / 2))
157156, 156oveq12d 7423 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) = (((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) / 2) + ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) / 2)))
158150, 151, 153divcld 11986 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) ∈ β„‚)
1591582halvesd 12454 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) / 2) + ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) / 2)) = (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
160157, 159eqtrd 2772 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) = (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
161160adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) = (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
162149, 161eqtrd 2772 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π‘Œβ€˜π‘–) + (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹))))) βˆ’ ((π‘Œβ€˜π‘–) βˆ’ (𝐸 / (2 Β· (βˆšβ€˜(β™―β€˜π‘‹)))))) = (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
163146, 162breqtrd 5173 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) < (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
164134adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) ∈ ℝ)
165 0red 11213 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ ℝ)
16696rpred 13012 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βˆšβ€˜(β™―β€˜π‘‹)) ∈ ℝ)
16777rpgt0d 13015 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < 𝐸)
16896rpgt0d 13015 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < (βˆšβ€˜(β™―β€˜π‘‹)))
16978, 166, 167, 168divgt0d 12145 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
170165, 134, 169ltled 11358 . . . . . . . . . . . 12 (πœ‘ β†’ 0 ≀ (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
171170adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 0 ≀ (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))
172 lt2sq 14094 . . . . . . . . . . 11 (((((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) ∈ ℝ ∧ 0 ≀ ((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))) ∧ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) ∈ ℝ ∧ 0 ≀ (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))))) β†’ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) < (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) ↔ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) < ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)))
17370, 120, 164, 171, 172syl22anc 837 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–)) < (𝐸 / (βˆšβ€˜(β™―β€˜π‘‹))) ↔ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) < ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)))
174163, 173mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) < ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2))
1751, 80, 71, 136, 174fsumlt 15742 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2))
1761, 136fsumrecl 15676 . . . . . . . . 9 (πœ‘ β†’ Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) ∈ ℝ)
177164sqge0d 14098 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ 𝑋) β†’ 0 ≀ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2))
1781, 136, 177fsumge0 15737 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2))
17972, 74, 176, 178sqrtltd 15370 . . . . . . . 8 (πœ‘ β†’ (Σ𝑖 ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) ↔ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)) < (βˆšβ€˜Ξ£π‘– ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2))))
180175, 179mpbid 231 . . . . . . 7 (πœ‘ β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)) < (βˆšβ€˜Ξ£π‘– ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)))
181135recnd 11238 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) ∈ β„‚)
182 fsumconst 15732 . . . . . . . . . . 11 ((𝑋 ∈ Fin ∧ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) ∈ β„‚) β†’ Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) = ((β™―β€˜π‘‹) Β· ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)))
1831, 181, 182syl2anc 584 . . . . . . . . . 10 (πœ‘ β†’ Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) = ((β™―β€˜π‘‹) Β· ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)))
184 sqdiv 14082 . . . . . . . . . . . . 13 ((𝐸 ∈ β„‚ ∧ (βˆšβ€˜(β™―β€˜π‘‹)) ∈ β„‚ ∧ (βˆšβ€˜(β™―β€˜π‘‹)) β‰  0) β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) = ((𝐸↑2) / ((βˆšβ€˜(β™―β€˜π‘‹))↑2)))
185150, 151, 153, 184syl3anc 1371 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) = ((𝐸↑2) / ((βˆšβ€˜(β™―β€˜π‘‹))↑2)))
18693recnd 11238 . . . . . . . . . . . . . 14 (πœ‘ β†’ (β™―β€˜π‘‹) ∈ β„‚)
187 sqrtth 15307 . . . . . . . . . . . . . 14 ((β™―β€˜π‘‹) ∈ β„‚ β†’ ((βˆšβ€˜(β™―β€˜π‘‹))↑2) = (β™―β€˜π‘‹))
188186, 187syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ ((βˆšβ€˜(β™―β€˜π‘‹))↑2) = (β™―β€˜π‘‹))
189188oveq2d 7421 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐸↑2) / ((βˆšβ€˜(β™―β€˜π‘‹))↑2)) = ((𝐸↑2) / (β™―β€˜π‘‹)))
190185, 189eqtrd 2772 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) = ((𝐸↑2) / (β™―β€˜π‘‹)))
191190oveq2d 7421 . . . . . . . . . 10 (πœ‘ β†’ ((β™―β€˜π‘‹) Β· ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)) = ((β™―β€˜π‘‹) Β· ((𝐸↑2) / (β™―β€˜π‘‹))))
192150sqcld 14105 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸↑2) ∈ β„‚)
193165, 94gtned 11345 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜π‘‹) β‰  0)
194192, 186, 193divcan2d 11988 . . . . . . . . . 10 (πœ‘ β†’ ((β™―β€˜π‘‹) Β· ((𝐸↑2) / (β™―β€˜π‘‹))) = (𝐸↑2))
195183, 191, 1943eqtrd 2776 . . . . . . . . 9 (πœ‘ β†’ Σ𝑖 ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2) = (𝐸↑2))
196195fveq2d 6892 . . . . . . . 8 (πœ‘ β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)) = (βˆšβ€˜(𝐸↑2)))
197165, 78, 167ltled 11358 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝐸)
198 sqrtsq 15212 . . . . . . . . 9 ((𝐸 ∈ ℝ ∧ 0 ≀ 𝐸) β†’ (βˆšβ€˜(𝐸↑2)) = 𝐸)
19978, 197, 198syl2anc 584 . . . . . . . 8 (πœ‘ β†’ (βˆšβ€˜(𝐸↑2)) = 𝐸)
200 eqidd 2733 . . . . . . . 8 (πœ‘ β†’ 𝐸 = 𝐸)
201196, 199, 2003eqtrd 2776 . . . . . . 7 (πœ‘ β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 ((𝐸 / (βˆšβ€˜(β™―β€˜π‘‹)))↑2)) = 𝐸)
202180, 201breqtrd 5173 . . . . . 6 (πœ‘ β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)) < 𝐸)
203202adantr 481 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (βˆšβ€˜Ξ£π‘– ∈ 𝑋 (((π·β€˜π‘–) βˆ’ (πΆβ€˜π‘–))↑2)) < 𝐸)
20469, 76, 79, 133, 203lttrd 11371 . . . 4 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (π‘Œ(distβ€˜(ℝ^β€˜π‘‹))𝑓) < 𝐸)
205 eqid 2732 . . . . . . . 8 (distβ€˜(ℝ^β€˜π‘‹)) = (distβ€˜(ℝ^β€˜π‘‹))
206205rrxmetfi 24920 . . . . . . 7 (𝑋 ∈ Fin β†’ (distβ€˜(ℝ^β€˜π‘‹)) ∈ (Metβ€˜(ℝ ↑m 𝑋)))
207 metxmet 23831 . . . . . . 7 ((distβ€˜(ℝ^β€˜π‘‹)) ∈ (Metβ€˜(ℝ ↑m 𝑋)) β†’ (distβ€˜(ℝ^β€˜π‘‹)) ∈ (∞Metβ€˜(ℝ ↑m 𝑋)))
2081, 206, 2073syl 18 . . . . . 6 (πœ‘ β†’ (distβ€˜(ℝ^β€˜π‘‹)) ∈ (∞Metβ€˜(ℝ ↑m 𝑋)))
209208adantr 481 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (distβ€˜(ℝ^β€˜π‘‹)) ∈ (∞Metβ€˜(ℝ ↑m 𝑋)))
21079rexrd 11260 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝐸 ∈ ℝ*)
21127, 3eleqtrdi 2843 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝑓 ∈ (ℝ ↑m 𝑋))
212 elbl2 23887 . . . . 5 ((((distβ€˜(ℝ^β€˜π‘‹)) ∈ (∞Metβ€˜(ℝ ↑m 𝑋)) ∧ 𝐸 ∈ ℝ*) ∧ (π‘Œ ∈ (ℝ ↑m 𝑋) ∧ 𝑓 ∈ (ℝ ↑m 𝑋))) β†’ (𝑓 ∈ (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸) ↔ (π‘Œ(distβ€˜(ℝ^β€˜π‘‹))𝑓) < 𝐸))
213209, 210, 17, 211, 212syl22anc 837 . . . 4 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ (𝑓 ∈ (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸) ↔ (π‘Œ(distβ€˜(ℝ^β€˜π‘‹))𝑓) < 𝐸))
214204, 213mpbird 256 . . 3 ((πœ‘ ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))) β†’ 𝑓 ∈ (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸))
215214ralrimiva 3146 . 2 (πœ‘ β†’ βˆ€π‘“ ∈ X 𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))𝑓 ∈ (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸))
216 dfss3 3969 . 2 (X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸) ↔ βˆ€π‘“ ∈ X 𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–))𝑓 ∈ (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸))
217215, 216sylibr 233 1 (πœ‘ β†’ X𝑖 ∈ 𝑋 ((πΆβ€˜π‘–)[,)(π·β€˜π‘–)) βŠ† (π‘Œ(ballβ€˜(distβ€˜(ℝ^β€˜π‘‹)))𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541  β„²wnf 1785   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   βŠ† wss 3947  βˆ…c0 4321   class class class wbr 5147  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∈ cmpo 7407   ↑m cmap 8816  Xcixp 8887  Fincfn 8935  β„‚cc 11104  β„cr 11105  0cc0 11106   + caddc 11109   Β· cmul 11111  β„*cxr 11243   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440   / cdiv 11867  β„•cn 12208  2c2 12263  β„•0cn0 12468  β„+crp 12970  (,)cioo 13320  [,)cico 13322  β†‘cexp 14023  β™―chash 14286  βˆšcsqrt 15176  abscabs 15177  Ξ£csu 15628  distcds 17202  βˆžMetcxmet 20921  Metcmet 20922  ballcbl 20923  β„^crrx 24891
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-tpos 8207  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-xadd 13089  df-ioo 13324  df-ico 13326  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-0g 17383  df-gsum 17384  df-prds 17389  df-pws 17391  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-grp 18818  df-minusg 18819  df-sbg 18820  df-subg 18997  df-ghm 19084  df-cntz 19175  df-cmn 19644  df-abl 19645  df-mgp 19982  df-ur 19999  df-ring 20051  df-cring 20052  df-oppr 20142  df-dvdsr 20163  df-unit 20164  df-invr 20194  df-dvr 20207  df-rnghom 20243  df-drng 20309  df-field 20310  df-subrg 20353  df-staf 20445  df-srng 20446  df-lmod 20465  df-lss 20535  df-sra 20777  df-rgmod 20778  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-cnfld 20937  df-refld 21149  df-dsmm 21278  df-frlm 21293  df-nm 24082  df-tng 24084  df-tcph 24677  df-rrx 24893
This theorem is referenced by:  hoiqssbllem3  45326
  Copyright terms: Public domain W3C validator