| Step | Hyp | Ref
| Expression |
| 1 | | climrec.1 |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | | climrec.2 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 3 | | climrec.3 |
. . . . 5
⊢ (𝜑 → 𝐺 ⇝ 𝐴) |
| 4 | | climcl 15535 |
. . . . 5
⊢ (𝐺 ⇝ 𝐴 → 𝐴 ∈ ℂ) |
| 5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 6 | | climrec.4 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 0) |
| 7 | 6 | neneqd 2945 |
. . . . 5
⊢ (𝜑 → ¬ 𝐴 = 0) |
| 8 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 9 | 8 | elsn2 4665 |
. . . . 5
⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
| 10 | 7, 9 | sylnibr 329 |
. . . 4
⊢ (𝜑 → ¬ 𝐴 ∈ {0}) |
| 11 | 5, 10 | eldifd 3962 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖
{0})) |
| 12 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → (𝑤 ∈ (ℂ ∖ {0})
↦ (1 / 𝑤)) = (𝑤 ∈ (ℂ ∖ {0})
↦ (1 / 𝑤))) |
| 13 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧) |
| 14 | 13 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧ 𝑤 = 𝑧) → (1 / 𝑤) = (1 / 𝑧)) |
| 15 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → 𝑧 ∈ (ℂ ∖
{0})) |
| 16 | 15 | eldifad 3963 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → 𝑧 ∈
ℂ) |
| 17 | | eldifsni 4790 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ≠
0) |
| 18 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → 𝑧 ≠ 0) |
| 19 | 16, 18 | reccld 12036 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → (1 /
𝑧) ∈
ℂ) |
| 20 | 12, 14, 15, 19 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → ((𝑤 ∈ (ℂ ∖ {0})
↦ (1 / 𝑤))‘𝑧) = (1 / 𝑧)) |
| 21 | 20, 19 | eqeltrd 2841 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (ℂ ∖ {0})) → ((𝑤 ∈ (ℂ ∖ {0})
↦ (1 / 𝑤))‘𝑧) ∈ ℂ) |
| 22 | | climrec.7 |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑊) |
| 23 | | eqid 2737 |
. . . . . 6
⊢ (if(1
≤ ((abs‘𝐴)
· 𝑥), 1,
((abs‘𝐴) ·
𝑥)) ·
((abs‘𝐴) / 2)) =
(if(1 ≤ ((abs‘𝐴)
· 𝑥), 1,
((abs‘𝐴) ·
𝑥)) ·
((abs‘𝐴) /
2)) |
| 24 | 23 | reccn2 15633 |
. . . . 5
⊢ ((𝐴 ∈ (ℂ ∖ {0})
∧ 𝑥 ∈
ℝ+) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (ℂ ∖
{0})((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥)) |
| 25 | 11, 24 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (ℂ ∖
{0})((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥)) |
| 26 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (𝑤 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑤)) = (𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))) |
| 27 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ (ℂ ∖ {0})
∧ 𝑤 = 𝑧) → 𝑤 = 𝑧) |
| 28 | 27 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ (ℂ ∖ {0})
∧ 𝑤 = 𝑧) → (1 / 𝑤) = (1 / 𝑧)) |
| 29 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈ (ℂ
∖ {0})) |
| 30 | | eldifi 4131 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ 𝑧 ∈
ℂ) |
| 31 | 30, 17 | reccld 12036 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (1 / 𝑧) ∈
ℂ) |
| 32 | 26, 28, 29, 31 | fvmptd 7023 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ ((𝑤 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑤))‘𝑧) = (1 / 𝑧)) |
| 33 | 32 | ad2antlr 727 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) = (1 / 𝑧)) |
| 34 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤)) = (𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))) |
| 35 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → 𝑤 = 𝐴) |
| 36 | 35 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → (1 / 𝑤) = (1 / 𝐴)) |
| 37 | 5, 6 | reccld 12036 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / 𝐴) ∈ ℂ) |
| 38 | 34, 36, 11, 37 | fvmptd 7023 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴) = (1 / 𝐴)) |
| 39 | 38 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴) = (1 / 𝐴)) |
| 40 | 33, 39 | oveq12d 7449 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → (((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴)) = ((1 / 𝑧) − (1 / 𝐴))) |
| 41 | 40 | fveq2d 6910 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘(((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴))) = (abs‘((1 / 𝑧) − (1 / 𝐴)))) |
| 42 | 29 | ad2antlr 727 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → 𝑧 ∈ (ℂ ∖
{0})) |
| 43 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘(𝑧 − 𝐴)) < 𝑦) |
| 44 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → (𝑧 ∈ (ℂ ∖ {0}) →
((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) |
| 45 | 42, 43, 44 | mp2d 49 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥) |
| 46 | 41, 45 | eqbrtrd 5165 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ (𝑧 ∈ (ℂ
∖ {0}) → ((abs‘(𝑧 − 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥))) ∧ 𝑧 ∈ (ℂ ∖ {0})) ∧
(abs‘(𝑧 − 𝐴)) < 𝑦) → (abs‘(((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴))) < 𝑥) |
| 47 | 46 | exp41 434 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑧 ∈ (ℂ ∖ {0})
→ ((abs‘(𝑧
− 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥)) → (𝑧 ∈ (ℂ ∖ {0}) →
((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘(((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴))) < 𝑥)))) |
| 48 | 47 | ralimdv2 3163 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∀𝑧 ∈ (ℂ
∖ {0})((abs‘(𝑧
− 𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥) → ∀𝑧 ∈ (ℂ ∖
{0})((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘(((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴))) < 𝑥))) |
| 49 | 48 | reximdv 3170 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (ℂ ∖
{0})((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘((1 / 𝑧) − (1 / 𝐴))) < 𝑥) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (ℂ ∖
{0})((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘(((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴))) < 𝑥))) |
| 50 | 25, 49 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑧 ∈ (ℂ ∖
{0})((abs‘(𝑧 −
𝐴)) < 𝑦 → (abs‘(((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝑧) − ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴))) < 𝑥)) |
| 51 | | climrec.5 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ (ℂ ∖
{0})) |
| 52 | | climrec.6 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (1 / (𝐺‘𝑘))) |
| 53 | | eqidd 2738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤)) = (𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))) |
| 54 | | oveq2 7439 |
. . . . . 6
⊢ (𝑤 = (𝐺‘𝑘) → (1 / 𝑤) = (1 / (𝐺‘𝑘))) |
| 55 | 54 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑤 = (𝐺‘𝑘)) → (1 / 𝑤) = (1 / (𝐺‘𝑘))) |
| 56 | 51 | eldifad 3963 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℂ) |
| 57 | | eldifsni 4790 |
. . . . . . 7
⊢ ((𝐺‘𝑘) ∈ (ℂ ∖ {0}) → (𝐺‘𝑘) ≠ 0) |
| 58 | 51, 57 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ≠ 0) |
| 59 | 56, 58 | reccld 12036 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (1 / (𝐺‘𝑘)) ∈ ℂ) |
| 60 | 53, 55, 51, 59 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘(𝐺‘𝑘)) = (1 / (𝐺‘𝑘))) |
| 61 | 52, 60 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘(𝐺‘𝑘))) |
| 62 | 1, 2, 11, 21, 3, 22, 50, 51, 61 | climcn1 15628 |
. 2
⊢ (𝜑 → 𝐻 ⇝ ((𝑤 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑤))‘𝐴)) |
| 63 | 62, 38 | breqtrd 5169 |
1
⊢ (𝜑 → 𝐻 ⇝ (1 / 𝐴)) |