Step | Hyp | Ref
| Expression |
1 | | hoiqssbllem2.x |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | eqid 2610 |
. . . . . . . . . 10
⊢
(ℝ^‘𝑋) =
(ℝ^‘𝑋) |
3 | | eqid 2610 |
. . . . . . . . . 10
⊢ (ℝ
↑𝑚 𝑋) = (ℝ ↑𝑚
𝑋) |
4 | 2, 3 | rrxdsfi 39181 |
. . . . . . . . 9
⊢ (𝑋 ∈ Fin →
(dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑𝑚
𝑋), ℎ ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑖
∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)))) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑𝑚
𝑋), ℎ ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑖
∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)))) |
6 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑𝑚
𝑋), ℎ ∈ (ℝ ↑𝑚
𝑋) ↦
(√‘Σ𝑖
∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)))) |
7 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑌 → (𝑔‘𝑖) = (𝑌‘𝑖)) |
8 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (𝑔‘𝑖) = (𝑌‘𝑖)) |
9 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (ℎ = 𝑓 → (ℎ‘𝑖) = (𝑓‘𝑖)) |
10 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (ℎ‘𝑖) = (𝑓‘𝑖)) |
11 | 8, 10 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → ((𝑔‘𝑖) − (ℎ‘𝑖)) = ((𝑌‘𝑖) − (𝑓‘𝑖))) |
12 | 11 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (((𝑔‘𝑖) − (ℎ‘𝑖))↑2) = (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) |
13 | 12 | sumeq2ad 38632 |
. . . . . . . . 9
⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2) = Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) |
14 | 13 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))) |
15 | 14 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ (𝑔 = 𝑌 ∧ ℎ = 𝑓)) → (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))) |
16 | | hoiqssbllem2.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (ℝ ↑𝑚
𝑋)) |
17 | 16 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑌 ∈ (ℝ ↑𝑚
𝑋)) |
18 | | hoiqssbllem2.i |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝜑 |
19 | | hoiqssbllem2.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶:𝑋⟶ℝ) |
20 | 19 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ) |
21 | | hoiqssbllem2.d |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷:𝑋⟶ℝ) |
22 | 21 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ) |
23 | 22 | rexrd 9968 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈
ℝ*) |
24 | 18, 20, 23 | hoissrrn2 39468 |
. . . . . . . . 9
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (ℝ
↑𝑚 𝑋)) |
25 | 24 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (ℝ
↑𝑚 𝑋)) |
26 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
27 | 25, 26 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (ℝ ↑𝑚
𝑋)) |
28 | | fvex 6113 |
. . . . . . . 8
⊢
(√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ V |
29 | 28 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ V) |
30 | 6, 15, 17, 27, 29 | ovmpt2d 6686 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))) |
31 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝑓 |
32 | | nfixp1 7814 |
. . . . . . . . . 10
⊢
Ⅎ𝑖X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) |
33 | 31, 32 | nfel 2763 |
. . . . . . . . 9
⊢
Ⅎ𝑖 𝑓 ∈ X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) |
34 | 18, 33 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
35 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝜑) |
36 | 35, 1 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑋 ∈ Fin) |
37 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ (ℝ
↑𝑚 𝑋) → 𝑌:𝑋⟶ℝ) |
38 | 16, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌:𝑋⟶ℝ) |
39 | 38 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ) |
40 | 35, 39 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ) |
41 | | icossre 12125 |
. . . . . . . . . . . . 13
⊢ (((𝐶‘𝑖) ∈ ℝ ∧ (𝐷‘𝑖) ∈ ℝ*) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ) |
42 | 20, 23, 41 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ) |
43 | 42 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ) |
44 | | fvixp2 38384 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
45 | 44 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
46 | 43, 45 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ) |
47 | 40, 46 | resubcld 10337 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝑓‘𝑖)) ∈ ℝ) |
48 | | 2nn0 11186 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
49 | 48 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 2 ∈
ℕ0) |
50 | 47, 49 | reexpcld 12887 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ) |
51 | 34, 36, 50 | fsumreclf 38643 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ) |
52 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (𝐶‘𝑖) = (𝐶‘𝑗)) |
53 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗)) |
54 | 52, 53 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
55 | 54 | cbvixpv 7812 |
. . . . . . . . . . 11
⊢ X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)) |
56 | 55 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
57 | 56 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑓 ∈ X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
58 | 57 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) |
59 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑋 ∈ Fin) |
60 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝜑) |
61 | 56 | biimpri 217 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ X𝑗 ∈
𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
62 | 61 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
63 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋) |
64 | 60, 62, 63, 50 | syl21anc 1317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ) |
65 | 47 | sqge0d 12898 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) |
66 | 60, 62, 63, 65 | syl21anc 1317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) |
67 | 59, 64, 66 | fsumge0 14368 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) |
68 | 35, 58, 67 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) |
69 | 51, 68 | resqrtcld 14004 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ ℝ) |
70 | 30, 69 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) ∈ ℝ) |
71 | 22, 20 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ) |
72 | 71 | resqcld 12897 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ) |
73 | 1, 72 | fsumrecl 14312 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ) |
74 | 71 | sqge0d 12898 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
75 | 1, 72, 74 | fsumge0 14368 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
76 | 73, 75 | resqrtcld 14004 |
. . . . . 6
⊢ (𝜑 →
(√‘Σ𝑖
∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) ∈ ℝ) |
77 | 76 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) ∈ ℝ) |
78 | | hoiqssbllem2.e |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
79 | 78 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℝ) |
80 | 79 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝐸 ∈ ℝ) |
81 | | hoiqssbllem2.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≠ ∅) |
82 | 81 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑋 ≠ ∅) |
83 | 72 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ) |
84 | 35, 22 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ) |
85 | 35, 20 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ) |
86 | 84, 85 | resubcld 10337 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ) |
87 | 20 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈
ℝ*) |
88 | 39 | rexrd 9968 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈
ℝ*) |
89 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 2 ∈
ℝ+ |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 2 ∈
ℝ+) |
91 | | hashnncl 13018 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
92 | 1, 91 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
93 | 81, 92 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
94 | 93 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (#‘𝑋) ∈ ℝ) |
95 | 93 | nngt0d 10941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 0 < (#‘𝑋)) |
96 | 94, 95 | elrpd 11745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (#‘𝑋) ∈
ℝ+) |
97 | 96 | rpsqrtcld 13998 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 →
(√‘(#‘𝑋))
∈ ℝ+) |
98 | 90, 97 | rpmulcld 11764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (2 ·
(√‘(#‘𝑋))) ∈
ℝ+) |
99 | 78, 98 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐸 / (2 · (√‘(#‘𝑋)))) ∈
ℝ+) |
100 | 99 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐸 / (2 · (√‘(#‘𝑋)))) ∈
ℝ) |
101 | 100 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (2 · (√‘(#‘𝑋)))) ∈
ℝ) |
102 | 39, 101 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈
ℝ) |
103 | 102 | rexrd 9968 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈
ℝ*) |
104 | | hoiqssbllem2.l |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋)))))(,)(𝑌‘𝑖))) |
105 | | iooltub 38582 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ*
∧ (𝑌‘𝑖) ∈ ℝ*
∧ (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋)))))(,)(𝑌‘𝑖))) → (𝐶‘𝑖) < (𝑌‘𝑖)) |
106 | 103, 88, 104, 105 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) < (𝑌‘𝑖)) |
107 | 20, 39, 106 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ≤ (𝑌‘𝑖)) |
108 | 39, 101 | readdcld 9948 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈
ℝ) |
109 | 108 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈
ℝ*) |
110 | | hoiqssbllem2.r |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))))) |
111 | | ioogtlb 38564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑌‘𝑖) ∈ ℝ* ∧ ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ*
∧ (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))))) → (𝑌‘𝑖) < (𝐷‘𝑖)) |
112 | 88, 109, 110, 111 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) < (𝐷‘𝑖)) |
113 | 87, 23, 88, 107, 112 | elicod 12095 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
114 | 35, 113 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖))) |
115 | | icodiamlt 14022 |
. . . . . . . . . . . . 13
⊢ ((((𝐶‘𝑖) ∈ ℝ ∧ (𝐷‘𝑖) ∈ ℝ) ∧ ((𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ∧ (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < ((𝐷‘𝑖) − (𝐶‘𝑖))) |
116 | 85, 84, 114, 45, 115 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < ((𝐷‘𝑖) − (𝐶‘𝑖))) |
117 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ∈ ℝ) |
118 | 20, 39, 22, 107, 112 | lelttrd 10074 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) < (𝐷‘𝑖)) |
119 | 20, 22 | posdifd 10493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖) < (𝐷‘𝑖) ↔ 0 < ((𝐷‘𝑖) − (𝐶‘𝑖)))) |
120 | 118, 119 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐷‘𝑖) − (𝐶‘𝑖))) |
121 | 117, 71, 120 | ltled 10064 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ ((𝐷‘𝑖) − (𝐶‘𝑖))) |
122 | 71, 121 | absidd 14009 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))) = ((𝐷‘𝑖) − (𝐶‘𝑖))) |
123 | 122 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) = (abs‘((𝐷‘𝑖) − (𝐶‘𝑖)))) |
124 | 123 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) = (abs‘((𝐷‘𝑖) − (𝐶‘𝑖)))) |
125 | 116, 124 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < (abs‘((𝐷‘𝑖) − (𝐶‘𝑖)))) |
126 | 47, 86, 125 | abslt2sqd 38517 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
127 | 60, 62, 63, 126 | syl21anc 1317 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
128 | 59, 82, 64, 83, 127 | fsumlt 14373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
129 | 35, 58, 128 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
130 | 35, 73 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ) |
131 | 35, 75 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) |
132 | 51, 68, 130, 131 | sqrtltd 14014 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ↔ (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)))) |
133 | 129, 132 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))) |
134 | 30, 133 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))) |
135 | 79, 97 | rerpdivcld 11779 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / (√‘(#‘𝑋))) ∈ ℝ) |
136 | 135 | resqcld 12897 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 / (√‘(#‘𝑋)))↑2) ∈ ℝ) |
137 | 136 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐸 / (√‘(#‘𝑋)))↑2) ∈ ℝ) |
138 | 22, 20 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ)) |
139 | 108, 102 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ ∧
((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈
ℝ)) |
140 | 138, 139 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ ∧
((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈
ℝ))) |
141 | | iooltub 38582 |
. . . . . . . . . . . . . 14
⊢ (((𝑌‘𝑖) ∈ ℝ* ∧ ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ*
∧ (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))))) → (𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋)))))) |
142 | 88, 109, 110, 141 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋)))))) |
143 | | ioogtlb 38564 |
. . . . . . . . . . . . . 14
⊢ ((((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ*
∧ (𝑌‘𝑖) ∈ ℝ*
∧ (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋)))))(,)(𝑌‘𝑖))) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) < (𝐶‘𝑖)) |
144 | 103, 88, 104, 143 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) < (𝐶‘𝑖)) |
145 | 142, 144 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) < (𝐶‘𝑖))) |
146 | | lt2sub 10405 |
. . . . . . . . . . . 12
⊢ ((((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ ∧
((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) ∈ ℝ)) →
(((𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))) < (𝐶‘𝑖)) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋)))))))) |
147 | 140, 145,
146 | sylc 63 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋))))))) |
148 | 39 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℂ) |
149 | 101 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (2 · (√‘(#‘𝑋)))) ∈
ℂ) |
150 | 148, 149,
149 | pnncand 10310 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋)))))) = ((𝐸 / (2 · (√‘(#‘𝑋)))) + (𝐸 / (2 · (√‘(#‘𝑋)))))) |
151 | 79 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐸 ∈ ℂ) |
152 | 97 | rpcnd 11750 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(√‘(#‘𝑋))
∈ ℂ) |
153 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) |
154 | 97 | rpne0d 11753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(√‘(#‘𝑋))
≠ 0) |
155 | 90 | rpne0d 11753 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≠ 0) |
156 | 151, 152,
153, 154, 155 | divdiv3d 38516 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐸 / (√‘(#‘𝑋))) / 2) = (𝐸 / (2 · (√‘(#‘𝑋))))) |
157 | 156 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 / (2 · (√‘(#‘𝑋)))) = ((𝐸 / (√‘(#‘𝑋))) / 2)) |
158 | 157, 157 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸 / (2 · (√‘(#‘𝑋)))) + (𝐸 / (2 · (√‘(#‘𝑋))))) = (((𝐸 / (√‘(#‘𝑋))) / 2) + ((𝐸 / (√‘(#‘𝑋))) / 2))) |
159 | 151, 152,
154 | divcld 10680 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸 / (√‘(#‘𝑋))) ∈ ℂ) |
160 | 159 | 2halvesd 11155 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐸 / (√‘(#‘𝑋))) / 2) + ((𝐸 / (√‘(#‘𝑋))) / 2)) = (𝐸 / (√‘(#‘𝑋)))) |
161 | 158, 160 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / (2 · (√‘(#‘𝑋)))) + (𝐸 / (2 · (√‘(#‘𝑋))))) = (𝐸 / (√‘(#‘𝑋)))) |
162 | 161 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐸 / (2 · (√‘(#‘𝑋)))) + (𝐸 / (2 · (√‘(#‘𝑋))))) = (𝐸 / (√‘(#‘𝑋)))) |
163 | 150, 162 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(#‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(#‘𝑋)))))) = (𝐸 / (√‘(#‘𝑋)))) |
164 | 147, 163 | breqtrd 4609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(#‘𝑋)))) |
165 | 135 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (√‘(#‘𝑋))) ∈ ℝ) |
166 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
167 | 97 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(√‘(#‘𝑋))
∈ ℝ) |
168 | 78 | rpgt0d 11751 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝐸) |
169 | 97 | rpgt0d 11751 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 <
(√‘(#‘𝑋))) |
170 | 79, 167, 168, 169 | divgt0d 10838 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (𝐸 / (√‘(#‘𝑋)))) |
171 | 166, 135,
170 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝐸 / (√‘(#‘𝑋)))) |
172 | 171 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ (𝐸 / (√‘(#‘𝑋)))) |
173 | | lt2sq 12799 |
. . . . . . . . . . 11
⊢
(((((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ ∧ 0 ≤ ((𝐷‘𝑖) − (𝐶‘𝑖))) ∧ ((𝐸 / (√‘(#‘𝑋))) ∈ ℝ ∧ 0 ≤ (𝐸 / (√‘(#‘𝑋))))) → (((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(#‘𝑋))) ↔ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(#‘𝑋)))↑2))) |
174 | 71, 121, 165, 172, 173 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(#‘𝑋))) ↔ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(#‘𝑋)))↑2))) |
175 | 164, 174 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(#‘𝑋)))↑2)) |
176 | 1, 81, 72, 137, 175 | fsumlt 14373 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2)) |
177 | 1, 137 | fsumrecl 14312 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2) ∈ ℝ) |
178 | 165 | sqge0d 12898 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ ((𝐸 / (√‘(#‘𝑋)))↑2)) |
179 | 1, 137, 178 | fsumge0 14368 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2)) |
180 | 73, 75, 177, 179 | sqrtltd 14014 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2) ↔
(√‘Σ𝑖
∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2)))) |
181 | 176, 180 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 →
(√‘Σ𝑖
∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2))) |
182 | 136 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / (√‘(#‘𝑋)))↑2) ∈ ℂ) |
183 | | fsumconst 14364 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Fin ∧ ((𝐸 / (√‘(#‘𝑋)))↑2) ∈ ℂ)
→ Σ𝑖 ∈
𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2) = ((#‘𝑋) · ((𝐸 / (√‘(#‘𝑋)))↑2))) |
184 | 1, 182, 183 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2) = ((#‘𝑋) · ((𝐸 / (√‘(#‘𝑋)))↑2))) |
185 | | sqdiv 12790 |
. . . . . . . . . . . . 13
⊢ ((𝐸 ∈ ℂ ∧
(√‘(#‘𝑋))
∈ ℂ ∧ (√‘(#‘𝑋)) ≠ 0) → ((𝐸 / (√‘(#‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(#‘𝑋))↑2))) |
186 | 151, 152,
154, 185 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / (√‘(#‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(#‘𝑋))↑2))) |
187 | 94 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝑋) ∈ ℂ) |
188 | | sqrtth 13952 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑋) ∈
ℂ → ((√‘(#‘𝑋))↑2) = (#‘𝑋)) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((√‘(#‘𝑋))↑2) = (#‘𝑋)) |
190 | 189 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸↑2) / ((√‘(#‘𝑋))↑2)) = ((𝐸↑2) / (#‘𝑋))) |
191 | 186, 190 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / (√‘(#‘𝑋)))↑2) = ((𝐸↑2) / (#‘𝑋))) |
192 | 191 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝑋) · ((𝐸 / (√‘(#‘𝑋)))↑2)) = ((#‘𝑋) · ((𝐸↑2) / (#‘𝑋)))) |
193 | 151 | sqcld 12868 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
194 | 166, 95 | gtned 10051 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝑋) ≠ 0) |
195 | 193, 187,
194 | divcan2d 10682 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝑋) · ((𝐸↑2) / (#‘𝑋))) = (𝐸↑2)) |
196 | 184, 192,
195 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2) = (𝐸↑2)) |
197 | 196 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 →
(√‘Σ𝑖
∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2)) =
(√‘(𝐸↑2))) |
198 | 166, 79, 168 | ltled 10064 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐸) |
199 | | sqrtsq 13858 |
. . . . . . . . 9
⊢ ((𝐸 ∈ ℝ ∧ 0 ≤
𝐸) →
(√‘(𝐸↑2))
= 𝐸) |
200 | 79, 198, 199 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (√‘(𝐸↑2)) = 𝐸) |
201 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 = 𝐸) |
202 | 197, 200,
201 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 →
(√‘Σ𝑖
∈ 𝑋 ((𝐸 / (√‘(#‘𝑋)))↑2)) = 𝐸) |
203 | 181, 202 | breqtrd 4609 |
. . . . . 6
⊢ (𝜑 →
(√‘Σ𝑖
∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < 𝐸) |
204 | 203 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < 𝐸) |
205 | 70, 77, 80, 134, 204 | lttrd 10077 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸) |
206 | | eqid 2610 |
. . . . . . . 8
⊢
(dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋)) |
207 | 206 | rrxmetfi 39183 |
. . . . . . 7
⊢ (𝑋 ∈ Fin →
(dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
208 | | metxmet 21949 |
. . . . . . 7
⊢
((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ
↑𝑚 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈
(∞Met‘(ℝ ↑𝑚 𝑋))) |
209 | 1, 207, 208 | 3syl 18 |
. . . . . 6
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ
↑𝑚 𝑋))) |
210 | 209 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (dist‘(ℝ^‘𝑋)) ∈
(∞Met‘(ℝ ↑𝑚 𝑋))) |
211 | 80 | rexrd 9968 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝐸 ∈
ℝ*) |
212 | 27, 3 | syl6eleq 2698 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (ℝ ↑𝑚
𝑋)) |
213 | | elbl2 22005 |
. . . . 5
⊢
((((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ
↑𝑚 𝑋)) ∧ 𝐸 ∈ ℝ*) ∧ (𝑌 ∈ (ℝ
↑𝑚 𝑋) ∧ 𝑓 ∈ (ℝ ↑𝑚
𝑋))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸)) |
214 | 210, 211,
17, 212, 213 | syl22anc 1319 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸)) |
215 | 205, 214 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) |
216 | 215 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) |
217 | | dfss3 3558 |
. 2
⊢ (X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) |
218 | 216, 217 | sylibr 223 |
1
⊢ (𝜑 → X𝑖 ∈
𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)) |