Step | Hyp | Ref
| Expression |
1 | | lmrel 22381 |
. 2
⊢ Rel
(⇝𝑡‘𝐽) |
2 | | fvex 6787 |
. . . . . . . 8
⊢ ( ⇝
‘(𝑡 ∈ ℕ
↦ ((𝐹‘𝑡)‘𝑚))) ∈ V |
3 | | rrncms.7 |
. . . . . . . 8
⊢ 𝑃 = (𝑚 ∈ 𝐼 ↦ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚)))) |
4 | 2, 3 | fnmpti 6576 |
. . . . . . 7
⊢ 𝑃 Fn 𝐼 |
5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑃 Fn 𝐼) |
6 | | nnuz 12621 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
7 | | 1zzd 12351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → 1 ∈ ℤ) |
8 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑘 → (𝐹‘𝑡) = (𝐹‘𝑘)) |
9 | 8 | fveq1d 6776 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑘 → ((𝐹‘𝑡)‘𝑛) = ((𝐹‘𝑘)‘𝑛)) |
10 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) = (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) |
11 | | fvex 6787 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘)‘𝑛) ∈ V |
12 | 9, 10, 11 | fvmpt 6875 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
13 | 12 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
14 | | rrncms.6 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:ℕ⟶𝑋) |
15 | 14 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
16 | | rrnval.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑋 = (ℝ ↑m
𝐼) |
17 | 15, 16 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ (ℝ ↑m 𝐼)) |
18 | | elmapi 8637 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ∈ (ℝ ↑m 𝐼) → (𝐹‘𝑘):𝐼⟶ℝ) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘):𝐼⟶ℝ) |
20 | 19 | ffvelrnda 6961 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ 𝐼) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
21 | 20 | an32s 649 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
22 | 13, 21 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) ∈ ℝ) |
23 | 22 | recnd 11003 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) ∈ ℂ) |
24 | | rrncms.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈
(Cau‘(ℝn‘𝐼))) |
25 | | rrncms.4 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐼 ∈ Fin) |
26 | 16 | rrnmet 35987 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
28 | | metxmet 23487 |
. . . . . . . . . . . . . . . 16
⊢
((ℝn‘𝐼) ∈ (Met‘𝑋) →
(ℝn‘𝐼) ∈ (∞Met‘𝑋)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(ℝn‘𝐼) ∈ (∞Met‘𝑋)) |
30 | | 1zzd 12351 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈
ℤ) |
31 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
32 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐹‘𝑗)) |
33 | 6, 29, 30, 31, 32, 14 | iscauf 24444 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 ∈
(Cau‘(ℝn‘𝐼)) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥)) |
34 | 24, 33 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) |
35 | 34 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) |
36 | 25 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐼 ∈ Fin) |
37 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝐼) |
38 | 14 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:ℕ⟶𝑋) |
39 | | eluznn 12658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
40 | 39 | adantll 711 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ ℕ) |
41 | 38, 40 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈ 𝑋) |
42 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ ℕ) |
43 | 38, 42 | ffvelrnd 6962 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑗) ∈ 𝑋) |
44 | | rrndstprj1.1 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑀 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
45 | 16, 44 | rrndstprj1 35988 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ Fin ∧ 𝑛 ∈ 𝐼) ∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗))) |
46 | 36, 37, 41, 43, 45 | syl22anc 836 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗))) |
47 | 27 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) →
(ℝn‘𝐼) ∈ (Met‘𝑋)) |
48 | | metsym 23503 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ (𝐹‘𝑗) ∈ 𝑋) → ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗)) = ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
49 | 47, 41, 43, 48 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)(ℝn‘𝐼)(𝐹‘𝑗)) = ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
50 | 46, 49 | breqtrd 5100 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
51 | 50 | adantllr 716 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘))) |
52 | 44 | remet 23953 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑀 ∈
(Met‘ℝ) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑀 ∈
(Met‘ℝ)) |
54 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝜑 ∧ 𝑛 ∈ 𝐼)) |
55 | 54, 40, 21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
56 | 14 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ 𝑋) |
57 | 56, 16 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ (ℝ ↑m 𝐼)) |
58 | | elmapi 8637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹‘𝑗) ∈ (ℝ ↑m 𝐼) → (𝐹‘𝑗):𝐼⟶ℝ) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗):𝐼⟶ℝ) |
60 | 59 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ 𝐼) → ((𝐹‘𝑗)‘𝑛) ∈ ℝ) |
61 | 60 | an32s 649 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑗)‘𝑛) ∈ ℝ) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑗)‘𝑛) ∈ ℝ) |
63 | | metcl 23485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ (Met‘ℝ)
∧ ((𝐹‘𝑘)‘𝑛) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑛) ∈ ℝ) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ) |
64 | 53, 55, 62, 63 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ) |
65 | 64 | adantllr 716 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ) |
66 | | metcl 23485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℝn‘𝐼) ∈ (Met‘𝑋) ∧ (𝐹‘𝑗) ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋) → ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ) |
67 | 47, 43, 41, 66 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ) |
68 | 67 | adantllr 716 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ) |
69 | | rpre 12738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
70 | 69 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
71 | 70 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → 𝑥 ∈ ℝ) |
72 | | lelttr 11065 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ∈ ℝ ∧ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∧ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
73 | 65, 68, 71, 72 | syl3anc 1370 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) ≤ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) ∧ ((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
74 | 51, 73 | mpand 692 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
75 | 74 | ralimdva 3108 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
76 | 75 | reximdva 3203 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
77 | 76 | ralimdva 3108 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥)) |
78 | 44 | remetdval 23952 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐹‘𝑘)‘𝑛) ∈ ℝ ∧ ((𝐹‘𝑗)‘𝑛) ∈ ℝ) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛)))) |
79 | 55, 62, 78 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛)))) |
80 | 40, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
81 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑗 → (𝐹‘𝑡) = (𝐹‘𝑗)) |
82 | 81 | fveq1d 6776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = 𝑗 → ((𝐹‘𝑡)‘𝑛) = ((𝐹‘𝑗)‘𝑛)) |
83 | | fvex 6787 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑗)‘𝑛) ∈ V |
84 | 82, 10, 83 | fvmpt 6875 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗) = ((𝐹‘𝑗)‘𝑛)) |
85 | 84 | ad2antlr 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗) = ((𝐹‘𝑗)‘𝑛)) |
86 | 80, 85 | oveq12d 7293 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗)) = (((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛))) |
87 | 86 | fveq2d 6778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) = (abs‘(((𝐹‘𝑘)‘𝑛) − ((𝐹‘𝑗)‘𝑛)))) |
88 | 79, 87 | eqtr4d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) = (abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗)))) |
89 | 88 | breq1d 5084 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ (abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
90 | 89 | ralbidva 3111 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
91 | 90 | rexbidva 3225 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
92 | 91 | ralbidv 3112 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀((𝐹‘𝑗)‘𝑛)) < 𝑥 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
93 | 77, 92 | sylibd 238 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑗)(ℝn‘𝐼)(𝐹‘𝑘)) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥)) |
94 | 35, 93 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) − ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑗))) < 𝑥) |
95 | | nnex 11979 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
96 | 95 | mptex 7099 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ V |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ V) |
98 | 6, 23, 94, 97 | caucvg 15390 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ dom ⇝ ) |
99 | | climdm 15263 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ∈ dom ⇝ ↔ (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
100 | 98, 99 | sylib 217 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
101 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑡)‘𝑚) = ((𝐹‘𝑡)‘𝑛)) |
102 | 101 | mpteq2dv 5176 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚)) = (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))) |
103 | 102 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑚))) = ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
104 | | fvex 6787 |
. . . . . . . . . . 11
⊢ ( ⇝
‘(𝑡 ∈ ℕ
↦ ((𝐹‘𝑡)‘𝑛))) ∈ V |
105 | 103, 3, 104 | fvmpt 6875 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝐼 → (𝑃‘𝑛) = ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
106 | 105 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑃‘𝑛) = ( ⇝ ‘(𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)))) |
107 | 100, 106 | breqtrrd 5102 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ (𝑃‘𝑛)) |
108 | 6, 7, 107, 22 | climrecl 15292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐼) → (𝑃‘𝑛) ∈ ℝ) |
109 | 108 | ralrimiva 3103 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ 𝐼 (𝑃‘𝑛) ∈ ℝ) |
110 | | ffnfv 6992 |
. . . . . 6
⊢ (𝑃:𝐼⟶ℝ ↔ (𝑃 Fn 𝐼 ∧ ∀𝑛 ∈ 𝐼 (𝑃‘𝑛) ∈ ℝ)) |
111 | 5, 109, 110 | sylanbrc 583 |
. . . . 5
⊢ (𝜑 → 𝑃:𝐼⟶ℝ) |
112 | | reex 10962 |
. . . . . 6
⊢ ℝ
∈ V |
113 | | elmapg 8628 |
. . . . . 6
⊢ ((ℝ
∈ V ∧ 𝐼 ∈
Fin) → (𝑃 ∈
(ℝ ↑m 𝐼) ↔ 𝑃:𝐼⟶ℝ)) |
114 | 112, 25, 113 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (𝑃 ∈ (ℝ ↑m 𝐼) ↔ 𝑃:𝐼⟶ℝ)) |
115 | 111, 114 | mpbird 256 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ (ℝ ↑m 𝐼)) |
116 | 115, 16 | eleqtrrdi 2850 |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝑋) |
117 | | 1nn 11984 |
. . . . . . 7
⊢ 1 ∈
ℕ |
118 | 25 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ∈ Fin) |
119 | 15 | adantlr 712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
120 | 116 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ 𝑋) |
121 | 16 | rrnmval 35986 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ Fin ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = (√‘Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2))) |
122 | 118, 119,
120, 121 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = (√‘Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2))) |
123 | | simplrr 775 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 = ∅) |
124 | 123 | sumeq1d 15413 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) →
Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2) = Σ𝑦 ∈ ∅ ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2)) |
125 | | sum0 15433 |
. . . . . . . . . . . . 13
⊢
Σ𝑦 ∈
∅ ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2) = 0 |
126 | 124, 125 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) →
Σ𝑦 ∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2) = 0) |
127 | 126 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘Σ𝑦
∈ 𝐼 ((((𝐹‘𝑘)‘𝑦) − (𝑃‘𝑦))↑2)) =
(√‘0)) |
128 | 122, 127 | eqtrd 2778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = (√‘0)) |
129 | | sqrt0 14953 |
. . . . . . . . . 10
⊢
(√‘0) = 0 |
130 | 128, 129 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) = 0) |
131 | | simplrl 774 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℝ+) |
132 | 131 | rpgt0d 12775 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → 0 <
𝑥) |
133 | 130, 132 | eqbrtrd 5096 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
134 | 133 | ralrimiva 3103 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) →
∀𝑘 ∈ ℕ
((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
135 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑗 = 1 →
(ℤ≥‘𝑗) =
(ℤ≥‘1)) |
136 | 135, 6 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑗 = 1 →
(ℤ≥‘𝑗) = ℕ) |
137 | 136 | raleqdv 3348 |
. . . . . . . 8
⊢ (𝑗 = 1 → (∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥 ↔ ∀𝑘 ∈ ℕ ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
138 | 137 | rspcev 3561 |
. . . . . . 7
⊢ ((1
∈ ℕ ∧ ∀𝑘 ∈ ℕ ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
139 | 117, 134,
138 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 = ∅)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
140 | 139 | expr 457 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐼 = ∅ → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
141 | | 1zzd 12351 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → 1 ∈ ℤ) |
142 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝑥 ∈
ℝ+) |
143 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝐼 ≠ ∅) |
144 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝐼 ∈ Fin) |
145 | | hashnncl 14081 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ Fin →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
((♯‘𝐼) ∈
ℕ ↔ 𝐼 ≠
∅)) |
147 | 143, 146 | mpbird 256 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(♯‘𝐼) ∈
ℕ) |
148 | 147 | nnrpd 12770 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(♯‘𝐼) ∈
ℝ+) |
149 | 148 | rpsqrtcld 15123 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(√‘(♯‘𝐼)) ∈
ℝ+) |
150 | 142, 149 | rpdivcld 12789 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → (𝑥 /
(√‘(♯‘𝐼))) ∈
ℝ+) |
151 | 150 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (𝑥 / (√‘(♯‘𝐼))) ∈
ℝ+) |
152 | 12 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛))‘𝑘) = ((𝐹‘𝑘)‘𝑛)) |
153 | 107 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (𝑡 ∈ ℕ ↦ ((𝐹‘𝑡)‘𝑛)) ⇝ (𝑃‘𝑛)) |
154 | 6, 141, 151, 152, 153 | climi2 15220 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼)))) |
155 | | 1z 12350 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
156 | 6 | rexuz3 15060 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (∃𝑗
∈ ℕ ∀𝑘
∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
157 | 155, 156 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
158 | 21 | adantllr 716 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)‘𝑛) ∈ ℝ) |
159 | 108 | adantlr 712 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (𝑃‘𝑛) ∈ ℝ) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑛) ∈ ℝ) |
161 | 44 | remetdval 23952 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐹‘𝑘)‘𝑛) ∈ ℝ ∧ (𝑃‘𝑛) ∈ ℝ) → (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛)))) |
162 | 158, 160,
161 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) = (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛)))) |
163 | 162 | breq1d 5084 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑘 ∈ ℕ) → ((((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
164 | 39, 163 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → ((((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
165 | 164 | anassrs 468 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ ℝ+
∧ 𝐼 ≠ ∅))
∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ (abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
166 | 165 | ralbidva 3111 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
167 | 166 | rexbidva 3225 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
168 | 157, 167 | bitr3id 285 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → (∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(((𝐹‘𝑘)‘𝑛) − (𝑃‘𝑛))) < (𝑥 / (√‘(♯‘𝐼))))) |
169 | 154, 168 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑛 ∈ 𝐼) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
170 | 169 | ralrimiva 3103 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
171 | 6 | rexuz3 15060 |
. . . . . . . . . 10
⊢ (1 ∈
ℤ → (∃𝑗
∈ ℕ ∀𝑘
∈ (ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
172 | 155, 171 | ax-mp 5 |
. . . . . . . . 9
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
173 | | rexfiuz 15059 |
. . . . . . . . . 10
⊢ (𝐼 ∈ Fin → (∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
174 | 144, 173 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
175 | 172, 174 | syl5bb 283 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) ↔ ∀𝑛 ∈ 𝐼 ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) |
176 | 170, 175 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼)))) |
177 | 25 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ∈ Fin) |
178 | | simplrr 775 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ≠ ∅) |
179 | | eldifsn 4720 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (Fin ∖ {∅})
↔ (𝐼 ∈ Fin ∧
𝐼 ≠
∅)) |
180 | 177, 178,
179 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝐼 ∈ (Fin ∖
{∅})) |
181 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) → 𝐹:ℕ⟶𝑋) |
182 | 181 | ffvelrnda 6961 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ 𝑋) |
183 | 116 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝑃 ∈ 𝑋) |
184 | 150 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → (𝑥 /
(√‘(♯‘𝐼))) ∈
ℝ+) |
185 | 16, 44 | rrndstprj2 35989 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ ((𝑥 / (√‘(♯‘𝐼))) ∈ ℝ+
∧ ∀𝑛 ∈
𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼)))) |
186 | 185 | expr 457 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ (Fin ∖ {∅})
∧ (𝐹‘𝑘) ∈ 𝑋 ∧ 𝑃 ∈ 𝑋) ∧ (𝑥 / (√‘(♯‘𝐼))) ∈ ℝ+)
→ (∀𝑛 ∈
𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))))) |
187 | 180, 182,
183, 184, 186 | syl31anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))))) |
188 | | simplrl 774 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℝ+) |
189 | 188 | rpcnd 12774 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → 𝑥 ∈
ℂ) |
190 | 149 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘(♯‘𝐼)) ∈
ℝ+) |
191 | 190 | rpcnd 12774 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘(♯‘𝐼)) ∈ ℂ) |
192 | 190 | rpne0d 12777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(√‘(♯‘𝐼)) ≠ 0) |
193 | 189, 191,
192 | divcan1d 11752 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → ((𝑥 /
(√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))) = 𝑥) |
194 | 193 | breq2d 5086 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) → (((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < ((𝑥 / (√‘(♯‘𝐼))) ·
(√‘(♯‘𝐼))) ↔ ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
195 | 187, 194 | sylibd 238 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑘 ∈ ℕ) →
(∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
196 | 39, 195 | sylan2 593 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ (𝑗 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑗))) → (∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
197 | 196 | anassrs 468 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈
(ℤ≥‘𝑗)) → (∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
198 | 197 | ralimdva 3108 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) ∧ 𝑗 ∈ ℕ) →
(∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
199 | 198 | reximdva 3203 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
(∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)∀𝑛 ∈ 𝐼 (((𝐹‘𝑘)‘𝑛)𝑀(𝑃‘𝑛)) < (𝑥 / (√‘(♯‘𝐼))) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
200 | 176, 199 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝐼 ≠ ∅)) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
201 | 200 | expr 457 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐼 ≠ ∅ →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥)) |
202 | 140, 201 | pm2.61dne 3031 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑗 ∈ ℕ
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
203 | 202 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥) |
204 | | rrncms.3 |
. . . 4
⊢ 𝐽 =
(MetOpen‘(ℝn‘𝐼)) |
205 | 204, 29, 6, 30, 31, 14 | lmmbrf 24426 |
. . 3
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘)(ℝn‘𝐼)𝑃) < 𝑥))) |
206 | 116, 203,
205 | mpbir2and 710 |
. 2
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) |
207 | | releldm 5853 |
. 2
⊢ ((Rel
(⇝𝑡‘𝐽) ∧ 𝐹(⇝𝑡‘𝐽)𝑃) → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
208 | 1, 206, 207 | sylancr 587 |
1
⊢ (𝜑 → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |