Step | Hyp | Ref
| Expression |
1 | | ulmdv.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
2 | 1 | adantr 466 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝑋⟶ℂ) |
3 | | ulmdvlem1.y |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋) |
4 | 2, 3 | ffvelrnd 6501 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝑌) ∈ ℂ) |
5 | | ulmdvlem1.c |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋) |
6 | 2, 5 | ffvelrnd 6501 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐶) ∈ ℂ) |
7 | 4, 6 | subcld 10592 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − (𝐺‘𝐶)) ∈ ℂ) |
8 | | ulmdvlem1.n |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍) |
9 | | fveq2 6330 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁)) |
10 | 9 | oveq2d 6807 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑁 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑁))) |
11 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) = (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) |
12 | | ovex 6821 |
. . . . . . . . . . . 12
⊢ (𝑆 D (𝐹‘𝑁)) ∈ V |
13 | 10, 11, 12 | fvmpt 6422 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁))) |
14 | 8, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁))) |
15 | | ovex 6821 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 D (𝐹‘𝑘)) ∈ V |
16 | 15 | rgenw 3073 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V |
17 | 11 | fnmpt 6158 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍) |
19 | | ulmdv.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) |
20 | | ulmf2 24351 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
21 | 18, 19, 20 | syl2anc 573 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
22 | 21 | adantr 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
23 | 22, 8 | ffvelrnd 6501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) ∈ (ℂ ↑𝑚
𝑋)) |
24 | 14, 23 | eqeltrrd 2851 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)) ∈ (ℂ
↑𝑚 𝑋)) |
25 | | elmapi 8029 |
. . . . . . . . 9
⊢ ((𝑆 D (𝐹‘𝑁)) ∈ (ℂ
↑𝑚 𝑋) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ) |
27 | | fdm 6189 |
. . . . . . . 8
⊢ ((𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ → dom (𝑆 D (𝐹‘𝑁)) = 𝑋) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → dom (𝑆 D (𝐹‘𝑁)) = 𝑋) |
29 | | dvbsss 23879 |
. . . . . . 7
⊢ dom
(𝑆 D (𝐹‘𝑁)) ⊆ 𝑆 |
30 | 28, 29 | syl6eqssr 3805 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ 𝑆) |
31 | | ulmdv.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
32 | | recnprss 23881 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
34 | 33 | adantr 466 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑆 ⊆ ℂ) |
35 | 30, 34 | sstrd 3762 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ ℂ) |
36 | 35, 3 | sseldd 3753 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ ℂ) |
37 | 35, 5 | sseldd 3753 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ ℂ) |
38 | 36, 37 | subcld 10592 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ∈ ℂ) |
39 | | ulmdvlem1.3 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶) |
40 | 36, 37, 39 | subne0d 10601 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ≠ 0) |
41 | 7, 38, 40 | divcld 11001 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ) |
42 | | ulmcl 24348 |
. . . . 5
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻 → 𝐻:𝑋⟶ℂ) |
43 | 19, 42 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐻:𝑋⟶ℂ) |
44 | 43 | adantr 466 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝐻:𝑋⟶ℂ) |
45 | 44, 5 | ffvelrnd 6501 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝐻‘𝐶) ∈ ℂ) |
46 | 26, 5 | ffvelrnd 6501 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑆 D (𝐹‘𝑁))‘𝐶) ∈ ℂ) |
47 | | ulmdvlem1.r |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈
ℝ+) |
48 | 47 | rpred 12068 |
. 2
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ) |
49 | 41, 46 | subcld 10592 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ) |
50 | 49 | abscld 14376 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ) |
51 | | ulmdv.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑋)) |
52 | 51 | adantr 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑋)) |
53 | 52, 8 | ffvelrnd 6501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁) ∈ (ℂ ↑𝑚
𝑋)) |
54 | | elmapi 8029 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑁) ∈ (ℂ ↑𝑚
𝑋) → (𝐹‘𝑁):𝑋⟶ℂ) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁):𝑋⟶ℂ) |
56 | 55, 3 | ffvelrnd 6501 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ) |
57 | 55, 5 | ffvelrnd 6501 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ) |
58 | 56, 57 | subcld 10592 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ) |
59 | 58, 38, 40 | divcld 11001 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ) |
60 | 41, 59 | subcld 10592 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))) ∈ ℂ) |
61 | 60 | abscld 14376 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ∈ ℝ) |
62 | 59, 46 | subcld 10592 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ) |
63 | 62 | abscld 14376 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ) |
64 | 61, 63 | readdcld 10269 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) ∈ ℝ) |
65 | 48 | rehalfcld 11479 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℝ) |
66 | 41, 46, 59 | abs3difd 14400 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ≤ ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))))) |
67 | 65 | rehalfcld 11479 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑅 / 2) / 2) ∈ ℝ) |
68 | 4, 56, 6, 57 | sub4d 10641 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)))) |
69 | 68 | oveq1d 6806 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) |
70 | 7, 58, 38, 40 | divsubdird 11040 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) |
71 | 69, 70 | eqtrd 2805 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) |
72 | 71 | fveq2d 6334 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))) |
73 | 4, 56 | subcld 10592 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ) |
74 | 6, 57 | subcld 10592 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ) |
75 | 73, 74 | subcld 10592 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ) |
76 | 75, 38, 40 | absdivd 14395 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶)))) |
77 | 72, 76 | eqtr3d 2807 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶)))) |
78 | | eqid 2771 |
. . . . . . . 8
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
79 | | ulmdv.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
80 | 8, 79 | syl6eleq 2860 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (ℤ≥‘𝑀)) |
81 | | eluzelz 11896 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ ℤ) |
83 | | ulmdv.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
84 | 83 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ) |
85 | | fveq2 6330 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑌 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑌)) |
86 | 85 | mpteq2dv 4879 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑌 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))) |
87 | | fveq2 6330 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑌 → (𝐺‘𝑧) = (𝐺‘𝑌)) |
88 | 86, 87 | breq12d 4799 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑌 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌))) |
89 | | ulmdv.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) |
90 | 89 | ralrimiva 3115 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) |
91 | 90 | adantr 466 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) |
92 | 88, 91, 3 | rspcdva 3466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌)) |
93 | 79 | fvexi 6341 |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈ V |
94 | 93 | mptex 6628 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V |
95 | 94 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V) |
96 | | fveq2 6330 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
97 | 96 | fveq1d 6332 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝑌) = ((𝐹‘𝑛)‘𝑌)) |
98 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) |
99 | | fvex 6340 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛)‘𝑌) ∈ V |
100 | 97, 98, 99 | fvmpt 6422 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌)) |
101 | 100 | adantl 467 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌)) |
102 | 52 | ffvelrnda 6500 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑𝑚
𝑋)) |
103 | | elmapi 8029 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛) ∈ (ℂ ↑𝑚
𝑋) → (𝐹‘𝑛):𝑋⟶ℂ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑋⟶ℂ) |
105 | 3 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝑌 ∈ 𝑋) |
106 | 104, 105 | ffvelrnd 6501 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑌) ∈ ℂ) |
107 | 101, 106 | eqeltrd 2850 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) ∈ ℂ) |
108 | 97 | oveq1d 6806 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
109 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
110 | | ovex 6821 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ V |
111 | 108, 109,
110 | fvmpt 6422 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
112 | 111 | adantl 467 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
113 | 101 | oveq1d 6806 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
114 | 112, 113 | eqtr4d 2808 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌))) |
115 | 79, 84, 92, 56, 95, 107, 114 | climsubc1 14569 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ⇝ ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
116 | 93 | mptex 6628 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V |
117 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V) |
118 | | fveq2 6330 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐶 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝐶)) |
119 | 118 | mpteq2dv 4879 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐶 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))) |
120 | | fveq2 6330 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐶 → (𝐺‘𝑧) = (𝐺‘𝐶)) |
121 | 119, 120 | breq12d 4799 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐶 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶))) |
122 | 121, 91, 5 | rspcdva 3466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶)) |
123 | 93 | mptex 6628 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V |
124 | 123 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V) |
125 | 96 | fveq1d 6332 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝐶) = ((𝐹‘𝑛)‘𝐶)) |
126 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) |
127 | | fvex 6340 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛)‘𝐶) ∈ V |
128 | 125, 126,
127 | fvmpt 6422 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶)) |
129 | 128 | adantl 467 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶)) |
130 | 5 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝐶 ∈ 𝑋) |
131 | 104, 130 | ffvelrnd 6501 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝐶) ∈ ℂ) |
132 | 129, 131 | eqeltrd 2850 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) ∈ ℂ) |
133 | 125 | oveq1d 6806 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
134 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
135 | | ovex 6821 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ V |
136 | 133, 134,
135 | fvmpt 6422 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
137 | 136 | adantl 467 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
138 | 129 | oveq1d 6806 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
139 | 137, 138 | eqtr4d 2808 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶))) |
140 | 79, 84, 122, 57, 124, 132, 139 | climsubc1 14569 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ⇝ ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
141 | 56 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ) |
142 | 106, 141 | subcld 10592 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ) |
143 | 112, 142 | eqeltrd 2850 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) ∈ ℂ) |
144 | 57 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ) |
145 | 131, 144 | subcld 10592 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ) |
146 | 137, 145 | eqeltrd 2850 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) ∈ ℂ) |
147 | 108, 133 | oveq12d 6809 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
148 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
149 | | ovex 6821 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V |
150 | 147, 148,
149 | fvmpt 6422 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
151 | 150 | adantl 467 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
152 | 112, 137 | oveq12d 6809 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
153 | 151, 152 | eqtr4d 2808 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛))) |
154 | 79, 84, 115, 117, 140, 143, 146, 153 | climsub 14565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ⇝ (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
155 | 93 | mptex 6628 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V |
156 | 155 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V) |
157 | 142, 145 | subcld 10592 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ) |
158 | 151, 157 | eqeltrd 2850 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) ∈ ℂ) |
159 | 147 | fveq2d 6334 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
160 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) = (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
161 | | fvex 6340 |
. . . . . . . . . . . 12
⊢
(abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V |
162 | 159, 160,
161 | fvmpt 6422 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
163 | 162 | adantl 467 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
164 | 151 | fveq2d 6334 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
165 | 163, 164 | eqtr4d 2808 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛))) |
166 | 79, 154, 156, 84, 158, 165 | climabs 14535 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ⇝ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
167 | 38 | abscld 14376 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ) |
168 | 67, 167 | remulcld 10270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ) |
169 | 168 | recnd 10268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ) |
170 | 79 | eqimss2i 3809 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ 𝑍 |
171 | 170, 93 | climconst2 14480 |
. . . . . . . . 9
⊢
(((((𝑅 / 2) / 2)
· (abs‘(𝑌
− 𝐶))) ∈ ℂ
∧ 𝑀 ∈ ℤ)
→ (𝑍 × {(((𝑅 / 2) / 2) ·
(abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) ·
(abs‘(𝑌 − 𝐶)))) |
172 | 169, 84, 171 | syl2anc 573 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
173 | 79 | uztrn2 11904 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
174 | 8, 173 | sylan 569 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
175 | 174, 162 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
176 | 157 | abscld 14376 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ) |
177 | 174, 176 | syldan 579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ) |
178 | 175, 177 | eqeltrd 2850 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ∈ ℝ) |
179 | | ovex 6821 |
. . . . . . . . . . 11
⊢ (((𝑅 / 2) / 2) ·
(abs‘(𝑌 − 𝐶))) ∈ V |
180 | 179 | fvconst2 6611 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
181 | 174, 180 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
182 | 168 | adantr 466 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ) |
183 | 181, 182 | eqeltrd 2850 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) ∈ ℝ) |
184 | 174, 104 | syldan 579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑛):𝑋⟶ℂ) |
185 | | ffn 6183 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛):𝑋⟶ℂ → (𝐹‘𝑛) Fn 𝑋) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑛) Fn 𝑋) |
187 | 55 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑁):𝑋⟶ℂ) |
188 | | ffn 6183 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑁):𝑋⟶ℂ → (𝐹‘𝑁) Fn 𝑋) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑁) Fn 𝑋) |
190 | | ulmscl 24346 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻 → 𝑋 ∈ V) |
191 | 19, 190 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ V) |
192 | 191 | ad2antrr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑋 ∈ V) |
193 | 3 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑌 ∈ 𝑋) |
194 | | fnfvof 7056 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝑌 ∈ 𝑋)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
195 | 186, 189,
192, 193, 194 | syl22anc 1477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
196 | 5 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ 𝑋) |
197 | | fnfvof 7056 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝐶 ∈ 𝑋)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
198 | 186, 189,
192, 196, 197 | syl22anc 1477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
199 | 195, 198 | oveq12d 6809 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
200 | 199 | fveq2d 6334 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
201 | 30, 3 | sseldd 3753 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑆) |
202 | 30, 5 | sseldd 3753 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑆) |
203 | 201, 202 | ovresd 6946 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (𝑌(abs ∘ − )𝐶)) |
204 | | eqid 2771 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
205 | 204 | cnmetdval 22787 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶))) |
206 | 36, 37, 205 | syl2anc 573 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶))) |
207 | 203, 206 | eqtrd 2805 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (abs‘(𝑌 − 𝐶))) |
208 | | ulmdvlem1.a |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈) |
209 | 207, 208 | eqbrtrd 4808 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈) |
210 | | cnxmet 22789 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
211 | | xmetres2 22379 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑆
× 𝑆)) ∈
(∞Met‘𝑆)) |
212 | 210, 34, 211 | sylancr 575 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → ((abs ∘ − ) ↾
(𝑆 × 𝑆)) ∈
(∞Met‘𝑆)) |
213 | | ulmdvlem1.u |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈
ℝ+) |
214 | 213 | rpxrd 12069 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈
ℝ*) |
215 | | elbl3 22410 |
. . . . . . . . . . . . . . 15
⊢ (((((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑈 ∈ ℝ*) ∧ (𝐶 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)) |
216 | 212, 214,
202, 201, 215 | syl22anc 1477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)) |
217 | 209, 216 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
218 | 217 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
219 | | blcntr 22431 |
. . . . . . . . . . . . . 14
⊢ ((((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ 𝑆 ∧ 𝑈 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
220 | 212, 202,
213, 219 | syl3anc 1476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
221 | 220 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
222 | 218, 221 | jca 501 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈))) |
223 | 31 | ad2antrr 705 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑆 ∈ {ℝ, ℂ}) |
224 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) |
225 | 30 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑋 ⊆ 𝑆) |
226 | 184 | ffvelrnda 6500 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ) |
227 | 187 | ffvelrnda 6500 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ ℂ) |
228 | 226, 227 | subcld 10592 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)) ∈ ℂ) |
229 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))) |
230 | 228, 229 | fmptd 6525 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))):𝑋⟶ℂ) |
231 | | fvexd 6342 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ V) |
232 | | fvexd 6342 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ V) |
233 | 184 | feqmptd 6389 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑛) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) |
234 | 187 | feqmptd 6389 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑁) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) |
235 | 192, 231,
232, 233, 234 | offval2 7059 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) |
236 | 235 | feq1d 6168 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)):𝑋⟶ℂ ↔ (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))):𝑋⟶ℂ)) |
237 | 230, 236 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)):𝑋⟶ℂ) |
238 | 202 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ 𝑆) |
239 | 214 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑈 ∈
ℝ*) |
240 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝐶(ball‘((abs ∘
− ) ↾ (𝑆
× 𝑆)))𝑈) = (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) |
241 | | ulmdvlem1.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ⊆ 𝑋) |
242 | 241 | adantr 466 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ⊆ 𝑋) |
243 | 235 | oveq2d 6807 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))))) |
244 | | fvexd 6342 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ V) |
245 | 233 | oveq2d 6807 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦)))) |
246 | 96 | oveq2d 6807 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑛 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑛))) |
247 | | ovex 6821 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆 D (𝐹‘𝑛)) ∈ V |
248 | 246, 11, 247 | fvmpt 6422 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛))) |
249 | 174, 248 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛))) |
250 | 21 | ad2antrr 705 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
251 | 250, 174 | ffvelrnd 6501 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) ∈ (ℂ ↑𝑚
𝑋)) |
252 | 249, 251 | eqeltrrd 2851 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑𝑚
𝑋)) |
253 | | elmapi 8029 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑𝑚
𝑋) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ) |
254 | 252, 253 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ) |
255 | 254 | feqmptd 6389 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦))) |
256 | 245, 255 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦))) |
257 | | fvexd 6342 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ V) |
258 | 234 | oveq2d 6807 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦)))) |
259 | 26 | adantr 466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ) |
260 | 259 | feqmptd 6389 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
261 | 258, 260 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
262 | 223, 226,
244, 256, 227, 257, 261 | dvmptsub 23943 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
263 | 243, 262 | eqtrd 2805 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
264 | 263 | dmeqd 5462 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
265 | | ovex 6821 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V |
266 | | eqid 2771 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
267 | 265, 266 | dmmpti 6161 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = 𝑋 |
268 | 264, 267 | syl6eq 2821 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = 𝑋) |
269 | 242, 268 | sseqtr4d 3791 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ⊆ dom (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))) |
270 | 67 | adantr 466 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑅 / 2) / 2) ∈ ℝ) |
271 | 242 | sselda 3752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) → 𝑦 ∈ 𝑋) |
272 | 263 | fveq1d 6332 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦) = ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦)) |
273 | 266 | fvmpt2 6431 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑋 ∧ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
274 | 265, 273 | mpan2 671 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
275 | 272, 274 | sylan9eq 2825 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
276 | 275 | fveq2d 6334 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦)) = (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
277 | 265 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) |
278 | 223, 228,
277, 262 | dvmptcl 23935 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ ℂ) |
279 | 278 | abscld 14376 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ∈ ℝ) |
280 | 67 | ad2antrr 705 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 / 2) / 2) ∈ ℝ) |
281 | 254 | ffvelrnda 6500 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ ℂ) |
282 | 259 | ffvelrnda 6500 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ ℂ) |
283 | 281, 282 | abssubd 14393 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))) |
284 | | ulmdvlem1.1 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2)) |
285 | | fveq2 6330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
286 | 285 | oveq2d 6807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑛 → (𝑆 D (𝐹‘𝑚)) = (𝑆 D (𝐹‘𝑛))) |
287 | 286 | fveq1d 6332 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → ((𝑆 D (𝐹‘𝑚))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑥)) |
288 | 287 | oveq2d 6807 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) |
289 | 288 | fveq2d 6334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)))) |
290 | 289 | breq1d 4796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))) |
291 | 290 | ralbidv 3135 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → (∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))) |
292 | 291 | rspccva 3459 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑚 ∈
(ℤ≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)) |
293 | 284, 292 | sylan 569 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)) |
294 | | fveq2 6330 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑁))‘𝑥) = ((𝑆 D (𝐹‘𝑁))‘𝑦)) |
295 | | fveq2 6330 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑛))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑦)) |
296 | 294, 295 | oveq12d 6809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) |
297 | 296 | fveq2d 6334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))) |
298 | 297 | breq1d 4796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2))) |
299 | 298 | rspccva 3459 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)) |
300 | 293, 299 | sylan 569 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)) |
301 | 283, 300 | eqbrtrd 4808 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) < ((𝑅 / 2) / 2)) |
302 | 279, 280,
301 | ltled 10385 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ≤ ((𝑅 / 2) / 2)) |
303 | 276, 302 | eqbrtrd 4808 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2)) |
304 | 271, 303 | syldan 579 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2)) |
305 | 223, 224,
225, 237, 238, 239, 240, 269, 270, 304 | dvlip2 23971 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈))) → (abs‘((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
306 | 222, 305 | mpdan 667 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
307 | 200, 306 | eqbrtrrd 4810 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
308 | 307, 175,
181 | 3brtr4d 4818 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ≤ ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛)) |
309 | 78, 82, 166, 172, 178, 183, 308 | climle 14571 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
310 | 75 | abscld 14376 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ) |
311 | 38, 40 | absrpcld 14388 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈
ℝ+) |
312 | 310, 67, 311 | ledivmul2d 12122 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2) ↔ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))) |
313 | 309, 312 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2)) |
314 | 77, 313 | eqbrtrd 4808 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ≤ ((𝑅 / 2) / 2)) |
315 | 213 | rpred 12068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ) |
316 | | ulmdvlem1.v |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈
ℝ+) |
317 | 316 | rpred 12068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ) |
318 | | ulmdvlem1.l |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊) |
319 | 167, 315,
317, 208, 318 | lttrd 10398 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑊) |
320 | | ulmdvlem1.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((abs‘(𝑌 − 𝐶)) < 𝑊 → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2))) |
321 | 319, 320 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2)) |
322 | 61, 63, 67, 67, 314, 321 | leltaddd 10849 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2))) |
323 | 65 | recnd 10268 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℂ) |
324 | 323 | 2halvesd 11478 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)) = (𝑅 / 2)) |
325 | 322, 324 | breqtrd 4812 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (𝑅 / 2)) |
326 | 50, 64, 65, 66, 325 | lelttrd 10395 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < (𝑅 / 2)) |
327 | | ulmdvlem1.2 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2)) |
328 | 41, 45, 46, 48, 326, 327 | abs3lemd 14401 |
1
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅) |