Step | Hyp | Ref
| Expression |
1 | | rlimadd.3 |
. . . 4
β’ ((π β§ π₯ β π΄) β π΅ β π) |
2 | | rlimadd.5 |
. . . 4
β’ (π β (π₯ β π΄ β¦ π΅) βπ π·) |
3 | 1, 2 | rlimmptrcl 15496 |
. . 3
β’ ((π β§ π₯ β π΄) β π΅ β β) |
4 | | rlimadd.4 |
. . . . 5
β’ ((π β§ π₯ β π΄) β πΆ β π) |
5 | | rlimadd.6 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ πΆ) βπ πΈ) |
6 | 4, 5 | rlimmptrcl 15496 |
. . . 4
β’ ((π β§ π₯ β π΄) β πΆ β β) |
7 | | rlimdiv.8 |
. . . 4
β’ ((π β§ π₯ β π΄) β πΆ β 0) |
8 | 6, 7 | reccld 11929 |
. . 3
β’ ((π β§ π₯ β π΄) β (1 / πΆ) β β) |
9 | | eldifsn 4748 |
. . . . . . 7
β’ (πΆ β (β β {0})
β (πΆ β β
β§ πΆ β
0)) |
10 | 6, 7, 9 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β πΆ β (β β
{0})) |
11 | 10 | fmpttd 7064 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ πΆ):π΄βΆ(β β
{0})) |
12 | | rlimcl 15391 |
. . . . . . 7
β’ ((π₯ β π΄ β¦ πΆ) βπ πΈ β πΈ β β) |
13 | 5, 12 | syl 17 |
. . . . . 6
β’ (π β πΈ β β) |
14 | | rlimdiv.7 |
. . . . . 6
β’ (π β πΈ β 0) |
15 | | eldifsn 4748 |
. . . . . 6
β’ (πΈ β (β β {0})
β (πΈ β β
β§ πΈ β
0)) |
16 | 13, 14, 15 | sylanbrc 584 |
. . . . 5
β’ (π β πΈ β (β β
{0})) |
17 | | eldifsn 4748 |
. . . . . . . 8
β’ (π¦ β (β β {0})
β (π¦ β β
β§ π¦ β
0)) |
18 | | reccl 11825 |
. . . . . . . 8
β’ ((π¦ β β β§ π¦ β 0) β (1 / π¦) β
β) |
19 | 17, 18 | sylbi 216 |
. . . . . . 7
β’ (π¦ β (β β {0})
β (1 / π¦) β
β) |
20 | 19 | adantl 483 |
. . . . . 6
β’ ((π β§ π¦ β (β β {0})) β (1 /
π¦) β
β) |
21 | 20 | fmpttd 7064 |
. . . . 5
β’ (π β (π¦ β (β β {0}) β¦ (1 /
π¦)):(β β
{0})βΆβ) |
22 | | eqid 2733 |
. . . . . . . 8
β’ (if(1
β€ ((absβπΈ)
Β· π§), 1,
((absβπΈ) Β·
π§)) Β·
((absβπΈ) / 2)) =
(if(1 β€ ((absβπΈ)
Β· π§), 1,
((absβπΈ) Β·
π§)) Β·
((absβπΈ) /
2)) |
23 | 22 | reccn2 15485 |
. . . . . . 7
β’ ((πΈ β (β β {0})
β§ π§ β
β+) β βπ€ β β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ((1 / π£) β (1 / πΈ))) < π§)) |
24 | 16, 23 | sylan 581 |
. . . . . 6
β’ ((π β§ π§ β β+) β
βπ€ β
β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ((1 / π£) β (1 / πΈ))) < π§)) |
25 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π¦ = π£ β (1 / π¦) = (1 / π£)) |
26 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π¦ β (β β {0})
β¦ (1 / π¦)) = (π¦ β (β β {0})
β¦ (1 / π¦)) |
27 | | ovex 7391 |
. . . . . . . . . . . . . 14
β’ (1 /
π£) β
V |
28 | 25, 26, 27 | fvmpt 6949 |
. . . . . . . . . . . . 13
β’ (π£ β (β β {0})
β ((π¦ β (β
β {0}) β¦ (1 / π¦))βπ£) = (1 / π£)) |
29 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π¦ = πΈ β (1 / π¦) = (1 / πΈ)) |
30 | | ovex 7391 |
. . . . . . . . . . . . . . 15
β’ (1 /
πΈ) β
V |
31 | 29, 26, 30 | fvmpt 6949 |
. . . . . . . . . . . . . 14
β’ (πΈ β (β β {0})
β ((π¦ β (β
β {0}) β¦ (1 / π¦))βπΈ) = (1 / πΈ)) |
32 | 16, 31 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ) = (1 / πΈ)) |
33 | 28, 32 | oveqan12rd 7378 |
. . . . . . . . . . . 12
β’ ((π β§ π£ β (β β {0})) β
(((π¦ β (β
β {0}) β¦ (1 / π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ)) = ((1 / π£) β (1 / πΈ))) |
34 | 33 | fveq2d 6847 |
. . . . . . . . . . 11
β’ ((π β§ π£ β (β β {0})) β
(absβ(((π¦ β
(β β {0}) β¦ (1 / π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) = (absβ((1 / π£) β (1 / πΈ)))) |
35 | 34 | breq1d 5116 |
. . . . . . . . . 10
β’ ((π β§ π£ β (β β {0})) β
((absβ(((π¦ β
(β β {0}) β¦ (1 / π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) < π§ β (absβ((1 / π£) β (1 / πΈ))) < π§)) |
36 | 35 | imbi2d 341 |
. . . . . . . . 9
β’ ((π β§ π£ β (β β {0})) β
(((absβ(π£ β
πΈ)) < π€ β (absβ(((π¦ β (β β {0}) β¦ (1 /
π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) < π§) β ((absβ(π£ β πΈ)) < π€ β (absβ((1 / π£) β (1 / πΈ))) < π§))) |
37 | 36 | ralbidva 3169 |
. . . . . . . 8
β’ (π β (βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ(((π¦ β (β β {0}) β¦ (1 /
π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) < π§) β βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ((1 / π£) β (1 / πΈ))) < π§))) |
38 | 37 | rexbidv 3172 |
. . . . . . 7
β’ (π β (βπ€ β β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ(((π¦ β (β β {0}) β¦ (1 /
π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) < π§) β βπ€ β β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ((1 / π£) β (1 / πΈ))) < π§))) |
39 | 38 | biimpar 479 |
. . . . . 6
β’ ((π β§ βπ€ β β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ((1 / π£) β (1 / πΈ))) < π§)) β βπ€ β β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ(((π¦ β (β β {0}) β¦ (1 /
π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) < π§)) |
40 | 24, 39 | syldan 592 |
. . . . 5
β’ ((π β§ π§ β β+) β
βπ€ β
β+ βπ£ β (β β
{0})((absβ(π£ β
πΈ)) < π€ β (absβ(((π¦ β (β β {0}) β¦ (1 /
π¦))βπ£) β ((π¦ β (β β {0}) β¦ (1 /
π¦))βπΈ))) < π§)) |
41 | 11, 16, 5, 21, 40 | rlimcn1 15476 |
. . . 4
β’ (π β ((π¦ β (β β {0}) β¦ (1 /
π¦)) β (π₯ β π΄ β¦ πΆ)) βπ ((π¦ β (β β {0})
β¦ (1 / π¦))βπΈ)) |
42 | | eqidd 2734 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ πΆ) = (π₯ β π΄ β¦ πΆ)) |
43 | | eqidd 2734 |
. . . . 5
β’ (π β (π¦ β (β β {0}) β¦ (1 /
π¦)) = (π¦ β (β β {0}) β¦ (1 /
π¦))) |
44 | | oveq2 7366 |
. . . . 5
β’ (π¦ = πΆ β (1 / π¦) = (1 / πΆ)) |
45 | 10, 42, 43, 44 | fmptco 7076 |
. . . 4
β’ (π β ((π¦ β (β β {0}) β¦ (1 /
π¦)) β (π₯ β π΄ β¦ πΆ)) = (π₯ β π΄ β¦ (1 / πΆ))) |
46 | 41, 45, 32 | 3brtr3d 5137 |
. . 3
β’ (π β (π₯ β π΄ β¦ (1 / πΆ)) βπ (1 / πΈ)) |
47 | 3, 8, 2, 46 | rlimmul 15534 |
. 2
β’ (π β (π₯ β π΄ β¦ (π΅ Β· (1 / πΆ))) βπ (π· Β· (1 / πΈ))) |
48 | 3, 6, 7 | divrecd 11939 |
. . 3
β’ ((π β§ π₯ β π΄) β (π΅ / πΆ) = (π΅ Β· (1 / πΆ))) |
49 | 48 | mpteq2dva 5206 |
. 2
β’ (π β (π₯ β π΄ β¦ (π΅ / πΆ)) = (π₯ β π΄ β¦ (π΅ Β· (1 / πΆ)))) |
50 | | rlimcl 15391 |
. . . 4
β’ ((π₯ β π΄ β¦ π΅) βπ π· β π· β β) |
51 | 2, 50 | syl 17 |
. . 3
β’ (π β π· β β) |
52 | 51, 13, 14 | divrecd 11939 |
. 2
β’ (π β (π· / πΈ) = (π· Β· (1 / πΈ))) |
53 | 47, 49, 52 | 3brtr4d 5138 |
1
β’ (π β (π₯ β π΄ β¦ (π΅ / πΆ)) βπ (π· / πΈ)) |