hoiqssbllem2 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hoiqssbllem2		Structured version Visualization version GIF version

Theorem hoiqssbllem2 47263

Description: The center of the n-dimensional ball belongs to the half-open interval. (Contributed by Glauco Siliprandi, 24-Dec-2020.)

**Hypotheses**
Ref	Expression
hoiqssbllem2.i	⊢ Ⅎ𝑖𝜑
hoiqssbllem2.x	⊢ (𝜑 → 𝑋 ∈ Fin)
hoiqssbllem2.n	⊢ (𝜑 → 𝑋 ≠ ∅)
hoiqssbllem2.y	⊢ (𝜑 → 𝑌 ∈ (ℝ ↑_m 𝑋))
hoiqssbllem2.c	⊢ (𝜑 → 𝐶:𝑋⟶ℝ)
hoiqssbllem2.d	⊢ (𝜑 → 𝐷:𝑋⟶ℝ)
hoiqssbllem2.e	⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
hoiqssbllem2.l	⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖)))
hoiqssbllem2.r	⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))

**Assertion**
Ref	Expression
hoiqssbllem2	⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))

Distinct variable groups: 𝐶,𝑖 𝐷,𝑖 𝑖,𝐸 𝑖,𝑋 𝑖,𝑌 𝜑,𝑖

