Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ (Fin ∖
{∅})) |
2 | 1 | eldifad 3586 |
. . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ Fin) |
3 | | simpl2 1065 |
. . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ 𝑋) |
4 | | simpl3 1066 |
. . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ 𝑋) |
5 | | rrnval.1 |
. . . 4
⊢ 𝑋 = (ℝ
↑𝑚 𝐼) |
6 | 5 | rrnmval 33627 |
. . 3
⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) |
7 | 2, 3, 4, 6 | syl3anc 1326 |
. 2
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) |
8 | | eldifsni 4320 |
. . . . . 6
⊢ (𝐼 ∈ (Fin ∖ {∅})
→ 𝐼 ≠
∅) |
9 | 1, 8 | syl 17 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ≠ ∅) |
10 | 3, 5 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ (ℝ ↑𝑚
𝐼)) |
11 | | elmapi 7879 |
. . . . . . . . 9
⊢ (𝐹 ∈ (ℝ
↑𝑚 𝐼) → 𝐹:𝐼⟶ℝ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹:𝐼⟶ℝ) |
13 | 12 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ) |
14 | 4, 5 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ (ℝ ↑𝑚
𝐼)) |
15 | | elmapi 7879 |
. . . . . . . . 9
⊢ (𝐺 ∈ (ℝ
↑𝑚 𝐼) → 𝐺:𝐼⟶ℝ) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺:𝐼⟶ℝ) |
17 | 16 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ) |
18 | 13, 17 | resubcld 10458 |
. . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ) |
19 | 18 | resqcld 13035 |
. . . . 5
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ) |
20 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈
ℝ+) |
21 | 20 | rpred 11872 |
. . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℝ) |
22 | 21 | resqcld 13035 |
. . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℝ) |
23 | 22 | adantr 481 |
. . . . 5
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑅↑2) ∈ ℝ) |
24 | | absresq 14042 |
. . . . . . 7
⊢ (((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) |
25 | 18, 24 | syl 17 |
. . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) |
26 | | rrndstprj1.1 |
. . . . . . . . . 10
⊢ 𝑀 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
27 | 26 | remetdval 22592 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))) |
28 | 13, 17, 27 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))) |
29 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅) |
30 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
31 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
32 | 30, 31 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) = ((𝐹‘𝑘)𝑀(𝐺‘𝑘))) |
33 | 32 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ↔ ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅)) |
34 | 33 | rspccva 3308 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅) |
35 | 29, 34 | sylan 488 |
. . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅) |
36 | 28, 35 | eqbrtrrd 4677 |
. . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅) |
37 | 18 | recnd 10068 |
. . . . . . . . 9
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℂ) |
38 | 37 | abscld 14175 |
. . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) ∈ ℝ) |
39 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝑅 ∈ ℝ) |
40 | 37 | absge0d 14183 |
. . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))) |
41 | 20 | rpge0d 11876 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ 𝑅) |
42 | 41 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ 𝑅) |
43 | 38, 39, 40, 42 | lt2sqd 13043 |
. . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅 ↔ ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2))) |
44 | 36, 43 | mpbid 222 |
. . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2)) |
45 | 25, 44 | eqbrtrrd 4677 |
. . . . 5
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < (𝑅↑2)) |
46 | 2, 9, 19, 23, 45 | fsumlt 14532 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < Σ𝑘 ∈ 𝐼 (𝑅↑2)) |
47 | 2, 19 | fsumrecl 14465 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ) |
48 | 18 | sqge0d 13036 |
. . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) |
49 | 2, 19, 48 | fsumge0 14527 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) |
50 | | resqrtth 13996 |
. . . . 5
⊢
((Σ𝑘 ∈
𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ ∧ 0 ≤
Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) →
((√‘Σ𝑘
∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) |
51 | 47, 49, 50 | syl2anc 693 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) |
52 | | hashnncl 13157 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ Fin →
((#‘𝐼) ∈ ℕ
↔ 𝐼 ≠
∅)) |
53 | 2, 52 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅)) |
54 | 9, 53 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (#‘𝐼) ∈ ℕ) |
55 | 54 | nnrpd 11870 |
. . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (#‘𝐼) ∈
ℝ+) |
56 | 55 | rpred 11872 |
. . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (#‘𝐼) ∈ ℝ) |
57 | 55 | rpge0d 11876 |
. . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (#‘𝐼)) |
58 | | resqrtth 13996 |
. . . . . . . 8
⊢
(((#‘𝐼) ∈
ℝ ∧ 0 ≤ (#‘𝐼)) → ((√‘(#‘𝐼))↑2) = (#‘𝐼)) |
59 | 56, 57, 58 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘(#‘𝐼))↑2) = (#‘𝐼)) |
60 | 59 | oveq2d 6666 |
. . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) ·
((√‘(#‘𝐼))↑2)) = ((𝑅↑2) · (#‘𝐼))) |
61 | 22 | recnd 10068 |
. . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℂ) |
62 | 55 | rpcnd 11874 |
. . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (#‘𝐼) ∈ ℂ) |
63 | 61, 62 | mulcomd 10061 |
. . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · (#‘𝐼)) = ((#‘𝐼) · (𝑅↑2))) |
64 | 60, 63 | eqtrd 2656 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) ·
((√‘(#‘𝐼))↑2)) = ((#‘𝐼) · (𝑅↑2))) |
65 | 20 | rpcnd 11874 |
. . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℂ) |
66 | 55 | rpsqrtcld 14150 |
. . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘(#‘𝐼)) ∈
ℝ+) |
67 | 66 | rpcnd 11874 |
. . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘(#‘𝐼)) ∈
ℂ) |
68 | 65, 67 | sqmuld 13020 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 · (√‘(#‘𝐼)))↑2) = ((𝑅↑2) ·
((√‘(#‘𝐼))↑2))) |
69 | | fsumconst 14522 |
. . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑅↑2) ∈ ℂ) →
Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((#‘𝐼) · (𝑅↑2))) |
70 | 2, 61, 69 | syl2anc 693 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((#‘𝐼) · (𝑅↑2))) |
71 | 64, 68, 70 | 3eqtr4d 2666 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 · (√‘(#‘𝐼)))↑2) = Σ𝑘 ∈ 𝐼 (𝑅↑2)) |
72 | 46, 51, 71 | 3brtr4d 4685 |
. . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 · (√‘(#‘𝐼)))↑2)) |
73 | 47, 49 | resqrtcld 14156 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) ∈ ℝ) |
74 | 20, 66 | rpmulcld 11888 |
. . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 · (√‘(#‘𝐼))) ∈
ℝ+) |
75 | 74 | rpred 11872 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 · (√‘(#‘𝐼))) ∈
ℝ) |
76 | 47, 49 | sqrtge0d 14159 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) |
77 | 74 | rpge0d 11876 |
. . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (𝑅 · (√‘(#‘𝐼)))) |
78 | 73, 75, 76, 77 | lt2sqd 13043 |
. . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 · (√‘(#‘𝐼))) ↔
((√‘Σ𝑘
∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 · (√‘(#‘𝐼)))↑2))) |
79 | 72, 78 | mpbird 247 |
. 2
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 · (√‘(#‘𝐼)))) |
80 | 7, 79 | eqbrtrd 4675 |
1
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) < (𝑅 · (√‘(#‘𝐼)))) |