Step | Hyp | Ref
| Expression |
1 | | imo72b2lem0.1 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
2 | | imo72b2lem0.3 |
. . . . . . . 8
β’ (π β π΄ β β) |
3 | 1, 2 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πΉβπ΄) β β) |
4 | 3 | recnd 11191 |
. . . . . 6
β’ (π β (πΉβπ΄) β β) |
5 | 4 | idi 1 |
. . . . 5
β’ (π β (πΉβπ΄) β β) |
6 | | imo72b2lem0.2 |
. . . . . . . 8
β’ (π β πΊ:ββΆβ) |
7 | | imo72b2lem0.4 |
. . . . . . . 8
β’ (π β π΅ β β) |
8 | 6, 7 | ffvelcdmd 7040 |
. . . . . . 7
β’ (π β (πΊβπ΅) β β) |
9 | 8 | recnd 11191 |
. . . . . 6
β’ (π β (πΊβπ΅) β β) |
10 | 9 | idi 1 |
. . . . 5
β’ (π β (πΊβπ΅) β β) |
11 | 5, 10 | mulcld 11183 |
. . . 4
β’ (π β ((πΉβπ΄) Β· (πΊβπ΅)) β β) |
12 | 11 | abscld 15330 |
. . 3
β’ (π β (absβ((πΉβπ΄) Β· (πΊβπ΅))) β β) |
13 | | imaco 6207 |
. . . . . 6
β’ ((abs
β πΉ) β β)
= (abs β (πΉ β
β)) |
14 | 13 | eqcomi 2742 |
. . . . 5
β’ (abs
β (πΉ β
β)) = ((abs β πΉ) β β) |
15 | | imassrn 6028 |
. . . . . . 7
β’ ((abs
β πΉ) β β)
β ran (abs β πΉ) |
16 | 15 | a1i 11 |
. . . . . 6
β’ (π β ((abs β πΉ) β β) β ran
(abs β πΉ)) |
17 | | absf 15231 |
. . . . . . . . . 10
β’
abs:ββΆβ |
18 | 17 | a1i 11 |
. . . . . . . . 9
β’ (π β
abs:ββΆβ) |
19 | | ax-resscn 11116 |
. . . . . . . . . 10
β’ β
β β |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β) |
21 | 18, 20 | fssresd 6713 |
. . . . . . . 8
β’ (π β (abs βΎ
β):ββΆβ) |
22 | 1, 21 | fco2d 42527 |
. . . . . . 7
β’ (π β (abs β πΉ):ββΆβ) |
23 | 22 | frnd 6680 |
. . . . . 6
β’ (π β ran (abs β πΉ) β
β) |
24 | 16, 23 | sstrd 3958 |
. . . . 5
β’ (π β ((abs β πΉ) β β) β
β) |
25 | 14, 24 | eqsstrid 3996 |
. . . 4
β’ (π β (abs β (πΉ β β)) β
β) |
26 | | 0re 11165 |
. . . . . . . . . 10
β’ 0 β
β |
27 | 26 | ne0ii 4301 |
. . . . . . . . 9
β’ β
β β
|
28 | 27 | a1i 11 |
. . . . . . . 8
β’ (π β β β
β
) |
29 | 28, 22 | wnefimgd 42526 |
. . . . . . 7
β’ (π β ((abs β πΉ) β β) β
β
) |
30 | 29 | necomd 2996 |
. . . . . 6
β’ (π β β
β ((abs β
πΉ) β
β)) |
31 | 14 | a1i 11 |
. . . . . 6
β’ (π β (abs β (πΉ β β)) = ((abs
β πΉ) β
β)) |
32 | 30, 31 | neeqtrrd 3015 |
. . . . 5
β’ (π β β
β (abs β
(πΉ β
β))) |
33 | 32 | necomd 2996 |
. . . 4
β’ (π β (abs β (πΉ β β)) β
β
) |
34 | | 1red 11164 |
. . . . 5
β’ (π β 1 β
β) |
35 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π = 1) β π = 1) |
36 | 35 | breq2d 5121 |
. . . . . 6
β’ ((π β§ π = 1) β (π₯ β€ π β π₯ β€ 1)) |
37 | 36 | ralbidv 3171 |
. . . . 5
β’ ((π β§ π = 1) β (βπ₯ β (abs β (πΉ β β))π₯ β€ π β βπ₯ β (abs β (πΉ β β))π₯ β€ 1)) |
38 | | imo72b2lem0.6 |
. . . . . 6
β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) |
39 | 1, 38 | extoimad 42529 |
. . . . 5
β’ (π β βπ₯ β (abs β (πΉ β β))π₯ β€ 1) |
40 | 34, 37, 39 | rspcedvd 3585 |
. . . 4
β’ (π β βπ β β βπ₯ β (abs β (πΉ β β))π₯ β€ π) |
41 | 25, 33, 40 | suprcld 12126 |
. . 3
β’ (π β sup((abs β (πΉ β β)), β,
< ) β β) |
42 | | 2re 12235 |
. . . 4
β’ 2 β
β |
43 | 42 | a1i 11 |
. . 3
β’ (π β 2 β
β) |
44 | | imo72b2lem0.5 |
. . . . . . . . 9
β’ (π β ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅))) = (2 Β· ((πΉβπ΄) Β· (πΊβπ΅)))) |
45 | 44 | idi 1 |
. . . . . . . 8
β’ (π β ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅))) = (2 Β· ((πΉβπ΄) Β· (πΊβπ΅)))) |
46 | 45 | fveq2d 6850 |
. . . . . . 7
β’ (π β (absβ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅)))) = (absβ(2 Β· ((πΉβπ΄) Β· (πΊβπ΅))))) |
47 | | 2cnd 12239 |
. . . . . . . . 9
β’ (π β 2 β
β) |
48 | 47, 11 | mulcld 11183 |
. . . . . . . 8
β’ (π β (2 Β· ((πΉβπ΄) Β· (πΊβπ΅))) β β) |
49 | 48 | abscld 15330 |
. . . . . . 7
β’ (π β (absβ(2 Β·
((πΉβπ΄) Β· (πΊβπ΅)))) β β) |
50 | 46, 49 | eqeltrd 2834 |
. . . . . 6
β’ (π β (absβ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅)))) β β) |
51 | 1 | idi 1 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
52 | 2 | idi 1 |
. . . . . . . . . . 11
β’ (π β π΄ β β) |
53 | 7 | idi 1 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
54 | 52, 53 | readdcld 11192 |
. . . . . . . . . 10
β’ (π β (π΄ + π΅) β β) |
55 | 51, 54 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (πΉβ(π΄ + π΅)) β β) |
56 | 55 | recnd 11191 |
. . . . . . . 8
β’ (π β (πΉβ(π΄ + π΅)) β β) |
57 | 56 | abscld 15330 |
. . . . . . 7
β’ (π β (absβ(πΉβ(π΄ + π΅))) β β) |
58 | 52, 53 | resubcld 11591 |
. . . . . . . . . 10
β’ (π β (π΄ β π΅) β β) |
59 | 51, 58 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (πΉβ(π΄ β π΅)) β β) |
60 | 59 | recnd 11191 |
. . . . . . . 8
β’ (π β (πΉβ(π΄ β π΅)) β β) |
61 | 60 | abscld 15330 |
. . . . . . 7
β’ (π β (absβ(πΉβ(π΄ β π΅))) β β) |
62 | 57, 61 | readdcld 11192 |
. . . . . 6
β’ (π β ((absβ(πΉβ(π΄ + π΅))) + (absβ(πΉβ(π΄ β π΅)))) β β) |
63 | 43, 41 | remulcld 11193 |
. . . . . 6
β’ (π β (2 Β· sup((abs
β (πΉ β
β)), β, < )) β β) |
64 | 56, 60 | abstrid 15350 |
. . . . . 6
β’ (π β (absβ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅)))) β€ ((absβ(πΉβ(π΄ + π΅))) + (absβ(πΉβ(π΄ β π΅))))) |
65 | 1, 54 | fvco3d 6945 |
. . . . . . . . . 10
β’ (π β ((abs β πΉ)β(π΄ + π΅)) = (absβ(πΉβ(π΄ + π΅)))) |
66 | 54, 22 | wfximgfd 42528 |
. . . . . . . . . . 11
β’ (π β ((abs β πΉ)β(π΄ + π΅)) β ((abs β πΉ) β β)) |
67 | 31 | idi 1 |
. . . . . . . . . . 11
β’ (π β (abs β (πΉ β β)) = ((abs
β πΉ) β
β)) |
68 | 66, 67 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (π β ((abs β πΉ)β(π΄ + π΅)) β (abs β (πΉ β β))) |
69 | 65, 68 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β (absβ(πΉβ(π΄ + π΅))) β (abs β (πΉ β β))) |
70 | 25, 33, 40, 69 | suprubd 12125 |
. . . . . . . 8
β’ (π β (absβ(πΉβ(π΄ + π΅))) β€ sup((abs β (πΉ β β)), β, <
)) |
71 | 1, 58 | fvco3d 6945 |
. . . . . . . . . 10
β’ (π β ((abs β πΉ)β(π΄ β π΅)) = (absβ(πΉβ(π΄ β π΅)))) |
72 | 58, 22 | wfximgfd 42528 |
. . . . . . . . . . 11
β’ (π β ((abs β πΉ)β(π΄ β π΅)) β ((abs β πΉ) β β)) |
73 | 72, 31 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (π β ((abs β πΉ)β(π΄ β π΅)) β (abs β (πΉ β β))) |
74 | 71, 73 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β (absβ(πΉβ(π΄ β π΅))) β (abs β (πΉ β β))) |
75 | 25, 33, 40, 74 | suprubd 12125 |
. . . . . . . 8
β’ (π β (absβ(πΉβ(π΄ β π΅))) β€ sup((abs β (πΉ β β)), β, <
)) |
76 | 57, 61, 41, 41, 70, 75 | le2addd 11782 |
. . . . . . 7
β’ (π β ((absβ(πΉβ(π΄ + π΅))) + (absβ(πΉβ(π΄ β π΅)))) β€ (sup((abs β (πΉ β β)), β,
< ) + sup((abs β (πΉ β β)), β, <
))) |
77 | 41 | recnd 11191 |
. . . . . . . . 9
β’ (π β sup((abs β (πΉ β β)), β,
< ) β β) |
78 | 77 | 2timesd 12404 |
. . . . . . . 8
β’ (π β (2 Β· sup((abs
β (πΉ β
β)), β, < )) = (sup((abs β (πΉ β β)), β, < ) +
sup((abs β (πΉ β
β)), β, < ))) |
79 | 78 | eqcomd 2739 |
. . . . . . 7
β’ (π β (sup((abs β (πΉ β β)), β,
< ) + sup((abs β (πΉ β β)), β, < )) = (2
Β· sup((abs β (πΉ β β)), β, <
))) |
80 | 79, 63 | eqeltrd 2834 |
. . . . . . 7
β’ (π β (sup((abs β (πΉ β β)), β,
< ) + sup((abs β (πΉ β β)), β, < )) β
β) |
81 | 76, 79, 62, 80 | leeq2d 42522 |
. . . . . 6
β’ (π β ((absβ(πΉβ(π΄ + π΅))) + (absβ(πΉβ(π΄ β π΅)))) β€ (2 Β· sup((abs β
(πΉ β β)),
β, < ))) |
82 | 50, 62, 63, 64, 81 | letrd 11320 |
. . . . 5
β’ (π β (absβ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅)))) β€ (2 Β· sup((abs β
(πΉ β β)),
β, < ))) |
83 | 82, 46, 50, 63 | leeq1d 42521 |
. . . 4
β’ (π β (absβ(2 Β·
((πΉβπ΄) Β· (πΊβπ΅)))) β€ (2 Β· sup((abs β
(πΉ β β)),
β, < ))) |
84 | | 0le2 12263 |
. . . . . 6
β’ 0 β€
2 |
85 | 84 | a1i 11 |
. . . . 5
β’ (π β 0 β€ 2) |
86 | 3 | idi 1 |
. . . . . 6
β’ (π β (πΉβπ΄) β β) |
87 | 8 | idi 1 |
. . . . . 6
β’ (π β (πΊβπ΅) β β) |
88 | 86, 87 | remulcld 11193 |
. . . . 5
β’ (π β ((πΉβπ΄) Β· (πΊβπ΅)) β β) |
89 | 85, 43, 88 | absmulrposd 42523 |
. . . 4
β’ (π β (absβ(2 Β·
((πΉβπ΄) Β· (πΊβπ΅)))) = (2 Β· (absβ((πΉβπ΄) Β· (πΊβπ΅))))) |
90 | 83, 89, 49, 63 | leeq1d 42521 |
. . 3
β’ (π β (2 Β·
(absβ((πΉβπ΄) Β· (πΊβπ΅)))) β€ (2 Β· sup((abs β
(πΉ β β)),
β, < ))) |
91 | | 2pos 12264 |
. . . 4
β’ 0 <
2 |
92 | 91 | a1i 11 |
. . 3
β’ (π β 0 < 2) |
93 | 12, 41, 43, 90, 92 | wwlemuld 42520 |
. 2
β’ (π β (absβ((πΉβπ΄) Β· (πΊβπ΅))) β€ sup((abs β (πΉ β β)), β, <
)) |
94 | 4, 9 | absmuld 15348 |
. . 3
β’ (π β (absβ((πΉβπ΄) Β· (πΊβπ΅))) = ((absβ(πΉβπ΄)) Β· (absβ(πΊβπ΅)))) |
95 | 94 | idi 1 |
. 2
β’ (π β (absβ((πΉβπ΄) Β· (πΊβπ΅))) = ((absβ(πΉβπ΄)) Β· (absβ(πΊβπ΅)))) |
96 | 93, 95, 12, 41 | leeq1d 42521 |
1
β’ (π β ((absβ(πΉβπ΄)) Β· (absβ(πΊβπ΅))) β€ sup((abs β (πΉ β β)), β, <
)) |