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 38968

Description: Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 38967 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 1210	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ (Fin ∖ {∅}))
2	1	eldifad 4054	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ∈ Fin)
3		simpl2 1211	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ 𝑋)
4		simpl3 1212	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ 𝑋)
5		rrnval.1	. . . 4 ⊢ 𝑋 = (ℝ ↑_m 𝐼)
6	5	rrnmval 38965	. . 3 ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹(ℝⁿ‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
7	2, 3, 4, 6	syl3anc 1399	. 2 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝⁿ‘𝐼)𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
8		eldifsni 4753	. . . . . 6 ⊢ (𝐼 ∈ (Fin ∖ {∅}) → 𝐼 ≠ ∅)
9	1, 8	syl 18	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐼 ≠ ∅)
10	3, 5	eleqtrdi 2874	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹 ∈ (ℝ ↑_m 𝐼))
11		elmapi 8900	. . . . . . . . 9 ⊢ (𝐹 ∈ (ℝ ↑_m 𝐼) → 𝐹:𝐼⟶ℝ)
12	10, 11	syl 18	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐹:𝐼⟶ℝ)
13	12	ffvelcdmda 7111	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐹‘𝑘) ∈ ℝ)
14	4, 5	eleqtrdi 2874	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺 ∈ (ℝ ↑_m 𝐼))
15		elmapi 8900	. . . . . . . . 9 ⊢ (𝐺 ∈ (ℝ ↑_m 𝐼) → 𝐺:𝐼⟶ℝ)
16	14, 15	syl 18	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝐺:𝐼⟶ℝ)
17	16	ffvelcdmda 7111	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ ℝ)
18	13, 17	resubcld 11774	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ)
19	18	resqcld 14298	. . . . 5 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ)
20		simprl 783	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℝ⁺)
21	20	rpred 13194	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℝ)
22	21	resqcld 14298	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℝ)
23	22	adantr 486	. . . . 5 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (𝑅↑2) ∈ ℝ)
24		absresq 15501	. . . . . . 7 ⊢ (((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℝ → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
25	18, 24	syl 18	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) = (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
26		rrndstprj1.1	. . . . . . . . . 10 ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))
27	26	remetdval 25141	. . . . . . . . 9 ⊢ (((𝐹‘𝑘) ∈ ℝ ∧ (𝐺‘𝑘) ∈ ℝ) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))))
28	13, 17, 27	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) = (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))))
29		simprr 785	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)
30		fveq2 6911	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
31		fveq2 6911	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘))
32	30, 31	oveq12d 7464	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) = ((𝐹‘𝑘)𝑀(𝐺‘𝑘)))
33	32	breq1d 5116	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ↔ ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅))
34	33	rspccva 3579	. . . . . . . . 9 ⊢ ((∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅 ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅)
35	29, 34	sylan 592	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘)𝑀(𝐺‘𝑘)) < 𝑅)
36	28, 35	eqbrtrrd 5133	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅)
37	18	recnd 11367	. . . . . . . . 9 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((𝐹‘𝑘) − (𝐺‘𝑘)) ∈ ℂ)
38	37	abscld 15638	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) ∈ ℝ)
39	21	adantr 486	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 𝑅 ∈ ℝ)
40	37	absge0d 15646	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (abs‘((𝐹‘𝑘) − (𝐺‘𝑘))))
41	20	rpge0d 13198	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ 𝑅)
42	41	adantr 486	. . . . . . . 8 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ 𝑅)
43	38, 39, 40, 42	lt2sqd 14430	. . . . . . 7 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘))) < 𝑅 ↔ ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2)))
44	36, 43	mpbid 235	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → ((abs‘((𝐹‘𝑘) − (𝐺‘𝑘)))↑2) < (𝑅↑2))
45	25, 44	eqbrtrrd 5133	. . . . 5 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < (𝑅↑2))
46	2, 9, 19, 23, 45	fsumlt 15999	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) < Σ𝑘 ∈ 𝐼 (𝑅↑2))
47	2, 19	fsumrecl 15932	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ)
48	18	sqge0d 14310	. . . . . 6 ⊢ ((((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) ∧ 𝑘 ∈ 𝐼) → 0 ≤ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
49	2, 19, 48	fsumge0 15994	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
50		resqrtth 15454	. . . . 5 ⊢ ((Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
51	47, 49, 50	syl2anc 596	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) = Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
52		hashnncl 14540	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ Fin → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
53	2, 52	syl 18	. . . . . . . . . . 11 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((♯‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅))
54	9, 53	mpbird 260	. . . . . . . . . 10 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℕ)
55	54	nnrpd 13192	. . . . . . . . 9 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℝ⁺)
56	55	rpred 13194	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℝ)
57	55	rpge0d 13198	. . . . . . . 8 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (♯‘𝐼))
58		resqrtth 15454	. . . . . . . 8 ⊢ (((♯‘𝐼) ∈ ℝ ∧ 0 ≤ (♯‘𝐼)) → ((√‘(♯‘𝐼))↑2) = (♯‘𝐼))
59	56, 57, 58	syl2anc 596	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘(♯‘𝐼))↑2) = (♯‘𝐼))
60	59	oveq2d 7462	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · ((√‘(♯‘𝐼))↑2)) = ((𝑅↑2) · (♯‘𝐼)))
61	22	recnd 11367	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅↑2) ∈ ℂ)
62	55	rpcnd 13196	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (♯‘𝐼) ∈ ℂ)
63	61, 62	mulcomd 11360	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · (♯‘𝐼)) = ((♯‘𝐼) · (𝑅↑2)))
64	60, 63	eqtrd 2798	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅↑2) · ((√‘(♯‘𝐼))↑2)) = ((♯‘𝐼) · (𝑅↑2)))
65	20	rpcnd 13196	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 𝑅 ∈ ℂ)
66	55	rpsqrtcld 15611	. . . . . . 7 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘(♯‘𝐼)) ∈ ℝ⁺)
67	66	rpcnd 13196	. . . . . 6 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘(♯‘𝐼)) ∈ ℂ)
68	65, 67	sqmuld 14331	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 · (√‘(♯‘𝐼)))↑2) = ((𝑅↑2) · ((√‘(♯‘𝐼))↑2)))
69		fsumconst 15988	. . . . . 6 ⊢ ((𝐼 ∈ Fin ∧ (𝑅↑2) ∈ ℂ) → Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((♯‘𝐼) · (𝑅↑2)))
70	2, 61, 69	syl2anc 596	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → Σ𝑘 ∈ 𝐼 (𝑅↑2) = ((♯‘𝐼) · (𝑅↑2)))
71	64, 68, 70	3eqtr4d 2808	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((𝑅 · (√‘(♯‘𝐼)))↑2) = Σ𝑘 ∈ 𝐼 (𝑅↑2))
72	46, 51, 71	3brtr4d 5141	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 · (√‘(♯‘𝐼)))↑2))
73	47, 49	resqrtcld 15617	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) ∈ ℝ)
74	20, 66	rpmulcld 13210	. . . . 5 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 · (√‘(♯‘𝐼))) ∈ ℝ⁺)
75	74	rpred 13194	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝑅 · (√‘(♯‘𝐼))) ∈ ℝ)
76	47, 49	sqrtge0d 15620	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
77	74	rpge0d 13198	. . . 4 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → 0 ≤ (𝑅 · (√‘(♯‘𝐼))))
78	73, 75, 76, 77	lt2sqd 14430	. . 3 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 · (√‘(♯‘𝐼))) ↔ ((√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))↑2) < ((𝑅 · (√‘(♯‘𝐼)))↑2)))
79	72, 78	mpbird 260	. 2 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) < (𝑅 · (√‘(♯‘𝐼))))
80	7, 79	eqbrtrd 5131	1 ⊢ (((𝐼 ∈ (Fin ∖ {∅}) ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) ∧ (𝑅 ∈ ℝ⁺ ∧ ∀𝑛 ∈ 𝐼 ((𝐹‘𝑛)𝑀(𝐺‘𝑛)) < 𝑅)) → (𝐹(ℝⁿ‘𝐼)𝐺) < (𝑅 · (√‘(♯‘𝐼))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∖ cdif 4048 ∅c0 4281 {csn 4588 class class class wbr 5106 × cxp 5654 ↾ cres 5658 ∘ ccom 5660 ⟶wf 6557 ‘cfv 6561 (class class class)co 7446 ↑_m cmap 8878 Fincfn 9004 ℂcc 11228 ℝcr 11229 0cc0 11230 · cmul 11235 < clt 11373 ≤ cle 11374 − cmin 11571 ℕcn 12365 2c2 12427 ℝ⁺crp 13150 ↑cexp 14234 ♯chash 14504 √csqrt 15432 abscabs 15433 Σcsu 15885 ℝⁿcrrn 38962

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-inf2 9672 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307 ax-pre-sup 11308

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-er 8748 df-map 8880 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-sup 9464 df-oi 9534 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-div 12004 df-nn 12366 df-2 12435 df-3 12436 df-n0 12637 df-z 12724 df-uz 12996 df-rp 13151 df-ico 13512 df-fz 13670 df-fzo 13819 df-seq 14175 df-exp 14235 df-hash 14505 df-cj 15298 df-re 15299 df-im 15300 df-sqrt 15434 df-abs 15435 df-clim 15687 df-sum 15886 df-rrn 38963

This theorem is used by: rrncmslem 38969 rrnequiv 38972

W3C validator