| Step | Hyp | Ref
| Expression |
| 1 | | radcnvlt.a |
. . . . 5
⊢ (𝜑 → (abs‘𝑋) < 𝑅) |
| 2 | | ressxr 11305 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
| 3 | | radcnvlt.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 4 | 3 | abscld 15475 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
| 5 | 2, 4 | sselid 3981 |
. . . . . 6
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ*) |
| 6 | | iccssxr 13470 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
| 7 | | pser.g |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
| 8 | | radcnv.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
| 9 | | radcnv.r |
. . . . . . . 8
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
| 10 | 7, 8, 9 | radcnvcl 26460 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
| 11 | 6, 10 | sselid 3981 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
| 12 | | xrltnle 11328 |
. . . . . 6
⊢
(((abs‘𝑋)
∈ ℝ* ∧ 𝑅 ∈ ℝ*) →
((abs‘𝑋) < 𝑅 ↔ ¬ 𝑅 ≤ (abs‘𝑋))) |
| 13 | 5, 11, 12 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((abs‘𝑋) < 𝑅 ↔ ¬ 𝑅 ≤ (abs‘𝑋))) |
| 14 | 1, 13 | mpbid 232 |
. . . 4
⊢ (𝜑 → ¬ 𝑅 ≤ (abs‘𝑋)) |
| 15 | 9 | breq1i 5150 |
. . . . . 6
⊢ (𝑅 ≤ (abs‘𝑋) ↔ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ≤ (abs‘𝑋)) |
| 16 | | ssrab2 4080 |
. . . . . . . 8
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ |
| 17 | 16, 2 | sstri 3993 |
. . . . . . 7
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* |
| 18 | | supxrleub 13368 |
. . . . . . 7
⊢ (({𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* ∧ (abs‘𝑋) ∈ ℝ*) →
(sup({𝑟 ∈ ℝ
∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ≤ (abs‘𝑋)
↔ ∀𝑠 ∈
{𝑟 ∈ ℝ ∣
seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋))) |
| 19 | 17, 5, 18 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ≤ (abs‘𝑋)
↔ ∀𝑠 ∈
{𝑟 ∈ ℝ ∣
seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋))) |
| 20 | 15, 19 | bitrid 283 |
. . . . 5
⊢ (𝜑 → (𝑅 ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋))) |
| 21 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑟 = 𝑠 → (𝐺‘𝑟) = (𝐺‘𝑠)) |
| 22 | 21 | seqeq3d 14050 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑠))) |
| 23 | 22 | eleq1d 2826 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ )) |
| 24 | 23 | ralrab 3699 |
. . . . 5
⊢
(∀𝑠 ∈
{𝑟 ∈ ℝ ∣
seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }𝑠 ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ ℝ (seq0( + ,
(𝐺‘𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋))) |
| 25 | 20, 24 | bitrdi 287 |
. . . 4
⊢ (𝜑 → (𝑅 ≤ (abs‘𝑋) ↔ ∀𝑠 ∈ ℝ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋)))) |
| 26 | 14, 25 | mtbid 324 |
. . 3
⊢ (𝜑 → ¬ ∀𝑠 ∈ ℝ (seq0( + ,
(𝐺‘𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋))) |
| 27 | | rexanali 3102 |
. . 3
⊢
(∃𝑠 ∈
ℝ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)) ↔ ¬ ∀𝑠 ∈ ℝ (seq0( + ,
(𝐺‘𝑠)) ∈ dom ⇝ → 𝑠 ≤ (abs‘𝑋))) |
| 28 | 26, 27 | sylibr 234 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℝ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋))) |
| 29 | | ltnle 11340 |
. . . . . . 7
⊢
(((abs‘𝑋)
∈ ℝ ∧ 𝑠
∈ ℝ) → ((abs‘𝑋) < 𝑠 ↔ ¬ 𝑠 ≤ (abs‘𝑋))) |
| 30 | 4, 29 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → ((abs‘𝑋) < 𝑠 ↔ ¬ 𝑠 ≤ (abs‘𝑋))) |
| 31 | 30 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ) →
((abs‘𝑋) < 𝑠 ↔ ¬ 𝑠 ≤ (abs‘𝑋))) |
| 32 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝐴:ℕ0⟶ℂ) |
| 33 | 3 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝑋 ∈ ℂ) |
| 34 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝑠 ∈ ℝ) |
| 35 | 34 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 𝑠 ∈ ℂ) |
| 36 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑋) < 𝑠) |
| 37 | | 0red 11264 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 ∈ ℝ) |
| 38 | 33 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑋) ∈ ℝ) |
| 39 | 33 | absge0d 15483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 ≤ (abs‘𝑋)) |
| 40 | 37, 38, 34, 39, 36 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 < 𝑠) |
| 41 | 37, 34, 40 | ltled 11409 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → 0 ≤ 𝑠) |
| 42 | 34, 41 | absidd 15461 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑠) = 𝑠) |
| 43 | 36, 42 | breqtrrd 5171 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (abs‘𝑋) < (abs‘𝑠)) |
| 44 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ) |
| 45 | | radcnvlt1.h |
. . . . . . . 8
⊢ 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
| 46 | 7, 32, 33, 35, 43, 44, 45 | radcnvlem1 26456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → seq0( + , 𝐻) ∈ dom ⇝ ) |
| 47 | 7, 32, 33, 35, 43, 44 | radcnvlem2 26457 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → seq0( + , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ) |
| 48 | 46, 47 | jca 511 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ (abs‘𝑋) < 𝑠)) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0( + , (abs
∘ (𝐺‘𝑋))) ∈ dom ⇝
)) |
| 49 | 48 | expr 456 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ) →
((abs‘𝑋) < 𝑠 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0(
+ , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))) |
| 50 | 31, 49 | sylbird 260 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ) ∧ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ) → (¬ 𝑠 ≤ (abs‘𝑋) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0(
+ , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))) |
| 51 | 50 | expimpd 453 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ) → ((seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0(
+ , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))) |
| 52 | 51 | rexlimdva 3155 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℝ (seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ ∧ ¬ 𝑠 ≤ (abs‘𝑋)) → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0(
+ , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ ))) |
| 53 | 28, 52 | mpd 15 |
1
⊢ (𝜑 → (seq0( + , 𝐻) ∈ dom ⇝ ∧ seq0(
+ , (abs ∘ (𝐺‘𝑋))) ∈ dom ⇝ )) |