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 26177 |
. . . . . 6
β’ (π β (1 β π β§ (π β {1}) β (0(ballβ(abs
β β ))1))) |
7 | 6 | simprd 495 |
. . . . 5
β’ (π β (π β {1}) β (0(ballβ(abs
β β ))1)) |
8 | | ssundif 4488 |
. . . . 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 3983 |
. . 3
β’ ((π β§ π β π) β π β ({1} βͺ (0(ballβ(abs
β β ))1))) |
11 | | elun 4149 |
. . 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 6961 |
. . . . . . 7
β’ (π β π΄ = (π β β0 β¦ (π΄βπ))) |
14 | 1 | ffvelcdmda 7087 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (π΄βπ) β β) |
15 | 14 | mulridd 11236 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π΄βπ) Β· 1) = (π΄βπ)) |
16 | 15 | mpteq2dva 5249 |
. . . . . . 7
β’ (π β (π β β0 β¦ ((π΄βπ) Β· 1)) = (π β β0 β¦ (π΄βπ))) |
17 | 13, 16 | eqtr4d 2774 |
. . . . . 6
β’ (π β π΄ = (π β β0 β¦ ((π΄βπ) Β· 1))) |
18 | | elsni 4646 |
. . . . . . . . . . 11
β’ (π β {1} β π = 1) |
19 | 18 | oveq1d 7427 |
. . . . . . . . . 10
β’ (π β {1} β (πβπ) = (1βπ)) |
20 | | nn0z 12588 |
. . . . . . . . . . 11
β’ (π β β0
β π β
β€) |
21 | | 1exp 14062 |
. . . . . . . . . . 11
β’ (π β β€ β
(1βπ) =
1) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β β0
β (1βπ) =
1) |
23 | 19, 22 | sylan9eq 2791 |
. . . . . . . . 9
β’ ((π β {1} β§ π β β0)
β (πβπ) = 1) |
24 | 23 | oveq2d 7428 |
. . . . . . . 8
β’ ((π β {1} β§ π β β0)
β ((π΄βπ) Β· (πβπ)) = ((π΄βπ) Β· 1)) |
25 | 24 | mpteq2dva 5249 |
. . . . . . 7
β’ (π β {1} β (π β β0
β¦ ((π΄βπ) Β· (πβπ))) = (π β β0 β¦ ((π΄βπ) Β· 1))) |
26 | 25 | eqcomd 2737 |
. . . . . 6
β’ (π β {1} β (π β β0
β¦ ((π΄βπ) Β· 1)) = (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) |
27 | 17, 26 | sylan9eq 2791 |
. . . . 5
β’ ((π β§ π β {1}) β π΄ = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
28 | 27 | seqeq3d 13979 |
. . . 4
β’ ((π β§ π β {1}) β seq0( + , π΄) = seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ))))) |
29 | 2 | adantr 480 |
. . . 4
β’ ((π β§ π β {1}) β seq0( + , π΄) β dom β
) |
30 | 28, 29 | eqeltrrd 2833 |
. . 3
β’ ((π β§ π β {1}) β seq0( + , (π β β0
β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |
31 | | cnxmet 24510 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
32 | | 0cn 11211 |
. . . . . . . 8
β’ 0 β
β |
33 | | 1xr 11278 |
. . . . . . . 8
β’ 1 β
β* |
34 | | blssm 24145 |
. . . . . . . 8
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ 1 β β*) β (0(ballβ(abs β β
))1) β β) |
35 | 31, 32, 33, 34 | mp3an 1460 |
. . . . . . 7
β’
(0(ballβ(abs β β ))1) β β |
36 | | simpr 484 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β π β
(0(ballβ(abs β β ))1)) |
37 | 35, 36 | sselid 3981 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β π β
β) |
38 | | oveq1 7419 |
. . . . . . . . 9
β’ (π§ = π β (π§βπ) = (πβπ)) |
39 | 38 | oveq2d 7428 |
. . . . . . . 8
β’ (π§ = π β ((π΄βπ) Β· (π§βπ)) = ((π΄βπ) Β· (πβπ))) |
40 | 39 | mpteq2dv 5251 |
. . . . . . 7
β’ (π§ = π β (π β β0 β¦ ((π΄βπ) Β· (π§βπ))) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
41 | | eqid 2731 |
. . . . . . 7
β’ (π§ β β β¦ (π β β0
β¦ ((π΄βπ) Β· (π§βπ)))) = (π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ)))) |
42 | | nn0ex 12483 |
. . . . . . . 8
β’
β0 β V |
43 | 42 | mptex 7228 |
. . . . . . 7
β’ (π β β0
β¦ ((π΄βπ) Β· (πβπ))) β V |
44 | 40, 41, 43 | fvmpt 6999 |
. . . . . 6
β’ (π β β β ((π§ β β β¦ (π β β0
β¦ ((π΄βπ) Β· (π§βπ))))βπ) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
45 | 37, 44 | syl 17 |
. . . . 5
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β ((π§ β
β β¦ (π β
β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ) = (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) |
46 | 45 | seqeq3d 13979 |
. . . 4
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , ((π§
β β β¦ (π
β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) = seq0( + , (π β β0 β¦ ((π΄βπ) Β· (πβπ))))) |
47 | 1 | adantr 480 |
. . . . 5
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β π΄:β0βΆβ) |
48 | | eqid 2731 |
. . . . 5
β’
sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) = sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) |
49 | 37 | abscld 15388 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
β β) |
50 | 49 | rexrd 11269 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
β β*) |
51 | | 1re 11219 |
. . . . . . 7
β’ 1 β
β |
52 | | rexr 11265 |
. . . . . . 7
β’ (1 β
β β 1 β β*) |
53 | 51, 52 | mp1i 13 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β 1 β β*) |
54 | | iccssxr 13412 |
. . . . . . 7
β’
(0[,]+β) β β* |
55 | 41, 47, 48 | radcnvcl 26162 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) β (0[,]+β)) |
56 | 54, 55 | sselid 3981 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β sup({π β
β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< ) β β*) |
57 | | eqid 2731 |
. . . . . . . . . 10
β’ (abs
β β ) = (abs β β ) |
58 | 57 | cnmetdval 24508 |
. . . . . . . . 9
β’ ((π β β β§ 0 β
β) β (π(abs
β β )0) = (absβ(π β 0))) |
59 | 37, 32, 58 | sylancl 585 |
. . . . . . . 8
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π(abs β
β )0) = (absβ(π
β 0))) |
60 | 37 | subid1d 11565 |
. . . . . . . . 9
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π β 0)
= π) |
61 | 60 | fveq2d 6896 |
. . . . . . . 8
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβ(π
β 0)) = (absβπ)) |
62 | 59, 61 | eqtrd 2771 |
. . . . . . 7
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (π(abs β
β )0) = (absβπ)) |
63 | | elbl3 24119 |
. . . . . . . . . 10
β’ ((((abs
β β ) β (βMetββ) β§ 1 β
β*) β§ (0 β β β§ π β β)) β (π β (0(ballβ(abs β β
))1) β (π(abs β
β )0) < 1)) |
64 | 31, 33, 63 | mpanl12 699 |
. . . . . . . . 9
β’ ((0
β β β§ π
β β) β (π
β (0(ballβ(abs β β ))1) β (π(abs β β )0) <
1)) |
65 | 32, 37, 64 | sylancr 586 |
. . . . . . . 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 5173 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
< 1) |
68 | 1, 2 | abelthlem1 26176 |
. . . . . . 7
β’ (π β 1 β€ sup({π β β β£ seq0( +
, ((π§ β β
β¦ (π β
β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< )) |
69 | 68 | adantr 480 |
. . . . . 6
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β 1 β€ sup({π
β β β£ seq0( + , ((π§ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< )) |
70 | 50, 53, 56, 67, 69 | xrltletrd 13145 |
. . . . 5
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β (absβπ)
< sup({π β β
β£ seq0( + , ((π§
β β β¦ (π
β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β }, β*,
< )) |
71 | 41, 47, 48, 37, 70 | radcnvlt2 26164 |
. . . 4
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , ((π§
β β β¦ (π
β β0 β¦ ((π΄βπ) Β· (π§βπ))))βπ)) β dom β ) |
72 | 46, 71 | eqeltrrd 2833 |
. . 3
β’ ((π β§ π β (0(ballβ(abs β β
))1)) β seq0( + , (π
β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |
73 | 30, 72 | jaodan 955 |
. 2
β’ ((π β§ (π β {1} β¨ π β (0(ballβ(abs β β
))1))) β seq0( + , (π
β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |
74 | 12, 73 | syldan 590 |
1
β’ ((π β§ π β π) β seq0( + , (π β β0 β¦ ((π΄βπ) Β· (πβπ)))) β dom β ) |