| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvdslelem.1 |
|- M e. ZZ |
| 2 |
|
dvdslelem.2 |
|- N e. NN |
| 3 |
|
dvdslelem.3 |
|- K e. ZZ |
| 4 |
3
|
zrei |
|- K e. RR |
| 5 |
|
0re |
|- 0 e. RR |
| 6 |
|
lelttric |
|- ( ( K e. RR /\ 0 e. RR ) -> ( K <_ 0 \/ 0 < K ) ) |
| 7 |
4 5 6
|
mp2an |
|- ( K <_ 0 \/ 0 < K ) |
| 8 |
|
zgt0ge1 |
|- ( K e. ZZ -> ( 0 < K <-> 1 <_ K ) ) |
| 9 |
3 8
|
ax-mp |
|- ( 0 < K <-> 1 <_ K ) |
| 10 |
9
|
orbi2i |
|- ( ( K <_ 0 \/ 0 < K ) <-> ( K <_ 0 \/ 1 <_ K ) ) |
| 11 |
7 10
|
mpbi |
|- ( K <_ 0 \/ 1 <_ K ) |
| 12 |
|
le0neg1 |
|- ( K e. RR -> ( K <_ 0 <-> 0 <_ -u K ) ) |
| 13 |
4 12
|
ax-mp |
|- ( K <_ 0 <-> 0 <_ -u K ) |
| 14 |
2
|
nngt0i |
|- 0 < N |
| 15 |
2
|
nnrei |
|- N e. RR |
| 16 |
1
|
zrei |
|- M e. RR |
| 17 |
5 15 16
|
lttri |
|- ( ( 0 < N /\ N < M ) -> 0 < M ) |
| 18 |
14 17
|
mpan |
|- ( N < M -> 0 < M ) |
| 19 |
5 16
|
ltlei |
|- ( 0 < M -> 0 <_ M ) |
| 20 |
18 19
|
syl |
|- ( N < M -> 0 <_ M ) |
| 21 |
4
|
renegcli |
|- -u K e. RR |
| 22 |
21 16
|
mulge0i |
|- ( ( 0 <_ -u K /\ 0 <_ M ) -> 0 <_ ( -u K x. M ) ) |
| 23 |
20 22
|
sylan2 |
|- ( ( 0 <_ -u K /\ N < M ) -> 0 <_ ( -u K x. M ) ) |
| 24 |
13 23
|
sylanb |
|- ( ( K <_ 0 /\ N < M ) -> 0 <_ ( -u K x. M ) ) |
| 25 |
24
|
expcom |
|- ( N < M -> ( K <_ 0 -> 0 <_ ( -u K x. M ) ) ) |
| 26 |
4 16
|
remulcli |
|- ( K x. M ) e. RR |
| 27 |
|
le0neg1 |
|- ( ( K x. M ) e. RR -> ( ( K x. M ) <_ 0 <-> 0 <_ -u ( K x. M ) ) ) |
| 28 |
26 27
|
ax-mp |
|- ( ( K x. M ) <_ 0 <-> 0 <_ -u ( K x. M ) ) |
| 29 |
4
|
recni |
|- K e. CC |
| 30 |
16
|
recni |
|- M e. CC |
| 31 |
29 30
|
mulneg1i |
|- ( -u K x. M ) = -u ( K x. M ) |
| 32 |
31
|
breq2i |
|- ( 0 <_ ( -u K x. M ) <-> 0 <_ -u ( K x. M ) ) |
| 33 |
28 32
|
bitr4i |
|- ( ( K x. M ) <_ 0 <-> 0 <_ ( -u K x. M ) ) |
| 34 |
25 33
|
imbitrrdi |
|- ( N < M -> ( K <_ 0 -> ( K x. M ) <_ 0 ) ) |
| 35 |
26 5 15
|
lelttri |
|- ( ( ( K x. M ) <_ 0 /\ 0 < N ) -> ( K x. M ) < N ) |
| 36 |
14 35
|
mpan2 |
|- ( ( K x. M ) <_ 0 -> ( K x. M ) < N ) |
| 37 |
34 36
|
syl6 |
|- ( N < M -> ( K <_ 0 -> ( K x. M ) < N ) ) |
| 38 |
|
lemulge12 |
|- ( ( ( M e. RR /\ K e. RR ) /\ ( 0 <_ M /\ 1 <_ K ) ) -> M <_ ( K x. M ) ) |
| 39 |
16 4 38
|
mpanl12 |
|- ( ( 0 <_ M /\ 1 <_ K ) -> M <_ ( K x. M ) ) |
| 40 |
20 39
|
sylan |
|- ( ( N < M /\ 1 <_ K ) -> M <_ ( K x. M ) ) |
| 41 |
40
|
ex |
|- ( N < M -> ( 1 <_ K -> M <_ ( K x. M ) ) ) |
| 42 |
15 16 26
|
ltletri |
|- ( ( N < M /\ M <_ ( K x. M ) ) -> N < ( K x. M ) ) |
| 43 |
42
|
ex |
|- ( N < M -> ( M <_ ( K x. M ) -> N < ( K x. M ) ) ) |
| 44 |
41 43
|
syld |
|- ( N < M -> ( 1 <_ K -> N < ( K x. M ) ) ) |
| 45 |
37 44
|
orim12d |
|- ( N < M -> ( ( K <_ 0 \/ 1 <_ K ) -> ( ( K x. M ) < N \/ N < ( K x. M ) ) ) ) |
| 46 |
11 45
|
mpi |
|- ( N < M -> ( ( K x. M ) < N \/ N < ( K x. M ) ) ) |
| 47 |
26 15
|
lttri2i |
|- ( ( K x. M ) =/= N <-> ( ( K x. M ) < N \/ N < ( K x. M ) ) ) |
| 48 |
46 47
|
sylibr |
|- ( N < M -> ( K x. M ) =/= N ) |