Step | Hyp | Ref
| Expression |
1 | | o1f 15418 |
. . . . 5
β’ (πΉ β π(1) β
πΉ:dom πΉβΆβ) |
2 | 1 | adantr 482 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΉ:dom πΉβΆβ) |
3 | 2 | ffnd 6674 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΉ Fn dom πΉ) |
4 | | rlimf 15390 |
. . . . 5
β’ (πΊ βπ 0
β πΊ:dom πΊβΆβ) |
5 | 4 | adantl 483 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ:dom πΊβΆβ) |
6 | 5 | ffnd 6674 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ Fn dom πΊ) |
7 | | o1dm 15419 |
. . . . 5
β’ (πΉ β π(1) β dom
πΉ β
β) |
8 | 7 | adantr 482 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΉ β
β) |
9 | | reex 11149 |
. . . 4
β’ β
β V |
10 | | ssexg 5285 |
. . . 4
β’ ((dom
πΉ β β β§
β β V) β dom πΉ β V) |
11 | 8, 9, 10 | sylancl 587 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΉ β
V) |
12 | | rlimss 15391 |
. . . . 5
β’ (πΊ βπ 0
β dom πΊ β
β) |
13 | 12 | adantl 483 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΊ β
β) |
14 | | ssexg 5285 |
. . . 4
β’ ((dom
πΊ β β β§
β β V) β dom πΊ β V) |
15 | 13, 9, 14 | sylancl 587 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΊ β
V) |
16 | | eqid 2737 |
. . 3
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
17 | | eqidd 2738 |
. . 3
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β dom πΉ) β (πΉβπ₯) = (πΉβπ₯)) |
18 | | eqidd 2738 |
. . 3
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β dom πΊ) β (πΊβπ₯) = (πΊβπ₯)) |
19 | 3, 6, 11, 15, 16, 17, 18 | offval 7631 |
. 2
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (πΉ
βf Β· πΊ) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
20 | | o1bdd 15420 |
. . . . . . 7
β’ ((πΉ β π(1) β§ πΉ:dom πΉβΆβ) β βπ β β βπ β β βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
21 | 1, 20 | mpdan 686 |
. . . . . 6
β’ (πΉ β π(1) β
βπ β β
βπ β β
βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
22 | 21 | ad2antrr 725 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β βπ β β βπ β β βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
23 | | fvexd 6862 |
. . . . . . . . 9
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π₯ β dom πΊ) β (πΊβπ₯) β V) |
24 | 23 | ralrimiva 3144 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β βπ₯ β dom πΊ(πΊβπ₯) β V) |
25 | | simplr 768 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β π¦ β β+) |
26 | | recn 11148 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
27 | 26 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β π β β) |
28 | 27 | abscld 15328 |
. . . . . . . . . 10
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (absβπ) β
β) |
29 | 27 | absge0d 15336 |
. . . . . . . . . 10
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β 0 β€
(absβπ)) |
30 | 28, 29 | ge0p1rpd 12994 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β ((absβπ) + 1) β
β+) |
31 | 25, 30 | rpdivcld 12981 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (π¦ / ((absβπ) + 1)) β
β+) |
32 | 5 | feqmptd 6915 |
. . . . . . . . . 10
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ = (π₯ β dom πΊ β¦ (πΊβπ₯))) |
33 | | simpr 486 |
. . . . . . . . . 10
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ
βπ 0) |
34 | 32, 33 | eqbrtrrd 5134 |
. . . . . . . . 9
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (π₯ β dom πΊ β¦ (πΊβπ₯)) βπ
0) |
35 | 34 | ad2antrr 725 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (π₯ β dom πΊ β¦ (πΊβπ₯)) βπ
0) |
36 | 24, 31, 35 | rlimi 15402 |
. . . . . . 7
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β βπ β β βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) |
37 | | inss1 4193 |
. . . . . . . . . . . . . 14
β’ (dom
πΉ β© dom πΊ) β dom πΉ |
38 | | ssralv 4015 |
. . . . . . . . . . . . . 14
β’ ((dom
πΉ β© dom πΊ) β dom πΉ β (βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
40 | | inss2 4194 |
. . . . . . . . . . . . . 14
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
41 | | ssralv 4015 |
. . . . . . . . . . . . . 14
β’ ((dom
πΉ β© dom πΊ) β dom πΊ β (βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) |
43 | 39, 42 | anim12i 614 |
. . . . . . . . . . . 12
β’
((βπ₯ β
dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
44 | | r19.26 3115 |
. . . . . . . . . . . 12
β’
(βπ₯ β
(dom πΉ β© dom πΊ)((π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ (π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
45 | 43, 44 | sylibr 233 |
. . . . . . . . . . 11
β’
((βπ₯ β
dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β βπ₯ β (dom πΉ β© dom πΊ)((π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ (π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
46 | | anim12 808 |
. . . . . . . . . . . 12
β’ (((π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ (π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β ((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
47 | 46 | ralimi 3087 |
. . . . . . . . . . 11
β’
(βπ₯ β
(dom πΉ β© dom πΊ)((π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ (π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β βπ₯ β (dom πΉ β© dom πΊ)((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
48 | 45, 47 | syl 17 |
. . . . . . . . . 10
β’
((βπ₯ β
dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β βπ₯ β (dom πΉ β© dom πΊ)((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
49 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
50 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
51 | 37, 8 | sstrid 3960 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (dom πΉ β© dom
πΊ) β
β) |
52 | 51 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (dom πΉ β© dom πΊ) β β) |
53 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β (dom πΉ β© dom πΊ)) |
54 | 52, 53 | sseldd 3950 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β β) |
55 | | maxle 13117 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β β§ π₯ β β) β
(if(π β€ π, π, π) β€ π₯ β (π β€ π₯ β§ π β€ π₯))) |
56 | 49, 50, 54, 55 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (if(π β€ π, π, π) β€ π₯ β (π β€ π₯ β§ π β€ π₯))) |
57 | 56 | biimpd 228 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (if(π β€ π, π, π) β€ π₯ β (π β€ π₯ β§ π β€ π₯))) |
58 | 5 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β πΊ:dom πΊβΆβ) |
59 | 40 | sseli 3945 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΊ) |
60 | 59 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β dom πΊ) |
61 | 58, 60 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (πΊβπ₯) β β) |
62 | 61 | subid1d 11508 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((πΊβπ₯) β 0) = (πΊβπ₯)) |
63 | 62 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ((πΊβπ₯) β 0)) = (absβ(πΊβπ₯))) |
64 | 63 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)) β (absβ(πΊβπ₯)) < (π¦ / ((absβπ) + 1)))) |
65 | 61 | abscld 15328 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ(πΊβπ₯)) β β) |
66 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π¦ / ((absβπ) + 1)) β
β+) |
67 | 66 | rpred 12964 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π¦ / ((absβπ) + 1)) β β) |
68 | | ltle 11250 |
. . . . . . . . . . . . . . . . . 18
β’
(((absβ(πΊβπ₯)) β β β§ (π¦ / ((absβπ) + 1)) β β) β
((absβ(πΊβπ₯)) < (π¦ / ((absβπ) + 1)) β (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1)))) |
69 | 65, 67, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ(πΊβπ₯)) < (π¦ / ((absβπ) + 1)) β (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1)))) |
70 | 64, 69 | sylbid 239 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)) β (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1)))) |
71 | 70 | anim2d 613 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) β€ π β§ (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1))))) |
72 | 2 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β πΉ:dom πΉβΆβ) |
73 | 37 | sseli 3945 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΉ) |
74 | 73 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β dom πΉ) |
75 | 72, 74 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (πΉβπ₯) β β) |
76 | 75 | abscld 15328 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ(πΉβπ₯)) β β) |
77 | 75 | absge0d 15336 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β 0 β€ (absβ(πΉβπ₯))) |
78 | 76, 77 | jca 513 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ(πΉβπ₯)) β β β§ 0 β€
(absβ(πΉβπ₯)))) |
79 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
80 | 61 | absge0d 15336 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β 0 β€ (absβ(πΊβπ₯))) |
81 | 65, 80 | jca 513 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ(πΊβπ₯)) β β β§ 0 β€
(absβ(πΊβπ₯)))) |
82 | | lemul12a 12020 |
. . . . . . . . . . . . . . . 16
β’
(((((absβ(πΉβπ₯)) β β β§ 0 β€
(absβ(πΉβπ₯))) β§ π β β) β§ (((absβ(πΊβπ₯)) β β β§ 0 β€
(absβ(πΊβπ₯))) β§ (π¦ / ((absβπ) + 1)) β β)) β
(((absβ(πΉβπ₯)) β€ π β§ (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))))) |
83 | 78, 79, 81, 67, 82 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ(πΉβπ₯)) β€ π β§ (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))))) |
84 | 75, 61 | absmuld 15346 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) = ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯)))) |
85 | 84 | breq1d 5120 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))))) |
86 | 79 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
87 | 25 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π¦ β β+) |
88 | 87 | rpcnd 12966 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π¦ β β) |
89 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β
β+) |
90 | 89 | rpcnd 12966 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β β) |
91 | 89 | rpne0d 12969 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β 0) |
92 | 86, 88, 90, 91 | divassd 11973 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((π Β· π¦) / ((absβπ) + 1)) = (π Β· (π¦ / ((absβπ) + 1)))) |
93 | | peano2re 11335 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((absβπ)
β β β ((absβπ) + 1) β β) |
94 | 28, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β ((absβπ) + 1) β
β) |
95 | 94 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β β) |
96 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβπ) β β) |
97 | 79 | leabsd 15306 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β€ (absβπ)) |
98 | 96 | ltp1d 12092 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβπ) < ((absβπ) + 1)) |
99 | 79, 96, 95, 97, 98 | lelttrd 11320 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π < ((absβπ) + 1)) |
100 | 79, 95, 87, 99 | ltmul1dd 13019 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· π¦) < (((absβπ) + 1) Β· π¦)) |
101 | 87 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π¦ β β) |
102 | 79, 101 | remulcld 11192 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· π¦) β β) |
103 | 102, 101,
89 | ltdivmuld 13015 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((π Β· π¦) / ((absβπ) + 1)) < π¦ β (π Β· π¦) < (((absβπ) + 1) Β· π¦))) |
104 | 100, 103 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((π Β· π¦) / ((absβπ) + 1)) < π¦) |
105 | 92, 104 | eqbrtrrd 5134 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· (π¦ / ((absβπ) + 1))) < π¦) |
106 | 75, 61 | mulcld 11182 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((πΉβπ₯) Β· (πΊβπ₯)) β β) |
107 | 106 | abscld 15328 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) β β) |
108 | 79, 67 | remulcld 11192 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· (π¦ / ((absβπ) + 1))) β β) |
109 | | lelttr 11252 |
. . . . . . . . . . . . . . . . . 18
β’
(((absβ((πΉβπ₯) Β· (πΊβπ₯))) β β β§ (π Β· (π¦ / ((absβπ) + 1))) β β β§ π¦ β β) β
(((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β§ (π Β· (π¦ / ((absβπ) + 1))) < π¦) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
110 | 107, 108,
101, 109 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β§ (π Β· (π¦ / ((absβπ) + 1))) < π¦) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
111 | 105, 110 | mpan2d 693 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
112 | 85, 111 | sylbird 260 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
113 | 71, 83, 112 | 3syld 60 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
114 | 57, 113 | imim12d 81 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
115 | 114 | anassrs 469 |
. . . . . . . . . . . 12
β’
((((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β§ π₯ β (dom πΉ β© dom πΊ)) β (((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
116 | 115 | ralimdva 3165 |
. . . . . . . . . . 11
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
(βπ₯ β (dom
πΉ β© dom πΊ)((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β βπ₯ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
117 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β π β
β) |
118 | | simplrl 776 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β π β
β) |
119 | 117, 118 | ifcld 4537 |
. . . . . . . . . . 11
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β if(π β€ π, π, π) β β) |
120 | 116, 119 | jctild 527 |
. . . . . . . . . 10
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
(βπ₯ β (dom
πΉ β© dom πΊ)((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (if(π β€ π, π, π) β β β§ βπ₯ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)))) |
121 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π§ = if(π β€ π, π, π) β (π§ β€ π₯ β if(π β€ π, π, π) β€ π₯)) |
122 | 121 | rspceaimv 3588 |
. . . . . . . . . 10
β’
((if(π β€ π, π, π) β β β§ βπ₯ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
123 | 48, 120, 122 | syl56 36 |
. . . . . . . . 9
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
((βπ₯ β dom
πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
124 | 123 | expcomd 418 |
. . . . . . . 8
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
(βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β (βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)))) |
125 | 124 | rexlimdva 3153 |
. . . . . . 7
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (βπ β β βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β (βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)))) |
126 | 36, 125 | mpd 15 |
. . . . . 6
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
127 | 126 | rexlimdvva 3206 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β (βπ β β βπ β β βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
128 | 22, 127 | mpd 15 |
. . . 4
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
129 | 128 | ralrimiva 3144 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β βπ¦ β
β+ βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
130 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((πΉ:dom πΉβΆβ β§ π₯ β dom πΉ) β (πΉβπ₯) β β) |
131 | 2, 73, 130 | syl2an 597 |
. . . . . 6
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β (dom πΉ β© dom πΊ)) β (πΉβπ₯) β β) |
132 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((πΊ:dom πΊβΆβ β§ π₯ β dom πΊ) β (πΊβπ₯) β β) |
133 | 5, 59, 132 | syl2an 597 |
. . . . . 6
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β (dom πΉ β© dom πΊ)) β (πΊβπ₯) β β) |
134 | 131, 133 | mulcld 11182 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β (dom πΉ β© dom πΊ)) β ((πΉβπ₯) Β· (πΊβπ₯)) β β) |
135 | 134 | ralrimiva 3144 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β βπ₯ β
(dom πΉ β© dom πΊ)((πΉβπ₯) Β· (πΊβπ₯)) β β) |
136 | 135, 51 | rlim0 15397 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β ((π₯ β (dom
πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) βπ 0 β
βπ¦ β
β+ βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
137 | 129, 136 | mpbird 257 |
. 2
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) βπ
0) |
138 | 19, 137 | eqbrtrd 5132 |
1
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (πΉ
βf Β· πΊ) βπ
0) |