Description: Lemma for dvdsle . (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvdslelem.1 | |
|
dvdslelem.2 | |
||
dvdslelem.3 | |
||
Assertion | dvdslelem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdslelem.1 | |
|
2 | dvdslelem.2 | |
|
3 | dvdslelem.3 | |
|
4 | 3 | zrei | |
5 | 0re | |
|
6 | lelttric | |
|
7 | 4 5 6 | mp2an | |
8 | zgt0ge1 | |
|
9 | 3 8 | ax-mp | |
10 | 9 | orbi2i | |
11 | 7 10 | mpbi | |
12 | le0neg1 | |
|
13 | 4 12 | ax-mp | |
14 | 2 | nngt0i | |
15 | 2 | nnrei | |
16 | 1 | zrei | |
17 | 5 15 16 | lttri | |
18 | 14 17 | mpan | |
19 | 5 16 | ltlei | |
20 | 18 19 | syl | |
21 | 4 | renegcli | |
22 | 21 16 | mulge0i | |
23 | 20 22 | sylan2 | |
24 | 13 23 | sylanb | |
25 | 24 | expcom | |
26 | 4 16 | remulcli | |
27 | le0neg1 | |
|
28 | 26 27 | ax-mp | |
29 | 4 | recni | |
30 | 16 | recni | |
31 | 29 30 | mulneg1i | |
32 | 31 | breq2i | |
33 | 28 32 | bitr4i | |
34 | 25 33 | syl6ibr | |
35 | 26 5 15 | lelttri | |
36 | 14 35 | mpan2 | |
37 | 34 36 | syl6 | |
38 | lemulge12 | |
|
39 | 16 4 38 | mpanl12 | |
40 | 20 39 | sylan | |
41 | 40 | ex | |
42 | 15 16 26 | ltletri | |
43 | 42 | ex | |
44 | 41 43 | syld | |
45 | 37 44 | orim12d | |
46 | 11 45 | mpi | |
47 | 26 15 | lttri2i | |
48 | 46 47 | sylibr | |