Step | Hyp | Ref
| Expression |
1 | | divalglem0.1 |
. . . . 5
โข ๐ โ โค |
2 | 1 | zrei 12510 |
. . . 4
โข ๐ โ โ |
3 | | 0re 11162 |
. . . 4
โข 0 โ
โ |
4 | 2, 3 | letrii 11285 |
. . 3
โข (๐ โค 0 โจ 0 โค ๐) |
5 | | divalglem0.2 |
. . . . . . . 8
โข ๐ท โ โค |
6 | | divalglem1.3 |
. . . . . . . 8
โข ๐ท โ 0 |
7 | | nnabscl 15216 |
. . . . . . . 8
โข ((๐ท โ โค โง ๐ท โ 0) โ (absโ๐ท) โ
โ) |
8 | 5, 6, 7 | mp2an 691 |
. . . . . . 7
โข
(absโ๐ท) โ
โ |
9 | | nnge1 12186 |
. . . . . . 7
โข
((absโ๐ท)
โ โ โ 1 โค (absโ๐ท)) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
โข 1 โค
(absโ๐ท) |
11 | | le0neg1 11668 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โค 0 โ 0 โค -๐)) |
12 | 2, 11 | ax-mp 5 |
. . . . . . 7
โข (๐ โค 0 โ 0 โค -๐) |
13 | 2 | renegcli 11467 |
. . . . . . . 8
โข -๐ โ โ |
14 | 5 | zrei 12510 |
. . . . . . . . . 10
โข ๐ท โ โ |
15 | 14 | recni 11174 |
. . . . . . . . 9
โข ๐ท โ โ |
16 | 15 | abscli 15286 |
. . . . . . . 8
โข
(absโ๐ท) โ
โ |
17 | | lemulge11 12022 |
. . . . . . . 8
โข (((-๐ โ โ โง
(absโ๐ท) โ
โ) โง (0 โค -๐
โง 1 โค (absโ๐ท))) โ -๐ โค (-๐ ยท (absโ๐ท))) |
18 | 13, 16, 17 | mpanl12 701 |
. . . . . . 7
โข ((0 โค
-๐ โง 1 โค
(absโ๐ท)) โ
-๐ โค (-๐ ยท (absโ๐ท))) |
19 | 12, 18 | sylanb 582 |
. . . . . 6
โข ((๐ โค 0 โง 1 โค
(absโ๐ท)) โ
-๐ โค (-๐ ยท (absโ๐ท))) |
20 | 10, 19 | mpan2 690 |
. . . . 5
โข (๐ โค 0 โ -๐ โค (-๐ ยท (absโ๐ท))) |
21 | 2 | recni 11174 |
. . . . . . 7
โข ๐ โ โ |
22 | 21, 15 | absmuli 15295 |
. . . . . 6
โข
(absโ(๐
ยท ๐ท)) =
((absโ๐) ยท
(absโ๐ท)) |
23 | 2 | absnidi 15269 |
. . . . . . 7
โข (๐ โค 0 โ (absโ๐) = -๐) |
24 | 23 | oveq1d 7373 |
. . . . . 6
โข (๐ โค 0 โ ((absโ๐) ยท (absโ๐ท)) = (-๐ ยท (absโ๐ท))) |
25 | 22, 24 | eqtrid 2785 |
. . . . 5
โข (๐ โค 0 โ (absโ(๐ ยท ๐ท)) = (-๐ ยท (absโ๐ท))) |
26 | 20, 25 | breqtrrd 5134 |
. . . 4
โข (๐ โค 0 โ -๐ โค (absโ(๐ ยท ๐ท))) |
27 | | le0neg2 11669 |
. . . . . 6
โข (๐ โ โ โ (0 โค
๐ โ -๐ โค 0)) |
28 | 2, 27 | ax-mp 5 |
. . . . 5
โข (0 โค
๐ โ -๐ โค 0) |
29 | 2, 14 | remulcli 11176 |
. . . . . . . 8
โข (๐ ยท ๐ท) โ โ |
30 | 29 | recni 11174 |
. . . . . . 7
โข (๐ ยท ๐ท) โ โ |
31 | 30 | absge0i 15287 |
. . . . . 6
โข 0 โค
(absโ(๐ ยท
๐ท)) |
32 | 30 | abscli 15286 |
. . . . . . 7
โข
(absโ(๐
ยท ๐ท)) โ
โ |
33 | 13, 3, 32 | letri 11289 |
. . . . . 6
โข ((-๐ โค 0 โง 0 โค
(absโ(๐ ยท
๐ท))) โ -๐ โค (absโ(๐ ยท ๐ท))) |
34 | 31, 33 | mpan2 690 |
. . . . 5
โข (-๐ โค 0 โ -๐ โค (absโ(๐ ยท ๐ท))) |
35 | 28, 34 | sylbi 216 |
. . . 4
โข (0 โค
๐ โ -๐ โค (absโ(๐ ยท ๐ท))) |
36 | 26, 35 | jaoi 856 |
. . 3
โข ((๐ โค 0 โจ 0 โค ๐) โ -๐ โค (absโ(๐ ยท ๐ท))) |
37 | 4, 36 | ax-mp 5 |
. 2
โข -๐ โค (absโ(๐ ยท ๐ท)) |
38 | | df-neg 11393 |
. . . 4
โข -๐ = (0 โ ๐) |
39 | 38 | breq1i 5113 |
. . 3
โข (-๐ โค (absโ(๐ ยท ๐ท)) โ (0 โ ๐) โค (absโ(๐ ยท ๐ท))) |
40 | 3, 2, 32 | lesubadd2i 11720 |
. . 3
โข ((0
โ ๐) โค
(absโ(๐ ยท
๐ท)) โ 0 โค (๐ + (absโ(๐ ยท ๐ท)))) |
41 | 39, 40 | bitri 275 |
. 2
โข (-๐ โค (absโ(๐ ยท ๐ท)) โ 0 โค (๐ + (absโ(๐ ยท ๐ท)))) |
42 | 37, 41 | mpbi 229 |
1
โข 0 โค
(๐ + (absโ(๐ ยท ๐ท))) |