Metamath Proof Explorer

Theorem quoremz

Description: Quotient and remainder of an integer divided by a positive integer. TODO - is this really needed for anything? Should we use mod to simplify it? Remark (AV): This is a special case of divalg . (Contributed by NM, 14-Aug-2008)

Ref Expression
Hypotheses quorem.1 
|- Q = ( |_ ` ( A / B ) )
quorem.2 
|- R = ( A - ( B x. Q ) )
Assertion quoremz 
|- ( ( A e. ZZ /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )

Proof

Step Hyp Ref Expression
1 quorem.1 
 |-  Q = ( |_ ` ( A / B ) )
2 quorem.2 
 |-  R = ( A - ( B x. Q ) )
3 zre 
 |-  ( A e. ZZ -> A e. RR )
4 3 adantr 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A e. RR )
5 nnre 
 |-  ( B e. NN -> B e. RR )
6 5 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. RR )
7 nnne0 
 |-  ( B e. NN -> B =/= 0 )
8 7 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B =/= 0 )
9 4 6 8 redivcld 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. RR )
10 9 flcld 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( |_ ` ( A / B ) ) e. ZZ )
11 1 10 eqeltrid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> Q e. ZZ )
12 11 zcnd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> Q e. CC )
13 nncn 
 |-  ( B e. NN -> B e. CC )
14 13 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. CC )
15 12 14 8 divcan3d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( B x. Q ) / B ) = Q )
16 flle 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) <_ ( A / B ) )
17 9 16 syl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( |_ ` ( A / B ) ) <_ ( A / B ) )
18 1 17 eqbrtrid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> Q <_ ( A / B ) )
19 15 18 eqbrtrd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( B x. Q ) / B ) <_ ( A / B ) )
20 nnz 
 |-  ( B e. NN -> B e. ZZ )
21 20 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. ZZ )
22 21 11 zmulcld 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B x. Q ) e. ZZ )
23 22 zred 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B x. Q ) e. RR )
24 nngt0 
 |-  ( B e. NN -> 0 < B )
25 24 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 0 < B )
26 lediv1 
 |-  ( ( ( B x. Q ) e. RR /\ A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( B x. Q ) <_ A <-> ( ( B x. Q ) / B ) <_ ( A / B ) ) )
27 23 4 6 25 26 syl112anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( B x. Q ) <_ A <-> ( ( B x. Q ) / B ) <_ ( A / B ) ) )
28 19 27 mpbird 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B x. Q ) <_ A )
29 simpl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A e. ZZ )
30 znn0sub 
 |-  ( ( ( B x. Q ) e. ZZ /\ A e. ZZ ) -> ( ( B x. Q ) <_ A <-> ( A - ( B x. Q ) ) e. NN0 ) )
31 22 29 30 syl2anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( B x. Q ) <_ A <-> ( A - ( B x. Q ) ) e. NN0 ) )
32 28 31 mpbid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A - ( B x. Q ) ) e. NN0 )
33 2 32 eqeltrid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> R e. NN0 )
34 1 oveq2i 
 |-  ( ( A / B ) - Q ) = ( ( A / B ) - ( |_ ` ( A / B ) ) )
35 fraclt1 
 |-  ( ( A / B ) e. RR -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < 1 )
36 9 35 syl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < 1 )
37 34 36 eqbrtrid 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A / B ) - Q ) < 1 )
38 2 oveq1i 
 |-  ( R / B ) = ( ( A - ( B x. Q ) ) / B )
39 zcn 
 |-  ( A e. ZZ -> A e. CC )
40 39 adantr 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A e. CC )
41 22 zcnd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B x. Q ) e. CC )
42 13 7 jca 
 |-  ( B e. NN -> ( B e. CC /\ B =/= 0 ) )
43 42 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B e. CC /\ B =/= 0 ) )
44 divsubdir 
 |-  ( ( A e. CC /\ ( B x. Q ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A - ( B x. Q ) ) / B ) = ( ( A / B ) - ( ( B x. Q ) / B ) ) )
45 40 41 43 44 syl3anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A - ( B x. Q ) ) / B ) = ( ( A / B ) - ( ( B x. Q ) / B ) ) )
46 15 oveq2d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A / B ) - ( ( B x. Q ) / B ) ) = ( ( A / B ) - Q ) )
47 45 46 eqtrd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A - ( B x. Q ) ) / B ) = ( ( A / B ) - Q ) )
48 38 47 syl5eq 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( R / B ) = ( ( A / B ) - Q ) )
49 13 7 dividd 
 |-  ( B e. NN -> ( B / B ) = 1 )
50 49 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B / B ) = 1 )
51 37 48 50 3brtr4d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( R / B ) < ( B / B ) )
52 33 nn0red 
 |-  ( ( A e. ZZ /\ B e. NN ) -> R e. RR )
53 ltdiv1 
 |-  ( ( R e. RR /\ B e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( R < B <-> ( R / B ) < ( B / B ) ) )
54 52 6 6 25 53 syl112anc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( R < B <-> ( R / B ) < ( B / B ) ) )
55 51 54 mpbird 
 |-  ( ( A e. ZZ /\ B e. NN ) -> R < B )
56 2 oveq2i 
 |-  ( ( B x. Q ) + R ) = ( ( B x. Q ) + ( A - ( B x. Q ) ) )
57 41 40 pncan3d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( B x. Q ) + ( A - ( B x. Q ) ) ) = A )
58 56 57 syl5req 
 |-  ( ( A e. ZZ /\ B e. NN ) -> A = ( ( B x. Q ) + R ) )
59 55 58 jca 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( R < B /\ A = ( ( B x. Q ) + R ) ) )
60 11 33 59 jca31 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( Q e. ZZ /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )