| Step | Hyp | Ref
| Expression |
| 1 | | ressxr 11305 |
. . 3
⊢ ℝ
⊆ ℝ* |
| 2 | | radcnvle.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 3 | 2 | abscld 15475 |
. . 3
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
| 4 | 1, 3 | sselid 3981 |
. 2
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ*) |
| 5 | | iccssxr 13470 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
| 6 | | pser.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
| 7 | | radcnv.a |
. . . 4
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
| 8 | | radcnv.r |
. . . 4
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
| 9 | 6, 7, 8 | radcnvcl 26460 |
. . 3
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
| 10 | 5, 9 | sselid 3981 |
. 2
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
| 11 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < (abs‘𝑋)) |
| 12 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈
ℝ*) |
| 13 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈ ℝ) |
| 14 | | 0xr 11308 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
| 15 | | pnfxr 11315 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
| 16 | | elicc1 13431 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
| 17 | 14, 15, 16 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞)) |
| 18 | 9, 17 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅 ∧ 𝑅 ≤ +∞)) |
| 19 | 18 | simp2d 1144 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑅) |
| 20 | | ge0gtmnf 13214 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
-∞ < 𝑅) |
| 21 | 10, 19, 20 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → -∞ < 𝑅) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → -∞ < 𝑅) |
| 23 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈
ℝ*) |
| 24 | 12, 23, 11 | xrltled 13192 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ≤ (abs‘𝑋)) |
| 25 | | xrre 13211 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ*
∧ (abs‘𝑋) ∈
ℝ) ∧ (-∞ < 𝑅 ∧ 𝑅 ≤ (abs‘𝑋))) → 𝑅 ∈ ℝ) |
| 26 | 12, 13, 22, 24, 25 | syl22anc 839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈ ℝ) |
| 27 | | avglt1 12504 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
| 28 | 26, 13, 27 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
| 29 | 11, 28 | mpbid 232 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
| 30 | 26, 13 | readdcld 11290 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 + (abs‘𝑋)) ∈ ℝ) |
| 31 | 30 | rehalfcld 12513 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ) |
| 32 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ |
| 33 | 32, 1 | sstri 3993 |
. . . . . 6
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* |
| 34 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝐴:ℕ0⟶ℂ) |
| 35 | 31 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℂ) |
| 36 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑋 ∈ ℂ) |
| 37 | | 0red 11264 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ∈ ℝ) |
| 38 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ 𝑅) |
| 39 | 37, 26, 31, 38, 29 | lelttrd 11419 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 < ((𝑅 + (abs‘𝑋)) / 2)) |
| 40 | 37, 31, 39 | ltled 11409 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ ((𝑅 + (abs‘𝑋)) / 2)) |
| 41 | 31, 40 | absidd 15461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) = ((𝑅 + (abs‘𝑋)) / 2)) |
| 42 | | avglt2 12505 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔
((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
| 43 | 26, 13, 42 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
| 44 | 11, 43 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋)) |
| 45 | 41, 44 | eqbrtrd 5165 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) < (abs‘𝑋)) |
| 46 | | radcnvle.a |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
| 47 | 46 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
| 48 | 6, 34, 35, 36, 45, 47 | radcnvlem3 26458 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
) |
| 49 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (𝐺‘𝑦) = (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) |
| 50 | 49 | seqeq3d 14050 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → seq0( + , (𝐺‘𝑦)) = seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2)))) |
| 51 | 50 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
| 52 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
| 53 | 52 | seqeq3d 14050 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑦 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑦))) |
| 54 | 53 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑟 = 𝑦 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ )) |
| 55 | 54 | cbvrabv 3447 |
. . . . . . . 8
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑦 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑦)) ∈ dom ⇝
} |
| 56 | 51, 55 | elrab2 3695 |
. . . . . . 7
⊢ (((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ (((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ ∧ seq0( + ,
(𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
| 57 | 31, 48, 56 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
| 58 | | supxrub 13366 |
. . . . . 6
⊢ (({𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* ∧ ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 59 | 33, 57, 58 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 60 | 59, 8 | breqtrrdi 5185 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ 𝑅) |
| 61 | 31, 26, 60 | lensymd 11412 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ¬ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
| 62 | 29, 61 | pm2.65da 817 |
. 2
⊢ (𝜑 → ¬ 𝑅 < (abs‘𝑋)) |
| 63 | 4, 10, 62 | xrnltled 11329 |
1
⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅) |