Step | Hyp | Ref
| Expression |
1 | | nn0uz 12812 |
. . 3
β’
β0 = (β€β₯β0) |
2 | | 0zd 12518 |
. . 3
β’ (π β 0 β
β€) |
3 | | 1rp 12926 |
. . . 4
β’ 1 β
β+ |
4 | 3 | a1i 11 |
. . 3
β’ (π β 1 β
β+) |
5 | | radcnvlem2.y |
. . . 4
β’ (π β π β β) |
6 | | pser.g |
. . . . 5
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
7 | 6 | pserval2 25786 |
. . . 4
β’ ((π β β β§ π β β0)
β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) |
8 | 5, 7 | sylan 581 |
. . 3
β’ ((π β§ π β β0) β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) |
9 | | fvexd 6862 |
. . . 4
β’ (π β (πΊβπ) β V) |
10 | | radcnvlem2.c |
. . . 4
β’ (π β seq0( + , (πΊβπ)) β dom β ) |
11 | | radcnv.a |
. . . . . 6
β’ (π β π΄:β0βΆβ) |
12 | 6, 11, 5 | psergf 25787 |
. . . . 5
β’ (π β (πΊβπ):β0βΆβ) |
13 | 12 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π β β0) β ((πΊβπ)βπ) β β) |
14 | 1, 2, 9, 10, 13 | serf0 15572 |
. . 3
β’ (π β (πΊβπ) β 0) |
15 | 1, 2, 4, 8, 14 | climi0 15401 |
. 2
β’ (π β βπ β β0 βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1) |
16 | | simprl 770 |
. . 3
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β π β β0) |
17 | | nn0re 12429 |
. . . . . . 7
β’ (π β β0
β π β
β) |
18 | 17 | adantl 483 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β β0) β π β
β) |
19 | | psergf.x |
. . . . . . . . . 10
β’ (π β π β β) |
20 | 19 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β π β β) |
21 | 20 | abscld 15328 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β (absβπ) β
β) |
22 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β π β β) |
23 | 22 | abscld 15328 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β (absβπ) β
β) |
24 | | 0red 11165 |
. . . . . . . . . . 11
β’ (π β 0 β
β) |
25 | 19 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβπ) β
β) |
26 | 5 | abscld 15328 |
. . . . . . . . . . 11
β’ (π β (absβπ) β
β) |
27 | 19 | absge0d 15336 |
. . . . . . . . . . 11
β’ (π β 0 β€ (absβπ)) |
28 | | radcnvlem2.a |
. . . . . . . . . . 11
β’ (π β (absβπ) < (absβπ)) |
29 | 24, 25, 26, 27, 28 | lelttrd 11320 |
. . . . . . . . . 10
β’ (π β 0 < (absβπ)) |
30 | 29 | gt0ne0d 11726 |
. . . . . . . . 9
β’ (π β (absβπ) β 0) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β (absβπ) β 0) |
32 | 21, 23, 31 | redivcld 11990 |
. . . . . . 7
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β ((absβπ) / (absβπ)) β β) |
33 | | reexpcl 13991 |
. . . . . . 7
β’
((((absβπ) /
(absβπ)) β
β β§ π β
β0) β (((absβπ) / (absβπ))βπ) β β) |
34 | 32, 33 | sylan 581 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β β0) β
(((absβπ) /
(absβπ))βπ) β
β) |
35 | 18, 34 | remulcld 11192 |
. . . . 5
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β β0) β (π Β· (((absβπ) / (absβπ))βπ)) β β) |
36 | | eqid 2737 |
. . . . 5
β’ (π β β0
β¦ (π Β·
(((absβπ) /
(absβπ))βπ))) = (π β β0 β¦ (π Β· (((absβπ) / (absβπ))βπ))) |
37 | 35, 36 | fmptd 7067 |
. . . 4
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β (π β β0 β¦ (π Β· (((absβπ) / (absβπ))βπ))):β0βΆβ) |
38 | 37 | ffvelcdmda 7040 |
. . 3
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β β0) β ((π β β0
β¦ (π Β·
(((absβπ) /
(absβπ))βπ)))βπ) β β) |
39 | | nn0re 12429 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
40 | 39 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β β0) β π β
β) |
41 | 6, 11, 19 | psergf 25787 |
. . . . . . . . . 10
β’ (π β (πΊβπ):β0βΆβ) |
42 | 41 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β β0) β ((πΊβπ)βπ) β β) |
43 | 42 | abscld 15328 |
. . . . . . . 8
β’ ((π β§ π β β0) β
(absβ((πΊβπ)βπ)) β β) |
44 | 40, 43 | remulcld 11192 |
. . . . . . 7
β’ ((π β§ π β β0) β (π Β· (absβ((πΊβπ)βπ))) β β) |
45 | | radcnvlem1.h |
. . . . . . 7
β’ π» = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
46 | 44, 45 | fmptd 7067 |
. . . . . 6
β’ (π β π»:β0βΆβ) |
47 | 46 | adantr 482 |
. . . . 5
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β π»:β0βΆβ) |
48 | 47 | ffvelcdmda 7040 |
. . . 4
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β β0) β (π»βπ) β β) |
49 | 48 | recnd 11190 |
. . 3
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β β0) β (π»βπ) β β) |
50 | 25, 26, 30 | redivcld 11990 |
. . . . . 6
β’ (π β ((absβπ) / (absβπ)) β β) |
51 | 50 | recnd 11190 |
. . . . 5
β’ (π β ((absβπ) / (absβπ)) β β) |
52 | | divge0 12031 |
. . . . . . . 8
β’
((((absβπ)
β β β§ 0 β€ (absβπ)) β§ ((absβπ) β β β§ 0 <
(absβπ))) β 0
β€ ((absβπ) /
(absβπ))) |
53 | 25, 27, 26, 29, 52 | syl22anc 838 |
. . . . . . 7
β’ (π β 0 β€ ((absβπ) / (absβπ))) |
54 | 50, 53 | absidd 15314 |
. . . . . 6
β’ (π β
(absβ((absβπ) /
(absβπ))) =
((absβπ) /
(absβπ))) |
55 | 26 | recnd 11190 |
. . . . . . . . 9
β’ (π β (absβπ) β
β) |
56 | 55 | mulid1d 11179 |
. . . . . . . 8
β’ (π β ((absβπ) Β· 1) = (absβπ)) |
57 | 28, 56 | breqtrrd 5138 |
. . . . . . 7
β’ (π β (absβπ) < ((absβπ) Β· 1)) |
58 | | 1red 11163 |
. . . . . . . 8
β’ (π β 1 β
β) |
59 | | ltdivmul 12037 |
. . . . . . . 8
β’
(((absβπ)
β β β§ 1 β β β§ ((absβπ) β β β§ 0 <
(absβπ))) β
(((absβπ) /
(absβπ)) < 1
β (absβπ) <
((absβπ) Β·
1))) |
60 | 25, 58, 26, 29, 59 | syl112anc 1375 |
. . . . . . 7
β’ (π β (((absβπ) / (absβπ)) < 1 β (absβπ) < ((absβπ) Β· 1))) |
61 | 57, 60 | mpbird 257 |
. . . . . 6
β’ (π β ((absβπ) / (absβπ)) < 1) |
62 | 54, 61 | eqbrtrd 5132 |
. . . . 5
β’ (π β
(absβ((absβπ) /
(absβπ))) <
1) |
63 | 36 | geomulcvg 15768 |
. . . . 5
β’
((((absβπ) /
(absβπ)) β
β β§ (absβ((absβπ) / (absβπ))) < 1) β seq0( + , (π β β0
β¦ (π Β·
(((absβπ) /
(absβπ))βπ)))) β dom β
) |
64 | 51, 62, 63 | syl2anc 585 |
. . . 4
β’ (π β seq0( + , (π β β0
β¦ (π Β·
(((absβπ) /
(absβπ))βπ)))) β dom β
) |
65 | 64 | adantr 482 |
. . 3
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β seq0( + , (π β β0
β¦ (π Β·
(((absβπ) /
(absβπ))βπ)))) β dom β
) |
66 | | 1red 11163 |
. . 3
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β 1 β
β) |
67 | 41 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (πΊβπ):β0βΆβ) |
68 | | eluznn0 12849 |
. . . . . . . . 9
β’ ((π β β0
β§ π β
(β€β₯βπ)) β π β β0) |
69 | 16, 68 | sylan 581 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β π β β0) |
70 | 67, 69 | ffvelcdmd 7041 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((πΊβπ)βπ) β β) |
71 | 70 | abscld 15328 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((πΊβπ)βπ)) β β) |
72 | 32 | adantr 482 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβπ) / (absβπ)) β β) |
73 | 72, 69 | reexpcld 14075 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (((absβπ) / (absβπ))βπ) β β) |
74 | 69 | nn0red 12481 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β π β β) |
75 | 69 | nn0ge0d 12483 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 β€ π) |
76 | 11 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β π΄:β0βΆβ) |
77 | 76, 69 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (π΄βπ) β β) |
78 | 5 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β π β β) |
79 | 78, 69 | expcld 14058 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (πβπ) β β) |
80 | 77, 79 | mulcld 11182 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((π΄βπ) Β· (πβπ)) β β) |
81 | 80 | abscld 15328 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((π΄βπ) Β· (πβπ))) β β) |
82 | | 1red 11163 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 1 β
β) |
83 | 19 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β π β β) |
84 | 83 | abscld 15328 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβπ) β
β) |
85 | 84, 69 | reexpcld 14075 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβπ)βπ) β β) |
86 | 83 | absge0d 15336 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 β€
(absβπ)) |
87 | 84, 69, 86 | expge0d 14076 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 β€
((absβπ)βπ)) |
88 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1) |
89 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π΄βπ) = (π΄βπ)) |
90 | | oveq2 7370 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβπ) = (πβπ)) |
91 | 89, 90 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π΄βπ) Β· (πβπ)) = ((π΄βπ) Β· (πβπ))) |
92 | 91 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = π β (absβ((π΄βπ) Β· (πβπ))) = (absβ((π΄βπ) Β· (πβπ)))) |
93 | 92 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π = π β ((absβ((π΄βπ) Β· (πβπ))) < 1 β (absβ((π΄βπ) Β· (πβπ))) < 1)) |
94 | 93 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1 β§ π β (β€β₯βπ)) β (absβ((π΄βπ) Β· (πβπ))) < 1) |
95 | 88, 94 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((π΄βπ) Β· (πβπ))) < 1) |
96 | | 1re 11162 |
. . . . . . . . . . . 12
β’ 1 β
β |
97 | | ltle 11250 |
. . . . . . . . . . . 12
β’
(((absβ((π΄βπ) Β· (πβπ))) β β β§ 1 β β)
β ((absβ((π΄βπ) Β· (πβπ))) < 1 β (absβ((π΄βπ) Β· (πβπ))) β€ 1)) |
98 | 81, 96, 97 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβ((π΄βπ) Β· (πβπ))) < 1 β (absβ((π΄βπ) Β· (πβπ))) β€ 1)) |
99 | 95, 98 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((π΄βπ) Β· (πβπ))) β€ 1) |
100 | 81, 82, 85, 87, 99 | lemul1ad 12101 |
. . . . . . . . 9
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ)) β€ (1 Β· ((absβπ)βπ))) |
101 | 83, 69 | expcld 14058 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (πβπ) β β) |
102 | 77, 101 | mulcld 11182 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((π΄βπ) Β· (πβπ)) β β) |
103 | 102, 79 | absmuld 15346 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(((π΄βπ) Β· (πβπ)) Β· (πβπ))) = ((absβ((π΄βπ) Β· (πβπ))) Β· (absβ(πβπ)))) |
104 | 80, 101 | absmuld 15346 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(((π΄βπ) Β· (πβπ)) Β· (πβπ))) = ((absβ((π΄βπ) Β· (πβπ))) Β· (absβ(πβπ)))) |
105 | 77, 79, 101 | mul32d 11372 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (((π΄βπ) Β· (πβπ)) Β· (πβπ)) = (((π΄βπ) Β· (πβπ)) Β· (πβπ))) |
106 | 105 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(((π΄βπ) Β· (πβπ)) Β· (πβπ))) = (absβ(((π΄βπ) Β· (πβπ)) Β· (πβπ)))) |
107 | 83, 69 | absexpd 15344 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(πβπ)) = ((absβπ)βπ)) |
108 | 107 | oveq2d 7378 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβ((π΄βπ) Β· (πβπ))) Β· (absβ(πβπ))) = ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ))) |
109 | 104, 106,
108 | 3eqtr3d 2785 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(((π΄βπ) Β· (πβπ)) Β· (πβπ))) = ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ))) |
110 | 78, 69 | absexpd 15344 |
. . . . . . . . . . 11
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(πβπ)) = ((absβπ)βπ)) |
111 | 110 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβ((π΄βπ) Β· (πβπ))) Β· (absβ(πβπ))) = ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ))) |
112 | 103, 109,
111 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ)) = ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ))) |
113 | 85 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβπ)βπ) β β) |
114 | 113 | mulid2d 11180 |
. . . . . . . . 9
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (1 Β·
((absβπ)βπ)) = ((absβπ)βπ)) |
115 | 100, 112,
114 | 3brtr3d 5141 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ)) β€ ((absβπ)βπ)) |
116 | 102 | abscld 15328 |
. . . . . . . . 9
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((π΄βπ) Β· (πβπ))) β β) |
117 | 23 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβπ) β
β) |
118 | 117, 69 | reexpcld 14075 |
. . . . . . . . 9
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((absβπ)βπ) β β) |
119 | | eluzelz 12780 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
120 | 119 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β π β β€) |
121 | 29 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 <
(absβπ)) |
122 | | expgt0 14008 |
. . . . . . . . . 10
β’
(((absβπ)
β β β§ π
β β€ β§ 0 < (absβπ)) β 0 < ((absβπ)βπ)) |
123 | 117, 120,
121, 122 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 <
((absβπ)βπ)) |
124 | | lemuldiv 12042 |
. . . . . . . . 9
β’
(((absβ((π΄βπ) Β· (πβπ))) β β β§ ((absβπ)βπ) β β β§ (((absβπ)βπ) β β β§ 0 <
((absβπ)βπ))) β (((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ)) β€ ((absβπ)βπ) β (absβ((π΄βπ) Β· (πβπ))) β€ (((absβπ)βπ) / ((absβπ)βπ)))) |
125 | 116, 85, 118, 123, 124 | syl112anc 1375 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (((absβ((π΄βπ) Β· (πβπ))) Β· ((absβπ)βπ)) β€ ((absβπ)βπ) β (absβ((π΄βπ) Β· (πβπ))) β€ (((absβπ)βπ) / ((absβπ)βπ)))) |
126 | 115, 125 | mpbid 231 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((π΄βπ) Β· (πβπ))) β€ (((absβπ)βπ) / ((absβπ)βπ))) |
127 | 6 | pserval2 25786 |
. . . . . . . . 9
β’ ((π β β β§ π β β0)
β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) |
128 | 83, 69, 127 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((πΊβπ)βπ) = ((π΄βπ) Β· (πβπ))) |
129 | 128 | fveq2d 6851 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((πΊβπ)βπ)) = (absβ((π΄βπ) Β· (πβπ)))) |
130 | 21 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β (absβπ) β
β) |
131 | 130 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβπ) β
β) |
132 | 23 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β (absβπ) β
β) |
133 | 132 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβπ) β
β) |
134 | 30 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβπ) β 0) |
135 | 131, 133,
134, 69 | expdivd 14072 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (((absβπ) / (absβπ))βπ) = (((absβπ)βπ) / ((absβπ)βπ))) |
136 | 126, 129,
135 | 3brtr4d 5142 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ((πΊβπ)βπ)) β€ (((absβπ) / (absβπ))βπ)) |
137 | 71, 73, 74, 75, 136 | lemul2ad 12102 |
. . . . 5
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (π Β· (absβ((πΊβπ)βπ))) β€ (π Β· (((absβπ) / (absβπ))βπ))) |
138 | 74, 71 | remulcld 11192 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (π Β· (absβ((πΊβπ)βπ))) β β) |
139 | 70 | absge0d 15336 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 β€
(absβ((πΊβπ)βπ))) |
140 | 74, 71, 75, 139 | mulge0d 11739 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β 0 β€ (π Β· (absβ((πΊβπ)βπ)))) |
141 | 138, 140 | absidd 15314 |
. . . . 5
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(π Β· (absβ((πΊβπ)βπ)))) = (π Β· (absβ((πΊβπ)βπ)))) |
142 | 74, 73 | remulcld 11192 |
. . . . . . 7
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (π Β· (((absβπ) / (absβπ))βπ)) β β) |
143 | 142 | recnd 11190 |
. . . . . 6
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (π Β· (((absβπ) / (absβπ))βπ)) β β) |
144 | 143 | mulid2d 11180 |
. . . . 5
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (1 Β· (π Β· (((absβπ) / (absβπ))βπ))) = (π Β· (((absβπ) / (absβπ))βπ))) |
145 | 137, 141,
144 | 3brtr4d 5142 |
. . . 4
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(π Β· (absβ((πΊβπ)βπ)))) β€ (1 Β· (π Β· (((absβπ) / (absβπ))βπ)))) |
146 | | ovex 7395 |
. . . . . 6
β’ (π Β· (absβ((πΊβπ)βπ))) β V |
147 | 45 | fvmpt2 6964 |
. . . . . 6
β’ ((π β β0
β§ (π Β·
(absβ((πΊβπ)βπ))) β V) β (π»βπ) = (π Β· (absβ((πΊβπ)βπ)))) |
148 | 69, 146, 147 | sylancl 587 |
. . . . 5
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (π»βπ) = (π Β· (absβ((πΊβπ)βπ)))) |
149 | 148 | fveq2d 6851 |
. . . 4
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(π»βπ)) = (absβ(π Β· (absβ((πΊβπ)βπ))))) |
150 | | id 22 |
. . . . . . . 8
β’ (π = π β π = π) |
151 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π β (((absβπ) / (absβπ))βπ) = (((absβπ) / (absβπ))βπ)) |
152 | 150, 151 | oveq12d 7380 |
. . . . . . 7
β’ (π = π β (π Β· (((absβπ) / (absβπ))βπ)) = (π Β· (((absβπ) / (absβπ))βπ))) |
153 | | ovex 7395 |
. . . . . . 7
β’ (π Β· (((absβπ) / (absβπ))βπ)) β V |
154 | 152, 36, 153 | fvmpt 6953 |
. . . . . 6
β’ (π β β0
β ((π β
β0 β¦ (π Β· (((absβπ) / (absβπ))βπ)))βπ) = (π Β· (((absβπ) / (absβπ))βπ))) |
155 | 69, 154 | syl 17 |
. . . . 5
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β ((π β β0 β¦ (π Β· (((absβπ) / (absβπ))βπ)))βπ) = (π Β· (((absβπ) / (absβπ))βπ))) |
156 | 155 | oveq2d 7378 |
. . . 4
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (1 Β· ((π β β0
β¦ (π Β·
(((absβπ) /
(absβπ))βπ)))βπ)) = (1 Β· (π Β· (((absβπ) / (absβπ))βπ)))) |
157 | 145, 149,
156 | 3brtr4d 5142 |
. . 3
β’ (((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β§ π β (β€β₯βπ)) β (absβ(π»βπ)) β€ (1 Β· ((π β β0 β¦ (π Β· (((absβπ) / (absβπ))βπ)))βπ))) |
158 | 1, 16, 38, 49, 65, 66, 157 | cvgcmpce 15710 |
. 2
β’ ((π β§ (π β β0 β§
βπ β
(β€β₯βπ)(absβ((π΄βπ) Β· (πβπ))) < 1)) β seq0( + , π») β dom β
) |
159 | 15, 158 | rexlimddv 3159 |
1
β’ (π β seq0( + , π») β dom β
) |