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

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 mullidd 
 |-  ( 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 )