Step | Hyp | Ref
| Expression |
1 | | dvdslelem.3 |
. . . . . 6
โข ๐พ โ โค |
2 | 1 | zrei 12439 |
. . . . 5
โข ๐พ โ โ |
3 | | 0re 11091 |
. . . . 5
โข 0 โ
โ |
4 | | lelttric 11196 |
. . . . 5
โข ((๐พ โ โ โง 0 โ
โ) โ (๐พ โค 0
โจ 0 < ๐พ)) |
5 | 2, 3, 4 | mp2an 691 |
. . . 4
โข (๐พ โค 0 โจ 0 < ๐พ) |
6 | | zgt0ge1 12488 |
. . . . . 6
โข (๐พ โ โค โ (0 <
๐พ โ 1 โค ๐พ)) |
7 | 1, 6 | ax-mp 5 |
. . . . 5
โข (0 <
๐พ โ 1 โค ๐พ) |
8 | 7 | orbi2i 912 |
. . . 4
โข ((๐พ โค 0 โจ 0 < ๐พ) โ (๐พ โค 0 โจ 1 โค ๐พ)) |
9 | 5, 8 | mpbi 229 |
. . 3
โข (๐พ โค 0 โจ 1 โค ๐พ) |
10 | | le0neg1 11597 |
. . . . . . . . 9
โข (๐พ โ โ โ (๐พ โค 0 โ 0 โค -๐พ)) |
11 | 2, 10 | ax-mp 5 |
. . . . . . . 8
โข (๐พ โค 0 โ 0 โค -๐พ) |
12 | | dvdslelem.2 |
. . . . . . . . . . . 12
โข ๐ โ โ |
13 | 12 | nngt0i 12126 |
. . . . . . . . . . 11
โข 0 <
๐ |
14 | 12 | nnrei 12096 |
. . . . . . . . . . . 12
โข ๐ โ โ |
15 | | dvdslelem.1 |
. . . . . . . . . . . . 13
โข ๐ โ โค |
16 | 15 | zrei 12439 |
. . . . . . . . . . . 12
โข ๐ โ โ |
17 | 3, 14, 16 | lttri 11215 |
. . . . . . . . . . 11
โข ((0 <
๐ โง ๐ < ๐) โ 0 < ๐) |
18 | 13, 17 | mpan 689 |
. . . . . . . . . 10
โข (๐ < ๐ โ 0 < ๐) |
19 | 3, 16 | ltlei 11211 |
. . . . . . . . . 10
โข (0 <
๐ โ 0 โค ๐) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
โข (๐ < ๐ โ 0 โค ๐) |
21 | 2 | renegcli 11396 |
. . . . . . . . . 10
โข -๐พ โ โ |
22 | 21, 16 | mulge0i 11636 |
. . . . . . . . 9
โข ((0 โค
-๐พ โง 0 โค ๐) โ 0 โค (-๐พ ยท ๐)) |
23 | 20, 22 | sylan2 594 |
. . . . . . . 8
โข ((0 โค
-๐พ โง ๐ < ๐) โ 0 โค (-๐พ ยท ๐)) |
24 | 11, 23 | sylanb 582 |
. . . . . . 7
โข ((๐พ โค 0 โง ๐ < ๐) โ 0 โค (-๐พ ยท ๐)) |
25 | 24 | expcom 415 |
. . . . . 6
โข (๐ < ๐ โ (๐พ โค 0 โ 0 โค (-๐พ ยท ๐))) |
26 | 2, 16 | remulcli 11105 |
. . . . . . . 8
โข (๐พ ยท ๐) โ โ |
27 | | le0neg1 11597 |
. . . . . . . 8
โข ((๐พ ยท ๐) โ โ โ ((๐พ ยท ๐) โค 0 โ 0 โค -(๐พ ยท ๐))) |
28 | 26, 27 | ax-mp 5 |
. . . . . . 7
โข ((๐พ ยท ๐) โค 0 โ 0 โค -(๐พ ยท ๐)) |
29 | 2 | recni 11103 |
. . . . . . . . 9
โข ๐พ โ โ |
30 | 16 | recni 11103 |
. . . . . . . . 9
โข ๐ โ โ |
31 | 29, 30 | mulneg1i 11535 |
. . . . . . . 8
โข (-๐พ ยท ๐) = -(๐พ ยท ๐) |
32 | 31 | breq2i 5112 |
. . . . . . 7
โข (0 โค
(-๐พ ยท ๐) โ 0 โค -(๐พ ยท ๐)) |
33 | 28, 32 | bitr4i 278 |
. . . . . 6
โข ((๐พ ยท ๐) โค 0 โ 0 โค (-๐พ ยท ๐)) |
34 | 25, 33 | syl6ibr 252 |
. . . . 5
โข (๐ < ๐ โ (๐พ โค 0 โ (๐พ ยท ๐) โค 0)) |
35 | 26, 3, 14 | lelttri 11216 |
. . . . . 6
โข (((๐พ ยท ๐) โค 0 โง 0 < ๐) โ (๐พ ยท ๐) < ๐) |
36 | 13, 35 | mpan2 690 |
. . . . 5
โข ((๐พ ยท ๐) โค 0 โ (๐พ ยท ๐) < ๐) |
37 | 34, 36 | syl6 35 |
. . . 4
โข (๐ < ๐ โ (๐พ โค 0 โ (๐พ ยท ๐) < ๐)) |
38 | | lemulge12 11952 |
. . . . . . . 8
โข (((๐ โ โ โง ๐พ โ โ) โง (0 โค
๐ โง 1 โค ๐พ)) โ ๐ โค (๐พ ยท ๐)) |
39 | 16, 2, 38 | mpanl12 701 |
. . . . . . 7
โข ((0 โค
๐ โง 1 โค ๐พ) โ ๐ โค (๐พ ยท ๐)) |
40 | 20, 39 | sylan 581 |
. . . . . 6
โข ((๐ < ๐ โง 1 โค ๐พ) โ ๐ โค (๐พ ยท ๐)) |
41 | 40 | ex 414 |
. . . . 5
โข (๐ < ๐ โ (1 โค ๐พ โ ๐ โค (๐พ ยท ๐))) |
42 | 14, 16, 26 | ltletri 11217 |
. . . . . 6
โข ((๐ < ๐ โง ๐ โค (๐พ ยท ๐)) โ ๐ < (๐พ ยท ๐)) |
43 | 42 | ex 414 |
. . . . 5
โข (๐ < ๐ โ (๐ โค (๐พ ยท ๐) โ ๐ < (๐พ ยท ๐))) |
44 | 41, 43 | syld 47 |
. . . 4
โข (๐ < ๐ โ (1 โค ๐พ โ ๐ < (๐พ ยท ๐))) |
45 | 37, 44 | orim12d 964 |
. . 3
โข (๐ < ๐ โ ((๐พ โค 0 โจ 1 โค ๐พ) โ ((๐พ ยท ๐) < ๐ โจ ๐ < (๐พ ยท ๐)))) |
46 | 9, 45 | mpi 20 |
. 2
โข (๐ < ๐ โ ((๐พ ยท ๐) < ๐ โจ ๐ < (๐พ ยท ๐))) |
47 | 26, 14 | lttri2i 11203 |
. 2
โข ((๐พ ยท ๐) โ ๐ โ ((๐พ ยท ๐) < ๐ โจ ๐ < (๐พ ยท ๐))) |
48 | 46, 47 | sylibr 233 |
1
โข (๐ < ๐ โ (๐พ ยท ๐) โ ๐) |