Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < (abs‘𝑋)) |
2 | | iccssxr 12256 |
. . . . . . . 8
⊢
(0[,]+∞) ⊆ ℝ* |
3 | | pser.g |
. . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
4 | | radcnv.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
5 | | radcnv.r |
. . . . . . . . 9
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
6 | 3, 4, 5 | radcnvcl 24171 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
7 | 2, 6 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
8 | 7 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈
ℝ*) |
9 | | radcnvle.x |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) |
10 | 9 | abscld 14175 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
11 | 10 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈ ℝ) |
12 | | 0xr 10086 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
13 | | pnfxr 10092 |
. . . . . . . . . . 11
⊢ +∞
∈ ℝ* |
14 | | elicc1 12219 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
15 | 12, 13, 14 | mp2an 708 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞)) |
16 | 6, 15 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅 ∧ 𝑅 ≤ +∞)) |
17 | 16 | simp2d 1074 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑅) |
18 | | ge0gtmnf 12003 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
-∞ < 𝑅) |
19 | 7, 17, 18 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → -∞ < 𝑅) |
20 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → -∞ < 𝑅) |
21 | | ressxr 10083 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℝ* |
22 | 21, 10 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ*) |
23 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘𝑋) ∈
ℝ*) |
24 | | xrltle 11982 |
. . . . . . . 8
⊢ ((𝑅 ∈ ℝ*
∧ (abs‘𝑋) ∈
ℝ*) → (𝑅 < (abs‘𝑋) → 𝑅 ≤ (abs‘𝑋))) |
25 | 8, 23, 24 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) → 𝑅 ≤ (abs‘𝑋))) |
26 | 1, 25 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ≤ (abs‘𝑋)) |
27 | | xrre 12000 |
. . . . . 6
⊢ (((𝑅 ∈ ℝ*
∧ (abs‘𝑋) ∈
ℝ) ∧ (-∞ < 𝑅 ∧ 𝑅 ≤ (abs‘𝑋))) → 𝑅 ∈ ℝ) |
28 | 8, 11, 20, 26, 27 | syl22anc 1327 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 ∈ ℝ) |
29 | | avglt1 11270 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
30 | 28, 11, 29 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
31 | 1, 30 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
32 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ |
33 | 32, 21 | sstri 3612 |
. . . . . 6
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* |
34 | 28, 11 | readdcld 10069 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 + (abs‘𝑋)) ∈ ℝ) |
35 | 34 | rehalfcld 11279 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ) |
36 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝐴:ℕ0⟶ℂ) |
37 | 35 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ ℂ) |
38 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 𝑋 ∈ ℂ) |
39 | | 0red 10041 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ∈ ℝ) |
40 | 17 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ 𝑅) |
41 | 39, 28, 35, 40, 31 | lelttrd 10195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 < ((𝑅 + (abs‘𝑋)) / 2)) |
42 | 39, 35, 41 | ltled 10185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → 0 ≤ ((𝑅 + (abs‘𝑋)) / 2)) |
43 | 35, 42 | absidd 14161 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) = ((𝑅 + (abs‘𝑋)) / 2)) |
44 | | avglt2 11271 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧
(abs‘𝑋) ∈
ℝ) → (𝑅 <
(abs‘𝑋) ↔
((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
45 | 28, 11, 44 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (𝑅 < (abs‘𝑋) ↔ ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋))) |
46 | 1, 45 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) < (abs‘𝑋)) |
47 | 43, 46 | eqbrtrd 4675 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (abs‘((𝑅 + (abs‘𝑋)) / 2)) < (abs‘𝑋)) |
48 | | radcnvle.a |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
49 | 48 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘𝑋)) ∈ dom ⇝ ) |
50 | 3, 36, 37, 38, 47, 49 | radcnvlem3 24169 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
) |
51 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (𝐺‘𝑦) = (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) |
52 | 51 | seqeq3d 12809 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → seq0( + , (𝐺‘𝑦)) = seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2)))) |
53 | 52 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑦 = ((𝑅 + (abs‘𝑋)) / 2) → (seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
54 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑦 → (𝐺‘𝑟) = (𝐺‘𝑦)) |
55 | 54 | seqeq3d 12809 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑦 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑦))) |
56 | 55 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑟 = 𝑦 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑦)) ∈ dom ⇝ )) |
57 | 56 | cbvrabv 3199 |
. . . . . . . 8
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑦 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑦)) ∈ dom ⇝
} |
58 | 53, 57 | elrab2 3366 |
. . . . . . 7
⊢ (((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ } ↔ (((𝑅 + (abs‘𝑋)) / 2) ∈ ℝ ∧ seq0( + ,
(𝐺‘((𝑅 + (abs‘𝑋)) / 2))) ∈ dom ⇝
)) |
59 | 35, 50, 58 | sylanbrc 698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) |
60 | | supxrub 12154 |
. . . . . 6
⊢ (({𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } ⊆
ℝ* ∧ ((𝑅 + (abs‘𝑋)) / 2) ∈ {𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
61 | 33, 59, 60 | sylancr 695 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
62 | 61, 5 | syl6breqr 4695 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ((𝑅 + (abs‘𝑋)) / 2) ≤ 𝑅) |
63 | 35, 28 | lenltd 10183 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → (((𝑅 + (abs‘𝑋)) / 2) ≤ 𝑅 ↔ ¬ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2))) |
64 | 62, 63 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝑅 < (abs‘𝑋)) → ¬ 𝑅 < ((𝑅 + (abs‘𝑋)) / 2)) |
65 | 31, 64 | pm2.65da 600 |
. 2
⊢ (𝜑 → ¬ 𝑅 < (abs‘𝑋)) |
66 | | xrlenlt 10103 |
. . 3
⊢
(((abs‘𝑋)
∈ ℝ* ∧ 𝑅 ∈ ℝ*) →
((abs‘𝑋) ≤ 𝑅 ↔ ¬ 𝑅 < (abs‘𝑋))) |
67 | 22, 7, 66 | syl2anc 693 |
. 2
⊢ (𝜑 → ((abs‘𝑋) ≤ 𝑅 ↔ ¬ 𝑅 < (abs‘𝑋))) |
68 | 65, 67 | mpbird 247 |
1
⊢ (𝜑 → (abs‘𝑋) ≤ 𝑅) |