Step | Hyp | Ref
| Expression |
1 | | imo72b2.2 |
. . . . 5
β’ (π β πΊ:ββΆβ) |
2 | | imo72b2.4 |
. . . . 5
β’ (π β π΅ β β) |
3 | 1, 2 | ffvelcdmd 7088 |
. . . 4
β’ (π β (πΊβπ΅) β β) |
4 | 3 | recnd 11242 |
. . 3
β’ (π β (πΊβπ΅) β β) |
5 | 4 | abscld 15383 |
. 2
β’ (π β (absβ(πΊβπ΅)) β β) |
6 | | 1red 11215 |
. 2
β’ (π β 1 β
β) |
7 | | simpr 486 |
. . 3
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 1 < (absβ(πΊβπ΅))) |
8 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β πΊ:ββΆβ) |
9 | 2 | adantr 482 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β π΅ β β) |
10 | 8, 9 | ffvelcdmd 7088 |
. . . . . 6
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (πΊβπ΅) β β) |
11 | 10 | recnd 11242 |
. . . . 5
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (πΊβπ΅) β β) |
12 | 11 | abscld 15383 |
. . . 4
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (absβ(πΊβπ΅)) β β) |
13 | 6 | adantr 482 |
. . . 4
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 1 β
β) |
14 | | ax-resscn 11167 |
. . . . . . . . 9
β’ β
β β |
15 | | imaco 6251 |
. . . . . . . . . . . 12
β’ ((abs
β πΉ) β β)
= (abs β (πΉ β
β)) |
16 | 15 | eqcomi 2742 |
. . . . . . . . . . 11
β’ (abs
β (πΉ β
β)) = ((abs β πΉ) β β) |
17 | | imassrn 6071 |
. . . . . . . . . . . . 13
β’ ((abs
β πΉ) β β)
β ran (abs β πΉ) |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β ((abs β πΉ) β β) β ran (abs β
πΉ)) |
19 | | imo72b2.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:ββΆβ) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β πΉ:ββΆβ) |
21 | | absf 15284 |
. . . . . . . . . . . . . . . 16
β’
abs:ββΆβ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β
abs:ββΆβ) |
23 | 14 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β β β
β) |
24 | 22, 23 | fssresd 6759 |
. . . . . . . . . . . . . 14
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (abs βΎ
β):ββΆβ) |
25 | 20, 24 | fco2d 42914 |
. . . . . . . . . . . . 13
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (abs β πΉ):ββΆβ) |
26 | 25 | frnd 6726 |
. . . . . . . . . . . 12
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β ran (abs β πΉ) β
β) |
27 | 18, 26 | sstrd 3993 |
. . . . . . . . . . 11
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β ((abs β πΉ) β β) β
β) |
28 | 16, 27 | eqsstrid 4031 |
. . . . . . . . . 10
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (abs β (πΉ β β)) β
β) |
29 | | 0re 11216 |
. . . . . . . . . . . . . . . 16
β’ 0 β
β |
30 | 29 | ne0ii 4338 |
. . . . . . . . . . . . . . 15
β’ β
β β
|
31 | 30 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β β β
β
) |
32 | 31, 25 | wnefimgd 42913 |
. . . . . . . . . . . . 13
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β ((abs β πΉ) β β) β
β
) |
33 | 32 | necomd 2997 |
. . . . . . . . . . . 12
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β β
β ((abs β πΉ) β
β)) |
34 | 16 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (abs β (πΉ β β)) = ((abs β πΉ) β
β)) |
35 | 33, 34 | neeqtrrd 3016 |
. . . . . . . . . . 11
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β β
β (abs β (πΉ β
β))) |
36 | 35 | necomd 2997 |
. . . . . . . . . 10
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (abs β (πΉ β β)) β
β
) |
37 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π = 1) β π = 1) |
38 | 37 | breq2d 5161 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π = 1) β (π‘ β€ π β π‘ β€ 1)) |
39 | 38 | ralbidv 3178 |
. . . . . . . . . . 11
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π = 1) β (βπ‘ β (abs β (πΉ β β))π‘ β€ π β βπ‘ β (abs β (πΉ β β))π‘ β€ 1)) |
40 | | imo72b2.6 |
. . . . . . . . . . . . 13
β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) |
41 | 19, 40 | extoimad 42916 |
. . . . . . . . . . . 12
β’ (π β βπ‘ β (abs β (πΉ β β))π‘ β€ 1) |
42 | 41 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β βπ‘ β (abs β (πΉ β β))π‘ β€ 1) |
43 | 13, 39, 42 | rspcedvd 3615 |
. . . . . . . . . 10
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β βπ β β βπ‘ β (abs β (πΉ β β))π‘ β€ π) |
44 | 28, 36, 43 | suprcld 12177 |
. . . . . . . . 9
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β sup((abs β (πΉ β β)), β,
< ) β β) |
45 | 14, 44 | sselid 3981 |
. . . . . . . 8
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β sup((abs β (πΉ β β)), β,
< ) β β) |
46 | 14, 12 | sselid 3981 |
. . . . . . . 8
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (absβ(πΊβπ΅)) β β) |
47 | 45, 46 | mulcomd 11235 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (sup((abs β (πΉ β β)), β,
< ) Β· (absβ(πΊβπ΅))) = ((absβ(πΊβπ΅)) Β· sup((abs β (πΉ β β)), β,
< ))) |
48 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 0 β
β) |
49 | | 0lt1 11736 |
. . . . . . . . . . . . 13
β’ 0 <
1 |
50 | 49 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 0 < 1) |
51 | 48, 13, 12, 50, 7 | lttrd 11375 |
. . . . . . . . . . 11
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 0 < (absβ(πΊβπ΅))) |
52 | 51 | gt0ne0d 11778 |
. . . . . . . . . 10
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (absβ(πΊβπ΅)) β 0) |
53 | 44, 12, 52 | redivcld 12042 |
. . . . . . . . 9
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (sup((abs β (πΉ β β)), β,
< ) / (absβ(πΊβπ΅))) β β) |
54 | 20 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β πΉ:ββΆβ) |
55 | 8 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β πΊ:ββΆβ) |
56 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β π’ β β) |
57 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β π΅ β β) |
58 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π£ = π΅) β π£ = π΅) |
59 | 58 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π£ = π΅) β (π’ + π£) = (π’ + π΅)) |
60 | 59 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π£ = π΅) β (πΉβ(π’ + π£)) = (πΉβ(π’ + π΅))) |
61 | 58 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π£ = π΅) β (π’ β π£) = (π’ β π΅)) |
62 | 61 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π£ = π΅) β (πΉβ(π’ β π£)) = (πΉβ(π’ β π΅))) |
63 | 60, 62 | oveq12d 7427 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ = π΅) β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = ((πΉβ(π’ + π΅)) + (πΉβ(π’ β π΅)))) |
64 | 58 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π£ = π΅) β (πΊβπ£) = (πΊβπ΅)) |
65 | 64 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π£ = π΅) β ((πΉβπ’) Β· (πΊβπ£)) = ((πΉβπ’) Β· (πΊβπ΅))) |
66 | 65 | oveq2d 7425 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π£ = π΅) β (2 Β· ((πΉβπ’) Β· (πΊβπ£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ΅)))) |
67 | 63, 66 | eqeq12d 2749 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π£ = π΅) β (((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£))) β ((πΉβ(π’ + π΅)) + (πΉβ(π’ β π΅))) = (2 Β· ((πΉβπ’) Β· (πΊβπ΅))))) |
68 | 67 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π£ = π΅) β (βπ’ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£))) β βπ’ β β ((πΉβ(π’ + π΅)) + (πΉβ(π’ β π΅))) = (2 Β· ((πΉβπ’) Β· (πΊβπ΅))))) |
69 | | imo72b2.5 |
. . . . . . . . . . . . . . . 16
β’ (π β βπ’ β β βπ£ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) |
70 | | ralcom 3287 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ’ β
β βπ£ β
β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£))) β βπ£ β β βπ’ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) |
71 | 70 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ’ β
β βπ£ β
β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£))) β βπ£ β β βπ’ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (βπ’ β β βπ£ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£))) β βπ£ β β βπ’ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£))))) |
73 | 72 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ βπ’ β β βπ£ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) β βπ£ β β βπ’ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) |
74 | 69, 73 | mpdan 686 |
. . . . . . . . . . . . . . 15
β’ (π β βπ£ β β βπ’ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) |
75 | 68, 2, 74 | rspcdv2 3608 |
. . . . . . . . . . . . . 14
β’ (π β βπ’ β β ((πΉβ(π’ + π΅)) + (πΉβ(π’ β π΅))) = (2 Β· ((πΉβπ’) Β· (πΊβπ΅)))) |
76 | 75 | r19.21bi 3249 |
. . . . . . . . . . . . 13
β’ ((π β§ π’ β β) β ((πΉβ(π’ + π΅)) + (πΉβ(π’ β π΅))) = (2 Β· ((πΉβπ’) Β· (πΊβπ΅)))) |
77 | 76 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β ((πΉβ(π’ + π΅)) + (πΉβ(π’ β π΅))) = (2 Β· ((πΉβπ’) Β· (πΊβπ΅)))) |
78 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β βπ¦ β β
(absβ(πΉβπ¦)) β€ 1) |
79 | 54, 55, 56, 57, 77, 78 | imo72b2lem0 42917 |
. . . . . . . . . . 11
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β ((absβ(πΉβπ’)) Β· (absβ(πΊβπ΅))) β€ sup((abs β (πΉ β β)), β, <
)) |
80 | | 0xr 11261 |
. . . . . . . . . . . . 13
β’ 0 β
β* |
81 | 80 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β 0 β
β*) |
82 | | 1xr 11273 |
. . . . . . . . . . . . 13
β’ 1 β
β* |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β 1 β
β*) |
84 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β (absβ(πΊβπ΅)) β β) |
85 | 84 | rexrd 11264 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β (absβ(πΊβπ΅)) β
β*) |
86 | 49 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β 0 <
1) |
87 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β 1 <
(absβ(πΊβπ΅))) |
88 | 81, 83, 85, 86, 87 | xrlttrd 13138 |
. . . . . . . . . . 11
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β 0 <
(absβ(πΊβπ΅))) |
89 | 20 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β (πΉβπ’) β β) |
90 | 89 | recnd 11242 |
. . . . . . . . . . . 12
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β (πΉβπ’) β β) |
91 | 90 | abscld 15383 |
. . . . . . . . . . 11
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β (absβ(πΉβπ’)) β β) |
92 | 44 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β sup((abs β
(πΉ β β)),
β, < ) β β) |
93 | 79, 88, 84, 91, 92 | lemuldiv3d 42922 |
. . . . . . . . . 10
β’ (((π β§ 1 < (absβ(πΊβπ΅))) β§ π’ β β) β (absβ(πΉβπ’)) β€ (sup((abs β (πΉ β β)), β, < ) /
(absβ(πΊβπ΅)))) |
94 | 93 | ralrimiva 3147 |
. . . . . . . . 9
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β βπ’ β β (absβ(πΉβπ’)) β€ (sup((abs β (πΉ β β)), β, < ) /
(absβ(πΊβπ΅)))) |
95 | 20, 53, 94 | imo72b2lem2 42919 |
. . . . . . . 8
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β sup((abs β (πΉ β β)), β,
< ) β€ (sup((abs β (πΉ β β)), β, < ) /
(absβ(πΊβπ΅)))) |
96 | 95, 51, 12, 44, 44 | lemuldiv4d 42923 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (sup((abs β (πΉ β β)), β,
< ) Β· (absβ(πΊβπ΅))) β€ sup((abs β (πΉ β β)), β, <
)) |
97 | 47, 96 | eqbrtrrd 5173 |
. . . . . 6
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β ((absβ(πΊβπ΅)) Β· sup((abs β (πΉ β β)), β,
< )) β€ sup((abs β (πΉ β β)), β, <
)) |
98 | | imo72b2.7 |
. . . . . . . 8
β’ (π β βπ₯ β β (πΉβπ₯) β 0) |
99 | 98 | adantr 482 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β βπ₯ β β (πΉβπ₯) β 0) |
100 | 40 | adantr 482 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) |
101 | 20, 99, 100 | imo72b2lem1 42921 |
. . . . . 6
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 0 < sup((abs β (πΉ β β)), β,
< )) |
102 | 97, 101, 44, 12, 44 | lemuldiv3d 42922 |
. . . . 5
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (absβ(πΊβπ΅)) β€ (sup((abs β (πΉ β β)), β, < ) /
sup((abs β (πΉ β
β)), β, < ))) |
103 | 23, 44 | sseldd 3984 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β sup((abs β (πΉ β β)), β,
< ) β β) |
104 | 101 | gt0ne0d 11778 |
. . . . . . 7
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β sup((abs β (πΉ β β)), β,
< ) β 0) |
105 | 103, 104 | dividd 11988 |
. . . . . 6
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (sup((abs β (πΉ β β)), β,
< ) / sup((abs β (πΉ β β)), β, < )) =
1) |
106 | 105 | eqcomd 2739 |
. . . . 5
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β 1 = (sup((abs β (πΉ β β)), β,
< ) / sup((abs β (πΉ β β)), β, <
))) |
107 | 102, 106 | breqtrrd 5177 |
. . . 4
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β (absβ(πΊβπ΅)) β€ 1) |
108 | 12, 13, 107 | lensymd 11365 |
. . 3
β’ ((π β§ 1 < (absβ(πΊβπ΅))) β Β¬ 1 < (absβ(πΊβπ΅))) |
109 | 7, 108 | pm2.65da 816 |
. 2
β’ (π β Β¬ 1 <
(absβ(πΊβπ΅))) |
110 | 5, 6, 109 | nltled 11364 |
1
β’ (π β (absβ(πΊβπ΅)) β€ 1) |