Metamath Proof Explorer


Theorem dvdslelem

Description: Lemma for dvdsle . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Hypotheses dvdslelem.1 M
dvdslelem.2 N
dvdslelem.3 K
Assertion dvdslelem N<MK MN

Proof

Step Hyp Ref Expression
1 dvdslelem.1 M
2 dvdslelem.2 N
3 dvdslelem.3 K
4 3 zrei K
5 0re 0
6 lelttric K0K00<K
7 4 5 6 mp2an K00<K
8 zgt0ge1 K0<K1K
9 3 8 ax-mp 0<K1K
10 9 orbi2i K00<KK01K
11 7 10 mpbi K01K
12 le0neg1 KK00K
13 4 12 ax-mp K00K
14 2 nngt0i 0<N
15 2 nnrei N
16 1 zrei M
17 5 15 16 lttri 0<NN<M0<M
18 14 17 mpan N<M0<M
19 5 16 ltlei 0<M0M
20 18 19 syl N<M0M
21 4 renegcli K
22 21 16 mulge0i 0K0M0K M
23 20 22 sylan2 0KN<M0K M
24 13 23 sylanb K0N<M0K M
25 24 expcom N<MK00K M
26 4 16 remulcli K M
27 le0neg1 K MK M00K M
28 26 27 ax-mp K M00K M
29 4 recni K
30 16 recni M
31 29 30 mulneg1i K M=K M
32 31 breq2i 0K M0K M
33 28 32 bitr4i K M00K M
34 25 33 syl6ibr N<MK0K M0
35 26 5 15 lelttri K M00<NK M<N
36 14 35 mpan2 K M0K M<N
37 34 36 syl6 N<MK0K M<N
38 lemulge12 MK0M1KMK M
39 16 4 38 mpanl12 0M1KMK M
40 20 39 sylan N<M1KMK M
41 40 ex N<M1KMK M
42 15 16 26 ltletri N<MMK MN<K M
43 42 ex N<MMK MN<K M
44 41 43 syld N<M1KN<K M
45 37 44 orim12d N<MK01KK M<NN<K M
46 11 45 mpi N<MK M<NN<K M
47 26 15 lttri2i K MNK M<NN<K M
48 46 47 sylibr N<MK MN