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	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑘 ) ∈ ℝ )
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	birani	⊢ ( ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
90		simpr	⊢ ( ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
91		rspa	⊢ ( ( ∀ 𝑖 ∈ 𝐼 ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
92	89 90 91	syl2anc	⊢ ( ( ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
93	92	adantll	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) )
94		elinel2	⊢ ( ( 𝑦 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
95	93 94	syl	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
96		simpr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → 𝑖 ∈ 𝐼 )
97	12	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ )
98	97	3adant2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ )
99		simp2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) )
100	99	elioored	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ )
101	98	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℝ* )
102	17	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 𝐸 ∈ ℝ )
103	2 22	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ )
104	103	nnred	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
105	104	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ♯ ‘ 𝐼 ) ∈ ℝ )
106		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
107	103	nngt0d	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝐼 ) )
108	106 104 107	ltled	⊢ ( 𝜑 → 0 ≤ ( ♯ ‘ 𝐼 ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → 0 ≤ ( ♯ ‘ 𝐼 ) )
110	105 109	resqrtcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
111		sqrtgt0	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℝ ∧ 0 < ( ♯ ‘ 𝐼 ) ) → 0 < ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
112	104 107 111	syl2anc	⊢ ( 𝜑 → 0 < ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
113	106 112	gtned	⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
114	113	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
115	102 110 114	redivcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
116	97 115	readdcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
117	116	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* )
118	117	3adant2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* )
119		ioogtlb	⊢ ( ( ( 𝑋 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑋 ‘ 𝑖 ) < ( 𝑦 ‘ 𝑖 ) )
120	101 118 99 119	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) < ( 𝑦 ‘ 𝑖 ) )
121	98 100 120	ltled	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ≤ ( 𝑦 ‘ 𝑖 ) )
122	98 100 121	abssuble0d	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 𝑦 ‘ 𝑖 ) − ( 𝑋 ‘ 𝑖 ) ) )
123	116	3adant2	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ )
124		iooltub	⊢ ( ( ( 𝑋 ‘ 𝑖 ) ∈ ℝ* ∧ ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ∈ ℝ* ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) → ( 𝑦 ‘ 𝑖 ) < ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
125	101 118 99 124	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 ‘ 𝑖 ) < ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
126	100 123 98 125	ltsub1dd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑖 ) − ( 𝑋 ‘ 𝑖 ) ) < ( ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) − ( 𝑋 ‘ 𝑖 ) ) )
127	98	recnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑖 ) ∈ ℂ )
128	104 108	resqrtcld	⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
129	17 128 113	redivcld	⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ )
130	129	recnd	⊢ ( 𝜑 → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℂ )
131	130	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℂ )
132	127 131	pncan2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) − ( 𝑋 ‘ 𝑖 ) ) = ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
133	126 132	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑖 ) − ( 𝑋 ‘ 𝑖 ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
134	122 133	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ‘ 𝑖 ) ∈ ( ( 𝑋 ‘ 𝑖 ) (,) ( ( 𝑋 ‘ 𝑖 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
135	81 95 96 134	syl3anc	⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
136	135	adantlrl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝐼 ) → ( abs ‘ ( ( 𝑋 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ) < ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) )
137	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝐸 ∈ ℝ+ )
138	104 107	elrpd	⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
139	138	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ♯ ‘ 𝐼 ) ∈ ℝ+ )
140	139	rpsqrtcld	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ+ )
141	137 140	rpdivcld	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ∈ ℝ+ )
142	77 78 79 80 76 136 141 4	rrndistlt	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) )
143	137	rpcnd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝐸 ∈ ℂ )
144	139	rpcnd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ♯ ‘ 𝐼 ) ∈ ℂ )
145	144	sqrtcld	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℂ )
146	140	rpne0d	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≠ 0 )
147	143 145 146	divcan2d	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) = 𝐸 )
148	142 147	breqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑋 𝐷 𝑦 ) < 𝐸 )
149	76 148	jca	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) )
150	4	rrxmetfi	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
151	1 150	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
152		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) )
153	151 152	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) )
154	17	rexrd	⊢ ( 𝜑 → 𝐸 ∈ ℝ* )
155		elbl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) ∧ 𝑋 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝐸 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) ) )
156	153 3 154 155	syl3anc	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) ) )
157	156	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ( 𝑦 ∈ ( ℝ ↑m 𝐼 ) ∧ ( 𝑋 𝐷 𝑦 ) < 𝐸 ) ) )
158	149 157	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )
159	70 158	jca	⊢ ( ( 𝜑 ∧ ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
160	159	ex	⊢ ( 𝜑 → ( ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) ) )
161	160	eximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑦 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑋 ‘ 𝑘 ) (,) ( ( 𝑋 ‘ 𝑘 ) + ( 𝐸 / ( √ ‘ ( ♯ ‘ 𝐼 ) ) ) ) ) ) ) → ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) ) )
162	58 161	mpd	⊢ ( 𝜑 → ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
163		df-rex	⊢ ( ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) ) )
164	162 163	sylibr	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝐸 ) )