| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1 1191 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ (Fin ∖
{∅})) | 
| 2 | 1 | eldifad 3962 | . . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ Fin) | 
| 3 |  | simpl2 1192 | . . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ 𝑋) | 
| 4 |  | simpl3 1193 | . . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ 𝑋) | 
| 5 |  | rrnval.1 | . . . 4
⊢ 𝑋 = (ℝ ↑m
𝐼) | 
| 6 | 5 | rrnmval 37836 | . . 3
⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | 
| 7 | 2, 3, 4, 6 | syl3anc 1372 | . 2
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | 
| 8 |  | eldifsni 4789 | . . . . . 6
⊢ (𝐼 ∈ (Fin ∖ {∅})
→ 𝐼 ≠
∅) | 
| 9 | 1, 8 | syl 17 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ≠ ∅) | 
| 10 | 3, 5 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ (ℝ ↑m 𝐼)) | 
| 11 |  | elmapi 8890 | . . . . . . . . 9
⊢ (𝐹 ∈ (ℝ
↑m 𝐼)
→ 𝐹:𝐼⟶ℝ) | 
| 12 | 10, 11 | syl 17 | . . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹:𝐼⟶ℝ) | 
| 13 | 12 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ) | 
| 14 | 4, 5 | eleqtrdi 2850 | . . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ (ℝ ↑m 𝐼)) | 
| 15 |  | elmapi 8890 | . . . . . . . . 9
⊢ (𝐺 ∈ (ℝ
↑m 𝐼)
→ 𝐺:𝐼⟶ℝ) | 
| 16 | 14, 15 | syl 17 | . . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺:𝐼⟶ℝ) | 
| 17 | 16 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ) | 
| 18 | 13, 17 | resubcld 11692 | . . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ) | 
| 19 | 18 | resqcld 14166 | . . . . 5
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ) | 
| 20 |  | simprl 770 | . . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈
ℝ+) | 
| 21 | 20 | rpred 13078 | . . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℝ) | 
| 22 | 21 | resqcld 14166 | . . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℝ) | 
| 23 | 22 | adantr 480 | . . . . 5
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑅↑2) ∈ ℝ) | 
| 24 |  | absresq 15342 | . . . . . . 7
⊢ (((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | 
| 25 | 18, 24 | syl 17 | . . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | 
| 26 |  | rrndstprj1.1 | . . . . . . . . . 10
⊢ 𝑀 = ((abs ∘ − )
↾ (ℝ × ℝ)) | 
| 27 | 26 | remetdval 24811 | . . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))) | 
| 28 | 13, 17, 27 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))) | 
| 29 |  | simprr 772 | . . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅) | 
| 30 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) | 
| 31 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) | 
| 32 | 30, 31 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) = ((𝐹‘𝑘)𝑀(𝐺‘𝑘))) | 
| 33 | 32 | breq1d 5152 | . . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ↔ ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅)) | 
| 34 | 33 | rspccva 3620 | . . . . . . . . 9
⊢
((∀𝑛 ∈
𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅) | 
| 35 | 29, 34 | sylan 580 | . . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅) | 
| 36 | 28, 35 | eqbrtrrd 5166 | . . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅) | 
| 37 | 18 | recnd 11290 | . . . . . . . . 9
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℂ) | 
| 38 | 37 | abscld 15476 | . . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) ∈ ℝ) | 
| 39 | 21 | adantr 480 | . . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝑅 ∈ ℝ) | 
| 40 | 37 | absge0d 15484 | . . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))) | 
| 41 | 20 | rpge0d 13082 | . . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ 𝑅) | 
| 42 | 41 | adantr 480 | . . . . . . . 8
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ 𝑅) | 
| 43 | 38, 39, 40, 42 | lt2sqd 14296 | . . . . . . 7
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅 ↔ ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2))) | 
| 44 | 36, 43 | mpbid 232 | . . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2)) | 
| 45 | 25, 44 | eqbrtrrd 5166 | . . . . 5
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < (𝑅↑2)) | 
| 46 | 2, 9, 19, 23, 45 | fsumlt 15837 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < Σ𝑘 ∈ 𝐼 (𝑅↑2)) | 
| 47 | 2, 19 | fsumrecl 15771 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ) | 
| 48 | 18 | sqge0d 14178 | . . . . . 6
⊢ ((((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | 
| 49 | 2, 19, 48 | fsumge0 15832 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | 
| 50 |  | resqrtth 15295 | . . . . 5
⊢
((Σ𝑘 ∈
𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ ∧ 0 ≤
Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) →
((√‘Σ𝑘
∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | 
| 51 | 47, 49, 50 | syl2anc 584 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | 
| 52 |  | hashnncl 14406 | . . . . . . . . . . . 12
⊢ (𝐼 ∈ Fin →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) | 
| 53 | 2, 52 | syl 17 | . . . . . . . . . . 11
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅)) | 
| 54 | 9, 53 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℕ) | 
| 55 | 54 | nnrpd 13076 | . . . . . . . . 9
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈
ℝ+) | 
| 56 | 55 | rpred 13078 | . . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℝ) | 
| 57 | 55 | rpge0d 13082 | . . . . . . . 8
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (♯‘𝐼)) | 
| 58 |  | resqrtth 15295 | . . . . . . . 8
⊢
(((♯‘𝐼)
∈ ℝ ∧ 0 ≤ (♯‘𝐼)) →
((√‘(♯‘𝐼))↑2) = (♯‘𝐼)) | 
| 59 | 56, 57, 58 | syl2anc 584 | . . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) →
((√‘(♯‘𝐼))↑2) = (♯‘𝐼)) | 
| 60 | 59 | oveq2d 7448 | . . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) ·
((√‘(♯‘𝐼))↑2)) = ((𝑅↑2) · (♯‘𝐼))) | 
| 61 | 22 | recnd 11290 | . . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℂ) | 
| 62 | 55 | rpcnd 13080 | . . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℂ) | 
| 63 | 61, 62 | mulcomd 11283 | . . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · (♯‘𝐼)) = ((♯‘𝐼) · (𝑅↑2))) | 
| 64 | 60, 63 | eqtrd 2776 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) ·
((√‘(♯‘𝐼))↑2)) = ((♯‘𝐼) · (𝑅↑2))) | 
| 65 | 20 | rpcnd 13080 | . . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℂ) | 
| 66 | 55 | rpsqrtcld 15451 | . . . . . . 7
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) →
(√‘(♯‘𝐼)) ∈
ℝ+) | 
| 67 | 66 | rpcnd 13080 | . . . . . 6
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) →
(√‘(♯‘𝐼)) ∈ ℂ) | 
| 68 | 65, 67 | sqmuld 14199 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 ·
(√‘(♯‘𝐼)))↑2) = ((𝑅↑2) ·
((√‘(♯‘𝐼))↑2))) | 
| 69 |  | fsumconst 15827 | . . . . . 6
⊢ ((𝐼 ∈ Fin ∧ (𝑅↑2) ∈ ℂ) →
Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((♯‘𝐼) · (𝑅↑2))) | 
| 70 | 2, 61, 69 | syl2anc 584 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((♯‘𝐼) · (𝑅↑2))) | 
| 71 | 64, 68, 70 | 3eqtr4d 2786 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 ·
(√‘(♯‘𝐼)))↑2) = Σ𝑘 ∈ 𝐼 (𝑅↑2)) | 
| 72 | 46, 51, 71 | 3brtr4d 5174 | . . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 ·
(√‘(♯‘𝐼)))↑2)) | 
| 73 | 47, 49 | resqrtcld 15457 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) ∈ ℝ) | 
| 74 | 20, 66 | rpmulcld 13094 | . . . . 5
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 ·
(√‘(♯‘𝐼))) ∈
ℝ+) | 
| 75 | 74 | rpred 13078 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 ·
(√‘(♯‘𝐼))) ∈ ℝ) | 
| 76 | 47, 49 | sqrtge0d 15460 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | 
| 77 | 74 | rpge0d 13082 | . . . 4
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (𝑅 ·
(√‘(♯‘𝐼)))) | 
| 78 | 73, 75, 76, 77 | lt2sqd 14296 | . . 3
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 ·
(√‘(♯‘𝐼))) ↔ ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 ·
(√‘(♯‘𝐼)))↑2))) | 
| 79 | 72, 78 | mpbird 257 | . 2
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 ·
(√‘(♯‘𝐼)))) | 
| 80 | 7, 79 | eqbrtrd 5164 | 1
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧
∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝn‘𝐼)𝐺) < (𝑅 ·
(√‘(♯‘𝐼)))) |