Step | Hyp | Ref
| Expression |
1 | | breq1 5109 |
. . . . . . . 8
β’ (π = if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β (π β€ (absβ(πΉβπ₯)) β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯)))) |
2 | 1 | anbi2d 630 |
. . . . . . 7
β’ (π = if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β (((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯))) β ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) |
3 | 2 | rexbidv 3172 |
. . . . . 6
β’ (π = if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β (βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯))) β βπ₯ β π ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) |
4 | 3 | ralbidv 3171 |
. . . . 5
β’ (π = if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β (βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯))) β βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) |
5 | | unblimceq0lem.3 |
. . . . . 6
β’ (π β βπ β β+ βπ β β+
βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ (π β β+ β§ π β β+))
β βπ β
β+ βπ β β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) |
7 | | unblimceq0lem.1 |
. . . . . . . . . . 11
β’ (π β πΉ:πβΆβ) |
8 | 7 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β πΉ:πβΆβ) |
9 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β π΄ β π) |
10 | 8, 9 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β (πΉβπ΄) β β) |
11 | 10 | abscld 15327 |
. . . . . . . 8
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β (absβ(πΉβπ΄)) β β) |
12 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π β β+ β§ π β β+))
β π β
β+) |
13 | 12 | rpred 12962 |
. . . . . . . . 9
β’ ((π β§ (π β β+ β§ π β β+))
β π β
β) |
14 | 13 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β π β β) |
15 | 11, 14 | readdcld 11189 |
. . . . . . 7
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β ((absβ(πΉβπ΄)) + π) β β) |
16 | 10 | absge0d 15335 |
. . . . . . . 8
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β 0 β€
(absβ(πΉβπ΄))) |
17 | 12 | rpgt0d 12965 |
. . . . . . . . 9
β’ ((π β§ (π β β+ β§ π β β+))
β 0 < π) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β 0 < π) |
19 | 11, 14, 16, 18 | addgegt0d 11733 |
. . . . . . 7
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β 0 <
((absβ(πΉβπ΄)) + π)) |
20 | 15, 19 | elrpd 12959 |
. . . . . 6
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β ((absβ(πΉβπ΄)) + π) β
β+) |
21 | | simplrl 776 |
. . . . . 6
β’ (((π β§ (π β β+ β§ π β β+))
β§ Β¬ π΄ β π) β π β β+) |
22 | 20, 21 | ifclda 4522 |
. . . . 5
β’ ((π β§ (π β β+ β§ π β β+))
β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β
β+) |
23 | 4, 6, 22 | rspcdva 3581 |
. . . 4
β’ ((π β§ (π β β+ β§ π β β+))
β βπ β
β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯)))) |
24 | | simprr 772 |
. . . 4
β’ ((π β§ (π β β+ β§ π β β+))
β π β
β+) |
25 | | rsp 3229 |
. . . 4
β’
(βπ β
β+ βπ₯ β π ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))) β (π β β+ β
βπ₯ β π ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) |
26 | 23, 24, 25 | sylc 65 |
. . 3
β’ ((π β§ (π β β+ β§ π β β+))
β βπ₯ β
π ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯)))) |
27 | | simprl 770 |
. . . 4
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β π₯ β π) |
28 | | neeq1 3003 |
. . . . . 6
β’ (π¦ = π₯ β (π¦ β π΄ β π₯ β π΄)) |
29 | | fvoveq1 7381 |
. . . . . . 7
β’ (π¦ = π₯ β (absβ(π¦ β π΄)) = (absβ(π₯ β π΄))) |
30 | 29 | breq1d 5116 |
. . . . . 6
β’ (π¦ = π₯ β ((absβ(π¦ β π΄)) < π β (absβ(π₯ β π΄)) < π)) |
31 | | 2fveq3 6848 |
. . . . . . 7
β’ (π¦ = π₯ β (absβ(πΉβπ¦)) = (absβ(πΉβπ₯))) |
32 | 31 | breq2d 5118 |
. . . . . 6
β’ (π¦ = π₯ β (π β€ (absβ(πΉβπ¦)) β π β€ (absβ(πΉβπ₯)))) |
33 | 28, 30, 32 | 3anbi123d 1437 |
. . . . 5
β’ (π¦ = π₯ β ((π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦))) β (π₯ β π΄ β§ (absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯))))) |
34 | 33 | adantl 483 |
. . . 4
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π¦ = π₯) β ((π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦))) β (π₯ β π΄ β§ (absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯))))) |
35 | 15 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β ((absβ(πΉβπ΄)) + π) β β) |
36 | 7 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β πΉ:πβΆβ) |
37 | 36, 27 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β (πΉβπ₯) β β) |
38 | 37 | abscld 15327 |
. . . . . . . . 9
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β (absβ(πΉβπ₯)) β β) |
39 | 38 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (absβ(πΉβπ₯)) β β) |
40 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β π΄ β π) |
41 | 40 | iftrued 4495 |
. . . . . . . . . 10
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) = ((absβ(πΉβπ΄)) + π)) |
42 | 41 | eqcomd 2739 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β ((absβ(πΉβπ΄)) + π) = if(π΄ β π, ((absβ(πΉβπ΄)) + π), π)) |
43 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))) |
44 | 43 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))) |
45 | 42, 44 | eqbrtrd 5128 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β ((absβ(πΉβπ΄)) + π) β€ (absβ(πΉβπ₯))) |
46 | 35, 39, 45 | lensymd 11311 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β Β¬ (absβ(πΉβπ₯)) < ((absβ(πΉβπ΄)) + π)) |
47 | | 2fveq3 6848 |
. . . . . . . . . . . 12
β’ (π₯ = π΄ β (absβ(πΉβπ₯)) = (absβ(πΉβπ΄))) |
48 | 47 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β§ π₯ = π΄) β (absβ(πΉβπ₯)) = (absβ(πΉβπ΄))) |
49 | 14, 11 | ltaddposd 11744 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β (0 < π β (absβ(πΉβπ΄)) < ((absβ(πΉβπ΄)) + π))) |
50 | 18, 49 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β (absβ(πΉβπ΄)) < ((absβ(πΉβπ΄)) + π)) |
51 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β§ π₯ = π΄) β (absβ(πΉβπ΄)) < ((absβ(πΉβπ΄)) + π)) |
52 | 48, 51 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ ((((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β§ π₯ = π΄) β (absβ(πΉβπ₯)) < ((absβ(πΉβπ΄)) + π)) |
53 | 52 | ex 414 |
. . . . . . . . 9
β’ (((π β§ (π β β+ β§ π β β+))
β§ π΄ β π) β (π₯ = π΄ β (absβ(πΉβπ₯)) < ((absβ(πΉβπ΄)) + π))) |
54 | 53 | adantlr 714 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (π₯ = π΄ β (absβ(πΉβπ₯)) < ((absβ(πΉβπ΄)) + π))) |
55 | 54 | necon3bd 2954 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (Β¬ (absβ(πΉβπ₯)) < ((absβ(πΉβπ΄)) + π) β π₯ β π΄)) |
56 | 46, 55 | mpd 15 |
. . . . . 6
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β π₯ β π΄) |
57 | | simprrl 780 |
. . . . . . 7
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β (absβ(π₯ β π΄)) < π) |
58 | 57 | adantr 482 |
. . . . . 6
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (absβ(π₯ β π΄)) < π) |
59 | 14 | adantlr 714 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β π β β) |
60 | 10 | adantlr 714 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (πΉβπ΄) β β) |
61 | 60 | absge0d 15335 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β 0 β€ (absβ(πΉβπ΄))) |
62 | 11 | adantlr 714 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (absβ(πΉβπ΄)) β β) |
63 | 59, 62 | addge02d 11749 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (0 β€ (absβ(πΉβπ΄)) β π β€ ((absβ(πΉβπ΄)) + π))) |
64 | 61, 63 | mpbid 231 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β π β€ ((absβ(πΉβπ΄)) + π)) |
65 | 59, 35, 39, 64, 45 | letrd 11317 |
. . . . . 6
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β π β€ (absβ(πΉβπ₯))) |
66 | 56, 58, 65 | 3jca 1129 |
. . . . 5
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ π΄ β π) β (π₯ β π΄ β§ (absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) |
67 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β Β¬ π΄ β π) |
68 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ (π β β+
β§ π β
β+)) β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β§ π₯ = π΄) β π₯ = π΄) |
69 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β π₯ β π) |
70 | 69 | adantr 482 |
. . . . . . . . . 10
β’
(((((π β§ (π β β+
β§ π β
β+)) β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β§ π₯ = π΄) β π₯ β π) |
71 | 68, 70 | eqeltrrd 2835 |
. . . . . . . . 9
β’
(((((π β§ (π β β+
β§ π β
β+)) β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β§ π₯ = π΄) β π΄ β π) |
72 | 71 | ex 414 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β (π₯ = π΄ β π΄ β π)) |
73 | 72 | necon3bd 2954 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β (Β¬ π΄ β π β π₯ β π΄)) |
74 | 67, 73 | mpd 15 |
. . . . . 6
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β π₯ β π΄) |
75 | 57 | adantr 482 |
. . . . . 6
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β (absβ(π₯ β π΄)) < π) |
76 | 67 | iffalsed 4498 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) = π) |
77 | 76 | eqcomd 2739 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β π = if(π΄ β π, ((absβ(πΉβπ΄)) + π), π)) |
78 | 43 | adantr 482 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))) |
79 | 77, 78 | eqbrtrd 5128 |
. . . . . 6
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β π β€ (absβ(πΉβπ₯))) |
80 | 74, 75, 79 | 3jca 1129 |
. . . . 5
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β§ Β¬ π΄ β π) β (π₯ β π΄ β§ (absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) |
81 | 66, 80 | pm2.61dan 812 |
. . . 4
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β (π₯ β π΄ β§ (absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΉβπ₯)))) |
82 | 27, 34, 81 | rspcedvd 3582 |
. . 3
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π₯ β π β§ ((absβ(π₯ β π΄)) < π β§ if(π΄ β π, ((absβ(πΉβπ΄)) + π), π) β€ (absβ(πΉβπ₯))))) β βπ¦ β π (π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦)))) |
83 | 26, 82 | rexlimddv 3155 |
. 2
β’ ((π β§ (π β β+ β§ π β β+))
β βπ¦ β
π (π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦)))) |
84 | 83 | ralrimivva 3194 |
1
β’ (π β βπ β β+ βπ β β+
βπ¦ β π (π¦ β π΄ β§ (absβ(π¦ β π΄)) < π β§ π β€ (absβ(πΉβπ¦)))) |