Metamath Proof Explorer


Theorem gtndiv

Description: A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion gtndiv
|- ( ( A e. RR /\ B e. NN /\ B < A ) -> -. ( B / A ) e. ZZ )

Proof

Step Hyp Ref Expression
1 0z
 |-  0 e. ZZ
2 nnre
 |-  ( B e. NN -> B e. RR )
3 2 3ad2ant2
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> B e. RR )
4 simp1
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> A e. RR )
5 nngt0
 |-  ( B e. NN -> 0 < B )
6 5 3ad2ant2
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> 0 < B )
7 5 adantl
 |-  ( ( A e. RR /\ B e. NN ) -> 0 < B )
8 0re
 |-  0 e. RR
9 lttr
 |-  ( ( 0 e. RR /\ B e. RR /\ A e. RR ) -> ( ( 0 < B /\ B < A ) -> 0 < A ) )
10 8 9 mp3an1
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( 0 < B /\ B < A ) -> 0 < A ) )
11 2 10 sylan
 |-  ( ( B e. NN /\ A e. RR ) -> ( ( 0 < B /\ B < A ) -> 0 < A ) )
12 11 ancoms
 |-  ( ( A e. RR /\ B e. NN ) -> ( ( 0 < B /\ B < A ) -> 0 < A ) )
13 7 12 mpand
 |-  ( ( A e. RR /\ B e. NN ) -> ( B < A -> 0 < A ) )
14 13 3impia
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> 0 < A )
15 3 4 6 14 divgt0d
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> 0 < ( B / A ) )
16 simp3
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> B < A )
17 1re
 |-  1 e. RR
18 ltdivmul2
 |-  ( ( B e. RR /\ 1 e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( B / A ) < 1 <-> B < ( 1 x. A ) ) )
19 17 18 mp3an2
 |-  ( ( B e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( B / A ) < 1 <-> B < ( 1 x. A ) ) )
20 3 4 14 19 syl12anc
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> ( ( B / A ) < 1 <-> B < ( 1 x. A ) ) )
21 recn
 |-  ( A e. RR -> A e. CC )
22 21 mulid2d
 |-  ( A e. RR -> ( 1 x. A ) = A )
23 22 breq2d
 |-  ( A e. RR -> ( B < ( 1 x. A ) <-> B < A ) )
24 23 3ad2ant1
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> ( B < ( 1 x. A ) <-> B < A ) )
25 20 24 bitrd
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> ( ( B / A ) < 1 <-> B < A ) )
26 16 25 mpbird
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> ( B / A ) < 1 )
27 0p1e1
 |-  ( 0 + 1 ) = 1
28 26 27 breqtrrdi
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> ( B / A ) < ( 0 + 1 ) )
29 btwnnz
 |-  ( ( 0 e. ZZ /\ 0 < ( B / A ) /\ ( B / A ) < ( 0 + 1 ) ) -> -. ( B / A ) e. ZZ )
30 1 15 28 29 mp3an2i
 |-  ( ( A e. RR /\ B e. NN /\ B < A ) -> -. ( B / A ) e. ZZ )