Step |
Hyp |
Ref |
Expression |
1 |
|
pser.g |
⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ) |
2 |
|
radcnv.a |
⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ ) |
3 |
|
radcnv.r |
⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) |
4 |
|
radcnvle.x |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
5 |
|
radcnvle.a |
⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ ) |
6 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
7 |
4
|
abscld |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ ) |
8 |
6 7
|
sselid |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ* ) |
9 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
10 |
1 2 3
|
radcnvcl |
⊢ ( 𝜑 → 𝑅 ∈ ( 0 [,] +∞ ) ) |
11 |
9 10
|
sselid |
⊢ ( 𝜑 → 𝑅 ∈ ℝ* ) |
12 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 < ( abs ‘ 𝑋 ) ) |
13 |
11
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ∈ ℝ* ) |
14 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ ) |
15 |
|
0xr |
⊢ 0 ∈ ℝ* |
16 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
17 |
|
elicc1 |
⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) ) |
18 |
15 16 17
|
mp2an |
⊢ ( 𝑅 ∈ ( 0 [,] +∞ ) ↔ ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) |
19 |
10 18
|
sylib |
⊢ ( 𝜑 → ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞ ) ) |
20 |
19
|
simp2d |
⊢ ( 𝜑 → 0 ≤ 𝑅 ) |
21 |
|
ge0gtmnf |
⊢ ( ( 𝑅 ∈ ℝ* ∧ 0 ≤ 𝑅 ) → -∞ < 𝑅 ) |
22 |
11 20 21
|
syl2anc |
⊢ ( 𝜑 → -∞ < 𝑅 ) |
23 |
22
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → -∞ < 𝑅 ) |
24 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ* ) |
25 |
13 24 12
|
xrltled |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ≤ ( abs ‘ 𝑋 ) ) |
26 |
|
xrre |
⊢ ( ( ( 𝑅 ∈ ℝ* ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) ∧ ( -∞ < 𝑅 ∧ 𝑅 ≤ ( abs ‘ 𝑋 ) ) ) → 𝑅 ∈ ℝ ) |
27 |
13 14 23 25 26
|
syl22anc |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 ∈ ℝ ) |
28 |
|
avglt1 |
⊢ ( ( 𝑅 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) |
29 |
27 14 28
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) |
30 |
12 29
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) |
31 |
27 14
|
readdcld |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 + ( abs ‘ 𝑋 ) ) ∈ ℝ ) |
32 |
31
|
rehalfcld |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℝ ) |
33 |
|
ssrab2 |
⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ |
34 |
33 6
|
sstri |
⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* |
35 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝐴 : ℕ0 ⟶ ℂ ) |
36 |
32
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℂ ) |
37 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 𝑋 ∈ ℂ ) |
38 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 ∈ ℝ ) |
39 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 ≤ 𝑅 ) |
40 |
38 27 32 39 30
|
lelttrd |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) |
41 |
38 32 40
|
ltled |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → 0 ≤ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) |
42 |
32 41
|
absidd |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) |
43 |
|
avglt2 |
⊢ ( ( 𝑅 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) ) |
44 |
27 14 43
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( 𝑅 < ( abs ‘ 𝑋 ) ↔ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) ) |
45 |
12 44
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) < ( abs ‘ 𝑋 ) ) |
46 |
42 45
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( abs ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) < ( abs ‘ 𝑋 ) ) |
47 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → seq 0 ( + , ( 𝐺 ‘ 𝑋 ) ) ∈ dom ⇝ ) |
48 |
1 35 36 37 46 47
|
radcnvlem3 |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) |
49 |
|
fveq2 |
⊢ ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) |
50 |
49
|
seqeq3d |
⊢ ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) = seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ) |
51 |
50
|
eleq1d |
⊢ ( 𝑦 = ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) → ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) ) |
52 |
|
fveq2 |
⊢ ( 𝑟 = 𝑦 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑦 ) ) |
53 |
52
|
seqeq3d |
⊢ ( 𝑟 = 𝑦 → seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ) |
54 |
53
|
eleq1d |
⊢ ( 𝑟 = 𝑦 → ( seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ ) ) |
55 |
54
|
cbvrabv |
⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ∈ dom ⇝ } |
56 |
51 55
|
elrab2 |
⊢ ( ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ↔ ( ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ ℝ ∧ seq 0 ( + , ( 𝐺 ‘ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) ) ∈ dom ⇝ ) ) |
57 |
32 48 56
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) |
58 |
|
supxrub |
⊢ ( ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* ∧ ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) |
59 |
34 57 58
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) |
60 |
59 3
|
breqtrrdi |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ≤ 𝑅 ) |
61 |
32 27 60
|
lensymd |
⊢ ( ( 𝜑 ∧ 𝑅 < ( abs ‘ 𝑋 ) ) → ¬ 𝑅 < ( ( 𝑅 + ( abs ‘ 𝑋 ) ) / 2 ) ) |
62 |
30 61
|
pm2.65da |
⊢ ( 𝜑 → ¬ 𝑅 < ( abs ‘ 𝑋 ) ) |
63 |
8 11 62
|
xrnltled |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 𝑅 ) |