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 5988 |
. . . . . . . . . . . 12
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
4 | | absf 15047 |
. . . . . . . . . . . . 13
⊢
abs:ℂ⟶ℝ |
5 | 4 | fdmi 6610 |
. . . . . . . . . . . 12
⊢ dom abs =
ℂ |
6 | 3, 5 | sseqtri 3962 |
. . . . . . . . . . 11
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
7 | 2, 6 | eqsstri 3960 |
. . . . . . . . . 10
⊢ 𝑆 ⊆
ℂ |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
9 | 8 | sselda 3926 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
10 | 9 | abscld 15146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
11 | | readdcl 10955 |
. . . . . . 7
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) + 𝑅) ∈ ℝ) |
12 | 10, 11 | sylan 580 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 𝑅) ∈ ℝ) |
13 | 12 | rehalfcld 12220 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (((abs‘𝑎) + 𝑅) / 2) ∈ ℝ) |
14 | | peano2re 11148 |
. . . . . . 7
⊢
((abs‘𝑎)
∈ ℝ → ((abs‘𝑎) + 1) ∈ ℝ) |
15 | 10, 14 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) + 1) ∈ ℝ) |
16 | 15 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 1) ∈
ℝ) |
17 | 13, 16 | ifclda 4500 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) ∈ ℝ) |
18 | 1, 17 | eqeltrid 2845 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
19 | | 0re 10978 |
. . . . 5
⊢ 0 ∈
ℝ |
20 | 19 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℝ) |
21 | 9 | absge0d 15154 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ (abs‘𝑎)) |
22 | | breq2 5083 |
. . . . . 6
⊢
((((abs‘𝑎) +
𝑅) / 2) = if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) |
23 | | breq2 5083 |
. . . . . 6
⊢
(((abs‘𝑎) + 1)
= if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) → ((abs‘𝑎) < ((abs‘𝑎) + 1) ↔ (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)))) |
24 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
25 | 24, 2 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ (◡abs “ (0[,)𝑅))) |
26 | | ffn 6598 |
. . . . . . . . . . . . 13
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
27 | | elpreima 6932 |
. . . . . . . . . . . . 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 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ (0[,)𝑅)) |
31 | | iccssxr 13161 |
. . . . . . . . . . . 12
⊢
(0[,]+∞) ⊆ ℝ* |
32 | | pserf.g |
. . . . . . . . . . . . . 14
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
33 | | pserf.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
34 | | pserf.r |
. . . . . . . . . . . . . 14
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
35 | 32, 33, 34 | radcnvcl 25574 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
36 | 35 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈ (0[,]+∞)) |
37 | 31, 36 | sselid 3924 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑅 ∈
ℝ*) |
38 | | elico2 13142 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 𝑅
∈ ℝ*) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) |
39 | 19, 37, 38 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ (0[,)𝑅) ↔ ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅))) |
40 | 30, 39 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) ∈ ℝ ∧ 0 ≤
(abs‘𝑎) ∧
(abs‘𝑎) < 𝑅)) |
41 | 40 | simp3d 1143 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑅) |
42 | 41 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < 𝑅) |
43 | | avglt1 12211 |
. . . . . . . 8
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) |
44 | 10, 43 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2))) |
45 | 42, 44 | mpbid 231 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (abs‘𝑎) < (((abs‘𝑎) + 𝑅) / 2)) |
46 | 10 | ltp1d 11905 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 1)) |
47 | 46 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → (abs‘𝑎) < ((abs‘𝑎) + 1)) |
48 | 22, 23, 45, 47 | ifbothda 4503 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))) |
49 | 48, 1 | breqtrrdi 5121 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) |
50 | 20, 10, 18, 21, 49 | lelttrd 11133 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 < 𝑀) |
51 | 18, 50 | elrpd 12768 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
52 | | breq1 5082 |
. . . 4
⊢
((((abs‘𝑎) +
𝑅) / 2) = if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) →
((((abs‘𝑎) + 𝑅) / 2) < 𝑅 ↔ if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅)) |
53 | | breq1 5082 |
. . . 4
⊢
(((abs‘𝑎) + 1)
= if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) →
(((abs‘𝑎) + 1) <
𝑅 ↔ if(𝑅 ∈ ℝ,
(((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅)) |
54 | | avglt2 12212 |
. . . . . 6
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑅
∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (((abs‘𝑎) + 𝑅) / 2) < 𝑅)) |
55 | 10, 54 | sylan 580 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → ((abs‘𝑎) < 𝑅 ↔ (((abs‘𝑎) + 𝑅) / 2) < 𝑅)) |
56 | 42, 55 | mpbid 231 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑅 ∈ ℝ) → (((abs‘𝑎) + 𝑅) / 2) < 𝑅) |
57 | 15 | rexrd 11026 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) + 1) ∈
ℝ*) |
58 | 37, 57 | xrlenltd 11042 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑅 ≤ ((abs‘𝑎) + 1) ↔ ¬ ((abs‘𝑎) + 1) < 𝑅)) |
59 | | 0xr 11023 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
60 | | pnfxr 11030 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
61 | | elicc1 13122 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ*) →
(𝑅 ∈ (0[,]+∞)
↔ (𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞))) |
62 | 59, 60, 61 | mp2an 689 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ (0[,]+∞) ↔
(𝑅 ∈
ℝ* ∧ 0 ≤ 𝑅 ∧ 𝑅 ≤ +∞)) |
63 | 35, 62 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∈ ℝ* ∧ 0 ≤
𝑅 ∧ 𝑅 ≤ +∞)) |
64 | 63 | simp2d 1142 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑅) |
65 | 64 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ 𝑅) |
66 | | ge0gtmnf 12905 |
. . . . . . . . 9
⊢ ((𝑅 ∈ ℝ*
∧ 0 ≤ 𝑅) →
-∞ < 𝑅) |
67 | 37, 65, 66 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → -∞ < 𝑅) |
68 | | xrre 12902 |
. . . . . . . . 9
⊢ (((𝑅 ∈ ℝ*
∧ ((abs‘𝑎) + 1)
∈ ℝ) ∧ (-∞ < 𝑅 ∧ 𝑅 ≤ ((abs‘𝑎) + 1))) → 𝑅 ∈ ℝ) |
69 | 68 | expr 457 |
. . . . . . . 8
⊢ (((𝑅 ∈ ℝ*
∧ ((abs‘𝑎) + 1)
∈ ℝ) ∧ -∞ < 𝑅) → (𝑅 ≤ ((abs‘𝑎) + 1) → 𝑅 ∈ ℝ)) |
70 | 37, 15, 67, 69 | syl21anc 835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑅 ≤ ((abs‘𝑎) + 1) → 𝑅 ∈ ℝ)) |
71 | 58, 70 | sylbird 259 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (¬ ((abs‘𝑎) + 1) < 𝑅 → 𝑅 ∈ ℝ)) |
72 | 71 | con1d 145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (¬ 𝑅 ∈ ℝ → ((abs‘𝑎) + 1) < 𝑅)) |
73 | 72 | imp 407 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ ¬ 𝑅 ∈ ℝ) → ((abs‘𝑎) + 1) < 𝑅) |
74 | 52, 53, 56, 73 | ifbothda 4503 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) < 𝑅) |
75 | 1, 74 | eqbrtrid 5114 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) |
76 | 51, 49, 75 | 3jca 1127 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |