Step | Hyp | Ref
| Expression |
1 | | ulmdv.g |
. . . . . 6
⊢ (𝜑 → 𝐺:𝑋⟶ℂ) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐺:𝑋⟶ℂ) |
3 | | ulmdvlem1.y |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑋) |
4 | 2, 3 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝑌) ∈ ℂ) |
5 | | ulmdvlem1.c |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑋) |
6 | 2, 5 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝐺‘𝐶) ∈ ℂ) |
7 | 4, 6 | subcld 10392 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − (𝐺‘𝐶)) ∈ ℂ) |
8 | | ulmdvlem1.n |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝑍) |
9 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑁 → (𝐹‘𝑘) = (𝐹‘𝑁)) |
10 | 9 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑁 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑁))) |
11 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) = (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) |
12 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑆 D (𝐹‘𝑁)) ∈ V |
13 | 10, 11, 12 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁))) |
14 | 8, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) = (𝑆 D (𝐹‘𝑁))) |
15 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 D (𝐹‘𝑘)) ∈ V |
16 | 15 | rgenw 2924 |
. . . . . . . . . . . . . 14
⊢
∀𝑘 ∈
𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V |
17 | 11 | fnmpt 6020 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
𝑍 (𝑆 D (𝐹‘𝑘)) ∈ V → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍) |
19 | | ulmdv.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) |
20 | | ulmf2 24138 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))) Fn 𝑍 ∧ (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
21 | 18, 19, 20 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
22 | 21 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
23 | 22, 8 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑁) ∈ (ℂ ↑𝑚
𝑋)) |
24 | 14, 23 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)) ∈ (ℂ
↑𝑚 𝑋)) |
25 | | elmapi 7879 |
. . . . . . . . 9
⊢ ((𝑆 D (𝐹‘𝑁)) ∈ (ℂ
↑𝑚 𝑋) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ) |
27 | | fdm 6051 |
. . . . . . . 8
⊢ ((𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ → dom (𝑆 D (𝐹‘𝑁)) = 𝑋) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → dom (𝑆 D (𝐹‘𝑁)) = 𝑋) |
29 | | dvbsss 23666 |
. . . . . . 7
⊢ dom
(𝑆 D (𝐹‘𝑁)) ⊆ 𝑆 |
30 | 28, 29 | syl6eqssr 3656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ 𝑆) |
31 | | ulmdv.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
32 | | recnprss 23668 |
. . . . . . . 8
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
34 | 33 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑆 ⊆ ℂ) |
35 | 30, 34 | sstrd 3613 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ⊆ ℂ) |
36 | 35, 3 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ ℂ) |
37 | 35, 5 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ ℂ) |
38 | 36, 37 | subcld 10392 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ∈ ℂ) |
39 | | ulmdvlem1.3 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ≠ 𝐶) |
40 | 36, 37, 39 | subne0d 10401 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑌 − 𝐶) ≠ 0) |
41 | 7, 38, 40 | divcld 10801 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ) |
42 | | ulmcl 24135 |
. . . . 5
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻 → 𝐻:𝑋⟶ℂ) |
43 | 19, 42 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐻:𝑋⟶ℂ) |
44 | 43 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝐻:𝑋⟶ℂ) |
45 | 44, 5 | ffvelrnd 6360 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝐻‘𝐶) ∈ ℂ) |
46 | 26, 5 | ffvelrnd 6360 |
. 2
⊢ ((𝜑 ∧ 𝜓) → ((𝑆 D (𝐹‘𝑁))‘𝐶) ∈ ℂ) |
47 | | ulmdvlem1.r |
. . 3
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈
ℝ+) |
48 | 47 | rpred 11872 |
. 2
⊢ ((𝜑 ∧ 𝜓) → 𝑅 ∈ ℝ) |
49 | 41, 46 | subcld 10392 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ) |
50 | 49 | abscld 14175 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ) |
51 | | ulmdv.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑋)) |
52 | 51 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝐹:𝑍⟶(ℂ ↑𝑚
𝑋)) |
53 | 52, 8 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁) ∈ (ℂ ↑𝑚
𝑋)) |
54 | | elmapi 7879 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑁) ∈ (ℂ ↑𝑚
𝑋) → (𝐹‘𝑁):𝑋⟶ℂ) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝐹‘𝑁):𝑋⟶ℂ) |
56 | 55, 3 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ) |
57 | 55, 5 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ) |
58 | 56, 57 | subcld 10392 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ) |
59 | 58, 38, 40 | divcld 10801 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) ∈ ℂ) |
60 | 41, 59 | subcld 10392 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))) ∈ ℂ) |
61 | 60 | abscld 14175 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ∈ ℝ) |
62 | 59, 46 | subcld 10392 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)) ∈ ℂ) |
63 | 62 | abscld 14175 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ∈ ℝ) |
64 | 61, 63 | readdcld 10069 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) ∈ ℝ) |
65 | 48 | rehalfcld 11279 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℝ) |
66 | 41, 46, 59 | abs3difd 14199 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) ≤ ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))))) |
67 | 65 | rehalfcld 11279 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑅 / 2) / 2) ∈ ℝ) |
68 | 4, 56, 6, 57 | sub4d 10441 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)))) |
69 | 68 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) |
70 | 7, 58, 38, 40 | divsubdird 10840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − (𝐺‘𝐶)) − (((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) |
71 | 69, 70 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶)) = ((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) |
72 | 71 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶))))) |
73 | 4, 56 | subcld 10392 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ) |
74 | 6, 57 | subcld 10392 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ) |
75 | 73, 74 | subcld 10392 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ) |
76 | 75, 38, 40 | absdivd 14194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) / (𝑌 − 𝐶))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶)))) |
77 | 72, 76 | eqtr3d 2658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) = ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶)))) |
78 | | eqid 2622 |
. . . . . . . 8
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
79 | | ulmdv.z |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
80 | 8, 79 | syl6eleq 2711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ (ℤ≥‘𝑀)) |
81 | | eluzelz 11697 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
82 | 80, 81 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ ℤ) |
83 | | ulmdv.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℤ) |
84 | 83 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ) |
85 | | ulmdv.l |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) |
86 | 85 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) |
87 | 86 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → ∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧)) |
88 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑌 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝑌)) |
89 | 88 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑌 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))) |
90 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑌 → (𝐺‘𝑧) = (𝐺‘𝑌)) |
91 | 89, 90 | breq12d 4666 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑌 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌))) |
92 | 91 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ 𝑋 → (∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌))) |
93 | 3, 87, 92 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) ⇝ (𝐺‘𝑌)) |
94 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) ∈ V |
95 | 79, 94 | eqeltri 2697 |
. . . . . . . . . . . . 13
⊢ 𝑍 ∈ V |
96 | 95 | mptex 6486 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V |
97 | 96 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ∈ V) |
98 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
99 | 98 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝑌) = ((𝐹‘𝑛)‘𝑌)) |
100 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌)) |
101 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛)‘𝑌) ∈ V |
102 | 99, 100, 101 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌)) |
103 | 102 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) = ((𝐹‘𝑛)‘𝑌)) |
104 | 52 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑𝑚
𝑋)) |
105 | | elmapi 7879 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛) ∈ (ℂ ↑𝑚
𝑋) → (𝐹‘𝑛):𝑋⟶ℂ) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑋⟶ℂ) |
107 | 3 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝑌 ∈ 𝑋) |
108 | 106, 107 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝑌) ∈ ℂ) |
109 | 103, 108 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) ∈ ℂ) |
110 | 99 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
111 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
112 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ V |
113 | 110, 111,
112 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
114 | 113 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
115 | 103 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌)) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
116 | 114, 115 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑌))‘𝑛) − ((𝐹‘𝑁)‘𝑌))) |
117 | 79, 84, 93, 56, 97, 109, 116 | climsubc1 14368 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) ⇝ ((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
118 | 95 | mptex 6486 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V |
119 | 118 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V) |
120 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐶 → ((𝐹‘𝑘)‘𝑧) = ((𝐹‘𝑘)‘𝐶)) |
121 | 120 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐶 → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))) |
122 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝐶 → (𝐺‘𝑧) = (𝐺‘𝐶)) |
123 | 121, 122 | breq12d 4666 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝐶 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) ↔ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶))) |
124 | 123 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑋 → (∀𝑧 ∈ 𝑋 (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝑧)) ⇝ (𝐺‘𝑧) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶))) |
125 | 5, 87, 124 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) ⇝ (𝐺‘𝐶)) |
126 | 95 | mptex 6486 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V |
127 | 126 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V) |
128 | 98 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝐶) = ((𝐹‘𝑛)‘𝐶)) |
129 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) = (𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶)) |
130 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛)‘𝐶) ∈ V |
131 | 128, 129,
130 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶)) |
132 | 131 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) = ((𝐹‘𝑛)‘𝐶)) |
133 | 5 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → 𝐶 ∈ 𝑋) |
134 | 106, 133 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑛)‘𝐶) ∈ ℂ) |
135 | 132, 134 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) ∈ ℂ) |
136 | 128 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
137 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
138 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ V |
139 | 136, 137,
138 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
140 | 139 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
141 | 132 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶)) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
142 | 140, 141 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ ((𝐹‘𝑘)‘𝐶))‘𝑛) − ((𝐹‘𝑁)‘𝐶))) |
143 | 79, 84, 125, 57, 127, 135, 142 | climsubc1 14368 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ⇝ ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
144 | 56 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝑌) ∈ ℂ) |
145 | 108, 144 | subcld 10392 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) ∈ ℂ) |
146 | 114, 145 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) ∈ ℂ) |
147 | 57 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝐹‘𝑁)‘𝐶) ∈ ℂ) |
148 | 134, 147 | subcld 10392 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)) ∈ ℂ) |
149 | 140, 148 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛) ∈ ℂ) |
150 | 110, 136 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
151 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
152 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ V |
153 | 150, 151,
152 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
154 | 153 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
155 | 114, 140 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
156 | 154, 155 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) = (((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)))‘𝑛) − ((𝑘 ∈ 𝑍 ↦ (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))‘𝑛))) |
157 | 79, 84, 117, 119, 143, 146, 149, 156 | climsub 14364 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ⇝ (((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
158 | 95 | mptex 6486 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V |
159 | 158 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ∈ V) |
160 | 145, 148 | subcld 10392 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) ∈ ℂ) |
161 | 154, 160 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛) ∈ ℂ) |
162 | 150 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
163 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) = (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
164 | | fvex 6201 |
. . . . . . . . . . . 12
⊢
(abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ V |
165 | 162, 163,
164 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
166 | 165 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
167 | 154 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛)) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
168 | 166, 167 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((𝑘 ∈ 𝑍 ↦ ((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))‘𝑛))) |
169 | 79, 157, 159, 84, 161, 168 | climabs 14334 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) ⇝ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
170 | 38 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈ ℝ) |
171 | 67, 170 | remulcld 10070 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ) |
172 | 171 | recnd 10068 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℂ) |
173 | 79 | eqimss2i 3660 |
. . . . . . . . . 10
⊢
(ℤ≥‘𝑀) ⊆ 𝑍 |
174 | 173, 95 | climconst2 14279 |
. . . . . . . . 9
⊢
(((((𝑅 / 2) / 2)
· (abs‘(𝑌
− 𝐶))) ∈ ℂ
∧ 𝑀 ∈ ℤ)
→ (𝑍 × {(((𝑅 / 2) / 2) ·
(abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) ·
(abs‘(𝑌 − 𝐶)))) |
175 | 172, 84, 174 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))}) ⇝ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
176 | 79 | uztrn2 11705 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
177 | 8, 176 | sylan 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ 𝑍) |
178 | 177, 165 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
179 | 160 | abscld 14175 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ 𝑍) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ) |
180 | 177, 179 | syldan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ) |
181 | 178, 180 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ∈ ℝ) |
182 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (((𝑅 / 2) / 2) ·
(abs‘(𝑌 − 𝐶))) ∈ V |
183 | 182 | fvconst2 6469 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
184 | 177, 183 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) = (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
185 | 171 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))) ∈ ℝ) |
186 | 184, 185 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛) ∈ ℝ) |
187 | 177, 106 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑛):𝑋⟶ℂ) |
188 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛):𝑋⟶ℂ → (𝐹‘𝑛) Fn 𝑋) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑛) Fn 𝑋) |
190 | 55 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑁):𝑋⟶ℂ) |
191 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑁):𝑋⟶ℂ → (𝐹‘𝑁) Fn 𝑋) |
192 | 190, 191 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑁) Fn 𝑋) |
193 | | ulmscl 24133 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))(⇝𝑢‘𝑋)𝐻 → 𝑋 ∈ V) |
194 | 19, 193 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ V) |
195 | 194 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑋 ∈ V) |
196 | 3 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑌 ∈ 𝑋) |
197 | | fnfvof 6911 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝑌 ∈ 𝑋)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
198 | 189, 192,
195, 196, 197 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) = (((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌))) |
199 | 5 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ 𝑋) |
200 | | fnfvof 6911 |
. . . . . . . . . . . . 13
⊢ ((((𝐹‘𝑛) Fn 𝑋 ∧ (𝐹‘𝑁) Fn 𝑋) ∧ (𝑋 ∈ V ∧ 𝐶 ∈ 𝑋)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
201 | 189, 192,
195, 199, 200 | syl22anc 1327 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶) = (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))) |
202 | 198, 201 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶)) = ((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) |
203 | 202 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶))) = (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶))))) |
204 | 30, 3 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ 𝑆) |
205 | 30, 5 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ 𝑆) |
206 | 204, 205 | ovresd 6801 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (𝑌(abs ∘ − )𝐶)) |
207 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
208 | 207 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶))) |
209 | 36, 37, 208 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (𝑌(abs ∘ − )𝐶) = (abs‘(𝑌 − 𝐶))) |
210 | 206, 209 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) = (abs‘(𝑌 − 𝐶))) |
211 | | ulmdvlem1.a |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑈) |
212 | 210, 211 | eqbrtrd 4675 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈) |
213 | | cnxmet 22576 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
214 | | xmetres2 22166 |
. . . . . . . . . . . . . . . 16
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑆
× 𝑆)) ∈
(∞Met‘𝑆)) |
215 | 213, 34, 214 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → ((abs ∘ − ) ↾
(𝑆 × 𝑆)) ∈
(∞Met‘𝑆)) |
216 | | ulmdvlem1.u |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈
ℝ+) |
217 | 216 | rpxrd 11873 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈
ℝ*) |
218 | | elbl3 22197 |
. . . . . . . . . . . . . . 15
⊢ (((((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝑈 ∈ ℝ*) ∧ (𝐶 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)) |
219 | 215, 217,
205, 204, 218 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ↔ (𝑌((abs ∘ − ) ↾ (𝑆 × 𝑆))𝐶) < 𝑈)) |
220 | 212, 219 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
221 | 220 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
222 | | blcntr 22218 |
. . . . . . . . . . . . . 14
⊢ ((((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ 𝐶 ∈ 𝑆 ∧ 𝑈 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
223 | 215, 205,
216, 222 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
224 | 223 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) |
225 | 221, 224 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈))) |
226 | 31 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑆 ∈ {ℝ, ℂ}) |
227 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) |
228 | 30 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑋 ⊆ 𝑆) |
229 | 187 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ ℂ) |
230 | 190 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ ℂ) |
231 | 229, 230 | subcld 10392 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)) ∈ ℂ) |
232 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))) |
233 | 231, 232 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))):𝑋⟶ℂ) |
234 | | fvexd 6203 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑛)‘𝑦) ∈ V) |
235 | | fvexd 6203 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝐹‘𝑁)‘𝑦) ∈ V) |
236 | 187 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑛) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) |
237 | 190 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐹‘𝑁) = (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) |
238 | 195, 234,
235, 236, 237 | offval2 6914 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) |
239 | 238 | feq1d 6030 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)):𝑋⟶ℂ ↔ (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))):𝑋⟶ℂ)) |
240 | 233, 239 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)):𝑋⟶ℂ) |
241 | 205 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝐶 ∈ 𝑆) |
242 | 217 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑈 ∈
ℝ*) |
243 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝐶(ball‘((abs ∘
− ) ↾ (𝑆
× 𝑆)))𝑈) = (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) |
244 | | ulmdvlem1.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ⊆ 𝑋) |
245 | 244 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ⊆ 𝑋) |
246 | 238 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦))))) |
247 | | fvexd 6203 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ V) |
248 | 236 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦)))) |
249 | 98 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑛 → (𝑆 D (𝐹‘𝑘)) = (𝑆 D (𝐹‘𝑛))) |
250 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆 D (𝐹‘𝑛)) ∈ V |
251 | 249, 11, 250 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛))) |
252 | 177, 251 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) = (𝑆 D (𝐹‘𝑛))) |
253 | 21 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘))):𝑍⟶(ℂ ↑𝑚
𝑋)) |
254 | 253, 177 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (𝑆 D (𝐹‘𝑘)))‘𝑛) ∈ (ℂ ↑𝑚
𝑋)) |
255 | 252, 254 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑𝑚
𝑋)) |
256 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 D (𝐹‘𝑛)) ∈ (ℂ ↑𝑚
𝑋) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ) |
257 | 255, 256 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)):𝑋⟶ℂ) |
258 | 257 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑛)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦))) |
259 | 248, 258 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑛)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑛))‘𝑦))) |
260 | | fvexd 6203 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ V) |
261 | 237 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦)))) |
262 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)):𝑋⟶ℂ) |
263 | 262 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝐹‘𝑁)) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
264 | 261, 263 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ ((𝐹‘𝑁)‘𝑦))) = (𝑦 ∈ 𝑋 ↦ ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
265 | 226, 229,
247, 259, 230, 260, 264 | dvmptsub 23730 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D (𝑦 ∈ 𝑋 ↦ (((𝐹‘𝑛)‘𝑦) − ((𝐹‘𝑁)‘𝑦)))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
266 | 246, 265 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
267 | 266 | dmeqd 5326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = dom (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
268 | | ovex 6678 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V |
269 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
270 | 268, 269 | dmmpti 6023 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = 𝑋 |
271 | 267, 270 | syl6eq 2672 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → dom (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))) = 𝑋) |
272 | 245, 271 | sseqtr4d 3642 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ⊆ dom (𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))) |
273 | 67 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑅 / 2) / 2) ∈ ℝ) |
274 | 245 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) → 𝑦 ∈ 𝑋) |
275 | 266 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦) = ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦)) |
276 | 269 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑋 ∧ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
277 | 268, 276 | mpan2 707 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑋 → ((𝑦 ∈ 𝑋 ↦ (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
278 | 275, 277 | sylan9eq 2676 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦) = (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) |
279 | 278 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦)) = (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)))) |
280 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ V) |
281 | 226, 231,
280, 265 | dvmptcl 23722 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦)) ∈ ℂ) |
282 | 281 | abscld 14175 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ∈ ℝ) |
283 | 67 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑅 / 2) / 2) ∈ ℝ) |
284 | 257 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑛))‘𝑦) ∈ ℂ) |
285 | 262 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → ((𝑆 D (𝐹‘𝑁))‘𝑦) ∈ ℂ) |
286 | 284, 285 | abssubd 14192 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))) |
287 | | ulmdvlem1.1 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ∀𝑚 ∈ (ℤ≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2)) |
288 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
289 | 288 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑛 → (𝑆 D (𝐹‘𝑚)) = (𝑆 D (𝐹‘𝑛))) |
290 | 289 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑛 → ((𝑆 D (𝐹‘𝑚))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑥)) |
291 | 290 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑛 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) |
292 | 291 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑛 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)))) |
293 | 292 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))) |
294 | 293 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → (∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ↔ ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2))) |
295 | 294 | rspccva 3308 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑚 ∈
(ℤ≥‘𝑁)∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑚))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)) |
296 | 287, 295 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ∀𝑥 ∈ 𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2)) |
297 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑁))‘𝑥) = ((𝑆 D (𝐹‘𝑁))‘𝑦)) |
298 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ((𝑆 D (𝐹‘𝑛))‘𝑥) = ((𝑆 D (𝐹‘𝑛))‘𝑦)) |
299 | 297, 298 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → (((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥)) = (((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) |
300 | 299 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) = (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦)))) |
301 | 300 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ↔ (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2))) |
302 | 301 | rspccva 3308 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝑋 (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑥) − ((𝑆 D (𝐹‘𝑛))‘𝑥))) < ((𝑅 / 2) / 2) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)) |
303 | 296, 302 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝑦) − ((𝑆 D (𝐹‘𝑛))‘𝑦))) < ((𝑅 / 2) / 2)) |
304 | 286, 303 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) < ((𝑅 / 2) / 2)) |
305 | 282, 283,
304 | ltled 10185 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘(((𝑆 D (𝐹‘𝑛))‘𝑦) − ((𝑆 D (𝐹‘𝑁))‘𝑦))) ≤ ((𝑅 / 2) / 2)) |
306 | 279, 305 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ 𝑋) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2)) |
307 | 274, 306 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ 𝑦 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈)) → (abs‘((𝑆 D ((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁)))‘𝑦)) ≤ ((𝑅 / 2) / 2)) |
308 | 226, 227,
228, 240, 241, 242, 243, 272, 273, 307 | dvlip2 23758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) ∧ (𝑌 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈) ∧ 𝐶 ∈ (𝐶(ball‘((abs ∘ − ) ↾
(𝑆 × 𝑆)))𝑈))) → (abs‘((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
309 | 225, 308 | mpdan 702 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝑌) − (((𝐹‘𝑛) ∘𝑓 − (𝐹‘𝑁))‘𝐶))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
310 | 203, 309 | eqbrtrrd 4677 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((((𝐹‘𝑛)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑛)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
311 | 310, 178,
184 | 3brtr4d 4685 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ 𝑍 ↦ (abs‘((((𝐹‘𝑘)‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − (((𝐹‘𝑘)‘𝐶) − ((𝐹‘𝑁)‘𝐶)))))‘𝑛) ≤ ((𝑍 × {(((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))})‘𝑛)) |
312 | 78, 82, 169, 175, 181, 186, 311 | climle 14370 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶)))) |
313 | 75 | abscld 14175 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ∈ ℝ) |
314 | 38, 40 | absrpcld 14187 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) ∈
ℝ+) |
315 | 313, 67, 314 | ledivmul2d 11926 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → (((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2) ↔ (abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) ≤ (((𝑅 / 2) / 2) · (abs‘(𝑌 − 𝐶))))) |
316 | 312, 315 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((abs‘(((𝐺‘𝑌) − ((𝐹‘𝑁)‘𝑌)) − ((𝐺‘𝐶) − ((𝐹‘𝑁)‘𝐶)))) / (abs‘(𝑌 − 𝐶))) ≤ ((𝑅 / 2) / 2)) |
317 | 77, 316 | eqbrtrd 4675 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) ≤ ((𝑅 / 2) / 2)) |
318 | 216 | rpred 11872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑈 ∈ ℝ) |
319 | | ulmdvlem1.v |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈
ℝ+) |
320 | 319 | rpred 11872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ ℝ) |
321 | | ulmdvlem1.l |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑈 < 𝑊) |
322 | 170, 318,
320, 211, 321 | lttrd 10198 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (abs‘(𝑌 − 𝐶)) < 𝑊) |
323 | | ulmdvlem1.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((abs‘(𝑌 − 𝐶)) < 𝑊 → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2))) |
324 | 322, 323 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < ((𝑅 / 2) / 2)) |
325 | 61, 63, 67, 67, 317, 324 | leltaddd 10649 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2))) |
326 | 65 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑅 / 2) ∈ ℂ) |
327 | 326 | 2halvesd 11278 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (((𝑅 / 2) / 2) + ((𝑅 / 2) / 2)) = (𝑅 / 2)) |
328 | 325, 327 | breqtrd 4679 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)))) + (abs‘(((((𝐹‘𝑁)‘𝑌) − ((𝐹‘𝑁)‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶)))) < (𝑅 / 2)) |
329 | 50, 64, 65, 66, 328 | lelttrd 10195 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − ((𝑆 D (𝐹‘𝑁))‘𝐶))) < (𝑅 / 2)) |
330 | | ulmdvlem1.2 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (abs‘(((𝑆 D (𝐹‘𝑁))‘𝐶) − (𝐻‘𝐶))) < (𝑅 / 2)) |
331 | 41, 45, 46, 48, 329, 330 | abs3lemd 14200 |
1
⊢ ((𝜑 ∧ 𝜓) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝐶)) / (𝑌 − 𝐶)) − (𝐻‘𝐶))) < 𝑅) |