Step | Hyp | Ref
| Expression |
1 | | rlimcl 15391 |
. . . 4
β’ ((π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ β πΆ β β) |
2 | 1 | a1i 11 |
. . 3
β’ (π β ((π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ β πΆ β β)) |
3 | | rlimcl 15391 |
. . . 4
β’ ((π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ β πΆ β β) |
4 | 3 | a1i 11 |
. . 3
β’ (π β ((π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ β πΆ β β)) |
5 | | rlimresb.2 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β β) |
6 | 5 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π΄ β β) |
7 | | simprrl 780 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π₯ β π΄) |
8 | 6, 7 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π₯ β β) |
9 | | rlimresb.3 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΅ β β) |
10 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π΅ β β) |
11 | | elicopnf 13368 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΅ β β β (π§ β (π΅[,)+β) β (π§ β β β§ π΅ β€ π§))) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π§ β (π΅[,)+β) β (π§ β β β§ π΅ β€ π§))) |
13 | 12 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π§ β (π΅[,)+β)) β (π§ β β β§ π΅ β€ π§)) |
14 | 13 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β (π§ β β β§ π΅ β€ π§)) |
15 | 14 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π§ β β) |
16 | 14 | simprd 497 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π΅ β€ π§) |
17 | | simprrr 781 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π§ β€ π₯) |
18 | 10, 15, 8, 16, 17 | letrd 11317 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π΅ β€ π₯) |
19 | | elicopnf 13368 |
. . . . . . . . . . . . . . . . . 18
β’ (π΅ β β β (π₯ β (π΅[,)+β) β (π₯ β β β§ π΅ β€ π₯))) |
20 | 10, 19 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β (π₯ β (π΅[,)+β) β (π₯ β β β§ π΅ β€ π₯))) |
21 | 8, 18, 20 | mpbir2and 712 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π§ β (π΅[,)+β) β§ (π₯ β π΄ β§ π§ β€ π₯))) β π₯ β (π΅[,)+β)) |
22 | 21 | anassrs 469 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β (π΅[,)+β)) β§ (π₯ β π΄ β§ π§ β€ π₯)) β π₯ β (π΅[,)+β)) |
23 | 22 | anassrs 469 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π§ β (π΅[,)+β)) β§ π₯ β π΄) β§ π§ β€ π₯) β π₯ β (π΅[,)+β)) |
24 | | biimt 361 |
. . . . . . . . . . . . . 14
β’ (π₯ β (π΅[,)+β) β ((absβ((πΉβπ₯) β πΆ)) < π¦ β (π₯ β (π΅[,)+β) β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π§ β (π΅[,)+β)) β§ π₯ β π΄) β§ π§ β€ π₯) β ((absβ((πΉβπ₯) β πΆ)) < π¦ β (π₯ β (π΅[,)+β) β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
26 | 25 | pm5.74da 803 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (π΅[,)+β)) β§ π₯ β π΄) β ((π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦) β (π§ β€ π₯ β (π₯ β (π΅[,)+β) β (absβ((πΉβπ₯) β πΆ)) < π¦)))) |
27 | | bi2.04 389 |
. . . . . . . . . . . 12
β’ ((π§ β€ π₯ β (π₯ β (π΅[,)+β) β (absβ((πΉβπ₯) β πΆ)) < π¦)) β (π₯ β (π΅[,)+β) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
28 | 26, 27 | bitrdi 287 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (π΅[,)+β)) β§ π₯ β π΄) β ((π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦) β (π₯ β (π΅[,)+β) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)))) |
29 | 28 | pm5.74da 803 |
. . . . . . . . . 10
β’ ((π β§ π§ β (π΅[,)+β)) β ((π₯ β π΄ β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)) β (π₯ β π΄ β (π₯ β (π΅[,)+β) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))))) |
30 | | elin 3927 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄ β© (π΅[,)+β)) β (π₯ β π΄ β§ π₯ β (π΅[,)+β))) |
31 | 30 | imbi1i 350 |
. . . . . . . . . . 11
β’ ((π₯ β (π΄ β© (π΅[,)+β)) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)) β ((π₯ β π΄ β§ π₯ β (π΅[,)+β)) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
32 | | impexp 452 |
. . . . . . . . . . 11
β’ (((π₯ β π΄ β§ π₯ β (π΅[,)+β)) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)) β (π₯ β π΄ β (π₯ β (π΅[,)+β) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)))) |
33 | 31, 32 | bitri 275 |
. . . . . . . . . 10
β’ ((π₯ β (π΄ β© (π΅[,)+β)) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)) β (π₯ β π΄ β (π₯ β (π΅[,)+β) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)))) |
34 | 29, 33 | bitr4di 289 |
. . . . . . . . 9
β’ ((π β§ π§ β (π΅[,)+β)) β ((π₯ β π΄ β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)) β (π₯ β (π΄ β© (π΅[,)+β)) β (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦)))) |
35 | 34 | ralbidv2 3167 |
. . . . . . . 8
β’ ((π β§ π§ β (π΅[,)+β)) β (βπ₯ β π΄ (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦) β βπ₯ β (π΄ β© (π΅[,)+β))(π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
36 | 35 | rexbidva 3170 |
. . . . . . 7
β’ (π β (βπ§ β (π΅[,)+β)βπ₯ β π΄ (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦) β βπ§ β (π΅[,)+β)βπ₯ β (π΄ β© (π΅[,)+β))(π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
37 | 36 | ralbidv 3171 |
. . . . . 6
β’ (π β (βπ¦ β β+
βπ§ β (π΅[,)+β)βπ₯ β π΄ (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦) β βπ¦ β β+ βπ§ β (π΅[,)+β)βπ₯ β (π΄ β© (π΅[,)+β))(π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β β) β (βπ¦ β β+
βπ§ β (π΅[,)+β)βπ₯ β π΄ (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦) β βπ¦ β β+ βπ§ β (π΅[,)+β)βπ₯ β (π΄ β© (π΅[,)+β))(π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
39 | | rlimresb.1 |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆβ) |
40 | 39 | ffvelcdmda 7036 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) β β) |
41 | 40 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ₯ β π΄ (πΉβπ₯) β β) |
42 | 41 | adantr 482 |
. . . . . 6
β’ ((π β§ πΆ β β) β βπ₯ β π΄ (πΉβπ₯) β β) |
43 | 5 | adantr 482 |
. . . . . 6
β’ ((π β§ πΆ β β) β π΄ β β) |
44 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΆ β β) β πΆ β β) |
45 | 9 | adantr 482 |
. . . . . 6
β’ ((π β§ πΆ β β) β π΅ β β) |
46 | 42, 43, 44, 45 | rlim3 15386 |
. . . . 5
β’ ((π β§ πΆ β β) β ((π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ β βπ¦ β β+
βπ§ β (π΅[,)+β)βπ₯ β π΄ (π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
47 | | elinel1 4156 |
. . . . . . . . 9
β’ (π₯ β (π΄ β© (π΅[,)+β)) β π₯ β π΄) |
48 | 47, 40 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄ β© (π΅[,)+β))) β (πΉβπ₯) β β) |
49 | 48 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ₯ β (π΄ β© (π΅[,)+β))(πΉβπ₯) β β) |
50 | 49 | adantr 482 |
. . . . . 6
β’ ((π β§ πΆ β β) β βπ₯ β (π΄ β© (π΅[,)+β))(πΉβπ₯) β β) |
51 | | inss1 4189 |
. . . . . . . 8
β’ (π΄ β© (π΅[,)+β)) β π΄ |
52 | 51, 5 | sstrid 3956 |
. . . . . . 7
β’ (π β (π΄ β© (π΅[,)+β)) β
β) |
53 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ πΆ β β) β (π΄ β© (π΅[,)+β)) β
β) |
54 | 50, 53, 44, 45 | rlim3 15386 |
. . . . 5
β’ ((π β§ πΆ β β) β ((π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ β βπ¦ β β+
βπ§ β (π΅[,)+β)βπ₯ β (π΄ β© (π΅[,)+β))(π§ β€ π₯ β (absβ((πΉβπ₯) β πΆ)) < π¦))) |
55 | 38, 46, 54 | 3bitr4d 311 |
. . . 4
β’ ((π β§ πΆ β β) β ((π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ β (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ)) |
56 | 55 | ex 414 |
. . 3
β’ (π β (πΆ β β β ((π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ β (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ))) |
57 | 2, 4, 56 | pm5.21ndd 381 |
. 2
β’ (π β ((π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ β (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ)) |
58 | 39 | feqmptd 6911 |
. . 3
β’ (π β πΉ = (π₯ β π΄ β¦ (πΉβπ₯))) |
59 | 58 | breq1d 5116 |
. 2
β’ (π β (πΉ βπ πΆ β (π₯ β π΄ β¦ (πΉβπ₯)) βπ πΆ)) |
60 | | resres 5951 |
. . . 4
β’ ((πΉ βΎ π΄) βΎ (π΅[,)+β)) = (πΉ βΎ (π΄ β© (π΅[,)+β))) |
61 | | ffn 6669 |
. . . . . 6
β’ (πΉ:π΄βΆβ β πΉ Fn π΄) |
62 | | fnresdm 6621 |
. . . . . 6
β’ (πΉ Fn π΄ β (πΉ βΎ π΄) = πΉ) |
63 | 39, 61, 62 | 3syl 18 |
. . . . 5
β’ (π β (πΉ βΎ π΄) = πΉ) |
64 | 63 | reseq1d 5937 |
. . . 4
β’ (π β ((πΉ βΎ π΄) βΎ (π΅[,)+β)) = (πΉ βΎ (π΅[,)+β))) |
65 | 58 | reseq1d 5937 |
. . . . 5
β’ (π β (πΉ βΎ (π΄ β© (π΅[,)+β))) = ((π₯ β π΄ β¦ (πΉβπ₯)) βΎ (π΄ β© (π΅[,)+β)))) |
66 | | resmpt 5992 |
. . . . . 6
β’ ((π΄ β© (π΅[,)+β)) β π΄ β ((π₯ β π΄ β¦ (πΉβπ₯)) βΎ (π΄ β© (π΅[,)+β))) = (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯))) |
67 | 51, 66 | ax-mp 5 |
. . . . 5
β’ ((π₯ β π΄ β¦ (πΉβπ₯)) βΎ (π΄ β© (π΅[,)+β))) = (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) |
68 | 65, 67 | eqtrdi 2789 |
. . . 4
β’ (π β (πΉ βΎ (π΄ β© (π΅[,)+β))) = (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯))) |
69 | 60, 64, 68 | 3eqtr3a 2797 |
. . 3
β’ (π β (πΉ βΎ (π΅[,)+β)) = (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯))) |
70 | 69 | breq1d 5116 |
. 2
β’ (π β ((πΉ βΎ (π΅[,)+β)) βπ
πΆ β (π₯ β (π΄ β© (π΅[,)+β)) β¦ (πΉβπ₯)) βπ πΆ)) |
71 | 57, 59, 70 | 3bitr4d 311 |
1
β’ (π β (πΉ βπ πΆ β (πΉ βΎ (π΅[,)+β)) βπ
πΆ)) |