Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < (abs‘𝑋)) |
2 | | iccssxr 12544 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
3 | | pser.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
4 | | radcnv.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
5 | | radcnv.r |
. . . . . . . . 9
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
6 | 3, 4, 5 | radcnvcl 24570 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
7 | 2, 6 | sseldi 3825 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
8 | 7 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈
ℝ*) |
9 | | radcnvle.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
10 | 9 | abscld 14552 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
11 | 10 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈ ℝ) |
12 | | 0xr 10403 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
13 | | pnfxr 10410 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
14 | | elicc1 12507 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
15 | 12, 13, 14 | mp2an 683 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞)) |
16 | 6, 15 | sylib 210 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅 ∧ 𝑅 ≤ +∞)) |
17 | 16 | simp2d 1177 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑅) |
18 | | ge0gtmnf 12291 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
-∞ < 𝑅) |
19 | 7, 17, 18 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → -∞ < 𝑅) |
20 | 19 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → -∞ < 𝑅) |
21 | | ressxr 10400 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
22 | 21, 10 | sseldi 3825 |
. . . . . . . 8
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ*) |
23 | 22 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈
ℝ*) |
24 | 8, 23, 1 | xrltled 12269 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ≤ (abs‘𝑋)) |
25 | | xrre 12288 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ*
∧ (abs‘𝑋) ∈
ℝ) ∧ (-∞ < 𝑅 ∧ 𝑅 ≤ (abs‘𝑋))) → 𝑅 ∈ ℝ) |
26 | 8, 11, 20, 24, 25 | syl22anc 872 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈ ℝ) |
27 | | avglt1 11596 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
28 | 26, 11, 27 | syl2anc 579 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
29 | 1, 28 | mpbid 224 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
30 | | ssrab2 3912 |
. . . . . . 7
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ |
31 | 30, 21 | sstri 3836 |
. . . . . 6
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* |
32 | 26, 11 | readdcld 10386 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 + (abs‘𝑋)) ∈ ℝ) |
33 | 32 | rehalfcld 11605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ) |
34 | 4 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝐴:ℕ0⟶ℂ) |
35 | 33 | recnd 10385 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℂ) |
36 | 9 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑋 ∈ ℂ) |
37 | | 0red 10360 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ∈ ℝ) |
38 | 17 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ 𝑅) |
39 | 37, 26, 33, 38, 29 | lelttrd 10514 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 < ((𝑅 + (abs‘𝑋)) / 2)) |
40 | 37, 33, 39 | ltled 10504 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ ((𝑅 + (abs‘𝑋)) / 2)) |
41 | 33, 40 | absidd 14538 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) = ((𝑅 + (abs‘𝑋)) / 2)) |
42 | | avglt2 11597 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔
((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
43 | 26, 11, 42 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
44 | 1, 43 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋)) |
45 | 41, 44 | eqbrtrd 4895 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) < (abs‘𝑋)) |
46 | | radcnvle.a |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
47 | 46 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
48 | 3, 34, 35, 36, 45, 47 | radcnvlem3 24568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
) |
49 | | fveq2 6433 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (𝐺‘𝑦) = (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) |
50 | 49 | seqeq3d 13103 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → seq0( + , (𝐺‘𝑦)) = seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2)))) |
51 | 50 | eleq1d 2891 |
. . . . . . . 8
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
52 | | fveq2 6433 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
53 | 52 | seqeq3d 13103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑦 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑦))) |
54 | 53 | eleq1d 2891 |
. . . . . . . . 9
⊢ (𝑟 = 𝑦 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ )) |
55 | 54 | cbvrabv 3412 |
. . . . . . . 8
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑦 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑦)) ∈ dom ⇝
} |
56 | 51, 55 | elrab2 3589 |
. . . . . . 7
⊢ (((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ (((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ ∧ seq0( + ,
(𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
57 | 33, 48, 56 | sylanbrc 578 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
58 | | supxrub 12442 |
. . . . . 6
⊢ (({𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* ∧ ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
59 | 31, 57, 58 | sylancr 581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
60 | 59, 5 | syl6breqr 4915 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ 𝑅) |
61 | 33, 26 | lenltd 10502 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (((𝑅 + (abs‘𝑋)) / 2) ≤ 𝑅 ↔ ¬ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
62 | 60, 61 | mpbid 224 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ¬ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
63 | 29, 62 | pm2.65da 851 |
. 2
⊢ (𝜑 → ¬ 𝑅 < (abs‘𝑋)) |
64 | | xrlenlt 10422 |
. . 3
⊢
(((abs‘𝑋)
∈ ℝ* ∧ 𝑅 ∈ ℝ*) →
((abs‘𝑋) ≤ 𝑅 ↔ ¬ 𝑅 < (abs‘𝑋))) |
65 | 22, 7, 64 | syl2anc 579 |
. 2
⊢ (𝜑 → ((abs‘𝑋) ≤ 𝑅 ↔ ¬ 𝑅 < (abs‘𝑋))) |
66 | 63, 65 | mpbird 249 |
1
⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅) |