Step | Hyp | Ref
| Expression |
1 | | qndenserrnbllem.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ Fin) |
2 | | inss1 3795 |
. . . . . 6
⊢ (ℚ
∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ⊆ ℚ |
3 | | qex 11676 |
. . . . . 6
⊢ ℚ
∈ V |
4 | | ssexg 4732 |
. . . . . 6
⊢
(((ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ⊆ ℚ ∧ ℚ ∈
V) → (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∈ V) |
5 | 2, 3, 4 | mp2an 704 |
. . . . 5
⊢ (ℚ
∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∈ V |
6 | 5 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∈ V) |
7 | | qndenserrnbllem.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (ℝ ↑𝑚
𝐼)) |
8 | | elmapi 7765 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (ℝ
↑𝑚 𝐼) → 𝑋:𝐼⟶ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋:𝐼⟶ℝ) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑋:𝐼⟶ℝ) |
11 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝑘 ∈ 𝐼) |
12 | 10, 11 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑋‘𝑘) ∈ ℝ) |
13 | 12 | rexrd 9968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑋‘𝑘) ∈
ℝ*) |
14 | | qndenserrnbllem.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
15 | 14 | rpred 11748 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℝ) |
16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈ ℝ) |
17 | | ne0i 3880 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝐼 → 𝐼 ≠ ∅) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐼 ≠ ∅) |
19 | | hashnncl 13018 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ Fin →
((#‘𝐼) ∈ ℕ
↔ 𝐼 ≠
∅)) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅)) |
21 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((#‘𝐼) ∈ ℕ ↔ 𝐼 ≠ ∅)) |
22 | 18, 21 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (#‘𝐼) ∈ ℕ) |
23 | 22 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (#‘𝐼) ∈ ℝ) |
24 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 0 ∈ ℝ) |
25 | 22 | nngt0d 10941 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 0 < (#‘𝐼)) |
26 | 24, 23, 25 | ltled 10064 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 0 ≤ (#‘𝐼)) |
27 | 23, 26 | resqrtcld 14004 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (√‘(#‘𝐼)) ∈
ℝ) |
28 | 23, 25 | elrpd 11745 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (#‘𝐼) ∈
ℝ+) |
29 | 28 | sqrtgt0d 13999 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 0 <
(√‘(#‘𝐼))) |
30 | 24, 29 | gtned 10051 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (√‘(#‘𝐼)) ≠ 0) |
31 | 16, 27, 30 | redivcld 10732 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ) |
32 | 12, 31 | readdcld 9948 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ) |
33 | 32 | rexrd 9968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈
ℝ*) |
34 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → 𝐸 ∈
ℝ+) |
35 | 27, 29 | elrpd 11745 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (√‘(#‘𝐼)) ∈
ℝ+) |
36 | 34, 35 | rpdivcld 11765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈
ℝ+) |
37 | 12, 36 | ltaddrpd 11781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑋‘𝑘) < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))) |
38 | | qbtwnxr 11905 |
. . . . . . . 8
⊢ (((𝑋‘𝑘) ∈ ℝ* ∧ ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ* ∧ (𝑋‘𝑘) < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))) → ∃𝑞 ∈ ℚ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) |
39 | 13, 33, 37, 38 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∃𝑞 ∈ ℚ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) |
40 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑞 ∈
ℚ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))) ↔ ∃𝑞(𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) |
41 | 39, 40 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∃𝑞(𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) |
42 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ ℚ) |
43 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑋‘𝑘) ∈
ℝ*) |
44 | 33 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))) ∈
ℝ*) |
45 | | qre 11669 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ℚ → 𝑞 ∈
ℝ) |
46 | 45 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ ℝ) |
47 | | simprrl 800 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑋‘𝑘) < 𝑞) |
48 | | simprrr 801 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))) |
49 | 43, 44, 46, 47, 48 | eliood 38567 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) |
50 | 42, 49 | elind 3760 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐼) ∧ (𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑞 ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) |
51 | 50 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → 𝑞 ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) |
52 | 51 | eximdv 1833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (∃𝑞(𝑞 ∈ ℚ ∧ ((𝑋‘𝑘) < 𝑞 ∧ 𝑞 < ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → ∃𝑞 𝑞 ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) |
53 | 41, 52 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ∃𝑞 𝑞 ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) |
54 | | n0 3890 |
. . . . 5
⊢ ((ℚ
∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ≠ ∅ ↔ ∃𝑞 𝑞 ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) |
55 | 53, 54 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ≠ ∅) |
56 | 1, 6, 55 | choicefi 38387 |
. . 3
⊢ (𝜑 → ∃𝑦(𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) |
57 | 2 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑦 Fn 𝐼 → (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ⊆ ℚ) |
58 | 57 | sseld 3567 |
. . . . . . . . . . 11
⊢ (𝑦 Fn 𝐼 → ((𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑦‘𝑘) ∈ ℚ)) |
59 | 58 | ralimdv 2946 |
. . . . . . . . . 10
⊢ (𝑦 Fn 𝐼 → (∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ ℚ)) |
60 | 59 | imdistani 722 |
. . . . . . . . 9
⊢ ((𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ ℚ)) |
61 | | ffnfv 6295 |
. . . . . . . . 9
⊢ (𝑦:𝐼⟶ℚ ↔ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ ℚ)) |
62 | 60, 61 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → 𝑦:𝐼⟶ℚ) |
63 | 62 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦:𝐼⟶ℚ) |
64 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℚ ∈
V) |
65 | | elmapg 7757 |
. . . . . . . . 9
⊢ ((ℚ
∈ V ∧ 𝐼 ∈
Fin) → (𝑦 ∈
(ℚ ↑𝑚 𝐼) ↔ 𝑦:𝐼⟶ℚ)) |
66 | 64, 1, 65 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (ℚ ↑𝑚
𝐼) ↔ 𝑦:𝐼⟶ℚ)) |
67 | 66 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (ℚ ↑𝑚
𝐼) ↔ 𝑦:𝐼⟶ℚ)) |
68 | 63, 67 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦 ∈ (ℚ ↑𝑚
𝐼)) |
69 | | reex 9906 |
. . . . . . . . . . 11
⊢ ℝ
∈ V |
70 | 45 | ssriv 3572 |
. . . . . . . . . . 11
⊢ ℚ
⊆ ℝ |
71 | | mapss 7786 |
. . . . . . . . . . 11
⊢ ((ℝ
∈ V ∧ ℚ ⊆ ℝ) → (ℚ
↑𝑚 𝐼) ⊆ (ℝ
↑𝑚 𝐼)) |
72 | 69, 70, 71 | mp2an 704 |
. . . . . . . . . 10
⊢ (ℚ
↑𝑚 𝐼) ⊆ (ℝ
↑𝑚 𝐼) |
73 | 72 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (ℚ
↑𝑚 𝐼) ⊆ (ℝ
↑𝑚 𝐼)) |
74 | 73, 68 | sseldd 3569 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦 ∈ (ℝ ↑𝑚
𝐼)) |
75 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐼 ∈ Fin) |
76 | | qndenserrnbllem.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ≠ ∅) |
77 | 76 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐼 ≠ ∅) |
78 | | eqid 2610 |
. . . . . . . . . 10
⊢
(#‘𝐼) =
(#‘𝐼) |
79 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑋 ∈ (ℝ ↑𝑚
𝐼)) |
80 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖 ∈ 𝐼) → 𝜑) |
81 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → (𝑦‘𝑘) = (𝑦‘𝑖)) |
82 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → (𝑋‘𝑘) = (𝑋‘𝑖)) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑖 → ((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))) = ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) |
84 | 82, 83 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑖 → ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))) = ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) |
85 | 84 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) = (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
86 | 81, 85 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → ((𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ↔ (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))))) |
87 | 86 | cbvralv 3147 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ↔ ∀𝑖 ∈ 𝐼 (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
88 | 87 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) → ∀𝑖 ∈ 𝐼 (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖 ∈ 𝐼) → ∀𝑖 ∈ 𝐼 (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
90 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑘 ∈
𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) |
91 | | rspa 2914 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑖 ∈
𝐼 (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
92 | 89, 90, 91 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((∀𝑘 ∈
𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
93 | 92 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))))) |
94 | | elinel2 3762 |
. . . . . . . . . . . . 13
⊢ ((𝑦‘𝑖) ∈ (ℚ ∩ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) |
96 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) |
97 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑋‘𝑖) ∈ ℝ) |
98 | 97 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑋‘𝑖) ∈ ℝ) |
99 | | ioossre 12106 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ⊆ ℝ |
100 | | simp2 1055 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) |
101 | 99, 100 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) ∈ ℝ) |
102 | 98 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑋‘𝑖) ∈
ℝ*) |
103 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐸 ∈ ℝ) |
104 | 76, 20 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (#‘𝐼) ∈ ℕ) |
105 | 104 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (#‘𝐼) ∈ ℝ) |
106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (#‘𝐼) ∈ ℝ) |
107 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ∈
ℝ) |
108 | 104 | nngt0d 10941 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 < (#‘𝐼)) |
109 | 107, 105,
108 | ltled 10064 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0 ≤ (#‘𝐼)) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 0 ≤ (#‘𝐼)) |
111 | 106, 110 | resqrtcld 14004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (√‘(#‘𝐼)) ∈
ℝ) |
112 | | sqrtgt0 13847 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝐼) ∈
ℝ ∧ 0 < (#‘𝐼)) → 0 <
(√‘(#‘𝐼))) |
113 | 105, 108,
112 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0 <
(√‘(#‘𝐼))) |
114 | 107, 113 | gtned 10051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(√‘(#‘𝐼))
≠ 0) |
115 | 114 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (√‘(#‘𝐼)) ≠ 0) |
116 | 103, 111,
115 | redivcld 10732 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ) |
117 | 97, 116 | readdcld 9948 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ) |
118 | 117 | rexrd 9968 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈
ℝ*) |
119 | 118 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈
ℝ*) |
120 | | ioogtlb 38564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋‘𝑖) ∈ ℝ* ∧ ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ* ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑋‘𝑖) < (𝑦‘𝑖)) |
121 | 102, 119,
100, 120 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑋‘𝑖) < (𝑦‘𝑖)) |
122 | 98, 101, 121 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑋‘𝑖) ≤ (𝑦‘𝑖)) |
123 | 98, 101, 122 | abssuble0d 14019 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑦‘𝑖))) = ((𝑦‘𝑖) − (𝑋‘𝑖))) |
124 | 117 | 3adant2 1073 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ) |
125 | | iooltub 38582 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋‘𝑖) ∈ ℝ* ∧ ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) ∈ ℝ* ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))))) → (𝑦‘𝑖) < ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) |
126 | 102, 119,
100, 125 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑦‘𝑖) < ((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) |
127 | 101, 124,
98, 126 | ltsub1dd 10518 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → ((𝑦‘𝑖) − (𝑋‘𝑖)) < (((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) − (𝑋‘𝑖))) |
128 | 98 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝑋‘𝑖) ∈ ℂ) |
129 | 105, 109 | resqrtcld 14004 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(√‘(#‘𝐼))
∈ ℝ) |
130 | 15, 129, 114 | redivcld 10732 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸 / (√‘(#‘𝐼))) ∈ ℝ) |
131 | 130 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 / (√‘(#‘𝐼))) ∈ ℂ) |
132 | 131 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (𝐸 / (√‘(#‘𝐼))) ∈ ℂ) |
133 | 128, 132 | pncan2d 10273 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼)))) − (𝑋‘𝑖)) = (𝐸 / (√‘(#‘𝐼)))) |
134 | 127, 133 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → ((𝑦‘𝑖) − (𝑋‘𝑖)) < (𝐸 / (√‘(#‘𝐼)))) |
135 | 123, 134 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦‘𝑖) ∈ ((𝑋‘𝑖)(,)((𝑋‘𝑖) + (𝐸 / (√‘(#‘𝐼))))) ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑦‘𝑖))) < (𝐸 / (√‘(#‘𝐼)))) |
136 | 80, 95, 96, 135 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑦‘𝑖))) < (𝐸 / (√‘(#‘𝐼)))) |
137 | 136 | adantlrl 752 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) ∧ 𝑖 ∈ 𝐼) → (abs‘((𝑋‘𝑖) − (𝑦‘𝑖))) < (𝐸 / (√‘(#‘𝐼)))) |
138 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐸 ∈
ℝ+) |
139 | 105, 108 | elrpd 11745 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘𝐼) ∈
ℝ+) |
140 | 139 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (#‘𝐼) ∈
ℝ+) |
141 | 140 | rpsqrtcld 13998 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) →
(√‘(#‘𝐼))
∈ ℝ+) |
142 | 138, 141 | rpdivcld 11765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝐸 / (√‘(#‘𝐼))) ∈
ℝ+) |
143 | | qndenserrnbllem.d |
. . . . . . . . . 10
⊢ 𝐷 =
(dist‘(ℝ^‘𝐼)) |
144 | 75, 77, 78, 79, 74, 137, 142, 143 | rrndistlt 39186 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑋𝐷𝑦) < ((√‘(#‘𝐼)) · (𝐸 / (√‘(#‘𝐼))))) |
145 | 138 | rpcnd 11750 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝐸 ∈ ℂ) |
146 | 140 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (#‘𝐼) ∈ ℂ) |
147 | 146 | sqrtcld 14024 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) →
(√‘(#‘𝐼))
∈ ℂ) |
148 | 141 | rpne0d 11753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) →
(√‘(#‘𝐼))
≠ 0) |
149 | 145, 147,
148 | divcan2d 10682 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) →
((√‘(#‘𝐼)) · (𝐸 / (√‘(#‘𝐼)))) = 𝐸) |
150 | 144, 149 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑋𝐷𝑦) < 𝐸) |
151 | 74, 150 | jca 553 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (ℝ ↑𝑚
𝐼) ∧ (𝑋𝐷𝑦) < 𝐸)) |
152 | 143 | rrxmetfi 39183 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ
↑𝑚 𝐼))) |
153 | 1, 152 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ (Met‘(ℝ
↑𝑚 𝐼))) |
154 | | metxmet 21949 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (Met‘(ℝ
↑𝑚 𝐼)) → 𝐷 ∈ (∞Met‘(ℝ
↑𝑚 𝐼))) |
155 | 153, 154 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ (∞Met‘(ℝ
↑𝑚 𝐼))) |
156 | 15 | rexrd 9968 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
157 | | elbl 22003 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(∞Met‘(ℝ ↑𝑚 𝐼)) ∧ 𝑋 ∈ (ℝ ↑𝑚
𝐼) ∧ 𝐸 ∈ ℝ*) → (𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ (𝑦 ∈ (ℝ ↑𝑚
𝐼) ∧ (𝑋𝐷𝑦) < 𝐸))) |
158 | 155, 7, 156, 157 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ (𝑦 ∈ (ℝ ↑𝑚
𝐼) ∧ (𝑋𝐷𝑦) < 𝐸))) |
159 | 158 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ (𝑦 ∈ (ℝ ↑𝑚
𝐼) ∧ (𝑋𝐷𝑦) < 𝐸))) |
160 | 151, 159 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → 𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) |
161 | 68, 160 | jca 553 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼)))))))) → (𝑦 ∈ (ℚ ↑𝑚
𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸))) |
162 | 161 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → (𝑦 ∈ (ℚ ↑𝑚
𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸)))) |
163 | 162 | eximdv 1833 |
. . 3
⊢ (𝜑 → (∃𝑦(𝑦 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑦‘𝑘) ∈ (ℚ ∩ ((𝑋‘𝑘)(,)((𝑋‘𝑘) + (𝐸 / (√‘(#‘𝐼))))))) → ∃𝑦(𝑦 ∈ (ℚ ↑𝑚
𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸)))) |
164 | 56, 163 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑦(𝑦 ∈ (ℚ ↑𝑚
𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸))) |
165 | | df-rex 2902 |
. 2
⊢
(∃𝑦 ∈
(ℚ ↑𝑚 𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸) ↔ ∃𝑦(𝑦 ∈ (ℚ ↑𝑚
𝐼) ∧ 𝑦 ∈ (𝑋(ball‘𝐷)𝐸))) |
166 | 164, 165 | sylibr 223 |
1
⊢ (𝜑 → ∃𝑦 ∈ (ℚ ↑𝑚
𝐼)𝑦 ∈ (𝑋(ball‘𝐷)𝐸)) |