Step | Hyp | Ref
| Expression |
1 | | rlim2.1 |
. . . 4
β’ (π β βπ§ β π΄ π΅ β β) |
2 | | eqid 2733 |
. . . . 5
β’ (π§ β π΄ β¦ π΅) = (π§ β π΄ β¦ π΅) |
3 | 2 | fmpt 7110 |
. . . 4
β’
(βπ§ β
π΄ π΅ β β β (π§ β π΄ β¦ π΅):π΄βΆβ) |
4 | 1, 3 | sylib 217 |
. . 3
β’ (π β (π§ β π΄ β¦ π΅):π΄βΆβ) |
5 | | rlim2.2 |
. . 3
β’ (π β π΄ β β) |
6 | | eqidd 2734 |
. . 3
β’ ((π β§ π€ β π΄) β ((π§ β π΄ β¦ π΅)βπ€) = ((π§ β π΄ β¦ π΅)βπ€)) |
7 | 4, 5, 6 | rlim 15439 |
. 2
β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β (πΆ β β β§ βπ₯ β β+
βπ¦ β β
βπ€ β π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯)))) |
8 | | rlim2.3 |
. . 3
β’ (π β πΆ β β) |
9 | 8 | biantrurd 534 |
. 2
β’ (π β (βπ₯ β β+
βπ¦ β β
βπ€ β π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) β (πΆ β β β§ βπ₯ β β+
βπ¦ β β
βπ€ β π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯)))) |
10 | | nfv 1918 |
. . . . . . 7
β’
β²π§ π¦ β€ π€ |
11 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π§abs |
12 | | nffvmpt1 6903 |
. . . . . . . . . 10
β’
β²π§((π§ β π΄ β¦ π΅)βπ€) |
13 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π§
β |
14 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π§πΆ |
15 | 12, 13, 14 | nfov 7439 |
. . . . . . . . 9
β’
β²π§(((π§ β π΄ β¦ π΅)βπ€) β πΆ) |
16 | 11, 15 | nffv 6902 |
. . . . . . . 8
β’
β²π§(absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) |
17 | | nfcv 2904 |
. . . . . . . 8
β’
β²π§
< |
18 | | nfcv 2904 |
. . . . . . . 8
β’
β²π§π₯ |
19 | 16, 17, 18 | nfbr 5196 |
. . . . . . 7
β’
β²π§(absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯ |
20 | 10, 19 | nfim 1900 |
. . . . . 6
β’
β²π§(π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) |
21 | | nfv 1918 |
. . . . . 6
β’
β²π€(π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯) |
22 | | breq2 5153 |
. . . . . . 7
β’ (π€ = π§ β (π¦ β€ π€ β π¦ β€ π§)) |
23 | 22 | imbrov2fvoveq 7434 |
. . . . . 6
β’ (π€ = π§ β ((π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) β (π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯))) |
24 | 20, 21, 23 | cbvralw 3304 |
. . . . 5
β’
(βπ€ β
π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) β βπ§ β π΄ (π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯)) |
25 | 2 | fvmpt2 7010 |
. . . . . . . . . 10
β’ ((π§ β π΄ β§ π΅ β β) β ((π§ β π΄ β¦ π΅)βπ§) = π΅) |
26 | 25 | fvoveq1d 7431 |
. . . . . . . . 9
β’ ((π§ β π΄ β§ π΅ β β) β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) = (absβ(π΅ β πΆ))) |
27 | 26 | breq1d 5159 |
. . . . . . . 8
β’ ((π§ β π΄ β§ π΅ β β) β ((absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯ β (absβ(π΅ β πΆ)) < π₯)) |
28 | 27 | imbi2d 341 |
. . . . . . 7
β’ ((π§ β π΄ β§ π΅ β β) β ((π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯) β (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
29 | 28 | ralimiaa 3083 |
. . . . . 6
β’
(βπ§ β
π΄ π΅ β β β βπ§ β π΄ ((π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯) β (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
30 | | ralbi 3104 |
. . . . . 6
β’
(βπ§ β
π΄ ((π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯) β (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯)) β (βπ§ β π΄ (π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯) β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
31 | 1, 29, 30 | 3syl 18 |
. . . . 5
β’ (π β (βπ§ β π΄ (π¦ β€ π§ β (absβ(((π§ β π΄ β¦ π΅)βπ§) β πΆ)) < π₯) β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
32 | 24, 31 | bitrid 283 |
. . . 4
β’ (π β (βπ€ β π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
33 | 32 | rexbidv 3179 |
. . 3
β’ (π β (βπ¦ β β βπ€ β π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) β βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
34 | 33 | ralbidv 3178 |
. 2
β’ (π β (βπ₯ β β+
βπ¦ β β
βπ€ β π΄ (π¦ β€ π€ β (absβ(((π§ β π΄ β¦ π΅)βπ€) β πΆ)) < π₯) β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
35 | 7, 9, 34 | 3bitr2d 307 |
1
β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+
βπ¦ β β
βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |