Step | Hyp | Ref
| Expression |
1 | | rlimcl 15064 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ)) |
3 | | rlimcl 15064 |
. . . 4
⊢ ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ)) |
5 | | rlimresb.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
6 | 5 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐴 ⊆ ℝ) |
7 | | simprrl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑥 ∈ 𝐴) |
8 | 6, 7 | sseldd 3902 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑥 ∈ ℝ) |
9 | | rlimresb.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
10 | 9 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐵 ∈ ℝ) |
11 | | elicopnf 13033 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ∈ ℝ → (𝑧 ∈ (𝐵[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧))) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑧 ∈ (𝐵[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧))) |
13 | 12 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧)) |
14 | 13 | adantrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧)) |
15 | 14 | simpld 498 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑧 ∈ ℝ) |
16 | 14 | simprd 499 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐵 ≤ 𝑧) |
17 | | simprrr 782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑧 ≤ 𝑥) |
18 | 10, 15, 8, 16, 17 | letrd 10989 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐵 ≤ 𝑥) |
19 | | elicopnf 13033 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ ℝ → (𝑥 ∈ (𝐵[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥))) |
20 | 10, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → (𝑥 ∈ (𝐵[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥))) |
21 | 8, 18, 20 | mpbir2and 713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑥 ∈ (𝐵[,)+∞)) |
22 | 21 | anassrs 471 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥)) → 𝑥 ∈ (𝐵[,)+∞)) |
23 | 22 | anassrs 471 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ≤ 𝑥) → 𝑥 ∈ (𝐵[,)+∞)) |
24 | | biimt 364 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐵[,)+∞) → ((abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦 ↔ (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ≤ 𝑥) → ((abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦 ↔ (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
26 | 25 | pm5.74da 804 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ (𝑧 ≤ 𝑥 → (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
27 | | bi2.04 392 |
. . . . . . . . . . . 12
⊢ ((𝑧 ≤ 𝑥 → (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
28 | 26, 27 | bitrdi 290 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
29 | 28 | pm5.74da 804 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → ((𝑥 ∈ 𝐴 → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))))) |
30 | | elin 3882 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵[,)+∞))) |
31 | 30 | imbi1i 353 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
32 | | impexp 454 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
33 | 31, 32 | bitri 278 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
34 | 29, 33 | bitr4di 292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → ((𝑥 ∈ 𝐴 → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
35 | 34 | ralbidv2 3116 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → (∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
36 | 35 | rexbidva 3215 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
37 | 36 | ralbidv 3118 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
38 | 37 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
39 | | rlimresb.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
40 | 39 | ffvelrnda 6904 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
41 | 40 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ ℂ) |
42 | 41 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ ℂ) |
43 | 5 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐴 ⊆ ℝ) |
44 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐶 ∈ ℂ) |
45 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ∈ ℝ) |
46 | 42, 43, 44, 45 | rlim3 15059 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ ∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
47 | | elinel1 4109 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → 𝑥 ∈ 𝐴) |
48 | 47, 40 | sylan2 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))) → (𝐹‘𝑥) ∈ ℂ) |
49 | 48 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝐹‘𝑥) ∈ ℂ) |
50 | 49 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝐹‘𝑥) ∈ ℂ) |
51 | | inss1 4143 |
. . . . . . . 8
⊢ (𝐴 ∩ (𝐵[,)+∞)) ⊆ 𝐴 |
52 | 51, 5 | sstrid 3912 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ (𝐵[,)+∞)) ⊆
ℝ) |
53 | 52 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐴 ∩ (𝐵[,)+∞)) ⊆
ℝ) |
54 | 50, 53, 44, 45 | rlim3 15059 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ ∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
55 | 38, 46, 54 | 3bitr4d 314 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
56 | 55 | ex 416 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶))) |
57 | 2, 4, 56 | pm5.21ndd 384 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
58 | 39 | feqmptd 6780 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
59 | 58 | breq1d 5063 |
. 2
⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
60 | | resres 5864 |
. . . 4
⊢ ((𝐹 ↾ 𝐴) ↾ (𝐵[,)+∞)) = (𝐹 ↾ (𝐴 ∩ (𝐵[,)+∞))) |
61 | | ffn 6545 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴) |
62 | | fnresdm 6496 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
63 | 39, 61, 62 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
64 | 63 | reseq1d 5850 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ (𝐵[,)+∞)) = (𝐹 ↾ (𝐵[,)+∞))) |
65 | 58 | reseq1d 5850 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ (𝐵[,)+∞))) = ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ∩ (𝐵[,)+∞)))) |
66 | | resmpt 5905 |
. . . . . 6
⊢ ((𝐴 ∩ (𝐵[,)+∞)) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ∩ (𝐵[,)+∞))) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥))) |
67 | 51, 66 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ∩ (𝐵[,)+∞))) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) |
68 | 65, 67 | eqtrdi 2794 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ (𝐵[,)+∞))) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥))) |
69 | 60, 64, 68 | 3eqtr3a 2802 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵[,)+∞)) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥))) |
70 | 69 | breq1d 5063 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟
𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
71 | 57, 59, 70 | 3bitr4d 314 |
1
⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟
𝐶)) |