Metamath Proof Explorer

Theorem hoiqssbllem3

Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoiqssbllem3.x ⊢φ→X∈Fin
hoiqssbllem3.n ⊢φ→X≠∅
hoiqssbllem3.y ⊢φ→Y∈ℝX
hoiqssbllem3.e ⊢φ→E∈ℝ+
Assertion hoiqssbllem3 ⊢φ→∃c∈ℚX∃d∈ℚXY∈⨉i∈Xc⁡id⁡i∧⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE

Proof

Step Hyp Ref Expression
1 hoiqssbllem3.x ⊢φ→X∈Fin
2 hoiqssbllem3.n ⊢φ→X≠∅
3 hoiqssbllem3.y ⊢φ→Y∈ℝX
4 hoiqssbllem3.e ⊢φ→E∈ℝ+
5 qex ⊢ℚ∈V
6 5 inex1 ⊢ℚ∩Y⁡i−E2⁢XY⁡i∈V
7 6 a1i ⊢φ∧i∈X→ℚ∩Y⁡i−E2⁢XY⁡i∈V
8 elmapi ⊢Y∈ℝX→Y:X⟶ℝ
9 3 8 syl ⊢φ→Y:X⟶ℝ
10 9 ffvelcdmda ⊢φ∧i∈X→Y⁡i∈ℝ
11 2rp ⊢2∈ℝ+
12 11 a1i ⊢φ→2∈ℝ+
13 hashnncl ⊢X∈Fin→X∈ℕ↔X≠∅
14 1 13 syl ⊢φ→X∈ℕ↔X≠∅
15 2 14 mpbird ⊢φ→X∈ℕ
16 nnrp ⊢X∈ℕ→X∈ℝ+
17 15 16 syl ⊢φ→X∈ℝ+
18 17 rpsqrtcld ⊢φ→X∈ℝ+
19 12 18 rpmulcld ⊢φ→2⁢X∈ℝ+
20 4 19 rpdivcld ⊢φ→E2⁢X∈ℝ+
21 20 adantr ⊢φ∧i∈X→E2⁢X∈ℝ+
22 10 21 ltsubrpd ⊢φ∧i∈X→Y⁡i−E2⁢X<Y⁡i
23 21 rpred ⊢φ∧i∈X→E2⁢X∈ℝ
24 10 23 resubcld ⊢φ∧i∈X→Y⁡i−E2⁢X∈ℝ
25 24 10 ltnled ⊢φ∧i∈X→Y⁡i−E2⁢X<Y⁡i↔¬Y⁡i≤Y⁡i−E2⁢X
26 22 25 mpbid ⊢φ∧i∈X→¬Y⁡i≤Y⁡i−E2⁢X
27 24 rexrd ⊢φ∧i∈X→Y⁡i−E2⁢X∈ℝ*
28 10 rexrd ⊢φ∧i∈X→Y⁡i∈ℝ*
29 27 28 qinioo ⊢φ∧i∈X→ℚ∩Y⁡i−E2⁢XY⁡i=∅↔Y⁡i≤Y⁡i−E2⁢X
30 26 29 mtbird ⊢φ∧i∈X→¬ℚ∩Y⁡i−E2⁢XY⁡i=∅
31 30 neqned ⊢φ∧i∈X→ℚ∩Y⁡i−E2⁢XY⁡i≠∅
32 1 7 31 choicefi ⊢φ→∃ccFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
33 simpl ⊢cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→cFnX
34 nfra1 ⊢Ⅎi∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
35 rspa ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧i∈X→c⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
36 elinel1 ⊢c⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→c⁡i∈ℚ
37 35 36 syl ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧i∈X→c⁡i∈ℚ
38 37 ex ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→i∈X→c⁡i∈ℚ
39 34 38 ralrimi ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→∀i∈Xc⁡i∈ℚ
40 39 adantl ⊢cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→∀i∈Xc⁡i∈ℚ
41 33 40 jca ⊢cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→cFnX∧∀i∈Xc⁡i∈ℚ
42 41 adantl ⊢φ∧cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→cFnX∧∀i∈Xc⁡i∈ℚ
43 ffnfv ⊢c:X⟶ℚ↔cFnX∧∀i∈Xc⁡i∈ℚ
44 42 43 sylibr ⊢φ∧cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→c:X⟶ℚ
45 5 a1i ⊢φ→ℚ∈V
46 elmapg ⊢ℚ∈V∧X∈Fin→c∈ℚX↔c:X⟶ℚ
47 45 1 46 syl2anc ⊢φ→c∈ℚX↔c:X⟶ℚ
48 47 adantr ⊢φ∧cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→c∈ℚX↔c:X⟶ℚ
49 44 48 mpbird ⊢φ∧cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→c∈ℚX
50 simprr ⊢φ∧cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
51 49 50 jca ⊢φ∧cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→c∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
52 51 ex ⊢φ→cFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→c∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
53 52 eximdv ⊢φ→∃ccFnX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→∃cc∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
54 32 53 mpd ⊢φ→∃cc∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
55 df-rex ⊢∃c∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i↔∃cc∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
56 54 55 sylibr ⊢φ→∃c∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i
57 5 inex1 ⊢ℚ∩Y⁡iY⁡i+E2⁢X∈V
58 57 a1i ⊢φ∧i∈X→ℚ∩Y⁡iY⁡i+E2⁢X∈V
59 10 21 ltaddrpd ⊢φ∧i∈X→Y⁡i<Y⁡i+E2⁢X
60 10 23 readdcld ⊢φ∧i∈X→Y⁡i+E2⁢X∈ℝ
61 10 60 ltnled ⊢φ∧i∈X→Y⁡i<Y⁡i+E2⁢X↔¬Y⁡i+E2⁢X≤Y⁡i
62 59 61 mpbid ⊢φ∧i∈X→¬Y⁡i+E2⁢X≤Y⁡i
63 60 rexrd ⊢φ∧i∈X→Y⁡i+E2⁢X∈ℝ*
64 28 63 qinioo ⊢φ∧i∈X→ℚ∩Y⁡iY⁡i+E2⁢X=∅↔Y⁡i+E2⁢X≤Y⁡i
65 62 64 mtbird ⊢φ∧i∈X→¬ℚ∩Y⁡iY⁡i+E2⁢X=∅
66 65 neqned ⊢φ∧i∈X→ℚ∩Y⁡iY⁡i+E2⁢X≠∅
67 1 58 66 choicefi ⊢φ→∃ddFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
68 simpl ⊢dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→dFnX
69 nfra1 ⊢Ⅎi∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
70 rspa ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→d⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
71 elinel1 ⊢d⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d⁡i∈ℚ
72 70 71 syl ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→d⁡i∈ℚ
73 72 ex ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→i∈X→d⁡i∈ℚ
74 69 73 ralrimi ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀i∈Xd⁡i∈ℚ
75 74 adantl ⊢dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀i∈Xd⁡i∈ℚ
76 68 75 jca ⊢dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→dFnX∧∀i∈Xd⁡i∈ℚ
77 76 adantl ⊢φ∧dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→dFnX∧∀i∈Xd⁡i∈ℚ
78 ffnfv ⊢d:X⟶ℚ↔dFnX∧∀i∈Xd⁡i∈ℚ
79 77 78 sylibr ⊢φ∧dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d:X⟶ℚ
80 elmapg ⊢ℚ∈V∧X∈Fin→d∈ℚX↔d:X⟶ℚ
81 45 1 80 syl2anc ⊢φ→d∈ℚX↔d:X⟶ℚ
82 81 adantr ⊢φ∧dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d∈ℚX↔d:X⟶ℚ
83 79 82 mpbird ⊢φ∧dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d∈ℚX
84 simprr ⊢φ∧dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
85 83 84 jca ⊢φ∧dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d∈ℚX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
86 85 ex ⊢φ→dFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d∈ℚX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
87 86 eximdv ⊢φ→∃ddFnX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∃dd∈ℚX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
88 67 87 mpd ⊢φ→∃dd∈ℚX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
89 df-rex ⊢∃d∈ℚX∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X↔∃dd∈ℚX∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
90 88 89 sylibr ⊢φ→∃d∈ℚX∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
91 56 90 jca ⊢φ→∃c∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∃d∈ℚX∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
92 reeanv ⊢∃c∈ℚX∃d∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X↔∃c∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∃d∈ℚX∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
93 91 92 sylibr ⊢φ→∃c∈ℚX∃d∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
94 nfv ⊢Ⅎiφ∧c∈ℚX∧d∈ℚX
95 34 69 nfan ⊢Ⅎi∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
96 94 95 nfan ⊢Ⅎiφ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X
97 1 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→X∈Fin
98 2 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→X≠∅
99 3 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→Y∈ℝX
100 elmapi ⊢c∈ℚX→c:X⟶ℚ
101 qssre ⊢ℚ⊆ℝ
102 101 a1i ⊢c∈ℚX→ℚ⊆ℝ
103 100 102 fssd ⊢c∈ℚX→c:X⟶ℝ
104 103 adantl ⊢φ∧c∈ℚX→c:X⟶ℝ
105 104 ad2antrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→c:X⟶ℝ
106 elmapi ⊢d∈ℚX→d:X⟶ℚ
107 101 a1i ⊢d∈ℚX→ℚ⊆ℝ
108 106 107 fssd ⊢d∈ℚX→d:X⟶ℝ
109 108 ad2antlr ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→d:X⟶ℝ
110 4 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→E∈ℝ+
111 35 elin2d ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧i∈X→c⁡i∈Y⁡i−E2⁢XY⁡i
112 111 adantlr ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→c⁡i∈Y⁡i−E2⁢XY⁡i
113 112 adantll ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→c⁡i∈Y⁡i−E2⁢XY⁡i
114 70 elin2d ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→d⁡i∈Y⁡iY⁡i+E2⁢X
115 114 adantll ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→d⁡i∈Y⁡iY⁡i+E2⁢X
116 115 adantll ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X∧i∈X→d⁡i∈Y⁡iY⁡i+E2⁢X
117 96 97 98 99 105 109 110 113 116 hoiqssbllem1 ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→Y∈⨉i∈Xc⁡id⁡i
118 simpl ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→φ∧c∈ℚX∧d∈ℚX
119 fveq2 ⊢i=k→c⁡i=c⁡k
120 fveq2 ⊢i=k→Y⁡i=Y⁡k
121 120 oveq1d ⊢i=k→Y⁡i−E2⁢X=Y⁡k−E2⁢X
122 121 120 oveq12d ⊢i=k→Y⁡i−E2⁢XY⁡i=Y⁡k−E2⁢XY⁡k
123 122 ineq2d ⊢i=k→ℚ∩Y⁡i−E2⁢XY⁡i=ℚ∩Y⁡k−E2⁢XY⁡k
124 119 123 eleq12d ⊢i=k→c⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i↔c⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k
125 124 cbvralvw ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i↔∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k
126 125 biimpi ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i→∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k
127 126 adantr ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k
128 fveq2 ⊢i=k→d⁡i=d⁡k
129 120 oveq1d ⊢i=k→Y⁡i+E2⁢X=Y⁡k+E2⁢X
130 120 129 oveq12d ⊢i=k→Y⁡iY⁡i+E2⁢X=Y⁡kY⁡k+E2⁢X
131 130 ineq2d ⊢i=k→ℚ∩Y⁡iY⁡i+E2⁢X=ℚ∩Y⁡kY⁡k+E2⁢X
132 128 131 eleq12d ⊢i=k→d⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X↔d⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
133 132 cbvralvw ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X↔∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
134 133 biimpi ⊢∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
135 134 adantl ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
136 127 135 jca ⊢∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
137 136 adantl ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
138 nfv ⊢Ⅎiφ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X
139 1 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→X∈Fin
140 2 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→X≠∅
141 3 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→Y∈ℝX
142 104 ad2antrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→c:X⟶ℝ
143 108 ad2antlr ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→d:X⟶ℝ
144 4 ad3antrrr ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→E∈ℝ+
145 125 111 sylanbr ⊢∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧i∈X→c⁡i∈Y⁡i−E2⁢XY⁡i
146 145 adantlr ⊢∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X∧i∈X→c⁡i∈Y⁡i−E2⁢XY⁡i
147 146 adantll ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X∧i∈X→c⁡i∈Y⁡i−E2⁢XY⁡i
148 133 114 sylanbr ⊢∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X∧i∈X→d⁡i∈Y⁡iY⁡i+E2⁢X
149 148 adantll ⊢∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X∧i∈X→d⁡i∈Y⁡iY⁡i+E2⁢X
150 149 adantll ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X∧i∈X→d⁡i∈Y⁡iY⁡i+E2⁢X
151 138 139 140 141 142 143 144 147 150 hoiqssbllem2 ⊢φ∧c∈ℚX∧d∈ℚX∧∀k∈Xc⁡k∈ℚ∩Y⁡k−E2⁢XY⁡k∧∀k∈Xd⁡k∈ℚ∩Y⁡kY⁡k+E2⁢X→⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE
152 118 137 151 syl2anc ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE
153 117 152 jca ⊢φ∧c∈ℚX∧d∈ℚX∧∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→Y∈⨉i∈Xc⁡id⁡i∧⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE
154 153 ex ⊢φ∧c∈ℚX∧d∈ℚX→∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→Y∈⨉i∈Xc⁡id⁡i∧⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE
155 154 reximdva ⊢φ∧c∈ℚX→∃d∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∃d∈ℚXY∈⨉i∈Xc⁡id⁡i∧⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE
156 155 reximdva ⊢φ→∃c∈ℚX∃d∈ℚX∀i∈Xc⁡i∈ℚ∩Y⁡i−E2⁢XY⁡i∧∀i∈Xd⁡i∈ℚ∩Y⁡iY⁡i+E2⁢X→∃c∈ℚX∃d∈ℚXY∈⨉i∈Xc⁡id⁡i∧⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE
157 93 156 mpd ⊢φ→∃c∈ℚX∃d∈ℚXY∈⨉i∈Xc⁡id⁡i∧⨉i∈Xc⁡id⁡i⊆Yball⁡dist⁡msupE