Step | Hyp | Ref
| Expression |
1 | | o1f 15469 |
. . . . 5
β’ (πΉ β π(1) β
πΉ:dom πΉβΆβ) |
2 | 1 | adantr 481 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΉ:dom πΉβΆβ) |
3 | 2 | ffnd 6715 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΉ Fn dom πΉ) |
4 | | rlimf 15441 |
. . . . 5
β’ (πΊ βπ 0
β πΊ:dom πΊβΆβ) |
5 | 4 | adantl 482 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ:dom πΊβΆβ) |
6 | 5 | ffnd 6715 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ Fn dom πΊ) |
7 | | o1dm 15470 |
. . . . 5
β’ (πΉ β π(1) β dom
πΉ β
β) |
8 | 7 | adantr 481 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΉ β
β) |
9 | | reex 11197 |
. . . 4
β’ β
β V |
10 | | ssexg 5322 |
. . . 4
β’ ((dom
πΉ β β β§
β β V) β dom πΉ β V) |
11 | 8, 9, 10 | sylancl 586 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΉ β
V) |
12 | | rlimss 15442 |
. . . . 5
β’ (πΊ βπ 0
β dom πΊ β
β) |
13 | 12 | adantl 482 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΊ β
β) |
14 | | ssexg 5322 |
. . . 4
β’ ((dom
πΊ β β β§
β β V) β dom πΊ β V) |
15 | 13, 9, 14 | sylancl 586 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β dom πΊ β
V) |
16 | | eqid 2732 |
. . 3
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
17 | | eqidd 2733 |
. . 3
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β dom πΉ) β (πΉβπ₯) = (πΉβπ₯)) |
18 | | eqidd 2733 |
. . 3
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β dom πΊ) β (πΊβπ₯) = (πΊβπ₯)) |
19 | 3, 6, 11, 15, 16, 17, 18 | offval 7675 |
. 2
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (πΉ
βf Β· πΊ) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
20 | | o1bdd 15471 |
. . . . . . 7
β’ ((πΉ β π(1) β§ πΉ:dom πΉβΆβ) β βπ β β βπ β β βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
21 | 1, 20 | mpdan 685 |
. . . . . 6
β’ (πΉ β π(1) β
βπ β β
βπ β β
βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
22 | 21 | ad2antrr 724 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β βπ β β βπ β β βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
23 | | fvexd 6903 |
. . . . . . . . 9
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π₯ β dom πΊ) β (πΊβπ₯) β V) |
24 | 23 | ralrimiva 3146 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β βπ₯ β dom πΊ(πΊβπ₯) β V) |
25 | | simplr 767 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β π¦ β β+) |
26 | | recn 11196 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
27 | 26 | ad2antll 727 |
. . . . . . . . . . 11
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β π β β) |
28 | 27 | abscld 15379 |
. . . . . . . . . 10
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (absβπ) β
β) |
29 | 27 | absge0d 15387 |
. . . . . . . . . 10
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β 0 β€
(absβπ)) |
30 | 28, 29 | ge0p1rpd 13042 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β ((absβπ) + 1) β
β+) |
31 | 25, 30 | rpdivcld 13029 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (π¦ / ((absβπ) + 1)) β
β+) |
32 | 5 | feqmptd 6957 |
. . . . . . . . . 10
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ = (π₯ β dom πΊ β¦ (πΊβπ₯))) |
33 | | simpr 485 |
. . . . . . . . . 10
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β πΊ
βπ 0) |
34 | 32, 33 | eqbrtrrd 5171 |
. . . . . . . . 9
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (π₯ β dom πΊ β¦ (πΊβπ₯)) βπ
0) |
35 | 34 | ad2antrr 724 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β (π₯ β dom πΊ β¦ (πΊβπ₯)) βπ
0) |
36 | 24, 31, 35 | rlimi 15453 |
. . . . . . 7
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β βπ β β βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) |
37 | | inss1 4227 |
. . . . . . . . . . . . . 14
β’ (dom
πΉ β© dom πΊ) β dom πΉ |
38 | | ssralv 4049 |
. . . . . . . . . . . . . 14
β’ ((dom
πΉ β© dom πΊ) β dom πΉ β (βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π))) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π)) |
40 | | inss2 4228 |
. . . . . . . . . . . . . 14
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
41 | | ssralv 4049 |
. . . . . . . . . . . . . 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 613 |
. . . . . . . . . . . 12
β’
((βπ₯ β
dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ βπ₯ β (dom πΉ β© dom πΊ)(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
44 | | r19.26 3111 |
. . . . . . . . . . . 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 807 |
. . . . . . . . . . . 12
β’ (((π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β§ (π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β ((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))))) |
47 | 46 | ralimi 3083 |
. . . . . . . . . . 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 775 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
50 | | simprl 769 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
51 | 37, 8 | sstrid 3992 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (dom πΉ β© dom
πΊ) β
β) |
52 | 51 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (dom πΉ β© dom πΊ) β β) |
53 | | simprr 771 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β (dom πΉ β© dom πΊ)) |
54 | 52, 53 | sseldd 3982 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β β) |
55 | | maxle 13166 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β β§ π₯ β β) β
(if(π β€ π, π, π) β€ π₯ β (π β€ π₯ β§ π β€ π₯))) |
56 | 49, 50, 54, 55 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (if(π β€ π, π, π) β€ π₯ β (π β€ π₯ β§ π β€ π₯))) |
57 | 56 | biimpd 228 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (if(π β€ π, π, π) β€ π₯ β (π β€ π₯ β§ π β€ π₯))) |
58 | 5 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β πΊ:dom πΊβΆβ) |
59 | 40 | sseli 3977 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΊ) |
60 | 59 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β dom πΊ) |
61 | 58, 60 | ffvelcdmd 7084 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (πΊβπ₯) β β) |
62 | 61 | subid1d 11556 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((πΊβπ₯) β 0) = (πΊβπ₯)) |
63 | 62 | fveq2d 6892 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ((πΊβπ₯) β 0)) = (absβ(πΊβπ₯))) |
64 | 63 | breq1d 5157 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)) β (absβ(πΊβπ₯)) < (π¦ / ((absβπ) + 1)))) |
65 | 61 | abscld 15379 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ(πΊβπ₯)) β β) |
66 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π¦ / ((absβπ) + 1)) β
β+) |
67 | 66 | rpred 13012 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π¦ / ((absβπ) + 1)) β β) |
68 | | ltle 11298 |
. . . . . . . . . . . . . . . . . 18
β’
(((absβ(πΊβπ₯)) β β β§ (π¦ / ((absβπ) + 1)) β β) β
((absβ(πΊβπ₯)) < (π¦ / ((absβπ) + 1)) β (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1)))) |
69 | 65, 67, 68 | syl2anc 584 |
. . . . . . . . . . . . . . . . 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 612 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) β€ π β§ (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1))))) |
72 | 2 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β πΉ:dom πΉβΆβ) |
73 | 37 | sseli 3977 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΉ) |
74 | 73 | ad2antll 727 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π₯ β dom πΉ) |
75 | 72, 74 | ffvelcdmd 7084 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (πΉβπ₯) β β) |
76 | 75 | abscld 15379 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ(πΉβπ₯)) β β) |
77 | 75 | absge0d 15387 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β 0 β€ (absβ(πΉβπ₯))) |
78 | 76, 77 | jca 512 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ(πΉβπ₯)) β β β§ 0 β€
(absβ(πΉβπ₯)))) |
79 | | simplrr 776 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
80 | 61 | absge0d 15387 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β 0 β€ (absβ(πΊβπ₯))) |
81 | 65, 80 | jca 512 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ(πΊβπ₯)) β β β§ 0 β€
(absβ(πΊβπ₯)))) |
82 | | lemul12a 12068 |
. . . . . . . . . . . . . . . 16
β’
(((((absβ(πΉβπ₯)) β β β§ 0 β€
(absβ(πΉβπ₯))) β§ π β β) β§ (((absβ(πΊβπ₯)) β β β§ 0 β€
(absβ(πΊβπ₯))) β§ (π¦ / ((absβπ) + 1)) β β)) β
(((absβ(πΉβπ₯)) β€ π β§ (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))))) |
83 | 78, 79, 81, 67, 82 | syl22anc 837 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ(πΉβπ₯)) β€ π β§ (absβ(πΊβπ₯)) β€ (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))))) |
84 | 75, 61 | absmuld 15397 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) = ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯)))) |
85 | 84 | breq1d 5157 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β ((absβ(πΉβπ₯)) Β· (absβ(πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))))) |
86 | 79 | recnd 11238 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β β) |
87 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π¦ β β+) |
88 | 87 | rpcnd 13014 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π¦ β β) |
89 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β
β+) |
90 | 89 | rpcnd 13014 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β β) |
91 | 89 | rpne0d 13017 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β 0) |
92 | 86, 88, 90, 91 | divassd 12021 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((π Β· π¦) / ((absβπ) + 1)) = (π Β· (π¦ / ((absβπ) + 1)))) |
93 | | peano2re 11383 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((absβπ)
β β β ((absβπ) + 1) β β) |
94 | 28, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β§ (π β β β§ π β β)) β ((absβπ) + 1) β
β) |
95 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβπ) + 1) β β) |
96 | 28 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβπ) β β) |
97 | 79 | leabsd 15357 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π β€ (absβπ)) |
98 | 96 | ltp1d 12140 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβπ) < ((absβπ) + 1)) |
99 | 79, 96, 95, 97, 98 | lelttrd 11368 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π < ((absβπ) + 1)) |
100 | 79, 95, 87, 99 | ltmul1dd 13067 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· π¦) < (((absβπ) + 1) Β· π¦)) |
101 | 87 | rpred 13012 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β π¦ β β) |
102 | 79, 101 | remulcld 11240 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· π¦) β β) |
103 | 102, 101,
89 | ltdivmuld 13063 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((π Β· π¦) / ((absβπ) + 1)) < π¦ β (π Β· π¦) < (((absβπ) + 1) Β· π¦))) |
104 | 100, 103 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((π Β· π¦) / ((absβπ) + 1)) < π¦) |
105 | 92, 104 | eqbrtrrd 5171 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· (π¦ / ((absβπ) + 1))) < π¦) |
106 | 75, 61 | mulcld 11230 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((πΉβπ₯) Β· (πΊβπ₯)) β β) |
107 | 106 | abscld 15379 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) β β) |
108 | 79, 67 | remulcld 11240 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (π Β· (π¦ / ((absβπ) + 1))) β β) |
109 | | lelttr 11300 |
. . . . . . . . . . . . . . . . . 18
β’
(((absβ((πΉβπ₯) Β· (πΊβπ₯))) β β β§ (π Β· (π¦ / ((absβπ) + 1))) β β β§ π¦ β β) β
(((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β§ (π Β· (π¦ / ((absβπ) + 1))) < π¦) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
110 | 107, 108,
101, 109 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β (((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β§ (π Β· (π¦ / ((absβπ) + 1))) < π¦) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
111 | 105, 110 | mpan2d 692 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ (π β β β§ π₯ β (dom πΉ β© dom πΊ))) β ((absβ((πΉβπ₯) Β· (πΊβπ₯))) β€ (π Β· (π¦ / ((absβπ) + 1))) β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
112 | 85, 111 | sylbird 259 |
. . . . . . . . . . . . . . 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 468 |
. . . . . . . . . . . 12
β’
((((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β§ π₯ β (dom πΉ β© dom πΊ)) β (((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
116 | 115 | ralimdva 3167 |
. . . . . . . . . . 11
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
(βπ₯ β (dom
πΉ β© dom πΊ)((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β βπ₯ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
117 | | simpr 485 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β π β
β) |
118 | | simplrl 775 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β π β
β) |
119 | 117, 118 | ifcld 4573 |
. . . . . . . . . . 11
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β if(π β€ π, π, π) β β) |
120 | 116, 119 | jctild 526 |
. . . . . . . . . 10
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
(βπ₯ β (dom
πΉ β© dom πΊ)((π β€ π₯ β§ π β€ π₯) β ((absβ(πΉβπ₯)) β€ π β§ (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1)))) β (if(π β€ π, π, π) β β β§ βπ₯ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)))) |
121 | | breq1 5150 |
. . . . . . . . . . 11
β’ (π§ = if(π β€ π, π, π) β (π§ β€ π₯ β if(π β€ π, π, π) β€ π₯)) |
122 | 121 | rspceaimv 3616 |
. . . . . . . . . 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 417 |
. . . . . . . 8
β’
(((((πΉ β
π(1) β§ πΊ
βπ 0) β§ π¦ β β+) β§ (π β β β§ π β β)) β§ π β β) β
(βπ₯ β dom πΊ(π β€ π₯ β (absβ((πΊβπ₯) β 0)) < (π¦ / ((absβπ) + 1))) β (βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)))) |
125 | 124 | rexlimdva 3155 |
. . . . . . 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 3211 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β (βπ β β βπ β β βπ₯ β dom πΉ(π β€ π₯ β (absβ(πΉβπ₯)) β€ π) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
128 | 22, 127 | mpd 15 |
. . . 4
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π¦ β
β+) β βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
129 | 128 | ralrimiva 3146 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β βπ¦ β
β+ βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦)) |
130 | | ffvelcdm 7080 |
. . . . . . 7
β’ ((πΉ:dom πΉβΆβ β§ π₯ β dom πΉ) β (πΉβπ₯) β β) |
131 | 2, 73, 130 | syl2an 596 |
. . . . . 6
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β (dom πΉ β© dom πΊ)) β (πΉβπ₯) β β) |
132 | | ffvelcdm 7080 |
. . . . . . 7
β’ ((πΊ:dom πΊβΆβ β§ π₯ β dom πΊ) β (πΊβπ₯) β β) |
133 | 5, 59, 132 | syl2an 596 |
. . . . . 6
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β (dom πΉ β© dom πΊ)) β (πΊβπ₯) β β) |
134 | 131, 133 | mulcld 11230 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ βπ 0)
β§ π₯ β (dom πΉ β© dom πΊ)) β ((πΉβπ₯) Β· (πΊβπ₯)) β β) |
135 | 134 | ralrimiva 3146 |
. . . 4
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β βπ₯ β
(dom πΉ β© dom πΊ)((πΉβπ₯) Β· (πΊβπ₯)) β β) |
136 | 135, 51 | rlim0 15448 |
. . 3
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β ((π₯ β (dom
πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) βπ 0 β
βπ¦ β
β+ βπ§ β β βπ₯ β (dom πΉ β© dom πΊ)(π§ β€ π₯ β (absβ((πΉβπ₯) Β· (πΊβπ₯))) < π¦))) |
137 | 129, 136 | mpbird 256 |
. 2
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) βπ
0) |
138 | 19, 137 | eqbrtrd 5169 |
1
β’ ((πΉ β π(1) β§ πΊ βπ 0)
β (πΉ
βf Β· πΊ) βπ
0) |