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 )