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 ∈ ℚ X Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i ∧ ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E

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 − E 2 ⁢ X Y ⁡ i ∈ V
7 6 a1i ⊢ φ ∧ i ∈ X → ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∈ V
8 elmapi ⊢ Y ∈ ℝ X → Y : X ⟶ ℝ
9 3 8 syl ⊢ φ → Y : X ⟶ ℝ
10 9 ffvelrnda ⊢ φ ∧ 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 ⊢ φ → E 2 ⁢ X ∈ ℝ +
21 20 adantr ⊢ φ ∧ i ∈ X → E 2 ⁢ X ∈ ℝ +
22 10 21 ltsubrpd ⊢ φ ∧ i ∈ X → Y ⁡ i − E 2 ⁢ X < Y ⁡ i
23 21 rpred ⊢ φ ∧ i ∈ X → E 2 ⁢ X ∈ ℝ
24 10 23 resubcld ⊢ φ ∧ i ∈ X → Y ⁡ i − E 2 ⁢ X ∈ ℝ
25 24 10 ltnled ⊢ φ ∧ i ∈ X → Y ⁡ i − E 2 ⁢ X < Y ⁡ i ↔ ¬ Y ⁡ i ≤ Y ⁡ i − E 2 ⁢ X
26 22 25 mpbid ⊢ φ ∧ i ∈ X → ¬ Y ⁡ i ≤ Y ⁡ i − E 2 ⁢ X
27 24 rexrd ⊢ φ ∧ i ∈ X → Y ⁡ i − E 2 ⁢ X ∈ ℝ *
28 10 rexrd ⊢ φ ∧ i ∈ X → Y ⁡ i ∈ ℝ *
29 27 28 qinioo ⊢ φ ∧ i ∈ X → ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i = ∅ ↔ Y ⁡ i ≤ Y ⁡ i − E 2 ⁢ X
30 26 29 mtbird ⊢ φ ∧ i ∈ X → ¬ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i = ∅
31 30 neqned ⊢ φ ∧ i ∈ X → ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ≠ ∅
32 1 7 31 choicefi ⊢ φ → ∃ c c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
33 simpl ⊢ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c Fn X
34 nfra1 ⊢ Ⅎ i ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
35 rspa ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ i ∈ X → c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
36 elinel1 ⊢ c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c ⁡ i ∈ ℚ
37 35 36 syl ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ i ∈ X → c ⁡ i ∈ ℚ
38 37 ex ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → i ∈ X → c ⁡ i ∈ ℚ
39 34 38 ralrimi ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → ∀ i ∈ X c ⁡ i ∈ ℚ
40 39 adantl ⊢ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → ∀ i ∈ X c ⁡ i ∈ ℚ
41 33 40 jca ⊢ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ
42 41 adantl ⊢ φ ∧ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ
43 ffnfv ⊢ c : X ⟶ ℚ ↔ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ
44 42 43 sylibr ⊢ φ ∧ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ 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 ⊢ φ ∧ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c ∈ ℚ X ↔ c : X ⟶ ℚ
49 44 48 mpbird ⊢ φ ∧ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c ∈ ℚ X
50 simprr ⊢ φ ∧ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
51 49 50 jca ⊢ φ ∧ c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
52 51 ex ⊢ φ → c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → c ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
53 52 eximdv ⊢ φ → ∃ c c Fn X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → ∃ c c ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
54 32 53 mpd ⊢ φ → ∃ c c ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
55 df-rex ⊢ ∃ c ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ↔ ∃ c c ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
56 54 55 sylibr ⊢ φ → ∃ c ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i
57 5 inex1 ⊢ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∈ V
58 57 a1i ⊢ φ ∧ i ∈ X → ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∈ V
59 10 21 ltaddrpd ⊢ φ ∧ i ∈ X → Y ⁡ i < Y ⁡ i + E 2 ⁢ X
60 10 23 readdcld ⊢ φ ∧ i ∈ X → Y ⁡ i + E 2 ⁢ X ∈ ℝ
61 10 60 ltnled ⊢ φ ∧ i ∈ X → Y ⁡ i < Y ⁡ i + E 2 ⁢ X ↔ ¬ Y ⁡ i + E 2 ⁢ X ≤ Y ⁡ i
62 59 61 mpbid ⊢ φ ∧ i ∈ X → ¬ Y ⁡ i + E 2 ⁢ X ≤ Y ⁡ i
63 60 rexrd ⊢ φ ∧ i ∈ X → Y ⁡ i + E 2 ⁢ X ∈ ℝ *
64 28 63 qinioo ⊢ φ ∧ i ∈ X → ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X = ∅ ↔ Y ⁡ i + E 2 ⁢ X ≤ Y ⁡ i
65 62 64 mtbird ⊢ φ ∧ i ∈ X → ¬ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X = ∅
66 65 neqned ⊢ φ ∧ i ∈ X → ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ≠ ∅
67 1 58 66 choicefi ⊢ φ → ∃ d d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
68 simpl ⊢ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d Fn X
69 nfra1 ⊢ Ⅎ i ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
70 rspa ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
71 elinel1 ⊢ d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d ⁡ i ∈ ℚ
72 70 71 syl ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ ℚ
73 72 ex ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → i ∈ X → d ⁡ i ∈ ℚ
74 69 73 ralrimi ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ i ∈ X d ⁡ i ∈ ℚ
75 74 adantl ⊢ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ i ∈ X d ⁡ i ∈ ℚ
76 68 75 jca ⊢ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ
77 76 adantl ⊢ φ ∧ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ
78 ffnfv ⊢ d : X ⟶ ℚ ↔ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ
79 77 78 sylibr ⊢ φ ∧ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d : X ⟶ ℚ
80 elmapg ⊢ ℚ ∈ V ∧ X ∈ Fin → d ∈ ℚ X ↔ d : X ⟶ ℚ
81 45 1 80 syl2anc ⊢ φ → d ∈ ℚ X ↔ d : X ⟶ ℚ
82 81 adantr ⊢ φ ∧ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d ∈ ℚ X ↔ d : X ⟶ ℚ
83 79 82 mpbird ⊢ φ ∧ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d ∈ ℚ X
84 simprr ⊢ φ ∧ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
85 83 84 jca ⊢ φ ∧ d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d ∈ ℚ X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
86 85 ex ⊢ φ → d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d ∈ ℚ X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
87 86 eximdv ⊢ φ → ∃ d d Fn X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∃ d d ∈ ℚ X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
88 67 87 mpd ⊢ φ → ∃ d d ∈ ℚ X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
89 df-rex ⊢ ∃ d ∈ ℚ X ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ↔ ∃ d d ∈ ℚ X ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
90 88 89 sylibr ⊢ φ → ∃ d ∈ ℚ X ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
91 56 90 jca ⊢ φ → ∃ c ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∃ d ∈ ℚ X ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
92 reeanv ⊢ ∃ c ∈ ℚ X ∃ d ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ↔ ∃ c ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∃ d ∈ ℚ X ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
93 91 92 sylibr ⊢ φ → ∃ c ∈ ℚ X ∃ d ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
94 nfv ⊢ Ⅎ i φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X
95 34 69 nfan ⊢ Ⅎ i ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
96 94 95 nfan ⊢ Ⅎ i φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X
97 1 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → X ∈ Fin
98 2 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → X ≠ ∅
99 3 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ 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 ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ 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 ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → d : X ⟶ ℝ
110 4 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → E ∈ ℝ +
111 35 elin2d ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ i ∈ X → c ⁡ i ∈ Y ⁡ i − E 2 ⁢ X Y ⁡ i
112 111 adantlr ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → c ⁡ i ∈ Y ⁡ i − E 2 ⁢ X Y ⁡ i
113 112 adantll ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → c ⁡ i ∈ Y ⁡ i − E 2 ⁢ X Y ⁡ i
114 70 elin2d ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ Y ⁡ i Y ⁡ i + E 2 ⁢ X
115 114 adantll ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ Y ⁡ i Y ⁡ i + E 2 ⁢ X
116 115 adantll ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ Y ⁡ i Y ⁡ i + E 2 ⁢ X
117 96 97 98 99 105 109 110 113 116 hoiqssbllem1 ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i
118 simpl ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ 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 − E 2 ⁢ X = Y ⁡ k − E 2 ⁢ X
122 121 120 oveq12d ⊢ i = k → Y ⁡ i − E 2 ⁢ X Y ⁡ i = Y ⁡ k − E 2 ⁢ X Y ⁡ k
123 122 ineq2d ⊢ i = k → ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i = ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k
124 119 123 eleq12d ⊢ i = k → c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ↔ c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k
125 124 cbvralvw ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ↔ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k
126 125 biimpi ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i → ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k
127 126 adantr ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k
128 fveq2 ⊢ i = k → d ⁡ i = d ⁡ k
129 120 oveq1d ⊢ i = k → Y ⁡ i + E 2 ⁢ X = Y ⁡ k + E 2 ⁢ X
130 120 129 oveq12d ⊢ i = k → Y ⁡ i Y ⁡ i + E 2 ⁢ X = Y ⁡ k Y ⁡ k + E 2 ⁢ X
131 130 ineq2d ⊢ i = k → ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X = ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
132 128 131 eleq12d ⊢ i = k → d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ↔ d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
133 132 cbvralvw ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X ↔ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
134 133 biimpi ⊢ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
135 134 adantl ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
136 127 135 jca ⊢ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
137 136 adantl ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
138 nfv ⊢ Ⅎ i φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X
139 1 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → X ∈ Fin
140 2 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → X ≠ ∅
141 3 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → Y ∈ ℝ X
142 104 ad2antrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → c : X ⟶ ℝ
143 108 ad2antlr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → d : X ⟶ ℝ
144 4 ad3antrrr ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → E ∈ ℝ +
145 125 111 sylanbr ⊢ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ i ∈ X → c ⁡ i ∈ Y ⁡ i − E 2 ⁢ X Y ⁡ i
146 145 adantlr ⊢ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X ∧ i ∈ X → c ⁡ i ∈ Y ⁡ i − E 2 ⁢ X Y ⁡ i
147 146 adantll ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X ∧ i ∈ X → c ⁡ i ∈ Y ⁡ i − E 2 ⁢ X Y ⁡ i
148 133 114 sylanbr ⊢ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ Y ⁡ i Y ⁡ i + E 2 ⁢ X
149 148 adantll ⊢ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ Y ⁡ i Y ⁡ i + E 2 ⁢ X
150 149 adantll ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X ∧ i ∈ X → d ⁡ i ∈ Y ⁡ i Y ⁡ i + E 2 ⁢ X
151 138 139 140 141 142 143 144 147 150 hoiqssbllem2 ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ k ∈ X c ⁡ k ∈ ℚ ∩ Y ⁡ k − E 2 ⁢ X Y ⁡ k ∧ ∀ k ∈ X d ⁡ k ∈ ℚ ∩ Y ⁡ k Y ⁡ k + E 2 ⁢ X → ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E
152 118 137 151 syl2anc ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E
153 117 152 jca ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X ∧ ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i ∧ ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E
154 153 ex ⊢ φ ∧ c ∈ ℚ X ∧ d ∈ ℚ X → ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i ∧ ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E
155 154 reximdva ⊢ φ ∧ c ∈ ℚ X → ∃ d ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∃ d ∈ ℚ X Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i ∧ ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E
156 155 reximdva ⊢ φ → ∃ c ∈ ℚ X ∃ d ∈ ℚ X ∀ i ∈ X c ⁡ i ∈ ℚ ∩ Y ⁡ i − E 2 ⁢ X Y ⁡ i ∧ ∀ i ∈ X d ⁡ i ∈ ℚ ∩ Y ⁡ i Y ⁡ i + E 2 ⁢ X → ∃ c ∈ ℚ X ∃ d ∈ ℚ X Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i ∧ ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E
157 93 156 mpd ⊢ φ → ∃ c ∈ ℚ X ∃ d ∈ ℚ X Y ∈ ⨉ i ∈ X c ⁡ i d ⁡ i ∧ ⨉ i ∈ X c ⁡ i d ⁡ i ⊆ Y ball ⁡ dist ⁡ X E