Proof of Theorem radcnvrat
Step | Hyp | Ref
| Expression |
1 | | radcnvrat.r |
. 2
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
2 | | xrltso 11850 |
. . . 4
⊢ < Or
ℝ* |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → < Or
ℝ*) |
4 | | radcnvrat.z |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
5 | | radcnvrat.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
6 | 5 | nn0zd 11356 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
7 | 4 | reseq2i 5314 |
. . . . . . 7
⊢ (𝐷 ↾ 𝑍) = (𝐷 ↾ (ℤ≥‘𝑀)) |
8 | | radcnvrat.l |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⇝ 𝐿) |
9 | | radcnvrat.rat |
. . . . . . . . . 10
⊢ 𝐷 = (𝑘 ∈ ℕ0 ↦
(abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) |
10 | | nn0ex 11175 |
. . . . . . . . . . 11
⊢
ℕ0 ∈ V |
11 | 10 | mptex 6390 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ∈ V |
12 | 9, 11 | eqeltri 2684 |
. . . . . . . . 9
⊢ 𝐷 ∈ V |
13 | | climres 14154 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐷 ∈ V) → ((𝐷 ↾
(ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿)) |
14 | 6, 12, 13 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿 ↔ 𝐷 ⇝ 𝐿)) |
15 | 8, 14 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ↾ (ℤ≥‘𝑀)) ⇝ 𝐿) |
16 | 7, 15 | syl5eqbr 4618 |
. . . . . 6
⊢ (𝜑 → (𝐷 ↾ 𝑍) ⇝ 𝐿) |
17 | 9 | reseq1i 5313 |
. . . . . . . . 9
⊢ (𝐷 ↾ 𝑍) = ((𝑘 ∈ ℕ0 ↦
(abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍) |
18 | | eluznn0 11633 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
19 | 5, 18 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
20 | 19 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘𝑀) → 𝑘 ∈
ℕ0)) |
21 | 20 | ssrdv 3574 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘𝑀) ⊆
ℕ0) |
22 | 4, 21 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ⊆
ℕ0) |
23 | 22 | resmptd 5371 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑘 ∈ ℕ0 ↦
(abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))) |
24 | 17, 23 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ↾ 𝑍) = (𝑘 ∈ 𝑍 ↦ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))))) |
25 | | fvex 6113 |
. . . . . . . . 9
⊢
(abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ V |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ V) |
27 | 24, 26 | fvmpt2d 6202 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) |
28 | 4 | peano2uzs 11618 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝑍 → (𝑘 + 1) ∈ 𝑍) |
29 | 22 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝑘 + 1) ∈
ℕ0) |
30 | | radcnvrat.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
31 | 30 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ ℕ0) →
(𝐴‘(𝑘 + 1)) ∈
ℂ) |
32 | 29, 31 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ) |
33 | 28, 32 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ) |
34 | 22 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0) |
35 | 30 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
36 | 34, 35 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ) |
37 | | radcnvrat.n0 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0) |
38 | 33, 36, 37 | divcld 10680 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ) |
39 | 38 | abscld 14023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) ∈ ℝ) |
40 | 27, 39 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) ∈ ℝ) |
41 | 4, 6, 16, 40 | climrecl 14162 |
. . . . 5
⊢ (𝜑 → 𝐿 ∈ ℝ) |
42 | | radcnvrat.ln0 |
. . . . 5
⊢ (𝜑 → 𝐿 ≠ 0) |
43 | 41, 42 | rereccld 10731 |
. . . 4
⊢ (𝜑 → (1 / 𝐿) ∈ ℝ) |
44 | 43 | rexrd 9968 |
. . 3
⊢ (𝜑 → (1 / 𝐿) ∈
ℝ*) |
45 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
46 | | elrabi 3328 |
. . . . 5
⊢ (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → 𝑥 ∈
ℝ) |
47 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 𝐿) ∈
ℝ) |
48 | | recn 9905 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
49 | 48 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
50 | 49 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈
ℝ) |
51 | 47, 50 | ltlend 10061 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿)))) |
52 | 51 | simplbda 652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → (abs‘𝑥) ≠ (1 / 𝐿)) |
53 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿)))) |
54 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿)) |
55 | 54 | biantrud 527 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ((1 / 𝐿) ≤ (abs‘𝑥) ∧ (abs‘𝑥) ≠ (1 / 𝐿)))) |
56 | 47, 50 | lenltd 10062 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿))) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) ≤ (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿))) |
58 | 53, 55, 57 | 3bitr2d 295 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ (abs‘𝑥) < (1 / 𝐿))) |
59 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
60 | 50 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈
ℂ) |
61 | 41 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐿 ∈ ℂ) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈ ℂ) |
63 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ≠ 0) |
64 | 59, 60, 62, 63 | divmul3d 10714 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) = (abs‘𝑥) ↔ 1 = ((abs‘𝑥) · 𝐿))) |
65 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 /
𝐿) = (abs‘𝑥) ↔ (abs‘𝑥) = (1 / 𝐿)) |
66 | | eqcom 2617 |
. . . . . . . . . . . . . . . . 17
⊢ (1 =
((abs‘𝑥) ·
𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1) |
67 | 64, 65, 66 | 3bitr3g 301 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) = (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) = 1)) |
68 | 67 | necon3bid 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) ≠ (1 / 𝐿) ↔ ((abs‘𝑥) · 𝐿) ≠ 1)) |
69 | 68 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) · 𝐿) ≠ 1) |
70 | | 1red 9934 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℝ) |
71 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑍 → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘)) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐷 ↾ 𝑍)‘𝑘) = (𝐷‘𝑘)) |
73 | 72, 40 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℝ) |
74 | 38 | absge0d 14031 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) |
75 | 74, 27 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ ((𝐷 ↾ 𝑍)‘𝑘)) |
76 | 75, 72 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ (𝐷‘𝑘)) |
77 | 4, 6, 8, 73, 76 | climge0 14163 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ≤ 𝐿) |
78 | 41, 77, 42 | ne0gt0d 10053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 < 𝐿) |
79 | 41, 78 | elrpd 11745 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐿 ∈
ℝ+) |
80 | 79 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐿 ∈
ℝ+) |
81 | 50, 70, 80 | ltmuldivd 11795 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿))) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ (abs‘𝑥) < (1 / 𝐿))) |
83 | | elun 3715 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((ℝ ∩ {0})
∪ (ℝ ∖ {0})) ↔ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖
{0}))) |
84 | | inundif 3998 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℝ
∩ {0}) ∪ (ℝ ∖ {0})) = ℝ |
85 | 84 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ((ℝ ∩ {0})
∪ (ℝ ∖ {0})) ↔ 𝑥 ∈ ℝ) |
86 | 83, 85 | bitr3i 265 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ℝ ∩ {0}) ∨
𝑥 ∈ (ℝ ∖
{0})) ↔ 𝑥 ∈
ℝ) |
87 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (ℝ ∩ {0})
↔ (𝑥 ∈ ℝ
∧ 𝑥 ∈
{0})) |
88 | 87 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (ℝ ∩ {0})
→ 𝑥 ∈
{0}) |
89 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (ℝ ∩ {0})
→ 𝑥 =
0) |
91 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 0 → (abs‘𝑥) =
(abs‘0)) |
92 | | abs0 13873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(abs‘0) = 0 |
93 | 91, 92 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 0 → (abs‘𝑥) = 0) |
94 | 93 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 0 → ((abs‘𝑥) · 𝐿) = (0 · 𝐿)) |
95 | 61 | mul02d 10113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (0 · 𝐿) = 0) |
96 | 94, 95 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) = 0) |
97 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
1 |
98 | 96, 97 | syl6eqbr 4622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 = 0) → ((abs‘𝑥) · 𝐿) < 1) |
99 | | radcnvrat.g |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
100 | 99, 30 | radcnv0 23974 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ∈ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝
}) |
101 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 0 → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ 0 ∈
{𝑟 ∈ ℝ ∣
seq0( + , (𝐺‘𝑟)) ∈ dom ⇝
})) |
102 | 100, 101 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑥 = 0 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
103 | 102 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 = 0) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
104 | 98, 103 | 2thd 254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 = 0) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
105 | 90, 104 | sylan2 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∩ {0})) →
(((abs‘𝑥) ·
𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
106 | 105 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∩ {0})) →
(((abs‘𝑥) ·
𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
107 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ℝ
⊆ ℂ |
108 | | ssdif 3707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℝ
⊆ ℂ → (ℝ ∖ {0}) ⊆ (ℂ ∖
{0})) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℝ
∖ {0}) ⊆ (ℂ ∖ {0}) |
110 | 109 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (ℝ ∖ {0})
→ 𝑥 ∈ (ℂ
∖ {0})) |
111 | | nn0uz 11598 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
ℕ0 = (ℤ≥‘0) |
112 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) → 𝑀 ∈
ℕ0) |
113 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘𝑥) ∈ V |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) → (𝐺‘𝑥) ∈ V) |
115 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ∈
ℂ) |
116 | 99 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))))) |
117 | 10 | mptex 6390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V |
118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ V) |
119 | 116, 118 | fvmpt2d 6202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
121 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘)) |
122 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (𝑥↑𝑛) = (𝑥↑𝑘)) |
123 | 121, 122 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
124 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
125 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
126 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V) |
128 | 120, 124,
125, 127 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
129 | 35 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
130 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → 𝑥 ∈
ℂ) |
131 | 130, 125 | expcld 12870 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑥↑𝑘) ∈ ℂ) |
132 | 129, 131 | mulcld 9939 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ) |
133 | 128, 132 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑥)‘𝑘) ∈ ℂ) |
134 | 115, 133 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ ℕ0)
→ ((𝐺‘𝑥)‘𝑘) ∈ ℂ) |
135 | 134 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) ∧ 𝑘 ∈ ℕ0)
→ ((𝐺‘𝑥)‘𝑘) ∈ ℂ) |
136 | 34 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0) |
137 | 136, 128 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
138 | 115, 137 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
139 | 36 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ∈ ℂ) |
140 | 115 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈
ℂ) |
141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ ℂ) |
142 | 34 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℕ0) |
143 | 141, 142 | expcld 12870 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ∈ ℂ) |
144 | 37 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘𝑘) ≠ 0) |
145 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ≠
0) |
146 | 145 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑥 ≠ 0) |
147 | 142 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
148 | 141, 146,
147 | expne0d 12876 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑𝑘) ≠ 0) |
149 | 139, 143,
144, 148 | mulne0d 10558 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ≠ 0) |
150 | 138, 149 | eqnetrd 2849 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0) |
151 | 150 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) ≠ 0) |
152 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
153 | 152 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘(𝑛 + 1)) = ((𝐺‘𝑥)‘(𝑘 + 1))) |
154 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑘 → ((𝐺‘𝑥)‘𝑛) = ((𝐺‘𝑥)‘𝑘)) |
155 | 153, 154 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑘 → (((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)) = (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) |
156 | 155 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑘 → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))) |
157 | 156 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑘 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))) |
158 | 4 | reseq2i 5314 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = ((𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾
(ℤ≥‘𝑀)) |
159 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑍 ⊆
ℕ0) |
160 | 159 | resmptd 5371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾ 𝑍) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))) |
161 | 158, 160 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾
(ℤ≥‘𝑀)) = (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))) |
162 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑀 ∈
ℤ) |
163 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝐷 ⇝ 𝐿) |
164 | 140 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℝ) |
165 | 164 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(abs‘𝑥) ∈
ℂ) |
166 | 10 | mptex 6390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V |
167 | 166 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V) |
168 | 73 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ) |
169 | 168 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) ∈ ℂ) |
170 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) = (𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))) |
171 | 156 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))) |
172 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) ∈ V |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) ∈ V) |
174 | 170, 171,
142, 173 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)))) |
175 | 119 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑥) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
176 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → 𝑛 = (𝑘 + 1)) |
177 | 176 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝐴‘𝑛) = (𝐴‘(𝑘 + 1))) |
178 | 176 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → (𝑥↑𝑛) = (𝑥↑(𝑘 + 1))) |
179 | 177, 178 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = (𝑘 + 1)) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1)))) |
180 | | 1nn0 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ 1 ∈
ℕ0 |
181 | 180 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → 1 ∈
ℕ0) |
182 | 136, 181 | nn0addcld 11232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈
ℕ0) |
183 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V |
184 | 183 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) ∈ V) |
185 | 175, 179,
182, 184 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1)))) |
186 | 123 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
187 | 126 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ V) |
188 | 175, 186,
136, 187 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑥)‘𝑘) = ((𝐴‘𝑘) · (𝑥↑𝑘))) |
189 | 185, 188 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘)))) |
190 | 115, 189 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘)))) |
191 | 33 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐴‘(𝑘 + 1)) ∈ ℂ) |
192 | 115, 182 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈
ℕ0) |
193 | 141, 192 | expcld 12870 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑(𝑘 + 1)) ∈ ℂ) |
194 | 191, 139,
193, 143, 144, 148 | divmuldivd 10721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) · (𝑥↑(𝑘 + 1))) / ((𝐴‘𝑘) · (𝑥↑𝑘)))) |
195 | 142 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℂ) |
196 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → 1 ∈ ℂ) |
197 | 195, 196 | pncan2d 10273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑘 + 1) − 𝑘) = 1) |
198 | 197 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = (𝑥↑1)) |
199 | 192 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑘 + 1) ∈ ℤ) |
200 | 141, 146,
147, 199 | expsubd 12881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑((𝑘 + 1) − 𝑘)) = ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) |
201 | 141 | exp1d 12865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝑥↑1) = 𝑥) |
202 | 198, 200,
201 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘)) = 𝑥) |
203 | 202 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · ((𝑥↑(𝑘 + 1)) / (𝑥↑𝑘))) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) |
204 | 190, 194,
203 | 3eqtr2d 2650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘)) = (((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) |
205 | 204 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐺‘𝑥)‘(𝑘 + 1)) / ((𝐺‘𝑥)‘𝑘))) = (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥))) |
206 | 38 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) ∈ ℂ) |
207 | 206, 141 | absmuld 14041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘(((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)) · 𝑥)) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥))) |
208 | 174, 205,
207 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥))) |
209 | 72, 27 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) |
210 | 209 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (𝐷‘𝑘) = (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘)))) |
211 | 210 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) = (𝐷‘𝑘)) |
212 | 211 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((abs‘((𝐴‘(𝑘 + 1)) / (𝐴‘𝑘))) · (abs‘𝑥)) = ((𝐷‘𝑘) · (abs‘𝑥))) |
213 | 165 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → (abs‘𝑥) ∈ ℂ) |
214 | 169, 213 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝐷‘𝑘) · (abs‘𝑥)) = ((abs‘𝑥) · (𝐷‘𝑘))) |
215 | 208, 212,
214 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑘 ∈ 𝑍) → ((𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛))))‘𝑘) = ((abs‘𝑥) · (𝐷‘𝑘))) |
216 | 4, 162, 163, 165, 167, 169, 215 | climmulc2 14215 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)) |
217 | | climres 14154 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℤ ∧ (𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ∈ V) → (((𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾
(ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))) |
218 | 162, 166,
217 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) →
(((𝑛 ∈
ℕ0 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾
(ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿) ↔ (𝑛 ∈ ℕ0 ↦
(abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿))) |
219 | 216, 218 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑛 ∈ ℕ0
↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ↾
(ℤ≥‘𝑀)) ⇝ ((abs‘𝑥) · 𝐿)) |
220 | 161, 219 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)) |
221 | 220 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) → (𝑛 ∈ 𝑍 ↦ (abs‘(((𝐺‘𝑥)‘(𝑛 + 1)) / ((𝐺‘𝑥)‘𝑛)))) ⇝ ((abs‘𝑥) · 𝐿)) |
222 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) →
((abs‘𝑥) ·
𝐿) ≠ 1) |
223 | 111, 4, 112, 114, 135, 151, 157, 221, 222 | cvgdvgrat 37534 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (ℂ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) →
(((abs‘𝑥) ·
𝐿) < 1 ↔ seq0( + ,
(𝐺‘𝑥)) ∈ dom ⇝ )) |
224 | 110, 223 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) →
(((abs‘𝑥) ·
𝐿) < 1 ↔ seq0( + ,
(𝐺‘𝑥)) ∈ dom ⇝ )) |
225 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (ℝ ∖ {0})
→ 𝑥 ∈
ℝ) |
226 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 = 𝑥 → (𝐺‘𝑟) = (𝐺‘𝑥)) |
227 | 226 | seqeq3d 12671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑟 = 𝑥 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑥))) |
228 | 227 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 = 𝑥 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑥)) ∈ dom ⇝ )) |
229 | 228 | elrab3 3332 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + ,
(𝐺‘𝑥)) ∈ dom ⇝ )) |
230 | 225, 229 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (ℝ ∖ {0})
→ (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ↔
seq0( + , (𝐺‘𝑥)) ∈ dom ⇝
)) |
231 | 230 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ seq0( + ,
(𝐺‘𝑥)) ∈ dom ⇝ )) |
232 | 224, 231 | bitr4d 270 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (ℝ ∖ {0})) ∧
((abs‘𝑥) ·
𝐿) ≠ 1) →
(((abs‘𝑥) ·
𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
233 | 232 | an32s 842 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ (ℝ ∖ {0})) →
(((abs‘𝑥) ·
𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
234 | 106, 233 | jaodan 822 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ (𝑥 ∈ (ℝ ∩ {0}) ∨ 𝑥 ∈ (ℝ ∖ {0})))
→ (((abs‘𝑥)
· 𝐿) < 1 ↔
𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝
})) |
235 | 86, 234 | sylan2br 492 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ((abs‘𝑥) · 𝐿) ≠ 1) ∧ 𝑥 ∈ ℝ) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
236 | 235 | an32s 842 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → (((abs‘𝑥) · 𝐿) < 1 ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
237 | 82, 236 | bitr3d 269 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ ((abs‘𝑥) · 𝐿) ≠ 1) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
238 | 69, 237 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) ↔ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
239 | 238 | notbid 307 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → (¬ (abs‘𝑥) < (1 / 𝐿) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
240 | 58, 239 | bitrd 267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) ↔ ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
241 | 240 | biimpd 218 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
242 | 241 | impancom 455 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ((abs‘𝑥) ≠ (1 / 𝐿) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
243 | 52, 242 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < (abs‘𝑥)) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
244 | 243 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < (abs‘𝑥) → ¬ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
245 | 244 | con2d 128 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 /
𝐿) < (abs‘𝑥))) |
246 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) ∈ ℝ) |
247 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ∈ ℝ) |
248 | 50 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (abs‘𝑥) ∈ ℝ) |
249 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < 𝑥) |
250 | 247 | leabsd 14001 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → 𝑥 ≤ (abs‘𝑥)) |
251 | 246, 247,
248, 249, 250 | ltletrd 10076 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (1 / 𝐿) < 𝑥) → (1 / 𝐿) < (abs‘𝑥)) |
252 | 251 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((1 / 𝐿) < 𝑥 → (1 / 𝐿) < (abs‘𝑥))) |
253 | 245, 252 | nsyld 153 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 /
𝐿) < 𝑥)) |
254 | 46, 253 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → (𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → ¬ (1 /
𝐿) < 𝑥)) |
255 | 45, 254 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ¬ (1 /
𝐿) < 𝑥) |
256 | 43 | renegcld 10336 |
. . . . . . . . 9
⊢ (𝜑 → -(1 / 𝐿) ∈ ℝ) |
257 | 256 | rexrd 9968 |
. . . . . . . 8
⊢ (𝜑 → -(1 / 𝐿) ∈
ℝ*) |
258 | | iooss1 12081 |
. . . . . . . 8
⊢ ((-(1 /
𝐿) ∈
ℝ* ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿))) |
259 | 257, 258 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿))) |
260 | 259 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → (𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿))) |
261 | | eliooord 12104 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → (𝑥 < 𝑘 ∧ 𝑘 < (1 / 𝐿))) |
262 | 261 | simpld 474 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (𝑥(,)(1 / 𝐿)) → 𝑥 < 𝑘) |
263 | 262 | rgen 2906 |
. . . . . . . . 9
⊢
∀𝑘 ∈
(𝑥(,)(1 / 𝐿))𝑥 < 𝑘 |
264 | | ioon0 12072 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ (1 / 𝐿) ∈
ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿))) |
265 | 44, 264 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝜑) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿))) |
266 | 265 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ 𝑥 < (1 / 𝐿))) |
267 | 266 | biimpar 501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (𝑥(,)(1 / 𝐿)) ≠ ∅) |
268 | | r19.2zb 4013 |
. . . . . . . . . 10
⊢ ((𝑥(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)) |
269 | 267, 268 | sylib 207 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → (∀𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘)) |
270 | 263, 269 | mpi 20 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ 𝑥 < (1 / 𝐿)) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘) |
271 | 270 | anasss 677 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘) |
272 | 271 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘) |
273 | | ssrexv 3630 |
. . . . . 6
⊢ ((𝑥(,)(1 / 𝐿)) ⊆ (-(1 / 𝐿)(,)(1 / 𝐿)) → (∃𝑘 ∈ (𝑥(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)) |
274 | 260, 272,
273 | sylc 63 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘) |
275 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) → 𝑥 ∈ ℝ*) |
276 | | xrltnle 9984 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ -(1 / 𝐿) ∈
ℝ*) → (𝑥 < -(1 / 𝐿) ↔ ¬ -(1 / 𝐿) ≤ 𝑥)) |
277 | | xrltle 11858 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ -(1 / 𝐿) ∈
ℝ*) → (𝑥 < -(1 / 𝐿) → 𝑥 ≤ -(1 / 𝐿))) |
278 | 276, 277 | sylbird 249 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ*
∧ -(1 / 𝐿) ∈
ℝ*) → (¬ -(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿))) |
279 | 257, 278 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ*
∧ 𝜑) → (¬ -(1 /
𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿))) |
280 | 279 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ*) → (¬
-(1 / 𝐿) ≤ 𝑥 → 𝑥 ≤ -(1 / 𝐿))) |
281 | 280 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) → 𝑥 ≤ -(1 / 𝐿)) |
282 | | iooss1 12081 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ*
∧ 𝑥 ≤ -(1 / 𝐿)) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿))) |
283 | 275, 281,
282 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ (𝑥(,)(1 / 𝐿))) |
284 | 283 | sselda 3568 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑘 ∈ (𝑥(,)(1 / 𝐿))) |
285 | 284, 262 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) ∧ 𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 < 𝑘) |
286 | 285 | ralrimiva 2949 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) → ∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘) |
287 | 41, 78 | recgt0d 10837 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (1 / 𝐿)) |
288 | 43, 43, 287, 287 | addgt0d 10481 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < ((1 / 𝐿) + (1 / 𝐿))) |
289 | 43 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 𝐿) ∈ ℂ) |
290 | 289, 289 | subnegd 10278 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((1 / 𝐿) − -(1 / 𝐿)) = ((1 / 𝐿) + (1 / 𝐿))) |
291 | 288, 290 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < ((1 / 𝐿) − -(1 / 𝐿))) |
292 | 256, 43 | posdifd 10493 |
. . . . . . . . . . 11
⊢ (𝜑 → (-(1 / 𝐿) < (1 / 𝐿) ↔ 0 < ((1 / 𝐿) − -(1 / 𝐿)))) |
293 | 291, 292 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → -(1 / 𝐿) < (1 / 𝐿)) |
294 | | ioon0 12072 |
. . . . . . . . . . 11
⊢ ((-(1 /
𝐿) ∈
ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → ((-(1 /
𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿))) |
295 | 257, 44, 294 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ -(1 / 𝐿) < (1 / 𝐿))) |
296 | 293, 295 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ≠ ∅) |
297 | | r19.2zb 4013 |
. . . . . . . . 9
⊢ ((-(1 /
𝐿)(,)(1 / 𝐿)) ≠ ∅ ↔ (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)) |
298 | 296, 297 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)) |
299 | 298 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) → (∀𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘)) |
300 | 286, 299 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ*) ∧ ¬ -(1
/ 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘) |
301 | 300 | adantlrr 753 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) ∧ ¬ -(1 / 𝐿) ≤ 𝑥) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘) |
302 | 274, 301 | pm2.61dan 828 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘) |
303 | | elioo2 12087 |
. . . . . . . . . . 11
⊢ ((-(1 /
𝐿) ∈
ℝ* ∧ (1 / 𝐿) ∈ ℝ*) → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) |
304 | 257, 44, 303 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) ↔ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) |
305 | 304 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) |
306 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
307 | 306, 47 | absltd 14016 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) ↔ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) |
308 | 50 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ∈ ℝ) |
309 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) < (1 / 𝐿)) |
310 | 308, 309 | ltned 10052 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → (abs‘𝑥) ≠ (1 / 𝐿)) |
311 | 238 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) ≠ (1 / 𝐿)) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
312 | 311 | impancom 455 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → ((abs‘𝑥) ≠ (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
313 | 310, 312 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (abs‘𝑥) < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
314 | 313 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) < (1 / 𝐿) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
315 | 307, 314 | sylbird 249 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
316 | 315 | impr 647 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ (-(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
317 | 316 | expcom 450 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ (-(1 /
𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
318 | 317 | 3impb 1252 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ -(1 /
𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿)) → (𝜑 → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
319 | 318 | impcom 445 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ -(1 / 𝐿) < 𝑥 ∧ 𝑥 < (1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
320 | 305, 319 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
321 | 320 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (-(1 / 𝐿)(,)(1 / 𝐿)) → 𝑥 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ })) |
322 | 321 | ssrdv 3574 |
. . . . . 6
⊢ (𝜑 → (-(1 / 𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
323 | | ssrexv 3630 |
. . . . . 6
⊢ ((-(1 /
𝐿)(,)(1 / 𝐿)) ⊆ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)) |
324 | 322, 323 | syl 17 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)) |
325 | 324 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → (∃𝑘 ∈ (-(1 / 𝐿)(,)(1 / 𝐿))𝑥 < 𝑘 → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘)) |
326 | 302, 325 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 𝑥 < (1 / 𝐿))) → ∃𝑘 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑥 < 𝑘) |
327 | 3, 44, 255, 326 | eqsupd 8246 |
. 2
⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = (1 / 𝐿)) |
328 | 1, 327 | syl5eq 2656 |
1
⊢ (𝜑 → 𝑅 = (1 / 𝐿)) |