Step | Hyp | Ref
| Expression |
1 | | abelth.1 |
. . . . . . 7
β’ (π β π΄:β0βΆβ) |
2 | | abelth.2 |
. . . . . . 7
β’ (π β seq0( + , π΄) β dom β
) |
3 | | abelth.3 |
. . . . . . 7
β’ (π β π β β) |
4 | | abelth.4 |
. . . . . . 7
β’ (π β 0 β€ π) |
5 | | abelth.5 |
. . . . . . 7
β’ π = {π§ β β β£ (absβ(1 β
π§)) β€ (π Β· (1 β (absβπ§)))} |
6 | 1, 2, 3, 4, 5 | abelthlem2 25814 |
. . . . . 6
β’ (π β (1 β π β§ (π β {1}) β (0(ballβ(abs
β β ))1))) |
7 | 6 | simprd 497 |
. . . . 5
β’ (π β (π β {1}) β (0(ballβ(abs
β β ))1)) |
8 | | ssundif 4449 |
. . . . 5
β’ (π β ({1} βͺ
(0(ballβ(abs β β ))1)) β (π β {1}) β (0(ballβ(abs
β β ))1)) |
9 | 7, 8 | sylibr 233 |
. . . 4
β’ (π β π β ({1} βͺ (0(ballβ(abs
β β ))1))) |
10 | 9 | sselda 3948 |
. . 3
β’ ((π β§ π β π) β π β ({1} βͺ (0(ballβ(abs
β β ))1))) |
11 | | elun 4112 |
. . 3
β’ (π β ({1} βͺ
(0(ballβ(abs β β ))1)) β (π β {1} β¨ π β (0(ballβ(abs β β
))1))) |
12 | 10, 11 | sylib 217 |
. 2
β’ ((π β§ π β π) β (π β {1} β¨ π β (0(ballβ(abs β β
))1))) |
13 | 1 | feqmptd 6914 |
. . . . . . 7
β’ (π β π΄ = (π β β0 β¦ (π΄βπ))) |
14 | 1 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π΄βπ) β β) |
15 | 14 | mulid1d 11180 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π΄βπ) Β· 1) = (π΄βπ)) |
16 | 15 | mpteq2dva 5209 |
. . . . . . 7
β’ (π β (π β β0 β¦ ((π΄βπ) Β· 1)) = (π β β0 β¦ (π΄βπ))) |
17 | 13, 16 | eqtr4d 2776 |
. . . . . 6
β’ (π β π΄ = (π β β0 β¦ ((π΄βπ) Β· 1))) |
18 | | elsni 4607 |
. . . . . . . . . . 11
β’ (π β {1} β π = 1) |
19 | 18 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π β {1} β (πβπ) = (1βπ)) |
20 | | nn0z 12532 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β€) |
21 | | 1exp 14006 |
. . . . . . . . . . 11
β’ (π β β€ β
(1βπ) =
1) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β β0
β (1βπ) =
1) |
23 | 19, 22 | sylan9eq 2793 |
. . . . . . . . 9
β’ ((π β {1} β§ π β β0)
β (πβπ) = 1) |
24 | 23 | oveq2d 7377 |
. . . . . . . 8
β’ ((π β {1} β§ π β β0)
β ((π΄βπ) Β· (πβπ)) = ((π΄βπ) Β· 1)) |
25 | 24 | mpteq2dva 5209 |
. . . . . . 7
β’ (π β {1} β (π β β0
β¦ ((π΄βπ) Β· (πβπ))) = (π β β0 β¦ ((π΄βπ) Β· 1))) |
26 | 25 | eqcomd 2739 |
. . . . . 6
β’ (π β {1} β (π β β0
β¦ ((π΄βπ) Β· 1)) = (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) |
27 | 17, 26 | sylan9eq 2793 |
. . . . 5
β’ ((π β§ π β {1}) β π΄ = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
28 | 27 | seqeq3d 13923 |
. . . 4
β’ ((π β§ π β {1}) β seq0( + , π΄) = seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ))))) |
29 | 2 | adantr 482 |
. . . 4
β’ ((π β§ π β {1}) β seq0( + , π΄) β dom β
) |
30 | 28, 29 | eqeltrrd 2835 |
. . 3
β’ ((π β§ π β {1}) β seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |
31 | | cnxmet 24159 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
32 | | 0cn 11155 |
. . . . . . . 8
β’ 0 β
β |
33 | | 1xr 11222 |
. . . . . . . 8
β’ 1 β
β* |
34 | | blssm 23794 |
. . . . . . . 8
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ 1 β β*) β (0(ballβ(abs β β
))1) β β) |
35 | 31, 32, 33, 34 | mp3an 1462 |
. . . . . . 7
β’
(0(ballβ(abs β β ))1) β β |
36 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β π β
(0(ballβ(abs β β ))1)) |
37 | 35, 36 | sselid 3946 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β π β
β) |
38 | | oveq1 7368 |
. . . . . . . . 9
β’ (π§ = π β (π§βπ) = (πβπ)) |
39 | 38 | oveq2d 7377 |
. . . . . . . 8
β’ (π§ = π β ((π΄βπ) Β· (π§βπ)) = ((π΄βπ) Β· (πβπ))) |
40 | 39 | mpteq2dv 5211 |
. . . . . . 7
β’ (π§ = π β (π β β0 β¦ ((π΄βπ) Β· (π§βπ))) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
41 | | eqid 2733 |
. . . . . . 7
β’ (π§ β β β¦ (π β β0
β¦ ((π΄βπ) Β· (π§βπ)))) = (π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ)))) |
42 | | nn0ex 12427 |
. . . . . . . 8
β’
β0 β V |
43 | 42 | mptex 7177 |
. . . . . . 7
β’ (π β β0
β¦ ((π΄βπ) Β· (πβπ))) β V |
44 | 40, 41, 43 | fvmpt 6952 |
. . . . . 6
β’ (π β β β ((π§ β β β¦ (π β β0
β¦ ((π΄βπ) Β· (π§βπ))))βπ) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
45 | 37, 44 | syl 17 |
. . . . 5
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β ((π§ β
β β¦ (π β
β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
46 | 45 | seqeq3d 13923 |
. . . 4
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , ((π§
β β β¦ (π
β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) = seq0( + , (π β β0 β¦ ((π΄βπ) Β· (πβπ))))) |
47 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β π΄:β0βΆβ) |
48 | | eqid 2733 |
. . . . 5
β’
sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) = sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) |
49 | 37 | abscld 15330 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
β β) |
50 | 49 | rexrd 11213 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
β β*) |
51 | | 1re 11163 |
. . . . . . 7
β’ 1 β
β |
52 | | rexr 11209 |
. . . . . . 7
β’ (1 β
β β 1 β β*) |
53 | 51, 52 | mp1i 13 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β 1 β β*) |
54 | | iccssxr 13356 |
. . . . . . 7
β’
(0[,]+β) β β* |
55 | 41, 47, 48 | radcnvcl 25799 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) β (0[,]+β)) |
56 | 54, 55 | sselid 3946 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) β β*) |
57 | | eqid 2733 |
. . . . . . . . . 10
β’ (abs
β β ) = (abs β β ) |
58 | 57 | cnmetdval 24157 |
. . . . . . . . 9
β’ ((π β β β§ 0 β
β) β (π(abs
β β )0) = (absβ(π β 0))) |
59 | 37, 32, 58 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π(abs β
β )0) = (absβ(π
β 0))) |
60 | 37 | subid1d 11509 |
. . . . . . . . 9
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π β 0)
= π) |
61 | 60 | fveq2d 6850 |
. . . . . . . 8
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβ(π
β 0)) = (absβπ)) |
62 | 59, 61 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π(abs β
β )0) = (absβπ)) |
63 | | elbl3 23768 |
. . . . . . . . . 10
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (0 β β β§ π β β)) β (π β (0(ballβ(abs β β
))1) β (π(abs β
β )0) < 1)) |
64 | 31, 33, 63 | mpanl12 701 |
. . . . . . . . 9
β’ ((0
β β β§ π
β β) β (π
β (0(ballβ(abs β β ))1) β (π(abs β β )0) <
1)) |
65 | 32, 37, 64 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π β
(0(ballβ(abs β β ))1) β (π(abs β β )0) <
1)) |
66 | 36, 65 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π(abs β
β )0) < 1) |
67 | 62, 66 | eqbrtrrd 5133 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
< 1) |
68 | 1, 2 | abelthlem1 25813 |
. . . . . . 7
β’ (π β 1 β€ sup({π β β β£ seq0( +
, ((π§ β β
β¦ (π β
β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< )) |
69 | 68 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β 1 β€ sup({π
β β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< )) |
70 | 50, 53, 56, 67, 69 | xrltletrd 13089 |
. . . . 5
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
< sup({π β β
β£ seq0( + , ((π§
β β β¦ (π
β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< )) |
71 | 41, 47, 48, 37, 70 | radcnvlt2 25801 |
. . . 4
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , ((π§
β β β¦ (π
β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β ) |
72 | 46, 71 | eqeltrrd 2835 |
. . 3
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , (π
β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |
73 | 30, 72 | jaodan 957 |
. 2
β’ ((π β§ (π β {1} β¨ π β (0(ballβ(abs β β
))1))) β seq0( + , (π
β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |
74 | 12, 73 | syldan 592 |
1
β’ ((π β§ π β π) β seq0( + , (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |