Theorem hoiqssbllem1

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

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

Proof

Step	Hyp	Ref	Expression
1		hoiqssbllem1.i	⊢ Ⅎ 𝑖 𝜑
2		hoiqssbllem1.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		hoiqssbllem1.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
4		hoiqssbllem1.y	⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
5		hoiqssbllem1.c	⊢ ( 𝜑 → 𝐶 : 𝑋 ⟶ ℝ )
6		hoiqssbllem1.d	⊢ ( 𝜑 → 𝐷 : 𝑋 ⟶ ℝ )
7		hoiqssbllem1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8		hoiqssbllem1.l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
9		hoiqssbllem1.r	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
10	4	elexd	⊢ ( 𝜑 → 𝑌 ∈ V )
11		elmapfn	⊢ ( 𝑌 ∈ ( ℝ ↑m 𝑋 ) → 𝑌 Fn 𝑋 )
12	4 11	syl	⊢ ( 𝜑 → 𝑌 Fn 𝑋 )
13	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
14	13	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ* )
15	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ )
16	15	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐷 ‘ 𝑖 ) ∈ ℝ* )
17		elmapi	⊢ ( 𝑌 ∈ ( ℝ ↑m 𝑋 ) → 𝑌 : 𝑋 ⟶ ℝ )
18	4 17	syl	⊢ ( 𝜑 → 𝑌 : 𝑋 ⟶ ℝ )
19	18	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ )
20	19	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ* )
21		2rp	⊢ 2 ∈ ℝ+
22	21	a1i	⊢ ( 𝜑 → 2 ∈ ℝ+ )
23		hashnncl	⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
24	2 23	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
25	3 24	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
26	25	nnred	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ )
27	25	nngt0d	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑋 ) )
28	26 27	elrpd	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ+ )
29	28	rpsqrtcld	⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℝ+ )
30	22 29	rpmulcld	⊢ ( 𝜑 → ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ+ )
31	7 30	rpdivcld	⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ+ )
32	31	rpred	⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
34	19 33	resubcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
35	34	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
36		iooltub	⊢ ( ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( 𝐶 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( 𝐶 ‘ 𝑖 ) < ( 𝑌 ‘ 𝑖 ) )
37	35 20 8 36	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) < ( 𝑌 ‘ 𝑖 ) )
38	13 19 37	ltled	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐶 ‘ 𝑖 ) ≤ ( 𝑌 ‘ 𝑖 ) )
39	19 33	readdcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
40	39	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
41		ioogtlb	⊢ ( ( ( 𝑌 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* ∧ ( 𝐷 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝑌 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
42	20 40 9 41	syl3anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) < ( 𝐷 ‘ 𝑖 ) )
43	14 16 20 38 42	elicod	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
44	43	ex	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑋 → ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) )
45	1 44	ralrimi	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑋 ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )
46	10 12 45	3jca	⊢ ( 𝜑 → ( 𝑌 ∈ V ∧ 𝑌 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) )
47		elixp2	⊢ ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ↔ ( 𝑌 ∈ V ∧ 𝑌 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑌 ‘ 𝑖 ) ∈ ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) ) )
48	46 47	sylibr	⊢ ( 𝜑 → 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝐶 ‘ 𝑖 ) [,) ( 𝐷 ‘ 𝑖 ) ) )