Step | Hyp | Ref
| Expression |
1 | | pserulm.y |
. . . . . 6
β’ (π β π β (β‘abs β (0[,]π))) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π < 0) β π β (β‘abs β (0[,]π))) |
3 | | 0xr 11209 |
. . . . . . . . 9
β’ 0 β
β* |
4 | | pserulm.m |
. . . . . . . . . 10
β’ (π β π β β) |
5 | 4 | rexrd 11212 |
. . . . . . . . 9
β’ (π β π β
β*) |
6 | | icc0 13319 |
. . . . . . . . 9
β’ ((0
β β* β§ π β β*) β
((0[,]π) = β
β
π < 0)) |
7 | 3, 5, 6 | sylancr 588 |
. . . . . . . 8
β’ (π β ((0[,]π) = β
β π < 0)) |
8 | 7 | biimpar 479 |
. . . . . . 7
β’ ((π β§ π < 0) β (0[,]π) = β
) |
9 | 8 | imaeq2d 6018 |
. . . . . 6
β’ ((π β§ π < 0) β (β‘abs β (0[,]π)) = (β‘abs β β
)) |
10 | | ima0 6034 |
. . . . . 6
β’ (β‘abs β β
) =
β
|
11 | 9, 10 | eqtrdi 2793 |
. . . . 5
β’ ((π β§ π < 0) β (β‘abs β (0[,]π)) = β
) |
12 | 2, 11 | sseqtrd 3989 |
. . . 4
β’ ((π β§ π < 0) β π β β
) |
13 | | ss0 4363 |
. . . 4
β’ (π β β
β π = β
) |
14 | 12, 13 | syl 17 |
. . 3
β’ ((π β§ π < 0) β π = β
) |
15 | | nn0uz 12812 |
. . . 4
β’
β0 = (β€β₯β0) |
16 | | 0zd 12518 |
. . . 4
β’ (π β 0 β
β€) |
17 | | 0zd 12518 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π) β 0 β β€) |
18 | | pserf.g |
. . . . . . . . . . . 12
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
19 | | pserf.a |
. . . . . . . . . . . . 13
β’ (π β π΄:β0βΆβ) |
20 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β π΄:β0βΆβ) |
21 | | cnvimass 6038 |
. . . . . . . . . . . . . . 15
β’ (β‘abs β (0[,]π)) β dom abs |
22 | | absf 15229 |
. . . . . . . . . . . . . . . 16
β’
abs:ββΆβ |
23 | 22 | fdmi 6685 |
. . . . . . . . . . . . . . 15
β’ dom abs =
β |
24 | 21, 23 | sseqtri 3985 |
. . . . . . . . . . . . . 14
β’ (β‘abs β (0[,]π)) β β |
25 | 1, 24 | sstrdi 3961 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
26 | 25 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β π¦ β β) |
27 | 18, 20, 26 | psergf 25787 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (πΊβπ¦):β0βΆβ) |
28 | 27 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ π β β0) β ((πΊβπ¦)βπ) β β) |
29 | 15, 17, 28 | serf 13943 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β seq0( + , (πΊβπ¦)):β0βΆβ) |
30 | 29 | ffvelcdmda 7040 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ π β β0) β (seq0( +
, (πΊβπ¦))βπ) β β) |
31 | 30 | an32s 651 |
. . . . . . 7
β’ (((π β§ π β β0) β§ π¦ β π) β (seq0( + , (πΊβπ¦))βπ) β β) |
32 | 31 | fmpttd 7068 |
. . . . . 6
β’ ((π β§ π β β0) β (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)):πβΆβ) |
33 | | cnex 11139 |
. . . . . . 7
β’ β
β V |
34 | | ssexg 5285 |
. . . . . . . . 9
β’ ((π β β β§ β
β V) β π β
V) |
35 | 25, 33, 34 | sylancl 587 |
. . . . . . . 8
β’ (π β π β V) |
36 | 35 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β0) β π β V) |
37 | | elmapg 8785 |
. . . . . . 7
β’ ((β
β V β§ π β V)
β ((π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) β (β βm π) β (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)):πβΆβ)) |
38 | 33, 36, 37 | sylancr 588 |
. . . . . 6
β’ ((π β§ π β β0) β ((π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) β (β βm π) β (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)):πβΆβ)) |
39 | 32, 38 | mpbird 257 |
. . . . 5
β’ ((π β§ π β β0) β (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) β (β βm π)) |
40 | | pserulm.h |
. . . . 5
β’ π» = (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) |
41 | 39, 40 | fmptd 7067 |
. . . 4
β’ (π β π»:β0βΆ(β
βm π)) |
42 | | eqidd 2738 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π β β0) β ((πΊβπ¦)βπ) = ((πΊβπ¦)βπ)) |
43 | | pserf.r |
. . . . . . 7
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
44 | 1 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β π) β π¦ β (β‘abs β (0[,]π))) |
45 | | ffn 6673 |
. . . . . . . . . . . . . 14
β’
(abs:ββΆβ β abs Fn β) |
46 | | elpreima 7013 |
. . . . . . . . . . . . . 14
β’ (abs Fn
β β (π¦ β
(β‘abs β (0[,]π)) β (π¦ β β β§ (absβπ¦) β (0[,]π)))) |
47 | 22, 45, 46 | mp2b 10 |
. . . . . . . . . . . . 13
β’ (π¦ β (β‘abs β (0[,]π)) β (π¦ β β β§ (absβπ¦) β (0[,]π))) |
48 | 44, 47 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β (π¦ β β β§ (absβπ¦) β (0[,]π))) |
49 | 48 | simprd 497 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β (absβπ¦) β (0[,]π)) |
50 | | 0re 11164 |
. . . . . . . . . . . 12
β’ 0 β
β |
51 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β π) β π β β) |
52 | | elicc2 13336 |
. . . . . . . . . . . 12
β’ ((0
β β β§ π
β β) β ((absβπ¦) β (0[,]π) β ((absβπ¦) β β β§ 0 β€
(absβπ¦) β§
(absβπ¦) β€ π))) |
53 | 50, 51, 52 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β ((absβπ¦) β (0[,]π) β ((absβπ¦) β β β§ 0 β€
(absβπ¦) β§
(absβπ¦) β€ π))) |
54 | 49, 53 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π¦ β π) β ((absβπ¦) β β β§ 0 β€
(absβπ¦) β§
(absβπ¦) β€ π)) |
55 | 54 | simp1d 1143 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β (absβπ¦) β β) |
56 | 55 | rexrd 11212 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (absβπ¦) β
β*) |
57 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β π β
β*) |
58 | | iccssxr 13354 |
. . . . . . . . . 10
β’
(0[,]+β) β β* |
59 | 18, 19, 43 | radcnvcl 25792 |
. . . . . . . . . 10
β’ (π β π
β (0[,]+β)) |
60 | 58, 59 | sselid 3947 |
. . . . . . . . 9
β’ (π β π
β
β*) |
61 | 60 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β π
β
β*) |
62 | 54 | simp3d 1145 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (absβπ¦) β€ π) |
63 | | pserulm.l |
. . . . . . . . 9
β’ (π β π < π
) |
64 | 63 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β π < π
) |
65 | 56, 57, 61, 62, 64 | xrlelttrd 13086 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (absβπ¦) < π
) |
66 | 18, 20, 43, 26, 65 | radcnvlt2 25794 |
. . . . . 6
β’ ((π β§ π¦ β π) β seq0( + , (πΊβπ¦)) β dom β ) |
67 | 15, 17, 42, 28, 66 | isumcl 15653 |
. . . . 5
β’ ((π β§ π¦ β π) β Ξ£π β β0 ((πΊβπ¦)βπ) β β) |
68 | | pserf.f |
. . . . 5
β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) |
69 | 67, 68 | fmptd 7067 |
. . . 4
β’ (π β πΉ:πβΆβ) |
70 | 15, 16, 41, 69 | ulm0 25766 |
. . 3
β’ ((π β§ π = β
) β π»(βπ’βπ)πΉ) |
71 | 14, 70 | syldan 592 |
. 2
β’ ((π β§ π < 0) β π»(βπ’βπ)πΉ) |
72 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β β0) β π β
β0) |
73 | 72, 15 | eleqtrdi 2848 |
. . . . . . . . 9
β’ ((π β§ π β β0) β π β
(β€β₯β0)) |
74 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β β0
β¦ (π€ β π β¦ ((πΊβπ€)βπ))) = (π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))) |
75 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π€ = π¦ β (πΊβπ€) = (πΊβπ¦)) |
76 | 75 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ (π€ = π¦ β ((πΊβπ€)βπ) = ((πΊβπ¦)βπ)) |
77 | 76 | cbvmptv 5223 |
. . . . . . . . . . 11
β’ (π€ β π β¦ ((πΊβπ€)βπ)) = (π¦ β π β¦ ((πΊβπ¦)βπ)) |
78 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β ((πΊβπ¦)βπ) = ((πΊβπ¦)βπ)) |
79 | 78 | mpteq2dv 5212 |
. . . . . . . . . . 11
β’ (π = π β (π¦ β π β¦ ((πΊβπ¦)βπ)) = (π¦ β π β¦ ((πΊβπ¦)βπ))) |
80 | 77, 79 | eqtrid 2789 |
. . . . . . . . . 10
β’ (π = π β (π€ β π β¦ ((πΊβπ€)βπ)) = (π¦ β π β¦ ((πΊβπ¦)βπ))) |
81 | | elfznn0 13541 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β0) |
82 | 81 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β (0...π)) β π β β0) |
83 | 35 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ π β (0...π)) β π β V) |
84 | 83 | mptexd 7179 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π β (0...π)) β (π¦ β π β¦ ((πΊβπ¦)βπ)) β V) |
85 | 74, 80, 82, 84 | fvmptd3 6976 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β (0...π)) β ((π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))βπ) = (π¦ β π β¦ ((πΊβπ¦)βπ))) |
86 | 36, 73, 85 | seqof 13972 |
. . . . . . . 8
β’ ((π β§ π β β0) β (seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))))βπ) = (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) |
87 | 86 | eqcomd 2743 |
. . . . . . 7
β’ ((π β§ π β β0) β (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) = (seq0( βf + , (π β β0
β¦ (π€ β π β¦ ((πΊβπ€)βπ))))βπ)) |
88 | 87 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π β β0 β¦ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) = (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))))βπ))) |
89 | | 0z 12517 |
. . . . . . . . 9
β’ 0 β
β€ |
90 | | seqfn 13925 |
. . . . . . . . 9
β’ (0 β
β€ β seq0( βf + , (π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) Fn
(β€β₯β0)) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . 8
β’ seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) Fn
(β€β₯β0) |
92 | 15 | fneq2i 6605 |
. . . . . . . 8
β’ (seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) Fn β0 β seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) Fn
(β€β₯β0)) |
93 | 91, 92 | mpbir 230 |
. . . . . . 7
β’ seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) Fn β0 |
94 | | dffn5 6906 |
. . . . . . 7
β’ (seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) Fn β0 β seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) = (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))))βπ))) |
95 | 93, 94 | mpbi 229 |
. . . . . 6
β’ seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) = (π β β0 β¦ (seq0(
βf + , (π
β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))))βπ)) |
96 | 88, 40, 95 | 3eqtr4g 2802 |
. . . . 5
β’ (π β π» = seq0( βf + , (π β β0
β¦ (π€ β π β¦ ((πΊβπ€)βπ))))) |
97 | 96 | adantr 482 |
. . . 4
β’ ((π β§ 0 β€ π) β π» = seq0( βf + , (π β β0
β¦ (π€ β π β¦ ((πΊβπ€)βπ))))) |
98 | | 0zd 12518 |
. . . . 5
β’ ((π β§ 0 β€ π) β 0 β β€) |
99 | 35 | adantr 482 |
. . . . 5
β’ ((π β§ 0 β€ π) β π β V) |
100 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β π) β π΄:β0βΆβ) |
101 | 25 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π€ β π) β π€ β β) |
102 | 18, 100, 101 | psergf 25787 |
. . . . . . . . . . 11
β’ ((π β§ π€ β π) β (πΊβπ€):β0βΆβ) |
103 | 102 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ (((π β§ π€ β π) β§ π β β0) β ((πΊβπ€)βπ) β β) |
104 | 103 | an32s 651 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π€ β π) β ((πΊβπ€)βπ) β β) |
105 | 104 | fmpttd 7068 |
. . . . . . . 8
β’ ((π β§ π β β0) β (π€ β π β¦ ((πΊβπ€)βπ)):πβΆβ) |
106 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β0) β π β V) |
107 | | elmapg 8785 |
. . . . . . . . 9
β’ ((β
β V β§ π β V)
β ((π€ β π β¦ ((πΊβπ€)βπ)) β (β βm π) β (π€ β π β¦ ((πΊβπ€)βπ)):πβΆβ)) |
108 | 33, 106, 107 | sylancr 588 |
. . . . . . . 8
β’ ((π β§ π β β0) β ((π€ β π β¦ ((πΊβπ€)βπ)) β (β βm π) β (π€ β π β¦ ((πΊβπ€)βπ)):πβΆβ)) |
109 | 105, 108 | mpbird 257 |
. . . . . . 7
β’ ((π β§ π β β0) β (π€ β π β¦ ((πΊβπ€)βπ)) β (β βm π)) |
110 | 109 | fmpttd 7068 |
. . . . . 6
β’ (π β (π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))):β0βΆ(β
βm π)) |
111 | 110 | adantr 482 |
. . . . 5
β’ ((π β§ 0 β€ π) β (π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ))):β0βΆ(β
βm π)) |
112 | | fex 7181 |
. . . . . . . 8
β’
((abs:ββΆβ β§ β β V) β abs β
V) |
113 | 22, 33, 112 | mp2an 691 |
. . . . . . 7
β’ abs
β V |
114 | | fvex 6860 |
. . . . . . 7
β’ (πΊβπ) β V |
115 | 113, 114 | coex 7872 |
. . . . . 6
β’ (abs
β (πΊβπ)) β V |
116 | 115 | a1i 11 |
. . . . 5
β’ ((π β§ 0 β€ π) β (abs β (πΊβπ)) β V) |
117 | 19 | adantr 482 |
. . . . . . . 8
β’ ((π β§ 0 β€ π) β π΄:β0βΆβ) |
118 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ 0 β€ π) β π β β) |
119 | 118 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ 0 β€ π) β π β β) |
120 | 18, 117, 119 | psergf 25787 |
. . . . . . 7
β’ ((π β§ 0 β€ π) β (πΊβπ):β0βΆβ) |
121 | | fco 6697 |
. . . . . . 7
β’
((abs:ββΆβ β§ (πΊβπ):β0βΆβ) β
(abs β (πΊβπ)):β0βΆβ) |
122 | 22, 120, 121 | sylancr 588 |
. . . . . 6
β’ ((π β§ 0 β€ π) β (abs β (πΊβπ)):β0βΆβ) |
123 | 122 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ 0 β€ π) β§ π β β0) β ((abs
β (πΊβπ))βπ) β β) |
124 | 25 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π β β) |
125 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π§ β π) |
126 | 124, 125 | sseldd 3950 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π§ β β) |
127 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π β β0) |
128 | 126, 127 | expcld 14058 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (π§βπ) β β) |
129 | 128 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(π§βπ)) β β) |
130 | 119 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π β β) |
131 | 130, 127 | expcld 14058 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (πβπ) β β) |
132 | 131 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(πβπ)) β β) |
133 | 19 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π΄:β0βΆβ) |
134 | 133, 127 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (π΄βπ) β β) |
135 | 134 | abscld 15328 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(π΄βπ)) β β) |
136 | 134 | absge0d 15336 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β 0 β€ (absβ(π΄βπ))) |
137 | 126 | abscld 15328 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβπ§) β β) |
138 | 4 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π β β) |
139 | 126 | absge0d 15336 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β 0 β€ (absβπ§)) |
140 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β (absβπ¦) = (absβπ§)) |
141 | 140 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π¦ = π§ β ((absβπ¦) β€ π β (absβπ§) β€ π)) |
142 | 62 | ralrimiva 3144 |
. . . . . . . . . . . 12
β’ (π β βπ¦ β π (absβπ¦) β€ π) |
143 | 142 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β βπ¦ β π (absβπ¦) β€ π) |
144 | 141, 143,
125 | rspcdva 3585 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβπ§) β€ π) |
145 | | leexp1a 14087 |
. . . . . . . . . 10
β’
((((absβπ§)
β β β§ π
β β β§ π
β β0) β§ (0 β€ (absβπ§) β§ (absβπ§) β€ π)) β ((absβπ§)βπ) β€ (πβπ)) |
146 | 137, 138,
127, 139, 144, 145 | syl32anc 1379 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((absβπ§)βπ) β€ (πβπ)) |
147 | 126, 127 | absexpd 15344 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(π§βπ)) = ((absβπ§)βπ)) |
148 | 130, 127 | absexpd 15344 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(πβπ)) = ((absβπ)βπ)) |
149 | | absid 15188 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 0 β€
π) β (absβπ) = π) |
150 | 4, 149 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ 0 β€ π) β (absβπ) = π) |
151 | 150 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβπ) = π) |
152 | 151 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((absβπ)βπ) = (πβπ)) |
153 | 148, 152 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(πβπ)) = (πβπ)) |
154 | 146, 147,
153 | 3brtr4d 5142 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(π§βπ)) β€ (absβ(πβπ))) |
155 | 129, 132,
135, 136, 154 | lemul2ad 12102 |
. . . . . . 7
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((absβ(π΄βπ)) Β· (absβ(π§βπ))) β€ ((absβ(π΄βπ)) Β· (absβ(πβπ)))) |
156 | 134, 128 | absmuld 15346 |
. . . . . . 7
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ((π΄βπ) Β· (π§βπ))) = ((absβ(π΄βπ)) Β· (absβ(π§βπ)))) |
157 | 134, 131 | absmuld 15346 |
. . . . . . 7
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ((π΄βπ) Β· (πβπ))) = ((absβ(π΄βπ)) Β· (absβ(πβπ)))) |
158 | 155, 156,
157 | 3brtr4d 5142 |
. . . . . 6
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ((π΄βπ) Β· (π§βπ))) β€ (absβ((π΄βπ) Β· (πβπ)))) |
159 | 35 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β π β V) |
160 | 159 | mptexd 7179 |
. . . . . . . . . 10
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (π¦ β π β¦ ((πΊβπ¦)βπ)) β V) |
161 | 74, 80, 127, 160 | fvmptd3 6976 |
. . . . . . . . 9
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))βπ) = (π¦ β π β¦ ((πΊβπ¦)βπ))) |
162 | 161 | fveq1d 6849 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (((π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))βπ)βπ§) = ((π¦ β π β¦ ((πΊβπ¦)βπ))βπ§)) |
163 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π¦ = π§ β (πΊβπ¦) = (πΊβπ§)) |
164 | 163 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π¦ = π§ β ((πΊβπ¦)βπ) = ((πΊβπ§)βπ)) |
165 | | eqid 2737 |
. . . . . . . . . 10
β’ (π¦ β π β¦ ((πΊβπ¦)βπ)) = (π¦ β π β¦ ((πΊβπ¦)βπ)) |
166 | | fvex 6860 |
. . . . . . . . . 10
β’ ((πΊβπ§)βπ) β V |
167 | 164, 165,
166 | fvmpt 6953 |
. . . . . . . . 9
β’ (π§ β π β ((π¦ β π β¦ ((πΊβπ¦)βπ))βπ§) = ((πΊβπ§)βπ)) |
168 | 167 | ad2antll 728 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((π¦ β π β¦ ((πΊβπ¦)βπ))βπ§) = ((πΊβπ§)βπ)) |
169 | 18 | pserval2 25786 |
. . . . . . . . 9
β’ ((π§ β β β§ π β β0)
β ((πΊβπ§)βπ) = ((π΄βπ) Β· (π§βπ))) |
170 | 126, 127,
169 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((πΊβπ§)βπ) = ((π΄βπ) Β· (π§βπ))) |
171 | 162, 168,
170 | 3eqtrd 2781 |
. . . . . . 7
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (((π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))βπ)βπ§) = ((π΄βπ) Β· (π§βπ))) |
172 | 171 | fveq2d 6851 |
. . . . . 6
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(((π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))βπ)βπ§)) = (absβ((π΄βπ) Β· (π§βπ)))) |
173 | 120 | adantr 482 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (πΊβπ):β0βΆβ) |
174 | | fvco3 6945 |
. . . . . . . 8
β’ (((πΊβπ):β0βΆβ β§
π β
β0) β ((abs β (πΊβπ))βπ) = (absβ((πΊβπ)βπ))) |
175 | 173, 127,
174 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((abs β (πΊβπ))βπ) = (absβ((πΊβπ)βπ))) |
176 | 18 | pserval2 25786 |
. . . . . . . . 9
β’ ((π β β β§ π β β0)
β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) |
177 | 130, 127,
176 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) |
178 | 177 | fveq2d 6851 |
. . . . . . 7
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ((πΊβπ)βπ)) = (absβ((π΄βπ) Β· (πβπ)))) |
179 | 175, 178 | eqtrd 2777 |
. . . . . 6
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β ((abs β (πΊβπ))βπ) = (absβ((π΄βπ) Β· (πβπ)))) |
180 | 158, 172,
179 | 3brtr4d 5142 |
. . . . 5
β’ (((π β§ 0 β€ π) β§ (π β β0 β§ π§ β π)) β (absβ(((π β β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))βπ)βπ§)) β€ ((abs β (πΊβπ))βπ)) |
181 | 63 | adantr 482 |
. . . . . . . 8
β’ ((π β§ 0 β€ π) β π < π
) |
182 | 150, 181 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ 0 β€ π) β (absβπ) < π
) |
183 | | id 22 |
. . . . . . . . 9
β’ (π = π β π = π) |
184 | | 2fveq3 6852 |
. . . . . . . . 9
β’ (π = π β (absβ((πΊβπ)βπ)) = (absβ((πΊβπ)βπ))) |
185 | 183, 184 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π β (π Β· (absβ((πΊβπ)βπ))) = (π Β· (absβ((πΊβπ)βπ)))) |
186 | 185 | cbvmptv 5223 |
. . . . . . 7
β’ (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
187 | 18, 117, 43, 119, 182, 186 | radcnvlt1 25793 |
. . . . . 6
β’ ((π β§ 0 β€ π) β (seq0( + , (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))) β dom β β§ seq0( + , (abs
β (πΊβπ))) β dom β
)) |
188 | 187 | simprd 497 |
. . . . 5
β’ ((π β§ 0 β€ π) β seq0( + , (abs β (πΊβπ))) β dom β ) |
189 | 15, 98, 99, 111, 116, 123, 180, 188 | mtest 25779 |
. . . 4
β’ ((π β§ 0 β€ π) β seq0( βf + ,
(π β
β0 β¦ (π€ β π β¦ ((πΊβπ€)βπ)))) β dom
(βπ’βπ)) |
190 | 97, 189 | eqeltrd 2838 |
. . 3
β’ ((π β§ 0 β€ π) β π» β dom
(βπ’βπ)) |
191 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π»(βπ’βπ)π) β π»(βπ’βπ)π) |
192 | | ulmcl 25756 |
. . . . . . . . . 10
β’ (π»(βπ’βπ)π β π:πβΆβ) |
193 | 192 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π»(βπ’βπ)π) β π:πβΆβ) |
194 | 193 | feqmptd 6915 |
. . . . . . . 8
β’ ((π β§ π»(βπ’βπ)π) β π = (π¦ β π β¦ (πβπ¦))) |
195 | | 0zd 12518 |
. . . . . . . . . . 11
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β 0 β β€) |
196 | | eqidd 2738 |
. . . . . . . . . . 11
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β ((πΊβπ¦)βπ) = ((πΊβπ¦)βπ)) |
197 | 27 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β (πΊβπ¦):β0βΆβ) |
198 | 197 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β ((πΊβπ¦)βπ) β β) |
199 | 41 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β π»:β0βΆ(β
βm π)) |
200 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β π¦ β π) |
201 | | seqex 13915 |
. . . . . . . . . . . . 13
β’ seq0( + ,
(πΊβπ¦)) β V |
202 | 201 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β seq0( + , (πΊβπ¦)) β V) |
203 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β π β
β0) |
204 | 35 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β π β V) |
205 | 204 | mptexd 7179 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) β V) |
206 | 40 | fvmpt2 6964 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) β V) β (π»βπ) = (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) |
207 | 203, 205,
206 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β (π»βπ) = (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))) |
208 | 207 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β ((π»βπ)βπ¦) = ((π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))βπ¦)) |
209 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β π¦ β π) |
210 | | fvex 6860 |
. . . . . . . . . . . . . 14
β’ (seq0( +
, (πΊβπ¦))βπ) β V |
211 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) = (π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ)) |
212 | 211 | fvmpt2 6964 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π β§ (seq0( + , (πΊβπ¦))βπ) β V) β ((π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))βπ¦) = (seq0( + , (πΊβπ¦))βπ)) |
213 | 209, 210,
212 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β ((π¦ β π β¦ (seq0( + , (πΊβπ¦))βπ))βπ¦) = (seq0( + , (πΊβπ¦))βπ)) |
214 | 208, 213 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((((π β§ π»(βπ’βπ)π) β§ π¦ β π) β§ π β β0) β ((π»βπ)βπ¦) = (seq0( + , (πΊβπ¦))βπ)) |
215 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β π»(βπ’βπ)π) |
216 | 15, 195, 199, 200, 202, 214, 215 | ulmclm 25762 |
. . . . . . . . . . 11
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β seq0( + , (πΊβπ¦)) β (πβπ¦)) |
217 | 15, 195, 196, 198, 216 | isumclim 15649 |
. . . . . . . . . 10
β’ (((π β§ π»(βπ’βπ)π) β§ π¦ β π) β Ξ£π β β0 ((πΊβπ¦)βπ) = (πβπ¦)) |
218 | 217 | mpteq2dva 5210 |
. . . . . . . . 9
β’ ((π β§ π»(βπ’βπ)π) β (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) = (π¦ β π β¦ (πβπ¦))) |
219 | 68, 218 | eqtrid 2789 |
. . . . . . . 8
β’ ((π β§ π»(βπ’βπ)π) β πΉ = (π¦ β π β¦ (πβπ¦))) |
220 | 194, 219 | eqtr4d 2780 |
. . . . . . 7
β’ ((π β§ π»(βπ’βπ)π) β π = πΉ) |
221 | 191, 220 | breqtrd 5136 |
. . . . . 6
β’ ((π β§ π»(βπ’βπ)π) β π»(βπ’βπ)πΉ) |
222 | 221 | ex 414 |
. . . . 5
β’ (π β (π»(βπ’βπ)π β π»(βπ’βπ)πΉ)) |
223 | 222 | exlimdv 1937 |
. . . 4
β’ (π β (βπ π»(βπ’βπ)π β π»(βπ’βπ)πΉ)) |
224 | | eldmg 5859 |
. . . . 5
β’ (π» β dom
(βπ’βπ) β (π» β dom
(βπ’βπ) β βπ π»(βπ’βπ)π)) |
225 | 224 | ibi 267 |
. . . 4
β’ (π» β dom
(βπ’βπ) β βπ π»(βπ’βπ)π) |
226 | 223, 225 | impel 507 |
. . 3
β’ ((π β§ π» β dom
(βπ’βπ)) β π»(βπ’βπ)πΉ) |
227 | 190, 226 | syldan 592 |
. 2
β’ ((π β§ 0 β€ π) β π»(βπ’βπ)πΉ) |
228 | | 0red 11165 |
. 2
β’ (π β 0 β
β) |
229 | 71, 227, 4, 228 | ltlecasei 11270 |
1
β’ (π β π»(βπ’βπ)πΉ) |