This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdsle

Description: The divisors of a positive integer are bounded by it. The proof does not use / . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdsle 
|- ( ( M e. ZZ /\ N e. NN ) -> ( M || N -> M <_ N ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( M = if ( M e. ZZ , M , 1 ) -> ( N < M <-> N < if ( M e. ZZ , M , 1 ) ) )
2 oveq2 
 |-  ( M = if ( M e. ZZ , M , 1 ) -> ( n x. M ) = ( n x. if ( M e. ZZ , M , 1 ) ) )
3 2 neeq1d 
 |-  ( M = if ( M e. ZZ , M , 1 ) -> ( ( n x. M ) =/= N <-> ( n x. if ( M e. ZZ , M , 1 ) ) =/= N ) )
4 1 3 imbi12d 
 |-  ( M = if ( M e. ZZ , M , 1 ) -> ( ( N < M -> ( n x. M ) =/= N ) <-> ( N < if ( M e. ZZ , M , 1 ) -> ( n x. if ( M e. ZZ , M , 1 ) ) =/= N ) ) )
5 breq1 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( N < if ( M e. ZZ , M , 1 ) <-> if ( N e. NN , N , 1 ) < if ( M e. ZZ , M , 1 ) ) )
6 neeq2 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( n x. if ( M e. ZZ , M , 1 ) ) =/= N <-> ( n x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) ) )
7 5 6 imbi12d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( N < if ( M e. ZZ , M , 1 ) -> ( n x. if ( M e. ZZ , M , 1 ) ) =/= N ) <-> ( if ( N e. NN , N , 1 ) < if ( M e. ZZ , M , 1 ) -> ( n x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) ) ) )
8 oveq1 
 |-  ( n = if ( n e. ZZ , n , 1 ) -> ( n x. if ( M e. ZZ , M , 1 ) ) = ( if ( n e. ZZ , n , 1 ) x. if ( M e. ZZ , M , 1 ) ) )
9 8 neeq1d 
 |-  ( n = if ( n e. ZZ , n , 1 ) -> ( ( n x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) <-> ( if ( n e. ZZ , n , 1 ) x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) ) )
10 9 imbi2d 
 |-  ( n = if ( n e. ZZ , n , 1 ) -> ( ( if ( N e. NN , N , 1 ) < if ( M e. ZZ , M , 1 ) -> ( n x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) ) <-> ( if ( N e. NN , N , 1 ) < if ( M e. ZZ , M , 1 ) -> ( if ( n e. ZZ , n , 1 ) x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) ) ) )
11 1z 
 |-  1 e. ZZ
12 11 elimel 
 |-  if ( M e. ZZ , M , 1 ) e. ZZ
13 1nn 
 |-  1 e. NN
14 13 elimel 
 |-  if ( N e. NN , N , 1 ) e. NN
15 11 elimel 
 |-  if ( n e. ZZ , n , 1 ) e. ZZ
16 12 14 15 dvdslelem 
 |-  ( if ( N e. NN , N , 1 ) < if ( M e. ZZ , M , 1 ) -> ( if ( n e. ZZ , n , 1 ) x. if ( M e. ZZ , M , 1 ) ) =/= if ( N e. NN , N , 1 ) )
17 4 7 10 16 dedth3h 
 |-  ( ( M e. ZZ /\ N e. NN /\ n e. ZZ ) -> ( N < M -> ( n x. M ) =/= N ) )
18 17 3expia 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( n e. ZZ -> ( N < M -> ( n x. M ) =/= N ) ) )
19 18 com23 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N < M -> ( n e. ZZ -> ( n x. M ) =/= N ) ) )
20 19 3impia 
 |-  ( ( M e. ZZ /\ N e. NN /\ N < M ) -> ( n e. ZZ -> ( n x. M ) =/= N ) )
21 20 imp 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ N < M ) /\ n e. ZZ ) -> ( n x. M ) =/= N )
22 21 neneqd 
 |-  ( ( ( M e. ZZ /\ N e. NN /\ N < M ) /\ n e. ZZ ) -> -. ( n x. M ) = N )
23 22 nrexdv 
 |-  ( ( M e. ZZ /\ N e. NN /\ N < M ) -> -. E. n e. ZZ ( n x. M ) = N )
24 nnz 
 |-  ( N e. NN -> N e. ZZ )
25 divides 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )
26 24 25 sylan2 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )
27 26 3adant3 
 |-  ( ( M e. ZZ /\ N e. NN /\ N < M ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )
28 23 27 mtbird 
 |-  ( ( M e. ZZ /\ N e. NN /\ N < M ) -> -. M || N )
29 28 3expia 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( N < M -> -. M || N ) )
30 29 con2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M || N -> -. N < M ) )
31 zre 
 |-  ( M e. ZZ -> M e. RR )
32 nnre 
 |-  ( N e. NN -> N e. RR )
33 lenlt 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> -. N < M ) )
34 31 32 33 syl2an 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M <_ N <-> -. N < M ) )
35 30 34 sylibrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M || N -> M <_ N ) )