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 47454

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 2760	. . . . . . . . . 10 ⊢ (ℝ^‘𝑋) = (ℝ^‘𝑋)
3		eqid 2760	. . . . . . . . . 10 ⊢ (ℝ ↑_m 𝑋) = (ℝ ↑_m 𝑋)
4	2, 3	rrxdsfi 25642	. . . . . . . . 9 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑_m 𝑋), ℎ ∈ (ℝ ↑_m 𝑋) ↦ (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2))))
5	1, 4	syl 18	. . . . . . . 8 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑_m 𝑋), ℎ ∈ (ℝ ↑_m 𝑋) ↦ (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2))))
6	5	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (dist‘(ℝ^‘𝑋)) = (𝑔 ∈ (ℝ ↑_m 𝑋), ℎ ∈ (ℝ ↑_m 𝑋) ↦ (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2))))
7		fveq1 6878	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑌 → (𝑔‘𝑖) = (𝑌‘𝑖))
8	7	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (𝑔‘𝑖) = (𝑌‘𝑖))
9		fveq1 6878	. . . . . . . . . . . . 13 ⊢ (ℎ = 𝑓 → (ℎ‘𝑖) = (𝑓‘𝑖))
10	9	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (ℎ‘𝑖) = (𝑓‘𝑖))
11	8, 10	oveq12d 7432	. . . . . . . . . . 11 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → ((𝑔‘𝑖) − (ℎ‘𝑖)) = ((𝑌‘𝑖) − (𝑓‘𝑖)))
12	11	oveq1d 7429	. . . . . . . . . 10 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (((𝑔‘𝑖) − (ℎ‘𝑖))↑2) = (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
13	12	sumeq2sdv 15793	. . . . . . . . 9 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2) = Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
14	13	fveq2d 6883	. . . . . . . 8 ⊢ ((𝑔 = 𝑌 ∧ ℎ = 𝑓) → (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)))
15	14	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ (𝑔 = 𝑌 ∧ ℎ = 𝑓)) → (√‘Σ𝑖 ∈ 𝑋 (((𝑔‘𝑖) − (ℎ‘𝑖))↑2)) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)))
16		hoiqssbllem2.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (ℝ ↑_m 𝑋))
17	16	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑌 ∈ (ℝ ↑_m 𝑋))
18		hoiqssbllem2.i	. . . . . . . . . 10 ⊢ Ⅎ𝑖𝜑
19		hoiqssbllem2.c	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶:𝑋⟶ℝ)
20	19	ffvelcdmda 7078	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ)
21		hoiqssbllem2.d	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷:𝑋⟶ℝ)
22	21	ffvelcdmda 7078	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ)
23	22	rexrd 11286	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ^*)
24	18, 20, 23	hoissrrn2 47409	. . . . . . . . 9 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (ℝ ↑_m 𝑋))
25	24	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (ℝ ↑_m 𝑋))
26		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
27	25, 26	sseldd 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (ℝ ↑_m 𝑋))
28		fvexd 6894	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ V)
29	6, 15, 17, 27, 28	ovmpod 7566	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) = (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)))
30		nfcv 2922	. . . . . . . . . 10 ⊢ Ⅎ𝑖𝑓
31		nfixp1 8928	. . . . . . . . . 10 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))
32	30, 31	nfel 2936	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))
33	18, 32	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
34		simpl 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝜑)
35	34, 1	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑋 ∈ Fin)
36		elmapi 8851	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ (ℝ ↑_m 𝑋) → 𝑌:𝑋⟶ℝ)
37	16, 36	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌:𝑋⟶ℝ)
38	37	ffvelcdmda 7078	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ)
39	34, 38	sylan 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ)
40		icossre 13484	. . . . . . . . . . . . 13 ⊢ (((𝐶‘𝑖) ∈ ℝ ∧ (𝐷‘𝑖) ∈ ℝ^*) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ)
41	20, 23, 40	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ)
42	41	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ ℝ)
43		fvixp2 46033	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
44	43	adantll 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
45	42, 44	sseldd 3932	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
46	39, 45	resubcld 11669	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝑓‘𝑖)) ∈ ℝ)
47		2nn0 12548	. . . . . . . . . 10 ⊢ 2 ∈ ℕ₀
48	47	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 2 ∈ ℕ₀)
49	46, 48	reexpcld 14230	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ)
50	33, 35, 49	fsumreclf 46409	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ)
51		fveq2 6879	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐶‘𝑖) = (𝐶‘𝑗))
52		fveq2 6879	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑗 → (𝐷‘𝑖) = (𝐷‘𝑗))
53	51, 52	oveq12d 7432	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
54	53	cbvixpv 8925	. . . . . . . . . 10 ⊢ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) = X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))
55	54	eleq2i 2852	. . . . . . . . 9 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ↔ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
56	55	bilani 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)))
57	1	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑋 ∈ Fin)
58		simpll 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
59	55	biimpri 231	. . . . . . . . . . 11 ⊢ (𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗)) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
60	59	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
61		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	58, 60, 61, 49	syl21anc 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) ∈ ℝ)
63	46	sqge0d 14204	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
64	58, 60, 61, 63	syl21anc 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
65	57, 62, 64	fsumge0 15885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
66	34, 56, 65	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2))
67	50, 66	resqrtcld 15508	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) ∈ ℝ)
68	29, 67	eqeltrd 2860	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) ∈ ℝ)
69	22, 20	resubcld 11669	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ)
70	69	resqcld 14192	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
71	1, 70	fsumrecl 15823	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
72	69	sqge0d 14204	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
73	1, 70, 72	fsumge0 15885	. . . . . . 7 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
74	71, 73	resqrtcld 15508	. . . . . 6 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) ∈ ℝ)
75	74	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) ∈ ℝ)
76		hoiqssbllem2.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
77	76	rpred 13089	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
78	77	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝐸 ∈ ℝ)
79		hoiqssbllem2.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ ∅)
80	79	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → 𝑋 ≠ ∅)
81	70	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ∈ ℝ)
82	34, 22	sylan 592	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ℝ)
83	34, 20	sylan 592	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ)
84	82, 83	resubcld 11669	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ)
85	20	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ ℝ^*)
86	38	rexrd 11286	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℝ^*)
87		2rp 13050	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℝ⁺
88	87	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 2 ∈ ℝ⁺)
89		hashnncl 14433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
90	1, 89	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
91	79, 90	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (♯‘𝑋) ∈ ℕ)
92	91	nnred 12275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (♯‘𝑋) ∈ ℝ)
93	91	nngt0d 12312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 0 < (♯‘𝑋))
94	92, 93	elrpd 13086	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (♯‘𝑋) ∈ ℝ⁺)
95	94	rpsqrtcld 15502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ⁺)
96	88, 95	rpmulcld 13105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (2 · (√‘(♯‘𝑋))) ∈ ℝ⁺)
97	76, 96	rpdivcld 13106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ⁺)
98	97	rpred 13089	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
99	98	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
100	38, 99	resubcld 11669	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
101	100	rexrd 11286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^*)
102		hoiqssbllem2.l	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖)))
103		iooltub 46343	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝑌‘𝑖) ∈ ℝ^* ∧ (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) → (𝐶‘𝑖) < (𝑌‘𝑖))
104	101, 86, 102, 103	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) < (𝑌‘𝑖))
105	20, 38, 104	ltled 11385	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) ≤ (𝑌‘𝑖))
106	38, 99	readdcld 11265	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
107	106	rexrd 11286	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^*)
108		hoiqssbllem2.r	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
109		ioogtlb 46328	. . . . . . . . . . . . . . . 16 ⊢ (((𝑌‘𝑖) ∈ ℝ^* ∧ ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝑌‘𝑖) < (𝐷‘𝑖))
110	86, 107, 108, 109	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) < (𝐷‘𝑖))
111	85, 23, 86, 105, 110	elicod 13451	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
112	34, 111	sylan 592	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))
113		icodiamlt 15528	. . . . . . . . . . . . 13 ⊢ ((((𝐶‘𝑖) ∈ ℝ ∧ (𝐷‘𝑖) ∈ ℝ) ∧ ((𝑌‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ∧ (𝑓‘𝑖) ∈ ((𝐶‘𝑖)[,)(𝐷‘𝑖)))) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < ((𝐷‘𝑖) − (𝐶‘𝑖)))
114	83, 82, 112, 44, 113	syl22anc 852	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < ((𝐷‘𝑖) − (𝐶‘𝑖)))
115		0red 11238	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ∈ ℝ)
116	20, 38, 22, 105, 110	lelttrd 11395	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐶‘𝑖) < (𝐷‘𝑖))
117	20, 22	posdifd 11828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐶‘𝑖) < (𝐷‘𝑖) ↔ 0 < ((𝐷‘𝑖) − (𝐶‘𝑖))))
118	116, 117	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 < ((𝐷‘𝑖) − (𝐶‘𝑖)))
119	115, 69, 118	ltled 11385	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ ((𝐷‘𝑖) − (𝐶‘𝑖)))
120	69, 119	absidd 15513	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))) = ((𝐷‘𝑖) − (𝐶‘𝑖)))
121	120	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) = (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))))
122	121	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) = (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))))
123	114, 122	breqtrd 5131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (abs‘((𝑌‘𝑖) − (𝑓‘𝑖))) < (abs‘((𝐷‘𝑖) − (𝐶‘𝑖))))
124	46, 84, 123	abslt2sqd 46193	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
125	58, 60, 61, 124	syl21anc 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
126	57, 80, 62, 81, 125	fsumlt 15890	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑗 ∈ 𝑋 ((𝐶‘𝑗)[,)(𝐷‘𝑗))) → Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))
127	34, 56, 126	syl2anc 596	. . . . . . 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 15518	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) ↔ (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2))))
131	127, 130	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝑌‘𝑖) − (𝑓‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)))
132	29, 131	eqbrtrd 5127	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)))
133	77, 95	rerpdivcld 13120	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / (√‘(♯‘𝑋))) ∈ ℝ)
134	133	resqcld 14192	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
135	134	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
136	22, 20	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ))
137	106, 100	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ))
138	136, 137	jca 521	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)))
139		iooltub 46343	. . . . . . . . . . . . . 14 ⊢ (((𝑌‘𝑖) ∈ ℝ^* ∧ ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝐷‘𝑖) ∈ ((𝑌‘𝑖)(,)((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
140	86, 107, 108, 139	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
141		ioogtlb 46328	. . . . . . . . . . . . . 14 ⊢ ((((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ^* ∧ (𝑌‘𝑖) ∈ ℝ^* ∧ (𝐶‘𝑖) ∈ (((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌‘𝑖))) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖))
142	101, 86, 102, 141	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖))
143	140, 142	jca 521	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖)))
144		lt2sub 11739	. . . . . . . . . . . 12 ⊢ ((((𝐷‘𝑖) ∈ ℝ ∧ (𝐶‘𝑖) ∈ ℝ) ∧ (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)) → (((𝐷‘𝑖) < ((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∧ ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝐶‘𝑖)) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))))))
145	138, 143, 144	sylc 66	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))))
146	38	recnd 11264	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑌‘𝑖) ∈ ℂ)
147	99	recnd 11264	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℂ)
148	146, 147, 147	pnncand 11635	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))) = ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
149	77	recnd 11264	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐸 ∈ ℂ)
150	95	rpcnd 13091	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(♯‘𝑋)) ∈ ℂ)
151		2cnd 12346	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ∈ ℂ)
152	95	rpne0d 13094	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (√‘(♯‘𝑋)) ≠ 0)
153	88	rpne0d 13094	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 2 ≠ 0)
154	149, 150, 151, 152, 153	divdiv3d 46192	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋))) / 2) = (𝐸 / (2 · (√‘(♯‘𝑋)))))
155	154	eqcomd 2766	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) = ((𝐸 / (√‘(♯‘𝑋))) / 2))
156	155, 155	oveq12d 7432	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (((𝐸 / (√‘(♯‘𝑋))) / 2) + ((𝐸 / (√‘(♯‘𝑋))) / 2)))
157	149, 150, 152	divcld 12018	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸 / (√‘(♯‘𝑋))) ∈ ℂ)
158	157	2halvesd 12517	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸 / (√‘(♯‘𝑋))) / 2) + ((𝐸 / (√‘(♯‘𝑋))) / 2)) = (𝐸 / (√‘(♯‘𝑋))))
159	156, 158	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (𝐸 / (√‘(♯‘𝑋))))
160	159	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐸 / (2 · (√‘(♯‘𝑋)))) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = (𝐸 / (√‘(♯‘𝑋))))
161	148, 160	eqtrd 2795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝑌‘𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) − ((𝑌‘𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))) = (𝐸 / (√‘(♯‘𝑋))))
162	145, 161	breqtrd 5131	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(♯‘𝑋))))
163	133	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐸 / (√‘(♯‘𝑋))) ∈ ℝ)
164		0red 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
165	95	rpred 13089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ)
166	76	rpgt0d 13092	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝐸)
167	95	rpgt0d 13092	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (√‘(♯‘𝑋)))
168	77, 165, 166, 167	divgt0d 12177	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < (𝐸 / (√‘(♯‘𝑋))))
169	164, 133, 168	ltled 11385	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝐸 / (√‘(♯‘𝑋))))
170	169	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ (𝐸 / (√‘(♯‘𝑋))))
171		lt2sq 14200	. . . . . . . . . . 11 ⊢ (((((𝐷‘𝑖) − (𝐶‘𝑖)) ∈ ℝ ∧ 0 ≤ ((𝐷‘𝑖) − (𝐶‘𝑖))) ∧ ((𝐸 / (√‘(♯‘𝑋))) ∈ ℝ ∧ 0 ≤ (𝐸 / (√‘(♯‘𝑋))))) → (((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(♯‘𝑋))) ↔ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2)))
172	69, 119, 163, 170, 171	syl22anc 852	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖)) < (𝐸 / (√‘(♯‘𝑋))) ↔ (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2)))
173	162, 172	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < ((𝐸 / (√‘(♯‘𝑋)))↑2))
174	1, 79, 70, 135, 173	fsumlt 15890	. . . . . . . 8 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))
175	1, 135	fsumrecl 15823	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℝ)
176	163	sqge0d 14204	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 0 ≤ ((𝐸 / (√‘(♯‘𝑋)))↑2))
177	1, 135, 176	fsumge0 15885	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))
178	71, 73, 175, 177	sqrtltd 15518	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2) < Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) ↔ (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2))))
179	174, 178	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)))
180	134	recnd 11264	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℂ)
181		fsumconst 15879	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ Fin ∧ ((𝐸 / (√‘(♯‘𝑋)))↑2) ∈ ℂ) → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)))
182	1, 180, 181	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)))
183		sqdiv 14188	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ ℂ ∧ (√‘(♯‘𝑋)) ∈ ℂ ∧ (√‘(♯‘𝑋)) ≠ 0) → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)))
184	149, 150, 152, 183	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)))
185	92	recnd 11264	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (♯‘𝑋) ∈ ℂ)
186		sqrtth 15455	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝑋) ∈ ℂ → ((√‘(♯‘𝑋))↑2) = (♯‘𝑋))
187	185, 186	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((√‘(♯‘𝑋))↑2) = (♯‘𝑋))
188	187	oveq2d 7430	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸↑2) / ((√‘(♯‘𝑋))↑2)) = ((𝐸↑2) / (♯‘𝑋)))
189	184, 188	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / (√‘(♯‘𝑋)))↑2) = ((𝐸↑2) / (♯‘𝑋)))
190	189	oveq2d 7430	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑋) · ((𝐸 / (√‘(♯‘𝑋)))↑2)) = ((♯‘𝑋) · ((𝐸↑2) / (♯‘𝑋))))
191	149	sqcld 14211	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
192	164, 93	gtned 11372	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑋) ≠ 0)
193	191, 185, 192	divcan2d 12020	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑋) · ((𝐸↑2) / (♯‘𝑋))) = (𝐸↑2))
194	182, 190, 193	3eqtrd 2799	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2) = (𝐸↑2))
195	194	fveq2d 6883	. . . . . . . 8 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)) = (√‘(𝐸↑2)))
196	164, 77, 166	ltled 11385	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
197		sqrtsq 15359	. . . . . . . . 9 ⊢ ((𝐸 ∈ ℝ ∧ 0 ≤ 𝐸) → (√‘(𝐸↑2)) = 𝐸)
198	77, 196, 197	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → (√‘(𝐸↑2)) = 𝐸)
199		eqidd 2761	. . . . . . . 8 ⊢ (𝜑 → 𝐸 = 𝐸)
200	195, 198, 199	3eqtrd 2799	. . . . . . 7 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 ((𝐸 / (√‘(♯‘𝑋)))↑2)) = 𝐸)
201	179, 200	breqtrd 5131	. . . . . 6 ⊢ (𝜑 → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < 𝐸)
202	201	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (√‘Σ𝑖 ∈ 𝑋 (((𝐷‘𝑖) − (𝐶‘𝑖))↑2)) < 𝐸)
203	68, 75, 78, 132, 202	lttrd 11398	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸)
204		eqid 2760	. . . . . . . 8 ⊢ (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
205	204	rrxmetfi 25643	. . . . . . 7 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
206		metxmet 24563	. . . . . . 7 ⊢ ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
207	1, 205, 206	3syl 19	. . . . . 6 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
208	207	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
209	78	rexrd 11286	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝐸 ∈ ℝ^*)
210	27, 3	eleqtrdi 2870	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (ℝ ↑_m 𝑋))
211		elbl2 24619	. . . . 5 ⊢ ((((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)) ∧ 𝐸 ∈ ℝ^*) ∧ (𝑌 ∈ (ℝ ↑_m 𝑋) ∧ 𝑓 ∈ (ℝ ↑_m 𝑋))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸))
212	208, 209, 17, 210, 211	syl22anc 852	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → (𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ (𝑌(dist‘(ℝ^‘𝑋))𝑓) < 𝐸))
213	203, 212	mpbird 260	. . 3 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))) → 𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
214	213	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
215		dfss3 3920	. 2 ⊢ (X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸) ↔ ∀𝑓 ∈ X 𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖))𝑓 ∈ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
216	214, 215	sylibr 237	1 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐶‘𝑖)[,)(𝐷‘𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 Ⅎwnf 1816 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 Vcvv 3450 ⊆ wss 3899 ∅c0 4279 class class class wbr 5103 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 ∈ cmpo 7416 ↑_m cmap 8829 Xcixp 8907 Fincfn 8955 ℂcc 11125 ℝcr 11126 0cc0 11127 + caddc 11130 · cmul 11132 ℝ^*cxr 11269 < clt 11270 ≤ cle 11271 − cmin 11468 / cdiv 11898 ℕcn 12260 2c2 12322 ℕ₀cn0 12531 ℝ⁺crp 13045 (,)cioo 13401 [,)cico 13403 ↑cexp 14128 ♯chash 14397 √csqrt 15323 abscabs 15324 Σcsu 15776 distcds 17354 ∞Metcxmet 21573 Metcmet 21574 ballcbl 21575 ℝ^crrx 25614

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205 ax-addf 11206 ax-mulf 11207

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 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-tpos 8225 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-er 8699 df-map 8831 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-sup 9415 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-rp 13046 df-xadd 13167 df-ioo 13405 df-ico 13407 df-fz 13565 df-fzo 13713 df-seq 14069 df-exp 14129 df-hash 14398 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-clim 15578 df-sum 15777 df-struct 17242 df-sets 17259 df-slot 17277 df-ndx 17289 df-base 17305 df-ress 17326 df-plusg 17358 df-mulr 17359 df-starv 17360 df-sca 17361 df-vsca 17362 df-ip 17363 df-tset 17364 df-ple 17365 df-ds 17367 df-unif 17368 df-hom 17369 df-cco 17370 df-0g 17529 df-gsum 17530 df-prds 17535 df-pws 17537 df-mgm 18733 df-sgrp 18824 df-mnd 18840 df-mhm 18894 df-grp 19063 df-minusg 19064 df-sbg 19065 df-subg 19249 df-ghm 19344 df-cntz 19447 df-cmn 19912 df-abl 19913 df-mgp 20277 df-rng 20291 df-ur 20324 df-ring 20377 df-cring 20378 df-oppr 20481 df-dvdsr 20501 df-unit 20502 df-invr 20532 df-dvr 20545 df-rhm 20616 df-subrng 20711 df-subrg 20735 df-drng 20895 df-field 20896 df-staf 21008 df-srng 21009 df-lmod 21049 df-lss 21119 df-sra 21360 df-rgmod 21361 df-psmet 21580 df-xmet 21581 df-met 21582 df-bl 21583 df-cnfld 21589 df-refld 21821 df-dsmm 21948 df-frlm 21963 df-nm 24811 df-tng 24813 df-tcph 25400 df-rrx 25616

This theorem is used by: hoiqssbllem3 47455

W3C validator