Proof of Theorem hoiqssbllem2 Dummy variables 𝑓 𝑔 ℎ 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hoiqssbllem2.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ Fin)
2		eqid 2769	. . . . . . . . . 10 ⊢ (ℝ^‘𝑋) = (ℝ^‘𝑋)
3		eqid 2769	. . . . . . . . . 10 ⊢ (ℝ ↑_m 𝑋) = (ℝ ↑_m 𝑋)
4	2, 3	rrxdsfi 25539	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑_m 𝑋), ℎ ∈ (ℝ ↑_m 𝑋) ↦ (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2))))
5	1, 4	syl 18	. . . . . . . 8 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑_m 𝑋), ℎ ∈ (ℝ ↑_m 𝑋) ↦ (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2))))
6	5	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑_m 𝑋), ℎ ∈ (ℝ ↑_m 𝑋) ↦ (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2))))
7		fveq1 6881	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑌 → (𝑔‘𝑖) = (𝑌‘𝑖))
8	7	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (𝑔‘𝑖) = (𝑌‘𝑖))
9		fveq1 6881	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑓 → (ℎ‘𝑖) = (𝑓‘𝑖))
10	9	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (ℎ‘𝑖) = (𝑓‘𝑖))
11	8, 10	oveq12d 7429	. . . . . . . . . . 11 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → ((𝑔‘𝑖) − (ℎ‘𝑖)) = ((𝑌‘𝑖) − (𝑓‘𝑖)))
12	11	oveq1d 7426	. . . . . . . . . 10 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (((𝑔‘𝑖) − (ℎ‘𝑖))↑2) = (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
13	12	sumeq2sdv 15754	. . . . . . . . 9 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2) = Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
14	13	fveq2d 6886	. . . . . . . 8 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)))
15	14	adantl 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ (𝑔 = 𝑌 ∧ ℎ = 𝑓)) → (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)))
16		hoiqssbllem2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑_m 𝑋))
17	16	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑌 ∈ (ℝ ↑_m 𝑋))
18		hoiqssbllem2.i	. . . . . . . . . 10 ⊢ Ⅎ𝑖𝜑
19		hoiqssbllem2.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶:𝑋⟶ℝ)
20	19	ffvelcdmda 7080	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ)
21		hoiqssbllem2.d	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷:𝑋⟶ℝ)
22	21	ffvelcdmda 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ)
23	22	rexrd 11259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ^*)
24	18, 20, 23	hoissrrn2 47218	. . . . . . . . 9 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (ℝ ↑_m 𝑋))
25	24	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (ℝ ↑_m 𝑋))
26		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
27	25, 26	sseldd 3946	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (ℝ ↑_m 𝑋))
28		fvexd 6897	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ V)
29	6, 15, 17, 27, 28	ovmpod 7563	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)))
30		nfcv 2931	. . . . . . . . . 10 ⊢ Ⅎ𝑖𝑓
31		nfixp1 8916	. . . . . . . . . 10 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))
32	30, 31	nfel 2945	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))
33	18, 32	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
34		simpl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝜑)
35	34, 1	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑋 ∈ Fin)
36		elmapi 8846	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ (ℝ ↑_m 𝑋) → 𝑌:𝑋⟶ℝ)
37	16, 36	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌:𝑋⟶ℝ)
38	37	ffvelcdmda 7080	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ)
39	34, 38	sylan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ)
40		icossre 13455	. . . . . . . . . . . . 13 ⊢ (((𝐶‘𝑖) ∈ ℝ ∧ (𝐷‘𝑖) ∈ ℝ^*) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ)
41	20, 23, 40	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ)
42	41	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ)
43		fvixp2 45842	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
44	43	adantll 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
45	42, 44	sseldd 3946	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
46	39, 45	resubcld 11642	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝑓‘𝑖)) ∈ ℝ)
47		2nn0 12521	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
48	47	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 2 ∈ ℕ₀)
49	46, 48	reexpcld 14199	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ)
50	33, 35, 49	fsumreclf 46218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ)
51		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐶‘𝑖) = (𝐶‘𝑗))
52		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗))
53	51, 52	oveq12d 7429	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
54	53	cbvixpv 8913	. . . . . . . . . 10 ⊢ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))
55	54	eleq2i 2861	. . . . . . . . 9 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
56	55	bilani 509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
57	1	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑋 ∈ Fin)
58		simpll 778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
59	55	biimpri 231	. . . . . . . . . . 11 ⊢ (𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
60	59	ad2antlr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
61		simpr 489	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	58, 60, 61, 49	syl21anc 850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ)
63	46	sqge0d 14173	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
64	58, 60, 61, 63	syl21anc 850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
65	57, 62, 64	fsumge0 15847	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
66	34, 56, 65	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
67	50, 66	resqrtcld 15469	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ ℝ)
68	29, 67	eqeltrd 2869	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) ∈ ℝ)
69	22, 20	resubcld 11642	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ)
70	69	resqcld 14161	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
71	1, 70	fsumrecl 15785	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
72	69	sqge0d 14173	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
73	1, 70, 72	fsumge0 15847	. . . . . . 7 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
74	71, 73	resqrtcld 15469	. . . . . 6 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) ∈ ℝ)
75	74	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) ∈ ℝ)
76		hoiqssbllem2.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
77	76	rpred 13060	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝐸 ∈ ℝ)
79		hoiqssbllem2.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ ∅)
80	79	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑋 ≠ ∅)
81	70	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
82	34, 22	sylan 591	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ)
83	34, 20	sylan 591	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ)
84	82, 83	resubcld 11642	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ)
85	20	rexrd 11259	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ^*)
86	38	rexrd 11259	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ^*)
87		2rp 13021	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ⁺
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 2 ∈ ℝ⁺)
89		hashnncl 14402	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
90	1, 89	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
91	79, 90	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ)
92	91	nnred 12248	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (♯‘𝑋) ∈ ℝ)
93	91	nngt0d 12285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 < (♯‘𝑋))
94	92, 93	elrpd 13057	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (♯‘𝑋) ∈ ℝ⁺)
95	94	rpsqrtcld 15463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ⁺)
96	88, 95	rpmulcld 13076	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · (√‘(♯‘𝑋))) ∈ ℝ⁺)
97	76, 96	rpdivcld 13077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ⁺)
98	97	rpred 13060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
99	98	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
100	38, 99	resubcld 11642	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
101	100	rexrd 11259	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^*)
102		hoiqssbllem2.l	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖)))
103		iooltub 46152	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝑌‘𝑖) ∈ ℝ^* ∧ (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) → (𝐶‘𝑖) < (𝑌‘𝑖))
104	101, 86, 102, 103	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) < (𝑌‘𝑖))
105	20, 38, 104	ltled 11358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ≤ (𝑌‘𝑖))
106	38, 99	readdcld 11238	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
107	106	rexrd 11259	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^*)
108		hoiqssbllem2.r	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
109		ioogtlb 46137	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌‘𝑖) ∈ ℝ^* ∧ ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝑌‘𝑖) < (𝐷‘𝑖))
110	86, 107, 108, 109	syl3anc 1396	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) < (𝐷‘𝑖))
111	85, 23, 86, 105, 110	elicod 13422	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
112	34, 111	sylan 591	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
113		icodiamlt 15489	. . . . . . . . . . . . 13 ⊢ ((((𝐶‘𝑖) ∈ ℝ ∧ (𝐷‘𝑖) ∈ ℝ) ∧ ((𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ∧ (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < ((𝐷‘𝑖) − (𝐶‘𝑖)))
114	83, 82, 112, 44, 113	syl22anc 851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < ((𝐷‘𝑖) − (𝐶‘𝑖)))
115		0red 11211	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ∈ ℝ)
116	20, 38, 22, 105, 110	lelttrd 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) < (𝐷‘𝑖))
117	20, 22	posdifd 11801	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖) < (𝐷‘𝑖) ↔ 0 < ((𝐷‘𝑖) − (𝐶‘𝑖))))
118	116, 117	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐷‘𝑖) − (𝐶‘𝑖)))
119	115, 69, 118	ltled 11358	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ ((𝐷‘𝑖) − (𝐶‘𝑖)))
120	69, 119	absidd 15474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))) = ((𝐷‘𝑖) − (𝐶‘𝑖)))
121	120	eqcomd 2775	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) = (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))))
122	121	adantlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) = (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))))
123	114, 122	breqtrd 5141	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))))
124	46, 84, 123	abslt2sqd 46002	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
125	58, 60, 61, 124	syl21anc 850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
126	57, 80, 62, 81, 125	fsumlt 15852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
127	34, 56, 126	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
128	34, 71	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
129	34, 73	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
130	50, 66, 128, 129	sqrtltd 15479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ↔ (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))))
131	127, 130	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)))
132	29, 131	eqbrtrd 5137	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)))
133	77, 95	rerpdivcld 13091	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / (√‘(♯‘𝑋))) ∈ ℝ)
134	133	resqcld 14161	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
135	134	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
136	22, 20	jca 520	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ))
137	106, 100	jca 520	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ))
138	136, 137	jca 520	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)))
139		iooltub 46152	. . . . . . . . . . . . . 14 ⊢ (((𝑌‘𝑖) ∈ ℝ^* ∧ ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
140	86, 107, 108, 139	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
141		ioogtlb 46137	. . . . . . . . . . . . . 14 ⊢ ((((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝑌‘𝑖) ∈ ℝ^* ∧ (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖))
142	101, 86, 102, 141	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖))
143	140, 142	jca 520	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖)))
144		lt2sub 11712	. . . . . . . . . . . 12 ⊢ ((((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)) → (((𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖)) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))))))
145	138, 143, 144	sylc 66	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))))
146	38	recnd 11237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℂ)
147	99	recnd 11237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℂ)
148	146, 147, 147	pnncand 11608	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))) = ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
149	77	recnd 11237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
150	95	rpcnd 13062	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(♯‘𝑋)) ∈ ℂ)
151		2cnd 12319	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
152	95	rpne0d 13065	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(♯‘𝑋)) ≠ 0)
153	88	rpne0d 13065	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ≠ 0)
154	149, 150, 151, 152, 153	divdiv3d 46001	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋))) / 2) = (𝐸 / (2 · (√‘(♯‘𝑋)))))
155	154	eqcomd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) = ((𝐸 / (√‘(♯‘𝑋))) / 2))
156	155, 155	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (((𝐸 / (√‘(♯‘𝑋))) / 2) + ((𝐸 / (√‘(♯‘𝑋))) / 2)))
157	149, 150, 152	divcld 11991	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 / (√‘(♯‘𝑋))) ∈ ℂ)
158	157	2halvesd 12490	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸 / (√‘(♯‘𝑋))) / 2) + ((𝐸 / (√‘(♯‘𝑋))) / 2)) = (𝐸 / (√‘(♯‘𝑋))))
159	156, 158	eqtrd 2804	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (𝐸 / (√‘(♯‘𝑋))))
160	159	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (𝐸 / (√‘(♯‘𝑋))))
161	148, 160	eqtrd 2804	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))) = (𝐸 / (√‘(♯‘𝑋))))
162	145, 161	breqtrd 5141	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(♯‘𝑋))))
163	133	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (√‘(♯‘𝑋))) ∈ ℝ)
164		0red 11211	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
165	95	rpred 13060	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ)
166	76	rpgt0d 13063	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝐸)
167	95	rpgt0d 13063	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (√‘(♯‘𝑋)))
168	77, 165, 166, 167	divgt0d 12150	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐸 / (√‘(♯‘𝑋))))
169	164, 133, 168	ltled 11358	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝐸 / (√‘(♯‘𝑋))))
170	169	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ (𝐸 / (√‘(♯‘𝑋))))
171		lt2sq 14169	. . . . . . . . . . 11 ⊢ (((((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ ∧ 0 ≤ ((𝐷‘𝑖) − (𝐶‘𝑖))) ∧ ((𝐸 / (√‘(♯‘𝑋))) ∈ ℝ ∧ 0 ≤ (𝐸 / (√‘(♯‘𝑋))))) → (((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(♯‘𝑋))) ↔ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2)))
172	69, 119, 163, 170, 171	syl22anc 851	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(♯‘𝑋))) ↔ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2)))
173	162, 172	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2))
174	1, 79, 70, 135, 173	fsumlt 15852	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))
175	1, 135	fsumrecl 15785	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
176	163	sqge0d 14173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ ((𝐸 / (√‘(♯‘𝑋)))↑2))
177	1, 135, 176	fsumge0 15847	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))
178	71, 73, 175, 177	sqrtltd 15479	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) ↔ (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))))
179	174, 178	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)))
180	134	recnd 11237	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℂ)
181		fsumconst 15841	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ Fin ∧ ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℂ) → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)))
182	1, 180, 181	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)))
183		sqdiv 14157	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ ℂ ∧ (√‘(♯‘𝑋)) ∈ ℂ ∧ (√‘(♯‘𝑋)) ≠ 0) → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)))
184	149, 150, 152, 183	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)))
185	92	recnd 11237	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
186		sqrtth 15416	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑋) ∈ ℂ → ((√‘(♯‘𝑋))↑2) = (♯‘𝑋))
187	185, 186	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(♯‘𝑋))↑2) = (♯‘𝑋))
188	187	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)) = ((𝐸↑2) / (♯‘𝑋)))
189	184, 188	eqtrd 2804	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / (♯‘𝑋)))
190	189	oveq2d 7427	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)) = ((♯‘𝑋) · ((𝐸↑2) / (♯‘𝑋))))
191	149	sqcld 14180	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
192	164, 93	gtned 11345	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑋) ≠ 0)
193	191, 185, 192	divcan2d 11993	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑋) · ((𝐸↑2) / (♯‘𝑋))) = (𝐸↑2))
194	182, 190, 193	3eqtrd 2808	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = (𝐸↑2))
195	194	fveq2d 6886	. . . . . . . 8 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)) = (√‘(𝐸↑2)))
196	164, 77, 166	ltled 11358	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
197		sqrtsq 15320	. . . . . . . . 9 ⊢ ((𝐸 ∈ ℝ ∧ 0 ≤ 𝐸) → (√‘(𝐸↑2)) = 𝐸)
198	77, 196, 197	syl2anc 595	. . . . . . . 8 ⊢ (𝜑 → (√‘(𝐸↑2)) = 𝐸)
199		eqidd 2770	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = 𝐸)
200	195, 198, 199	3eqtrd 2808	. . . . . . 7 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)) = 𝐸)
201	179, 200	breqtrd 5141	. . . . . 6 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < 𝐸)
202	201	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < 𝐸)
203	68, 75, 78, 132, 202	lttrd 11371	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸)
204		eqid 2769	. . . . . . . 8 ⊢ (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
205	204	rrxmetfi 25540	. . . . . . 7 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
206		metxmet 24460	. . . . . . 7 ⊢ ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
207	1, 205, 206	3syl 19	. . . . . 6 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
208	207	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
209	78	rexrd 11259	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝐸 ∈ ℝ^*)
210	27, 3	eleqtrdi 2879	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (ℝ ↑_m 𝑋))
211		elbl2 24516	. . . . 5 ⊢ ((((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)) ∧ 𝐸 ∈ ℝ^*) ∧ (𝑌 ∈ (ℝ ↑_m 𝑋) ∧ 𝑓 ∈ (ℝ ↑_m 𝑋))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸))
212	208, 209, 17, 210, 211	syl22anc 851	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸))
213	203, 212	mpbird 260	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
214	213	ralrimiva 3163	. 2 ⊢ (𝜑 → ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
215		dfss3 3934	. 2 ⊢ (X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
216	214, 215	sylibr 237	1 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 Ⅎwnf 1810 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 Vcvv 3463 ⊆ wss 3913 ∅c0 4294 class class class wbr 5113 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 ∈ cmpo 7413 ↑_m cmap 8824 Xcixp 8895 Fincfn 8943 ℂcc 11098 ℝcr 11099 0cc0 11100 + caddc 11103 · cmul 11105 ℝ^*cxr 11242 < clt 11243 ≤ cle 11244 − cmin 11441 / cdiv 11871 ℕcn 12233 2c2 12295 ℕ₀cn0 12504 ℝ⁺crp 13016 (,)cioo 13372 [,)cico 13374 ↑cexp 14097 ♯chash 14366 √csqrt 15284 abscabs 15285 Σcsu 15737 distcds 17319 ∞Metcxmet 21476 Metcmet 21477 ballcbl 21478 ℝ^crrx 25511

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178 ax-addf 11179 ax-mulf 11180

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7863 df-1st 7986 df-2nd 7987 df-supp 8157 df-tpos 8222 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9322 df-sup 9402 df-oi 9472 df-card 9925 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-z 12592 df-dec 12712 df-uz 12863 df-rp 13017 df-xadd 13138 df-ioo 13376 df-ico 13378 df-fz 13536 df-fzo 13683 df-seq 14038 df-exp 14098 df-hash 14367 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-clim 15539 df-sum 15738 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-starv 17325 df-sca 17326 df-vsca 17327 df-ip 17328 df-tset 17329 df-ple 17330 df-ds 17332 df-unif 17333 df-hom 17334 df-cco 17335 df-0g 17494 df-gsum 17495 df-prds 17500 df-pws 17502 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-mhm 18841 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-ghm 19284 df-cntz 19387 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-cring 20318 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-rhm 20554 df-subrng 20631 df-subrg 20655 df-drng 20815 df-field 20816 df-staf 20920 df-srng 20921 df-lmod 20961 df-lss 21031 df-sra 21272 df-rgmod 21273 df-psmet 21483 df-xmet 21484 df-met 21485 df-bl 21486 df-cnfld 21492 df-refld 21724 df-dsmm 21851 df-frlm 21866 df-nm 24708 df-tng 24710 df-tcph 25297 df-rrx 25513

This theorem is referenced by: hoiqssbllem3 47264

W3C validator