Step | Hyp | Ref
| Expression |
1 | | limccl 23445 |
. . 3
⊢ ((𝐹 ↾ 𝐴) limℂ 𝐷) ⊆ ℂ |
2 | | limcperiod.clim |
. . 3
⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐷)) |
3 | 1, 2 | sseldi 3566 |
. 2
⊢ (𝜑 → 𝐶 ∈ ℂ) |
4 | | limcperiod.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
5 | | limcperiod.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) |
6 | 4, 5 | fssresd 5984 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶ℂ) |
7 | | limcperiod.assc |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
8 | | limcrcl 23444 |
. . . . . . . . . 10
⊢ (𝐶 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐷) → ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
9 | 2, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ ℂ ∧ 𝐷 ∈ ℂ)) |
10 | 9 | simp3d 1068 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℂ) |
11 | 6, 7, 10 | ellimc3 23449 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐷) ↔ (𝐶 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)))) |
12 | 2, 11 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤))) |
13 | 12 | simprd 478 |
. . . . 5
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) |
14 | 13 | r19.21bi 2916 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) |
15 | | simpl1l 1105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) → 𝜑) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → 𝜑) |
17 | | simplr 788 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → 𝑏 ∈ 𝐵) |
18 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝐵) |
19 | | limcperiod.b |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} |
20 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑧 → (𝑦 + 𝑇) = (𝑧 + 𝑇)) |
21 | 20 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → (𝑥 = (𝑦 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇))) |
22 | 21 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑦 ∈
𝐴 𝑥 = (𝑦 + 𝑇) ↔ ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 + 𝑇)) |
23 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑤 = (𝑧 + 𝑇))) |
24 | 23 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (∃𝑧 ∈ 𝐴 𝑥 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇))) |
25 | 22, 24 | syl5bb 271 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇) ↔ ∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇))) |
26 | 25 | cbvrabv 3172 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥 ∈ ℂ ∣
∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇)} |
27 | 19, 26 | eqtri 2632 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇)} |
28 | 18, 27 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇)}) |
29 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑏 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑏 = (𝑧 + 𝑇))) |
30 | 29 | rexbidv 3034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑏 → (∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ 𝐴 𝑏 = (𝑧 + 𝑇))) |
31 | 30 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇)} ↔ (𝑏 ∈ ℂ ∧ ∃𝑧 ∈ 𝐴 𝑏 = (𝑧 + 𝑇))) |
32 | 28, 31 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐵 → (𝑏 ∈ ℂ ∧ ∃𝑧 ∈ 𝐴 𝑏 = (𝑧 + 𝑇))) |
33 | 32 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐵 → ∃𝑧 ∈ 𝐴 𝑏 = (𝑧 + 𝑇)) |
34 | 33 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑧 ∈ 𝐴 𝑏 = (𝑧 + 𝑇)) |
35 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑧 + 𝑇) → (𝑏 − 𝑇) = ((𝑧 + 𝑇) − 𝑇)) |
36 | 35 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑏 = (𝑧 + 𝑇)) → (𝑏 − 𝑇) = ((𝑧 + 𝑇) − 𝑇)) |
37 | 7 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℂ) |
38 | | limcperiod.t |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑇 ∈ ℂ) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑇 ∈ ℂ) |
40 | 37, 39 | pncand 10272 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ((𝑧 + 𝑇) − 𝑇) = 𝑧) |
41 | 40 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑏 = (𝑧 + 𝑇)) → ((𝑧 + 𝑇) − 𝑇) = 𝑧) |
42 | 36, 41 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑏 = (𝑧 + 𝑇)) → (𝑏 − 𝑇) = 𝑧) |
43 | | simp2 1055 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑏 = (𝑧 + 𝑇)) → 𝑧 ∈ 𝐴) |
44 | 42, 43 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑏 = (𝑧 + 𝑇)) → (𝑏 − 𝑇) ∈ 𝐴) |
45 | 44 | 3exp 1256 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧 ∈ 𝐴 → (𝑏 = (𝑧 + 𝑇) → (𝑏 − 𝑇) ∈ 𝐴))) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑧 ∈ 𝐴 → (𝑏 = (𝑧 + 𝑇) → (𝑏 − 𝑇) ∈ 𝐴))) |
47 | 46 | rexlimdv 3012 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (∃𝑧 ∈ 𝐴 𝑏 = (𝑧 + 𝑇) → (𝑏 − 𝑇) ∈ 𝐴)) |
48 | 34, 47 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝑏 − 𝑇) ∈ 𝐴) |
49 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑤 ∈ ℂ ∣
∃𝑧 ∈ 𝐴 𝑤 = (𝑧 + 𝑇)} ⊆ ℂ |
50 | 27, 49 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝐵 ⊆
ℂ |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
52 | 51 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ℂ) |
53 | 38 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑇 ∈ ℂ) |
54 | 52, 53 | npcand 10275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝑏 − 𝑇) + 𝑇) = 𝑏) |
55 | 54 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 = ((𝑏 − 𝑇) + 𝑇)) |
56 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑏 − 𝑇) → (𝑥 + 𝑇) = ((𝑏 − 𝑇) + 𝑇)) |
57 | 56 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑏 − 𝑇) → (𝑏 = (𝑥 + 𝑇) ↔ 𝑏 = ((𝑏 − 𝑇) + 𝑇))) |
58 | 57 | rspcev 3282 |
. . . . . . . . . . 11
⊢ (((𝑏 − 𝑇) ∈ 𝐴 ∧ 𝑏 = ((𝑏 − 𝑇) + 𝑇)) → ∃𝑥 ∈ 𝐴 𝑏 = (𝑥 + 𝑇)) |
59 | 48, 55, 58 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑏 = (𝑥 + 𝑇)) |
60 | 16, 17, 59 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → ∃𝑥 ∈ 𝐴 𝑏 = (𝑥 + 𝑇)) |
61 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) |
62 | | nfrab1 3099 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥{𝑥 ∈ ℂ ∣ ∃𝑦 ∈ 𝐴 𝑥 = (𝑦 + 𝑇)} |
63 | 19, 62 | nfcxfr 2749 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐵 |
64 | 63 | nfcri 2745 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑏 ∈ 𝐵 |
65 | 61, 64 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) |
66 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) |
67 | 65, 66 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) |
68 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥abs |
69 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐹 |
70 | 69, 63 | nfres 5319 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥(𝐹 ↾ 𝐵) |
71 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥𝑏 |
72 | 70, 71 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝐹 ↾ 𝐵)‘𝑏) |
73 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥
− |
74 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐶 |
75 | 72, 73, 74 | nfov 6575 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶) |
76 | 68, 75 | nffv 6110 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) |
77 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥
< |
78 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
79 | 76, 77, 78 | nfbr 4629 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤 |
80 | | simp3 1056 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑏 = (𝑥 + 𝑇)) |
81 | 80 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ((𝐹 ↾ 𝐵)‘𝑏) = ((𝐹 ↾ 𝐵)‘(𝑥 + 𝑇))) |
82 | 17 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑏 ∈ 𝐵) |
83 | 80, 82 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (𝑥 + 𝑇) ∈ 𝐵) |
84 | | fvres 6117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 + 𝑇) ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘(𝑥 + 𝑇)) = (𝐹‘(𝑥 + 𝑇))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ((𝐹 ↾ 𝐵)‘(𝑥 + 𝑇)) = (𝐹‘(𝑥 + 𝑇))) |
86 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝜑) |
87 | | simp2 1055 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑥 ∈ 𝐴) |
88 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) |
89 | 88 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((𝜑 ∧ 𝑦 ∈ 𝐴) ↔ (𝜑 ∧ 𝑥 ∈ 𝐴))) |
90 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = 𝑥 → (𝑦 + 𝑇) = (𝑥 + 𝑇)) |
91 | 90 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘(𝑥 + 𝑇))) |
92 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
93 | 91, 92 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → ((𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦) ↔ (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))) |
94 | 89, 93 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → (((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)))) |
95 | | limcperiod.fper |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) |
96 | 94, 95 | chvarv 2251 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
97 | 86, 87, 96 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) |
98 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
99 | 87, 98 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ((𝐹 ↾ 𝐴)‘𝑥) = (𝐹‘𝑥)) |
100 | 97, 99 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (𝐹‘(𝑥 + 𝑇)) = ((𝐹 ↾ 𝐴)‘𝑥)) |
101 | 81, 85, 100 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ((𝐹 ↾ 𝐵)‘𝑏) = ((𝐹 ↾ 𝐴)‘𝑥)) |
102 | 101 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (((𝐹 ↾ 𝐵)‘𝑏) − 𝐶) = (((𝐹 ↾ 𝐴)‘𝑥) − 𝐶)) |
103 | 102 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) = (abs‘(((𝐹 ↾ 𝐴)‘𝑥) − 𝐶))) |
104 | | simpll3 1095 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) |
105 | 104 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) |
106 | 105, 87 | jca 553 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤) ∧ 𝑥 ∈ 𝐴)) |
107 | | simp1rl 1119 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑏 ≠ (𝐷 + 𝑇)) |
108 | 107 | neneqd 2787 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ¬ 𝑏 = (𝐷 + 𝑇)) |
109 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐷 → (𝑥 + 𝑇) = (𝐷 + 𝑇)) |
110 | 80, 109 | sylan9eq 2664 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) ∧ 𝑥 = 𝐷) → 𝑏 = (𝐷 + 𝑇)) |
111 | 108, 110 | mtand 689 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ¬ 𝑥 = 𝐷) |
112 | 111 | neqned 2789 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑥 ≠ 𝐷) |
113 | 80 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (𝑏 − (𝐷 + 𝑇)) = ((𝑥 + 𝑇) − (𝐷 + 𝑇))) |
114 | 7 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
115 | 86, 87, 114 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑥 ∈ ℂ) |
116 | 86, 10 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝐷 ∈ ℂ) |
117 | 86, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → 𝑇 ∈ ℂ) |
118 | 115, 116,
117 | pnpcan2d 10309 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → ((𝑥 + 𝑇) − (𝐷 + 𝑇)) = (𝑥 − 𝐷)) |
119 | 113, 118 | eqtr2d 2645 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (𝑥 − 𝐷) = (𝑏 − (𝐷 + 𝑇))) |
120 | 119 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (abs‘(𝑥 − 𝐷)) = (abs‘(𝑏 − (𝐷 + 𝑇)))) |
121 | | simp1rr 1120 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) |
122 | 120, 121 | eqbrtrd 4605 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (abs‘(𝑥 − 𝐷)) < 𝑧) |
123 | 112, 122 | jca 553 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (𝑥 ≠ 𝐷 ∧ (abs‘(𝑥 − 𝐷)) < 𝑧)) |
124 | | neeq1 2844 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑦 ≠ 𝐷 ↔ 𝑥 ≠ 𝐷)) |
125 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → (𝑦 − 𝐷) = (𝑥 − 𝐷)) |
126 | 125 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝐷)) = (abs‘(𝑥 − 𝐷))) |
127 | 126 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝐷)) < 𝑧 ↔ (abs‘(𝑥 − 𝐷)) < 𝑧)) |
128 | 124, 127 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) ↔ (𝑥 ≠ 𝐷 ∧ (abs‘(𝑥 − 𝐷)) < 𝑧))) |
129 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((𝐹 ↾ 𝐴)‘𝑦) = ((𝐹 ↾ 𝐴)‘𝑥)) |
130 | 129 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (((𝐹 ↾ 𝐴)‘𝑦) − 𝐶) = (((𝐹 ↾ 𝐴)‘𝑥) − 𝐶)) |
131 | 130 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) = (abs‘(((𝐹 ↾ 𝐴)‘𝑥) − 𝐶))) |
132 | 131 | breq1d 4593 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑥 → ((abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤 ↔ (abs‘(((𝐹 ↾ 𝐴)‘𝑥) − 𝐶)) < 𝑤)) |
133 | 128, 132 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑥 → (((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤) ↔ ((𝑥 ≠ 𝐷 ∧ (abs‘(𝑥 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑥) − 𝐶)) < 𝑤))) |
134 | 133 | rspccva 3281 |
. . . . . . . . . . . . 13
⊢
((∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≠ 𝐷 ∧ (abs‘(𝑥 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑥) − 𝐶)) < 𝑤)) |
135 | 106, 123,
134 | sylc 63 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (abs‘(((𝐹 ↾ 𝐴)‘𝑥) − 𝐶)) < 𝑤) |
136 | 103, 135 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) ∧ 𝑥 ∈ 𝐴 ∧ 𝑏 = (𝑥 + 𝑇)) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤) |
137 | 136 | 3exp 1256 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → (𝑥 ∈ 𝐴 → (𝑏 = (𝑥 + 𝑇) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤))) |
138 | 67, 79, 137 | rexlimd 3008 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → (∃𝑥 ∈ 𝐴 𝑏 = (𝑥 + 𝑇) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)) |
139 | 60, 138 | mpd 15 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑤 ∈ ℝ+)
∧ 𝑧 ∈
ℝ+ ∧ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) ∧ (𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧)) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤) |
140 | 139 | ex 449 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) ∧ 𝑏 ∈ 𝐵) → ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)) |
141 | 140 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑤 ∈ ℝ+) ∧ 𝑧 ∈ ℝ+
∧ ∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤)) → ∀𝑏 ∈ 𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)) |
142 | 141 | 3exp 1256 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (𝑧 ∈ ℝ+
→ (∀𝑦 ∈
𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤) → ∀𝑏 ∈ 𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)))) |
143 | 142 | reximdvai 2998 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
(∃𝑧 ∈
ℝ+ ∀𝑦 ∈ 𝐴 ((𝑦 ≠ 𝐷 ∧ (abs‘(𝑦 − 𝐷)) < 𝑧) → (abs‘(((𝐹 ↾ 𝐴)‘𝑦) − 𝐶)) < 𝑤) → ∃𝑧 ∈ ℝ+ ∀𝑏 ∈ 𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤))) |
144 | 14, 143 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑏 ∈ 𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)) |
145 | 144 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑏 ∈ 𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)) |
146 | | limcperiod.bss |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ dom 𝐹) |
147 | 4, 146 | fssresd 5984 |
. . 3
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶ℂ) |
148 | 10, 38 | addcld 9938 |
. . 3
⊢ (𝜑 → (𝐷 + 𝑇) ∈ ℂ) |
149 | 147, 51, 148 | ellimc3 23449 |
. 2
⊢ (𝜑 → (𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝐷 + 𝑇)) ↔ (𝐶 ∈ ℂ ∧ ∀𝑤 ∈ ℝ+
∃𝑧 ∈
ℝ+ ∀𝑏 ∈ 𝐵 ((𝑏 ≠ (𝐷 + 𝑇) ∧ (abs‘(𝑏 − (𝐷 + 𝑇))) < 𝑧) → (abs‘(((𝐹 ↾ 𝐵)‘𝑏) − 𝐶)) < 𝑤)))) |
150 | 3, 145, 149 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐶 ∈ ((𝐹 ↾ 𝐵) limℂ (𝐷 + 𝑇))) |