Step | Hyp | Ref
| Expression |
1 | | 0re 11162 |
. . . 4
โข 0 โ
โ |
2 | | leloe 11246 |
. . . 4
โข ((0
โ โ โง ๐ด
โ โ) โ (0 โค ๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
3 | 1, 2 | mpan 689 |
. . 3
โข (๐ด โ โ โ (0 โค
๐ด โ (0 < ๐ด โจ 0 = ๐ด))) |
4 | | recn 11146 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ ๐ด โ
โ) |
5 | | sqval 14026 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ (๐ดโ2) = (๐ด ยท ๐ด)) |
7 | 6 | breq1d 5116 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ด))) |
8 | 7 | 3ad2ant1 1134 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด โ โ โง 0 <
๐ด)) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ด))) |
9 | | lemul1 12012 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด โ โ โง 0 <
๐ด)) โ (๐ด โค ๐ต โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ด))) |
10 | 8, 9 | bitr4d 282 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ด โ โ โง 0 <
๐ด)) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)) |
11 | 10 | 3exp 1120 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ต โ โ โ ((๐ด โ โ โง 0 <
๐ด) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
12 | 11 | exp4a 433 |
. . . . . . 7
โข (๐ด โ โ โ (๐ต โ โ โ (๐ด โ โ โ (0 <
๐ด โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต))))) |
13 | 12 | pm2.43a 54 |
. . . . . 6
โข (๐ด โ โ โ (๐ต โ โ โ (0 <
๐ด โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
14 | 13 | adantrd 493 |
. . . . 5
โข (๐ด โ โ โ ((๐ต โ โ โง 0 โค
๐ต) โ (0 < ๐ด โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
15 | 14 | com23 86 |
. . . 4
โข (๐ด โ โ โ (0 <
๐ด โ ((๐ต โ โ โง 0 โค
๐ต) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
16 | | sq0 14102 |
. . . . . . . . . . . 12
โข
(0โ2) = 0 |
17 | | 0le0 12259 |
. . . . . . . . . . . 12
โข 0 โค
0 |
18 | 16, 17 | eqbrtri 5127 |
. . . . . . . . . . 11
โข
(0โ2) โค 0 |
19 | | recn 11146 |
. . . . . . . . . . . 12
โข (๐ต โ โ โ ๐ต โ
โ) |
20 | 19 | mul01d 11359 |
. . . . . . . . . . 11
โข (๐ต โ โ โ (๐ต ยท 0) =
0) |
21 | 18, 20 | breqtrrid 5144 |
. . . . . . . . . 10
โข (๐ต โ โ โ
(0โ2) โค (๐ต ยท
0)) |
22 | 21 | adantl 483 |
. . . . . . . . 9
โข ((0 =
๐ด โง ๐ต โ โ) โ (0โ2) โค
(๐ต ยท
0)) |
23 | | oveq1 7365 |
. . . . . . . . . . 11
โข (0 =
๐ด โ (0โ2) =
(๐ดโ2)) |
24 | | oveq2 7366 |
. . . . . . . . . . 11
โข (0 =
๐ด โ (๐ต ยท 0) = (๐ต ยท ๐ด)) |
25 | 23, 24 | breq12d 5119 |
. . . . . . . . . 10
โข (0 =
๐ด โ ((0โ2) โค
(๐ต ยท 0) โ
(๐ดโ2) โค (๐ต ยท ๐ด))) |
26 | 25 | adantr 482 |
. . . . . . . . 9
โข ((0 =
๐ด โง ๐ต โ โ) โ ((0โ2) โค
(๐ต ยท 0) โ
(๐ดโ2) โค (๐ต ยท ๐ด))) |
27 | 22, 26 | mpbid 231 |
. . . . . . . 8
โข ((0 =
๐ด โง ๐ต โ โ) โ (๐ดโ2) โค (๐ต ยท ๐ด)) |
28 | 27 | adantrr 716 |
. . . . . . 7
โข ((0 =
๐ด โง (๐ต โ โ โง 0 โค ๐ต)) โ (๐ดโ2) โค (๐ต ยท ๐ด)) |
29 | | breq1 5109 |
. . . . . . . . 9
โข (0 =
๐ด โ (0 โค ๐ต โ ๐ด โค ๐ต)) |
30 | 29 | biimpa 478 |
. . . . . . . 8
โข ((0 =
๐ด โง 0 โค ๐ต) โ ๐ด โค ๐ต) |
31 | 30 | adantrl 715 |
. . . . . . 7
โข ((0 =
๐ด โง (๐ต โ โ โง 0 โค ๐ต)) โ ๐ด โค ๐ต) |
32 | 28, 31 | 2thd 265 |
. . . . . 6
โข ((0 =
๐ด โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)) |
33 | 32 | ex 414 |
. . . . 5
โข (0 =
๐ด โ ((๐ต โ โ โง 0 โค
๐ต) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต))) |
34 | 33 | a1i 11 |
. . . 4
โข (๐ด โ โ โ (0 =
๐ด โ ((๐ต โ โ โง 0 โค
๐ต) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
35 | 15, 34 | jaod 858 |
. . 3
โข (๐ด โ โ โ ((0 <
๐ด โจ 0 = ๐ด) โ ((๐ต โ โ โง 0 โค ๐ต) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
36 | 3, 35 | sylbid 239 |
. 2
โข (๐ด โ โ โ (0 โค
๐ด โ ((๐ต โ โ โง 0 โค
๐ต) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)))) |
37 | 36 | imp31 419 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 โค ๐ต)) โ ((๐ดโ2) โค (๐ต ยท ๐ด) โ ๐ด โค ๐ต)) |