Step | Hyp | Ref
| Expression |
1 | | lmrel 21981 |
. 2
⊢ Rel
(⇝𝑡‘𝐽) |
2 | | fvex 6687 |
. . . . . . . 8
⊢ ( ⇝
‘(𝑡 ∈ ℕ
↦ ((𝐹‘𝑡)‘𝑚))) ∈ V |
3 | | rrncms.7 |
. . . . . . . 8
⊢ 𝑃 = (𝑚 ∈ 𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚)))) |
4 | 2, 3 | fnmpti 6480 |
. . . . . . 7
⊢ 𝑃 Fn 𝐼 |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑃 Fn 𝐼) |
6 | | nnuz 12363 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
7 | | 1zzd 12094 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 1 ∈ ℤ) |
8 | | fveq2 6674 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑘 → (𝐹‘𝑡) = (𝐹‘𝑘)) |
9 | 8 | fveq1d 6676 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑘 → ((𝐹‘𝑡)‘𝑛) = ((𝐹‘𝑘)‘𝑛)) |
10 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) = (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) |
11 | | fvex 6687 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘)‘𝑛) ∈ V |
12 | 9, 10, 11 | fvmpt 6775 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
13 | 12 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
14 | | rrncms.6 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
15 | 14 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
16 | | rrnval.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑋 = (ℝ ↑m
𝐼) |
17 | 15, 16 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (ℝ ↑m 𝐼)) |
18 | | elmapi 8459 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ∈ (ℝ ↑m 𝐼) → (𝐹‘𝑘):𝐼⟶ℝ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):𝐼⟶ℝ) |
20 | 19 | ffvelrnda 6861 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝐼) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
21 | 20 | an32s 652 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
22 | 13, 21 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) ∈ ℝ) |
23 | 22 | recnd 10747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) ∈ ℂ) |
24 | | rrncms.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈
(Cau‘(ℝn‘𝐼))) |
25 | | rrncms.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐼 ∈ Fin) |
26 | 16 | rrnmet 35610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
28 | | metxmet 23087 |
. . . . . . . . . . . . . . . 16
⊢
((ℝn‘𝐼) ∈ (Met‘𝑋) →
(ℝn‘𝐼) ∈ (∞Met‘𝑋)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℝn‘𝐼) ∈ (∞Met‘𝑋)) |
30 | | 1zzd 12094 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℤ) |
31 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
32 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐹‘𝑗)) |
33 | 6, 29, 30, 31, 32, 14 | iscauf 24032 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∈
(Cau‘(ℝn‘𝐼)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥)) |
34 | 24, 33 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) |
35 | 34 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) |
36 | 25 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐼 ∈ Fin) |
37 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝐼) |
38 | 14 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:ℕ⟶𝑋) |
39 | | eluznn 12400 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
40 | 39 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
41 | 38, 40 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ 𝑋) |
42 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) |
43 | 38, 42 | ffvelrnd 6862 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ∈ 𝑋) |
44 | | rrndstprj1.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑀 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
45 | 16, 44 | rrndstprj1 35611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗))) |
46 | 36, 37, 41, 43, 45 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗))) |
47 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
48 | | metsym 23103 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋) → ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗)) = ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
49 | 47, 41, 43, 48 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗)) = ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
50 | 46, 49 | breqtrd 5056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
51 | 50 | adantllr 719 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
52 | 44 | remet 23542 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑀 ∈
(Met‘ℝ) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑀 ∈
(Met‘ℝ)) |
54 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝜑 ∧ 𝑛 ∈ 𝐼)) |
55 | 54, 40, 21 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
56 | 14 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ 𝑋) |
57 | 56, 16 | eleqtrdi 2843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ ↑m 𝐼)) |
58 | | elmapi 8459 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑗) ∈ (ℝ ↑m 𝐼) → (𝐹‘𝑗):𝐼⟶ℝ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):𝐼⟶ℝ) |
60 | 59 | ffvelrnda 6861 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ 𝐼) → ((𝐹‘𝑗)‘𝑛) ∈ ℝ) |
61 | 60 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑛) ∈ ℝ) |
62 | 61 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑗)‘𝑛) ∈ ℝ) |
63 | | metcl 23085 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ (Met‘ℝ)
∧ ((𝐹‘𝑘)‘𝑛) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑛) ∈ ℝ) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ) |
64 | 53, 55, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ) |
65 | 64 | adantllr 719 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ) |
66 | | metcl 23085 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ (𝐹‘𝑗) ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋) → ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ) |
67 | 47, 43, 41, 66 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ) |
68 | 67 | adantllr 719 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ) |
69 | | rpre 12480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
70 | 69 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
71 | 70 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) |
72 | | lelttr 10809 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ ∧ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∧ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
73 | 65, 68, 71, 72 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∧ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
74 | 51, 73 | mpand 695 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
75 | 74 | ralimdva 3091 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
76 | 75 | reximdva 3184 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
77 | 76 | ralimdva 3091 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
78 | 44 | remetdval 23541 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑘)‘𝑛) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑛) ∈ ℝ) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛)))) |
79 | 55, 62, 78 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛)))) |
80 | 40, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
81 | | fveq2 6674 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑗 → (𝐹‘𝑡) = (𝐹‘𝑗)) |
82 | 81 | fveq1d 6676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑗 → ((𝐹‘𝑡)‘𝑛) = ((𝐹‘𝑗)‘𝑛)) |
83 | | fvex 6687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑗)‘𝑛) ∈ V |
84 | 82, 10, 83 | fvmpt 6775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗) = ((𝐹‘𝑗)‘𝑛)) |
85 | 84 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗) = ((𝐹‘𝑗)‘𝑛)) |
86 | 80, 85 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗)) = (((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛))) |
87 | 86 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) = (abs‘(((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛)))) |
88 | 79, 87 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) = (abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗)))) |
89 | 88 | breq1d 5040 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ (abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
90 | 89 | ralbidva 3108 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
91 | 90 | rexbidva 3206 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
92 | 91 | ralbidv 3109 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
93 | 77, 92 | sylibd 242 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
94 | 35, 93 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥) |
95 | | nnex 11722 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
96 | 95 | mptex 6996 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ V |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ V) |
98 | 6, 23, 94, 97 | caucvg 15128 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ dom ⇝ ) |
99 | | climdm 15001 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ dom ⇝ ↔ (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
100 | 98, 99 | sylib 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
101 | | fveq2 6674 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑡)‘𝑚) = ((𝐹‘𝑡)‘𝑛)) |
102 | 101 | mpteq2dv 5126 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚)) = (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))) |
103 | 102 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚))) = ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
104 | | fvex 6687 |
. . . . . . . . . . 11
⊢ ( ⇝
‘(𝑡 ∈ ℕ
↦ ((𝐹‘𝑡)‘𝑛))) ∈ V |
105 | 103, 3, 104 | fvmpt 6775 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝐼 → (𝑃‘𝑛) = ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
106 | 105 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑃‘𝑛) = ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
107 | 100, 106 | breqtrrd 5058 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ (𝑃‘𝑛)) |
108 | 6, 7, 107, 22 | climrecl 15030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑃‘𝑛) ∈ ℝ) |
109 | 108 | ralrimiva 3096 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ 𝐼 (𝑃‘𝑛) ∈ ℝ) |
110 | | ffnfv 6892 |
. . . . . 6
⊢ (𝑃:𝐼⟶ℝ ↔ (𝑃 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑃‘𝑛) ∈ ℝ)) |
111 | 5, 109, 110 | sylanbrc 586 |
. . . . 5
⊢ (𝜑 → 𝑃:𝐼⟶ℝ) |
112 | | reex 10706 |
. . . . . 6
⊢ ℝ
∈ V |
113 | | elmapg 8450 |
. . . . . 6
⊢ ((ℝ
∈ V ∧ 𝐼 ∈
Fin) → (𝑃 ∈
(ℝ ↑m 𝐼) ↔ 𝑃:𝐼⟶ℝ)) |
114 | 112, 25, 113 | sylancr 590 |
. . . . 5
⊢ (𝜑 → (𝑃 ∈ (ℝ ↑m 𝐼) ↔ 𝑃:𝐼⟶ℝ)) |
115 | 111, 114 | mpbird 260 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m 𝐼)) |
116 | 115, 16 | eleqtrrdi 2844 |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
117 | | 1nn 11727 |
. . . . . . 7
⊢ 1 ∈
ℕ |
118 | 25 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ∈ Fin) |
119 | 15 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
120 | 116 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ 𝑋) |
121 | 16 | rrnmval 35609 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ Fin ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = (√‘Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2))) |
122 | 118, 119,
120, 121 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = (√‘Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2))) |
123 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 = ∅) |
124 | 123 | sumeq1d 15151 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) →
Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2) = Σ𝑦 ∈ ∅ ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2)) |
125 | | sum0 15171 |
. . . . . . . . . . . . 13
⊢
Σ𝑦 ∈
∅ ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2) = 0 |
126 | 124, 125 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) →
Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2) = 0) |
127 | 126 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘Σ𝑦
∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2)) =
(√‘0)) |
128 | 122, 127 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = (√‘0)) |
129 | | sqrt0 14691 |
. . . . . . . . . 10
⊢
(√‘0) = 0 |
130 | 128, 129 | eqtrdi 2789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = 0) |
131 | | simplrl 777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℝ+) |
132 | 131 | rpgt0d 12517 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 0 <
𝑥) |
133 | 130, 132 | eqbrtrd 5052 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
134 | 133 | ralrimiva 3096 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) →
∀𝑘 ∈ ℕ
((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
135 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑗 = 1 →
(ℤ≥‘𝑗) =
(ℤ≥‘1)) |
136 | 135, 6 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑗 = 1 →
(ℤ≥‘𝑗) = ℕ) |
137 | 136 | raleqdv 3316 |
. . . . . . . 8
⊢ (𝑗 = 1 → (∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
138 | 137 | rspcev 3526 |
. . . . . . 7
⊢ ((1
∈ ℕ ∧ ∀𝑘 ∈ ℕ ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
139 | 117, 134,
138 | sylancr 590 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
140 | 139 | expr 460 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐼 = ∅ → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
141 | | 1zzd 12094 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → 1 ∈ ℤ) |
142 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝑥 ∈
ℝ+) |
143 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝐼 ≠ ∅) |
144 | 25 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin) |
145 | | hashnncl 13819 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) |
147 | 143, 146 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(♯‘𝐼) ∈
ℕ) |
148 | 147 | nnrpd 12512 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(♯‘𝐼) ∈
ℝ+) |
149 | 148 | rpsqrtcld 14861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(√‘(♯‘𝐼)) ∈
ℝ+) |
150 | 142, 149 | rpdivcld 12531 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → (𝑥 /
(√‘(♯‘𝐼))) ∈
ℝ+) |
151 | 150 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (𝑥 / (√‘(♯‘𝐼))) ∈
ℝ+) |
152 | 12 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
153 | 107 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ (𝑃‘𝑛)) |
154 | 6, 141, 151, 152, 153 | climi2 14958 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼)))) |
155 | | 1z 12093 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
156 | 6 | rexuz3 14798 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (∃𝑗
∈ ℕ ∀𝑘
∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
157 | 155, 156 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
158 | 21 | adantllr 719 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
159 | 108 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (𝑃‘𝑛) ∈ ℝ) |
160 | 159 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑛) ∈ ℝ) |
161 | 44 | remetdval 23541 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑘)‘𝑛) ∈ ℝ ∧ (𝑃‘𝑛) ∈ ℝ) → (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛)))) |
162 | 158, 160,
161 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛)))) |
163 | 162 | breq1d 5040 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
164 | 39, 163 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
165 | 164 | anassrs 471 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ ℝ+
∧ 𝐼 ≠ ∅))
∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
166 | 165 | ralbidva 3108 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
167 | 166 | rexbidva 3206 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
168 | 157, 167 | bitr3id 288 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
169 | 154, 168 | mpbird 260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
170 | 169 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
171 | 6 | rexuz3 14798 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → (∃𝑗
∈ ℕ ∀𝑘
∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
172 | 155, 171 | ax-mp 5 |
. . . . . . . . 9
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
173 | | rexfiuz 14797 |
. . . . . . . . . 10
⊢ (𝐼 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
174 | 144, 173 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
175 | 172, 174 | syl5bb 286 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
176 | 170, 175 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
177 | 25 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ∈ Fin) |
178 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ≠ ∅) |
179 | | eldifsn 4675 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (Fin ∖ {∅})
↔ (𝐼 ∈ Fin ∧
𝐼 ≠
∅)) |
180 | 177, 178,
179 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ∈ (Fin ∖
{∅})) |
181 | 14 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝐹:ℕ⟶𝑋) |
182 | 181 | ffvelrnda 6861 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
183 | 116 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ 𝑋) |
184 | 150 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → (𝑥 /
(√‘(♯‘𝐼))) ∈
ℝ+) |
185 | 16, 44 | rrndstprj2 35612 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ((𝑥 / (√‘(♯‘𝐼))) ∈ ℝ+
∧ ∀𝑛 ∈
𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼)))) |
186 | 185 | expr 460 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ (𝑥 / (√‘(♯‘𝐼))) ∈ ℝ+)
→ (∀𝑛 ∈
𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))))) |
187 | 180, 182,
183, 184, 186 | syl31anc 1374 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))))) |
188 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℝ+) |
189 | 188 | rpcnd 12516 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℂ) |
190 | 149 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘(♯‘𝐼)) ∈
ℝ+) |
191 | 190 | rpcnd 12516 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘(♯‘𝐼)) ∈ ℂ) |
192 | 190 | rpne0d 12519 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘(♯‘𝐼)) ≠ 0) |
193 | 189, 191,
192 | divcan1d 11495 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → ((𝑥 /
(√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))) = 𝑥) |
194 | 193 | breq2d 5042 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))) ↔ ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
195 | 187, 194 | sylibd 242 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
196 | 39, 195 | sylan2 596 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗))) → (∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
197 | 196 | anassrs 471 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
198 | 197 | ralimdva 3091 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
199 | 198 | reximdva 3184 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
200 | 176, 199 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
201 | 200 | expr 460 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐼 ≠ ∅ →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
202 | 140, 201 | pm2.61dne 3020 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
203 | 202 | ralrimiva 3096 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
204 | | rrncms.3 |
. . . 4
⊢ 𝐽 =
(MetOpen‘(ℝn‘𝐼)) |
205 | 204, 29, 6, 30, 31, 14 | lmmbrf 24014 |
. . 3
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥))) |
206 | 116, 203,
205 | mpbir2and 713 |
. 2
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) |
207 | | releldm 5787 |
. 2
⊢ ((Rel
(⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
208 | 1, 206, 207 | sylancr 590 |
1
⊢ (𝜑 → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |