Theorem qndenserrnbllem

Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	qndenserrnbllem.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	qndenserrnbllem.n	⊢ ( 𝜑 → 𝐼 ≠ ∅ )
	qndenserrnbllem.x	⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
	qndenserrnbllem.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
	qndenserrnbllem.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
Assertion	qndenserrnbllem	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		qndenserrnbllem.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
2		qndenserrnbllem.n	⊢ ( 𝜑 → 𝐼 ≠ ∅ )
3		qndenserrnbllem.x	⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
4		qndenserrnbllem.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
5		qndenserrnbllem.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6		inss1	⊢ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ⊆ ℚ
7		qex	⊢ ℚ ∈ V
8		ssexg	⊢ ( ( ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ⊆ ℚ ∧ ℚ ∈ V ) → ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∈ V )
9	6 7 8	mp2an	⊢ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∈ V
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∈ V )
11		elmapi	⊢ ( 𝑋 ∈ ( ℝ ↑m 𝐼 ) → 𝑋 : 𝐼 ⟶ ℝ )
12	3 11	syl	⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ ℝ )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑋 : 𝐼 ⟶ ℝ )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
15	13 14	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℝ )
16	15	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℝ* )
17	5	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ℝ )
19		ne0i	⊢ ( 𝑘 ∈ 𝐼 → 𝐼 ≠ ∅ )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ≠ ∅ )
21		hashnncl	⊢ ( 𝐼 ∈ Fin → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
22	1 21	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( ♯ ‘ 𝐼 ) ∈ ℕ ↔ 𝐼 ≠ ∅ ) )
24	20 23	mpbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) ∈ ℕ )
25	24	nnred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
26		0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 0 ∈ ℝ )
27	24	nngt0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 0 < ( ♯ ‘ 𝐼 ) )
28	26 25 27	ltled	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 0 ≤ ( ♯ ‘ 𝐼 ) )
29	25 28	resqrtcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
30	25 27	elrpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
31	30	sqrtgt0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 0 < ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
32	26 31	gtned	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
33	18 29 32	redivcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
34	15 33	readdcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
35	34	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* )
36	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ℝ+ )
37	29 31	elrpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ+ )
38	36 37	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ+ )
39	15 38	ltaddrpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑘 ) < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
40		qbtwnxr	⊢ ( ( ( 𝑋 ‘ 𝑘 ) ∈ ℝ* ∧ ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* ∧ ( 𝑋 ‘ 𝑘 ) < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) → ∃ 𝑞 ∈ ℚ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
41	16 35 39 40	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∃ 𝑞 ∈ ℚ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
42		df-rex	⊢ ( ∃ 𝑞 ∈ ℚ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ↔ ∃ 𝑞 ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
43	41 42	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∃ 𝑞 ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
44		simprl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → 𝑞 ∈ ℚ )
45	16	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ( 𝑋 ‘ 𝑘 ) ∈ ℝ* )
46	35	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* )
47		qre	⊢ ( 𝑞 ∈ ℚ → 𝑞 ∈ ℝ )
48	47	ad2antrl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → 𝑞 ∈ ℝ )
49		simprrl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ( 𝑋 ‘ 𝑘 ) < 𝑞 )
50		simprrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
51	45 46 48 49 50	eliood	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → 𝑞 ∈ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
52	44 51	elind	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → 𝑞 ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
53	52	ex	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → 𝑞 ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) )
54	53	eximdv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ∃ 𝑞 ( 𝑞 ∈ ℚ ∧ ( ( 𝑋 ‘ 𝑘 ) < 𝑞 ∧ 𝑞 < ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ∃ 𝑞 𝑞 ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) )
55	43 54	mpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∃ 𝑞 𝑞 ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
56		n0	⊢ ( ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ≠ ∅ ↔ ∃ 𝑞 𝑞 ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
57	55 56	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ≠ ∅ )
58	1 10 57	choicefi	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) )
59	6	a1i	⊢ ( 𝑦 Fn 𝐼 → ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ⊆ ℚ )
60	59	sseld	⊢ ( 𝑦 Fn 𝐼 → ( ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑦 ‘ 𝑘 ) ∈ ℚ ) )
61	60	ralimdv	⊢ ( 𝑦 Fn 𝐼 → ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ℚ ) )
62	61	imdistani	⊢ ( ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ℚ ) )
63		ffnfv	⊢ ( 𝑦 : 𝐼 ⟶ ℚ ↔ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ℚ ) )
64	62 63	sylibr	⊢ ( ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → 𝑦 : 𝐼 ⟶ ℚ )
65	64	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝑦 : 𝐼 ⟶ ℚ )
66	7	a1i	⊢ ( 𝜑 → ℚ ∈ V )
67		elmapg	⊢ ( ( ℚ ∈ V ∧ 𝐼 ∈ Fin ) → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ↔ 𝑦 : 𝐼 ⟶ ℚ ) )
68	66 1 67	syl2anc	⊢ ( 𝜑 → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ↔ 𝑦 : 𝐼 ⟶ ℚ ) )
69	68	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ↔ 𝑦 : 𝐼 ⟶ ℚ ) )
70	65 69	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝑦 ∈ ( ℚ ↑m 𝐼 ) )
71		reex	⊢ ℝ ∈ V
72	47	ssriv	⊢ ℚ ⊆ ℝ
73		mapss	⊢ ( ( ℝ ∈ V ∧ ℚ ⊆ ℝ ) → ( ℚ ↑m 𝐼 ) ⊆ ( ℝ ↑m 𝐼 ) )
74	71 72 73	mp2an	⊢ ( ℚ ↑m 𝐼 ) ⊆ ( ℝ ↑m 𝐼 )
75	74	a1i	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ℚ ↑m 𝐼 ) ⊆ ( ℝ ↑m 𝐼 ) )
76	75 70	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝑦 ∈ ( ℝ ↑m 𝐼 ) )
77	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝐼 ∈ Fin )
78	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝐼 ≠ ∅ )
79		eqid	⊢ ( ♯ ‘ 𝐼 ) = ( ♯ ‘ 𝐼 )
80	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
81		simpll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝜑 )
82		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝑦 ‘ 𝑘 ) = ( 𝑦 ‘ 𝑖 ) )
83		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝑋 ‘ 𝑘 ) = ( 𝑋 ‘ 𝑖 ) )
84	83	oveq1d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) = ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
85	83 84	oveq12d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) = ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
86	85	ineq2d	⊢ ( 𝑘 = 𝑖 → ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) = ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
87	82 86	eleq12d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ↔ ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) )
88	87	cbvralvw	⊢ ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ↔ ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
89	88	biimpi	⊢ ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
90	89	adantr	⊢ ( ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
91		simpr	⊢ ( ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
92		rspa	⊢ ( ( ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
93	90 91 92	syl2anc	⊢ ( ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
94	93	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
95		elinel2	⊢ ( ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
96	94 95	syl	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
97		simpr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
98	12	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ )
99	98	3adant2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ )
100		simp2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
101	100	elioored	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ )
102	99	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ* )
103	17	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐸 ∈ ℝ )
104	2 22	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ )
105	104	nnred	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
106	105	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
107		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
108	104	nngt0d	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐼 ) )
109	107 105 108	ltled	⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ 𝐼 ) )
110	109	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 0 ≤ ( ♯ ‘ 𝐼 ) )
111	106 110	resqrtcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
112		sqrtgt0	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℝ ∧ 0 < ( ♯ ‘ 𝐼 ) ) → 0 < ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
113	105 108 112	syl2anc	⊢ ( 𝜑 → 0 < ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
114	107 113	gtned	⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
115	114	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
116	103 111 115	redivcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
117	98 116	readdcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
118	117	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* )
119	118	3adant2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* )
120		ioogtlb	⊢ ( ( ( 𝑋 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑋 ‘ 𝑖 ) < ( 𝑦 ‘ 𝑖 ) )
121	102 119 100 120	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) < ( 𝑦 ‘ 𝑖 ) )
122	99 101 121	ltled	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ≤ ( 𝑦 ‘ 𝑖 ) )
123	99 101 122	abssuble0d	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 𝑦 ‘ 𝑖 ) − ( 𝑋 ‘ 𝑖 ) ) )
124	117	3adant2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
125		iooltub	⊢ ( ( ( 𝑋 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑦 ‘ 𝑖 ) < ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
126	102 119 100 125	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) < ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
127	101 124 99 126	ltsub1dd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑖 ) − ( 𝑋 ‘ 𝑖 ) ) < ( ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) − ( 𝑋 ‘ 𝑖 ) ) )
128	99	recnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℂ )
129	105 109	resqrtcld	⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
130	17 129 114	redivcld	⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
131	130	recnd	⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℂ )
132	131	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℂ )
133	128 132	pncan2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) − ( 𝑋 ‘ 𝑖 ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
134	127 133	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑖 ) − ( 𝑋 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
135	123 134	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
136	81 96 97 135	syl3anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
137	136	adantlrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
138	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝐸 ∈ ℝ+ )
139	105 108	elrpd	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
140	139	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
141	140	rpsqrtcld	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ+ )
142	138 141	rpdivcld	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ+ )
143	77 78 79 80 76 137 142 4	rrndistlt	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
144	138	rpcnd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝐸 ∈ ℂ )
145	140	rpcnd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ♯ ‘ 𝐼 ) ∈ ℂ )
146	145	sqrtcld	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℂ )
147	141	rpne0d	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
148	144 146 147	divcan2d	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) = 𝐸 )
149	143 148	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < 𝐸 )
150	76 149	jca	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) )
151	4	rrxmetfi	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
152	1 151	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
153		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) )
154	152 153	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) )
155	17	rexrd	⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
156		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) ∧ 𝑋 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝐸 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) ) )
157	154 3 155 156	syl3anc	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) ) )
158	157	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) ) )
159	150 158	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
160	70 159	jca	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
161	160	ex	⊢ ( 𝜑 → ( ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) ) )
162	161	eximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) ) )
163	58 162	mpd	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
164		df-rex	⊢ ( ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
165	163 164	sylibr	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )