Step | Hyp | Ref
| Expression |
1 | | nn0uz 12812 |
. 2
β’
β0 = (β€β₯β0) |
2 | | 1nn0 12436 |
. . 3
β’ 1 β
β0 |
3 | 2 | a1i 11 |
. 2
β’ (π β 1 β
β0) |
4 | | id 22 |
. . . . . 6
β’ (π = π β π = π) |
5 | | 2fveq3 6852 |
. . . . . 6
β’ (π = π β (absβ((πΊβπ)βπ)) = (absβ((πΊβπ)βπ))) |
6 | 4, 5 | oveq12d 7380 |
. . . . 5
β’ (π = π β (π Β· (absβ((πΊβπ)βπ))) = (π Β· (absβ((πΊβπ)βπ)))) |
7 | | eqid 2737 |
. . . . 5
β’ (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
8 | | ovex 7395 |
. . . . 5
β’ (π Β· (absβ((πΊβπ)βπ))) β V |
9 | 6, 7, 8 | fvmpt 6953 |
. . . 4
β’ (π β β0
β ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))βπ) = (π Β· (absβ((πΊβπ)βπ)))) |
10 | 9 | adantl 483 |
. . 3
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))βπ) = (π Β· (absβ((πΊβπ)βπ)))) |
11 | | nn0re 12429 |
. . . . 5
β’ (π β β0
β π β
β) |
12 | 11 | adantl 483 |
. . . 4
β’ ((π β§ π β β0) β π β
β) |
13 | | pser.g |
. . . . . . 7
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
14 | | radcnv.a |
. . . . . . 7
β’ (π β π΄:β0βΆβ) |
15 | | psergf.x |
. . . . . . 7
β’ (π β π β β) |
16 | 13, 14, 15 | psergf 25787 |
. . . . . 6
β’ (π β (πΊβπ):β0βΆβ) |
17 | 16 | ffvelcdmda 7040 |
. . . . 5
β’ ((π β§ π β β0) β ((πΊβπ)βπ) β β) |
18 | 17 | abscld 15328 |
. . . 4
β’ ((π β§ π β β0) β
(absβ((πΊβπ)βπ)) β β) |
19 | 12, 18 | remulcld 11192 |
. . 3
β’ ((π β§ π β β0) β (π Β· (absβ((πΊβπ)βπ))) β β) |
20 | 10, 19 | eqeltrd 2838 |
. 2
β’ ((π β§ π β β0) β ((π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))βπ) β β) |
21 | | fvco3 6945 |
. . . 4
β’ (((πΊβπ):β0βΆβ β§
π β
β0) β ((abs β (πΊβπ))βπ) = (absβ((πΊβπ)βπ))) |
22 | 16, 21 | sylan 581 |
. . 3
β’ ((π β§ π β β0) β ((abs
β (πΊβπ))βπ) = (absβ((πΊβπ)βπ))) |
23 | 18 | recnd 11190 |
. . 3
β’ ((π β§ π β β0) β
(absβ((πΊβπ)βπ)) β β) |
24 | 22, 23 | eqeltrd 2838 |
. 2
β’ ((π β§ π β β0) β ((abs
β (πΊβπ))βπ) β β) |
25 | | radcnvlem2.y |
. . 3
β’ (π β π β β) |
26 | | radcnvlem2.a |
. . 3
β’ (π β (absβπ) < (absβπ)) |
27 | | radcnvlem2.c |
. . 3
β’ (π β seq0( + , (πΊβπ)) β dom β ) |
28 | 6 | cbvmptv 5223 |
. . 3
β’ (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ)))) = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
29 | 13, 14, 15, 25, 26, 27, 28 | radcnvlem1 25788 |
. 2
β’ (π β seq0( + , (π β β0
β¦ (π Β·
(absβ((πΊβπ)βπ))))) β dom β ) |
30 | | 1red 11163 |
. 2
β’ (π β 1 β
β) |
31 | | 1red 11163 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β 1 β β) |
32 | | elnnuz 12814 |
. . . . . 6
β’ (π β β β π β
(β€β₯β1)) |
33 | | nnnn0 12427 |
. . . . . 6
β’ (π β β β π β
β0) |
34 | 32, 33 | sylbir 234 |
. . . . 5
β’ (π β
(β€β₯β1) β π β β0) |
35 | 34, 12 | sylan2 594 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β π β
β) |
36 | 34, 18 | sylan2 594 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β (absβ((πΊβπ)βπ)) β β) |
37 | 17 | absge0d 15336 |
. . . . 5
β’ ((π β§ π β β0) β 0 β€
(absβ((πΊβπ)βπ))) |
38 | 34, 37 | sylan2 594 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β 0 β€ (absβ((πΊβπ)βπ))) |
39 | | eluzle 12783 |
. . . . 5
β’ (π β
(β€β₯β1) β 1 β€ π) |
40 | 39 | adantl 483 |
. . . 4
β’ ((π β§ π β (β€β₯β1))
β 1 β€ π) |
41 | 31, 35, 36, 38, 40 | lemul1ad 12101 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (1 Β· (absβ((πΊβπ)βπ))) β€ (π Β· (absβ((πΊβπ)βπ)))) |
42 | | absidm 15215 |
. . . . . 6
β’ (((πΊβπ)βπ) β β β
(absβ(absβ((πΊβπ)βπ))) = (absβ((πΊβπ)βπ))) |
43 | 17, 42 | syl 17 |
. . . . 5
β’ ((π β§ π β β0) β
(absβ(absβ((πΊβπ)βπ))) = (absβ((πΊβπ)βπ))) |
44 | 22 | fveq2d 6851 |
. . . . 5
β’ ((π β§ π β β0) β
(absβ((abs β (πΊβπ))βπ)) = (absβ(absβ((πΊβπ)βπ)))) |
45 | 23 | mulid2d 11180 |
. . . . 5
β’ ((π β§ π β β0) β (1
Β· (absβ((πΊβπ)βπ))) = (absβ((πΊβπ)βπ))) |
46 | 43, 44, 45 | 3eqtr4d 2787 |
. . . 4
β’ ((π β§ π β β0) β
(absβ((abs β (πΊβπ))βπ)) = (1 Β· (absβ((πΊβπ)βπ)))) |
47 | 34, 46 | sylan2 594 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (absβ((abs β (πΊβπ))βπ)) = (1 Β· (absβ((πΊβπ)βπ)))) |
48 | 10 | oveq2d 7378 |
. . . . 5
β’ ((π β§ π β β0) β (1
Β· ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))βπ)) = (1 Β· (π Β· (absβ((πΊβπ)βπ))))) |
49 | 19 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β β0) β (π Β· (absβ((πΊβπ)βπ))) β β) |
50 | 49 | mulid2d 11180 |
. . . . 5
β’ ((π β§ π β β0) β (1
Β· (π Β·
(absβ((πΊβπ)βπ)))) = (π Β· (absβ((πΊβπ)βπ)))) |
51 | 48, 50 | eqtrd 2777 |
. . . 4
β’ ((π β§ π β β0) β (1
Β· ((π β
β0 β¦ (π Β· (absβ((πΊβπ)βπ))))βπ)) = (π Β· (absβ((πΊβπ)βπ)))) |
52 | 34, 51 | sylan2 594 |
. . 3
β’ ((π β§ π β (β€β₯β1))
β (1 Β· ((π
β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))βπ)) = (π Β· (absβ((πΊβπ)βπ)))) |
53 | 41, 47, 52 | 3brtr4d 5142 |
. 2
β’ ((π β§ π β (β€β₯β1))
β (absβ((abs β (πΊβπ))βπ)) β€ (1 Β· ((π β β0 β¦ (π Β· (absβ((πΊβπ)βπ))))βπ))) |
54 | 1, 3, 20, 24, 29, 30, 53 | cvgcmpce 15710 |
1
β’ (π β seq0( + , (abs β
(πΊβπ))) β dom β ) |