Step | Hyp | Ref
| Expression |
1 | | ressxr 10775 |
. . 3
⊢ ℝ
⊆ ℝ* |
2 | | radcnvle.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℂ) |
3 | 2 | abscld 14898 |
. . 3
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
4 | 1, 3 | sseldi 3885 |
. 2
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ*) |
5 | | iccssxr 12916 |
. . 3
⊢
(0[,]+∞) ⊆ ℝ* |
6 | | pser.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
7 | | radcnv.a |
. . . 4
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
8 | | radcnv.r |
. . . 4
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
9 | 6, 7, 8 | radcnvcl 25176 |
. . 3
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
10 | 5, 9 | sseldi 3885 |
. 2
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
11 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < (abs‘𝑋)) |
12 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈
ℝ*) |
13 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈ ℝ) |
14 | | 0xr 10778 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
15 | | pnfxr 10785 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
16 | | elicc1 12877 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
17 | 14, 15, 16 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞)) |
18 | 9, 17 | sylib 221 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅 ∧ 𝑅 ≤ +∞)) |
19 | 18 | simp2d 1144 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑅) |
20 | | ge0gtmnf 12660 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
-∞ < 𝑅) |
21 | 10, 19, 20 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → -∞ < 𝑅) |
22 | 21 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → -∞ < 𝑅) |
23 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈
ℝ*) |
24 | 12, 23, 11 | xrltled 12638 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ≤ (abs‘𝑋)) |
25 | | xrre 12657 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ*
∧ (abs‘𝑋) ∈
ℝ) ∧ (-∞ < 𝑅 ∧ 𝑅 ≤ (abs‘𝑋))) → 𝑅 ∈ ℝ) |
26 | 12, 13, 22, 24, 25 | syl22anc 838 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈ ℝ) |
27 | | avglt1 11966 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
28 | 26, 13, 27 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
29 | 11, 28 | mpbid 235 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
30 | 26, 13 | readdcld 10760 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 + (abs‘𝑋)) ∈ ℝ) |
31 | 30 | rehalfcld 11975 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ) |
32 | | ssrab2 3979 |
. . . . . . 7
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ |
33 | 32, 1 | sstri 3896 |
. . . . . 6
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* |
34 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝐴:ℕ0⟶ℂ) |
35 | 31 | recnd 10759 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℂ) |
36 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑋 ∈ ℂ) |
37 | | 0red 10734 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ∈ ℝ) |
38 | 19 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ 𝑅) |
39 | 37, 26, 31, 38, 29 | lelttrd 10888 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 < ((𝑅 + (abs‘𝑋)) / 2)) |
40 | 37, 31, 39 | ltled 10878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ ((𝑅 + (abs‘𝑋)) / 2)) |
41 | 31, 40 | absidd 14884 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) = ((𝑅 + (abs‘𝑋)) / 2)) |
42 | | avglt2 11967 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔
((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
43 | 26, 13, 42 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
44 | 11, 43 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋)) |
45 | 41, 44 | eqbrtrd 5062 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) < (abs‘𝑋)) |
46 | | radcnvle.a |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
47 | 46 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
48 | 6, 34, 35, 36, 45, 47 | radcnvlem3 25174 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
) |
49 | | fveq2 6686 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (𝐺‘𝑦) = (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) |
50 | 49 | seqeq3d 13480 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → seq0( + , (𝐺‘𝑦)) = seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2)))) |
51 | 50 | eleq1d 2818 |
. . . . . . . 8
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
52 | | fveq2 6686 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
53 | 52 | seqeq3d 13480 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑦 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑦))) |
54 | 53 | eleq1d 2818 |
. . . . . . . . 9
⊢ (𝑟 = 𝑦 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ )) |
55 | 54 | cbvrabv 3394 |
. . . . . . . 8
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑦 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑦)) ∈ dom ⇝
} |
56 | 51, 55 | elrab2 3596 |
. . . . . . 7
⊢ (((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ (((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ ∧ seq0( + ,
(𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
57 | 31, 48, 56 | sylanbrc 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
58 | | supxrub 12812 |
. . . . . 6
⊢ (({𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* ∧ ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
59 | 33, 57, 58 | sylancr 590 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
60 | 59, 8 | breqtrrdi 5082 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ 𝑅) |
61 | 31, 26, 60 | lensymd 10881 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ¬ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
62 | 29, 61 | pm2.65da 817 |
. 2
⊢ (𝜑 → ¬ 𝑅 < (abs‘𝑋)) |
63 | 4, 10, 62 | xrnltled 10799 |
1
⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅) |