Proof of Theorem psercnlem1
Step | Hyp | Ref
| Expression |
1 | | psercn.m |
. . . 4
⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) |
2 | | psercn.s |
. . . . . . . . . . 11
⊢ 𝑆 = (◡abs “ (0[,)𝑅)) |
3 | | cnvimass 5990 |
. . . . . . . . . . . 12
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
4 | | absf 15077 |
. . . . . . . . . . . . 13
⊢
abs:ℂ⟶ℝ |
5 | 4 | fdmi 6630 |
. . . . . . . . . . . 12
⊢ dom abs =
ℂ |
6 | 3, 5 | sseqtri 3959 |
. . . . . . . . . . 11
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
7 | 2, 6 | eqsstri 3957 |
. . . . . . . . . 10
⊢ 𝑆 ⊆
ℂ |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
9 | 8 | sselda 3923 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
10 | 9 | abscld 15176 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
11 | | readdcl 10982 |
. . . . . . 7
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) + 𝑅) ∈ ℝ) |
12 | 10, 11 | sylan 579 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 𝑅) ∈ ℝ) |
13 | 12 | rehalfcld 12248 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (((abs‘𝑎) + 𝑅) / 2) ∈ ℝ) |
14 | | peano2re 11176 |
. . . . . . 7
⊢
((abs‘𝑎)
∈ ℝ → ((abs‘𝑎) + 1) ∈ ℝ) |
15 | 10, 14 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) + 1) ∈ ℝ) |
16 | 15 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 1) ∈
ℝ) |
17 | 13, 16 | ifclda 4497 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ∈ ℝ) |
18 | 1, 17 | eqeltrid 2838 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
19 | | 0re 11005 |
. . . . 5
⊢ 0 ∈
ℝ |
20 | 19 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℝ) |
21 | 9 | absge0d 15184 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ (abs‘𝑎)) |
22 | | breq2 5081 |
. . . . . 6
⊢
((((abs‘𝑎) +
𝑅) / 2) = if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) |
23 | | breq2 5081 |
. . . . . 6
⊢
(((abs‘𝑎) + 1)
= if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < ((abs‘𝑎) + 1) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) |
24 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
25 | 24, 2 | eleqtrdi 2844 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (◡abs “ (0[,)𝑅))) |
26 | | ffn 6618 |
. . . . . . . . . . . . 13
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
27 | | elpreima 6955 |
. . . . . . . . . . . . 13
⊢ (abs Fn
ℂ → (𝑎 ∈
(◡abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅)))) |
28 | 4, 26, 27 | mp2b 10 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (◡abs “ (0[,)𝑅)) ↔ (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))) |
29 | 25, 28 | sylib 217 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ ℂ ∧ (abs‘𝑎) ∈ (0[,)𝑅))) |
30 | 29 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ (0[,)𝑅)) |
31 | | iccssxr 13190 |
. . . . . . . . . . . 12
⊢
(0[,]+∞) ⊆ ℝ* |
32 | | pserf.g |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
33 | | pserf.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
34 | | pserf.r |
. . . . . . . . . . . . . 14
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
35 | 32, 33, 34 | radcnvcl 25604 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
36 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈ (0[,]+∞)) |
37 | 31, 36 | sselid 3921 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈
ℝ*) |
38 | | elico2 13171 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝑅
∈ ℝ*) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) |
39 | 19, 37, 38 | sylancr 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) |
40 | 30, 39 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅)) |
41 | 40 | simp3d 1142 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑅) |
42 | 41 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < 𝑅) |
43 | | avglt1 12239 |
. . . . . . . 8
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) |
44 | 10, 43 | sylan 579 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) |
45 | 42, 44 | mpbid 231 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)) |
46 | 10 | ltp1d 11933 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 1)) |
47 | 46 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → (abs‘𝑎) < ((abs‘𝑎) + 1)) |
48 | 22, 23, 45, 47 | ifbothda 4500 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))) |
49 | 48, 1 | breqtrrdi 5119 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) |
50 | 20, 10, 18, 21, 49 | lelttrd 11161 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 < 𝑀) |
51 | 18, 50 | elrpd 12797 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
52 | | breq1 5080 |
. . . 4
⊢
((((abs‘𝑎) +
𝑅) / 2) = if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) →
((((abs‘𝑎) + 𝑅) / 2) < 𝑅 ↔ if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅)) |
53 | | breq1 5080 |
. . . 4
⊢
(((abs‘𝑎) + 1)
= if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) →
(((abs‘𝑎) + 1) <
𝑅 ↔ if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅)) |
54 | | avglt2 12240 |
. . . . . 6
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (((abs‘𝑎) + 𝑅) / 2) < 𝑅)) |
55 | 10, 54 | sylan 579 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (((abs‘𝑎) + 𝑅) / 2) < 𝑅)) |
56 | 42, 55 | mpbid 231 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (((abs‘𝑎) + 𝑅) / 2) < 𝑅) |
57 | 15 | rexrd 11053 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) + 1) ∈
ℝ*) |
58 | 37, 57 | xrlenltd 11069 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑅 ≤ ((abs‘𝑎) + 1) ↔ ¬ ((abs‘𝑎) + 1) < 𝑅)) |
59 | | 0xr 11050 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
60 | | pnfxr 11057 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
61 | | elicc1 13151 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
62 | 59, 60, 61 | mp2an 688 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞)) |
63 | 35, 62 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅 ∧ 𝑅 ≤ +∞)) |
64 | 63 | simp2d 1141 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑅) |
65 | 64 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ 𝑅) |
66 | | ge0gtmnf 12934 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
-∞ < 𝑅) |
67 | 37, 65, 66 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → -∞ < 𝑅) |
68 | | xrre 12931 |
. . . . . . . . 9
⊢ (((𝑅 ∈ ℝ*
∧ ((abs‘𝑎) + 1)
∈ ℝ) ∧ (-∞ < 𝑅 ∧ 𝑅 ≤ ((abs‘𝑎) + 1))) → 𝑅 ∈ ℝ) |
69 | 68 | expr 456 |
. . . . . . . 8
⊢ (((𝑅 ∈ ℝ*
∧ ((abs‘𝑎) + 1)
∈ ℝ) ∧ -∞ < 𝑅) → (𝑅 ≤ ((abs‘𝑎) + 1) → 𝑅 ∈ ℝ)) |
70 | 37, 15, 67, 69 | syl21anc 834 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑅 ≤ ((abs‘𝑎) + 1) → 𝑅 ∈ ℝ)) |
71 | 58, 70 | sylbird 259 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (¬ ((abs‘𝑎) + 1) < 𝑅 → 𝑅 ∈ ℝ)) |
72 | 71 | con1d 145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (¬ 𝑅 ∈ ℝ → ((abs‘𝑎) + 1) < 𝑅)) |
73 | 72 | imp 406 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 1) < 𝑅) |
74 | 52, 53, 56, 73 | ifbothda 4500 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅) |
75 | 1, 74 | eqbrtrid 5112 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) |
76 | 51, 49, 75 | 3jca 1126 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |