rrndstprj2 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rrndstprj2		Structured version Visualization version GIF version

Theorem rrndstprj2 38166

Description: Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 38165 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)

**Hypotheses**
Ref	Expression
rrnval.1	⊢ 𝑋 = (ℝ ↑_m 𝐼)
rrndstprj1.1	⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))

**Assertion**
Ref	Expression
rrndstprj2	⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝⁿ‘𝐼)𝐺) < (𝑅 · (√‘(♯‘𝐼))))

Distinct variable groups: 𝑛,𝐺 𝑛,𝐼 𝑛,𝑀 𝑅,𝑛 𝑛,𝐹 Allowed substitution hint: 𝑋(𝑛)

Proof of Theorem rrndstprj2 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1193	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ (Fin ∖ {∅}))
2	1	eldifad 3902	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ Fin)
3		simpl2 1194	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ 𝑋)
4		simpl3 1195	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ 𝑋)
5		rrnval.1	. . . 4 ⊢ 𝑋 = (ℝ ↑_m 𝐼)
6	5	rrnmval 38163	. . 3 ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝⁿ‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
7	2, 3, 4, 6	syl3anc 1374	. 2 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝⁿ‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
8		eldifsni 4734	. . . . . 6 ⊢ (𝐼 ∈ (Fin ∖ {∅}) → 𝐼 ≠ ∅)
9	1, 8	syl 17	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ≠ ∅)
10	3, 5	eleqtrdi 2847	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ (ℝ ↑_m 𝐼))
11		elmapi 8789	. . . . . . . . 9 ⊢ (𝐹 ∈ (ℝ ↑_m 𝐼) → 𝐹:𝐼⟶ℝ)
12	10, 11	syl 17	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹:𝐼⟶ℝ)
13	12	ffvelcdmda 7030	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ)
14	4, 5	eleqtrdi 2847	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ (ℝ ↑_m 𝐼))
15		elmapi 8789	. . . . . . . . 9 ⊢ (𝐺 ∈ (ℝ ↑_m 𝐼) → 𝐺:𝐼⟶ℝ)
16	14, 15	syl 17	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺:𝐼⟶ℝ)
17	16	ffvelcdmda 7030	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ)
18	13, 17	resubcld 11569	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ)
19	18	resqcld 14078	. . . . 5 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ)
20		simprl 771	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℝ⁺)
21	20	rpred 12977	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℝ)
22	21	resqcld 14078	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℝ)
23	22	adantr 480	. . . . 5 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑅↑2) ∈ ℝ)
24		absresq 15255	. . . . . . 7 ⊢ (((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
25	18, 24	syl 17	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
26		rrndstprj1.1	. . . . . . . . . 10 ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))
27	26	remetdval 24764	. . . . . . . . 9 ⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))))
28	13, 17, 27	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))))
29		simprr 773	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)
30		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
31		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
32	30, 31	oveq12d 7378	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) = ((𝐹‘𝑘)𝑀(𝐺‘𝑘)))
33	32	breq1d 5096	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ↔ ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅))
34	33	rspccva 3564	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅)
35	29, 34	sylan 581	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅)
36	28, 35	eqbrtrrd 5110	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅)
37	18	recnd 11164	. . . . . . . . 9 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℂ)
38	37	abscld 15392	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) ∈ ℝ)
39	21	adantr 480	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝑅 ∈ ℝ)
40	37	absge0d 15400	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))))
41	20	rpge0d 12981	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ 𝑅)
42	41	adantr 480	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ 𝑅)
43	38, 39, 40, 42	lt2sqd 14209	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅 ↔ ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2)))
44	36, 43	mpbid 232	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2))
45	25, 44	eqbrtrrd 5110	. . . . 5 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < (𝑅↑2))
46	2, 9, 19, 23, 45	fsumlt 15754	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < Σ𝑘 ∈ 𝐼 (𝑅↑2))
47	2, 19	fsumrecl 15687	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ)
48	18	sqge0d 14090	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
49	2, 19, 48	fsumge0 15749	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
50		resqrtth 15208	. . . . 5 ⊢ ((Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
51	47, 49, 50	syl2anc 585	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
52		hashnncl 14319	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ Fin → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
53	2, 52	syl 17	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
54	9, 53	mpbird 257	. . . . . . . . . 10 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℕ)
55	54	nnrpd 12975	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℝ⁺)
56	55	rpred 12977	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℝ)
57	55	rpge0d 12981	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (♯‘𝐼))
58		resqrtth 15208	. . . . . . . 8 ⊢ (((♯‘𝐼) ∈ ℝ ∧ 0 ≤ (♯‘𝐼)) → ((√‘(♯‘𝐼))↑2) = (♯‘𝐼))
59	56, 57, 58	syl2anc 585	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘(♯‘𝐼))↑2) = (♯‘𝐼))
60	59	oveq2d 7376	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · ((√‘(♯‘𝐼))↑2)) = ((𝑅↑2) · (♯‘𝐼)))
61	22	recnd 11164	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℂ)
62	55	rpcnd 12979	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℂ)
63	61, 62	mulcomd 11157	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · (♯‘𝐼)) = ((♯‘𝐼) · (𝑅↑2)))
64	60, 63	eqtrd 2772	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · ((√‘(♯‘𝐼))↑2)) = ((♯‘𝐼) · (𝑅↑2)))
65	20	rpcnd 12979	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℂ)
66	55	rpsqrtcld 15365	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘(♯‘𝐼)) ∈ ℝ⁺)
67	66	rpcnd 12979	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘(♯‘𝐼)) ∈ ℂ)
68	65, 67	sqmuld 14111	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 · (√‘(♯‘𝐼)))↑2) = ((𝑅↑2) · ((√‘(♯‘𝐼))↑2)))
69		fsumconst 15743	. . . . . 6 ⊢ ((𝐼 ∈ Fin ∧ (𝑅↑2) ∈ ℂ) → Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((♯‘𝐼) · (𝑅↑2)))
70	2, 61, 69	syl2anc 585	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((♯‘𝐼) · (𝑅↑2)))
71	64, 68, 70	3eqtr4d 2782	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 · (√‘(♯‘𝐼)))↑2) = Σ𝑘 ∈ 𝐼 (𝑅↑2))
72	46, 51, 71	3brtr4d 5118	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 · (√‘(♯‘𝐼)))↑2))
73	47, 49	resqrtcld 15371	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) ∈ ℝ)
74	20, 66	rpmulcld 12993	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 · (√‘(♯‘𝐼))) ∈ ℝ⁺)
75	74	rpred 12977	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 · (√‘(♯‘𝐼))) ∈ ℝ)
76	47, 49	sqrtge0d 15374	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
77	74	rpge0d 12981	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (𝑅 · (√‘(♯‘𝐼))))
78	73, 75, 76, 77	lt2sqd 14209	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 · (√‘(♯‘𝐼))) ↔ ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 · (√‘(♯‘𝐼)))↑2)))
79	72, 78	mpbird 257	. 2 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 · (√‘(♯‘𝐼))))
80	7, 79	eqbrtrd 5108	1 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝⁿ‘𝐼)𝐺) < (𝑅 · (√‘(♯‘𝐼))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∖ cdif 3887 ∅c0 4274 {csn 4568 class class class wbr 5086 × cxp 5622 ↾ cres 5626 ∘ ccom 5628 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 ↑_m cmap 8766 Fincfn 8886 ℂcc 11027 ℝcr 11028 0cc0 11029 · cmul 11034 < clt 11170 ≤ cle 11171 − cmin 11368 ℕcn 12165 2c2 12227 ℝ⁺crp 12933 ↑cexp 14014 ♯chash 14283 √csqrt 15186 abscabs 15187 Σcsu 15639 ℝⁿcrrn 38160

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-er 8636 df-map 8768 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-sup 9348 df-oi 9418 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-ico 13295 df-fz 13453 df-fzo 13600 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-rrn 38161

This theorem is referenced by: rrncmslem 38167 rrnequiv 38170

W3C validator