| Step | Hyp | Ref
| Expression |
| 1 | | rlimcl 15539 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ)) |
| 3 | | rlimcl 15539 |
. . . 4
⊢ ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ) |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 → 𝐶 ∈ ℂ)) |
| 5 | | rlimresb.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 6 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐴 ⊆ ℝ) |
| 7 | | simprrl 781 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑥 ∈ 𝐴) |
| 8 | 6, 7 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑥 ∈ ℝ) |
| 9 | | rlimresb.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐵 ∈ ℝ) |
| 11 | | elicopnf 13485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ∈ ℝ → (𝑧 ∈ (𝐵[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧))) |
| 12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑧 ∈ (𝐵[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧))) |
| 13 | 12 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧)) |
| 14 | 13 | adantrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → (𝑧 ∈ ℝ ∧ 𝐵 ≤ 𝑧)) |
| 15 | 14 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑧 ∈ ℝ) |
| 16 | 14 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐵 ≤ 𝑧) |
| 17 | | simprrr 782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑧 ≤ 𝑥) |
| 18 | 10, 15, 8, 16, 17 | letrd 11418 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝐵 ≤ 𝑥) |
| 19 | | elicopnf 13485 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈ ℝ → (𝑥 ∈ (𝐵[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥))) |
| 20 | 10, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → (𝑥 ∈ (𝐵[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝐵 ≤ 𝑥))) |
| 21 | 8, 18, 20 | mpbir2and 713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ (𝐵[,)+∞) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥))) → 𝑥 ∈ (𝐵[,)+∞)) |
| 22 | 21 | anassrs 467 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ≤ 𝑥)) → 𝑥 ∈ (𝐵[,)+∞)) |
| 23 | 22 | anassrs 467 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ≤ 𝑥) → 𝑥 ∈ (𝐵[,)+∞)) |
| 24 | | biimt 360 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐵[,)+∞) → ((abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦 ↔ (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ≤ 𝑥) → ((abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦 ↔ (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 26 | 25 | pm5.74da 804 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ (𝑧 ≤ 𝑥 → (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
| 27 | | bi2.04 387 |
. . . . . . . . . . . 12
⊢ ((𝑧 ≤ 𝑥 → (𝑥 ∈ (𝐵[,)+∞) → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 28 | 26, 27 | bitrdi 287 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) ∧ 𝑥 ∈ 𝐴) → ((𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
| 29 | 28 | pm5.74da 804 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → ((𝑥 ∈ 𝐴 → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))))) |
| 30 | | elin 3967 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵[,)+∞))) |
| 31 | 30 | imbi1i 349 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 32 | | impexp 450 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
| 33 | 31, 32 | bitri 275 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵[,)+∞) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
| 34 | 29, 33 | bitr4di 289 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → ((𝑥 ∈ 𝐴 → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)) ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦)))) |
| 35 | 34 | ralbidv2 3174 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐵[,)+∞)) → (∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 36 | 35 | rexbidva 3177 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 37 | 36 | ralbidv 3178 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦) ↔ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 39 | | rlimresb.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
| 40 | 39 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
| 41 | 40 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ ℂ) |
| 42 | 41 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ ℂ) |
| 43 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐴 ⊆ ℝ) |
| 44 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐶 ∈ ℂ) |
| 45 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ∈ ℝ) |
| 46 | 42, 43, 44, 45 | rlim3 15534 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ ∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ 𝐴 (𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 47 | | elinel1 4201 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) → 𝑥 ∈ 𝐴) |
| 48 | 47, 40 | sylan2 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))) → (𝐹‘𝑥) ∈ ℂ) |
| 49 | 48 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝐹‘𝑥) ∈ ℂ) |
| 50 | 49 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝐹‘𝑥) ∈ ℂ) |
| 51 | | inss1 4237 |
. . . . . . . 8
⊢ (𝐴 ∩ (𝐵[,)+∞)) ⊆ 𝐴 |
| 52 | 51, 5 | sstrid 3995 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∩ (𝐵[,)+∞)) ⊆
ℝ) |
| 53 | 52 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐴 ∩ (𝐵[,)+∞)) ⊆
ℝ) |
| 54 | 50, 53, 44, 45 | rlim3 15534 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ ∀𝑦 ∈ ℝ+
∃𝑧 ∈ (𝐵[,)+∞)∀𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞))(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) − 𝐶)) < 𝑦))) |
| 55 | 38, 46, 54 | 3bitr4d 311 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
| 56 | 55 | ex 412 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ℂ → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶))) |
| 57 | 2, 4, 56 | pm5.21ndd 379 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
| 58 | 39 | feqmptd 6977 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
| 59 | 58 | breq1d 5153 |
. 2
⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
| 60 | | resres 6010 |
. . . 4
⊢ ((𝐹 ↾ 𝐴) ↾ (𝐵[,)+∞)) = (𝐹 ↾ (𝐴 ∩ (𝐵[,)+∞))) |
| 61 | | ffn 6736 |
. . . . . 6
⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴) |
| 62 | | fnresdm 6687 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
| 63 | 39, 61, 62 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
| 64 | 63 | reseq1d 5996 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ (𝐵[,)+∞)) = (𝐹 ↾ (𝐵[,)+∞))) |
| 65 | 58 | reseq1d 5996 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ (𝐵[,)+∞))) = ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ∩ (𝐵[,)+∞)))) |
| 66 | | resmpt 6055 |
. . . . . 6
⊢ ((𝐴 ∩ (𝐵[,)+∞)) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ∩ (𝐵[,)+∞))) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥))) |
| 67 | 51, 66 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ↾ (𝐴 ∩ (𝐵[,)+∞))) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) |
| 68 | 65, 67 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ (𝐵[,)+∞))) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥))) |
| 69 | 60, 64, 68 | 3eqtr3a 2801 |
. . 3
⊢ (𝜑 → (𝐹 ↾ (𝐵[,)+∞)) = (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥))) |
| 70 | 69 | breq1d 5153 |
. 2
⊢ (𝜑 → ((𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟
𝐶 ↔ (𝑥 ∈ (𝐴 ∩ (𝐵[,)+∞)) ↦ (𝐹‘𝑥)) ⇝𝑟 𝐶)) |
| 71 | 57, 59, 70 | 3bitr4d 311 |
1
⊢ (𝜑 → (𝐹 ⇝𝑟 𝐶 ↔ (𝐹 ↾ (𝐵[,)+∞)) ⇝𝑟
𝐶)) |