Metamath Proof Explorer

Theorem quoremnn0ALT

Description: Alternate proof of quoremnn0 not using quoremz . TODO - Keep either quoremnn0ALT (if we don't keep quoremz ) or quoremnn0 ? (Contributed by NM, 14-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses quorem.1 
|- Q = ( |_ ` ( A / B ) )
quorem.2 
|- R = ( A - ( B x. Q ) )
Assertion quoremnn0ALT 
|- ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. NN0 /\ 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 fldivnn0 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( |_ ` ( A / B ) ) e. NN0 )
4 1 3 eqeltrid 
 |-  ( ( A e. NN0 /\ B e. NN ) -> Q e. NN0 )
5 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
6 5 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> B e. NN0 )
7 6 4 nn0mulcld 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B x. Q ) e. NN0 )
8 simpl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> A e. NN0 )
9 4 nn0cnd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> Q e. CC )
10 nncn 
 |-  ( B e. NN -> B e. CC )
11 10 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> B e. CC )
12 nnne0 
 |-  ( B e. NN -> B =/= 0 )
13 12 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> B =/= 0 )
14 9 11 13 divcan3d 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( B x. Q ) / B ) = Q )
15 nn0nndivcl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) e. RR )
16 flle 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) <_ ( A / B ) )
17 15 16 syl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( |_ ` ( A / B ) ) <_ ( A / B ) )
18 1 17 eqbrtrid 
 |-  ( ( A e. NN0 /\ B e. NN ) -> Q <_ ( A / B ) )
19 14 18 eqbrtrd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( B x. Q ) / B ) <_ ( A / B ) )
20 7 nn0red 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B x. Q ) e. RR )
21 nn0re 
 |-  ( A e. NN0 -> A e. RR )
22 21 adantr 
 |-  ( ( A e. NN0 /\ B e. NN ) -> A e. RR )
23 nnre 
 |-  ( B e. NN -> B e. RR )
24 23 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> B e. RR )
25 nngt0 
 |-  ( B e. NN -> 0 < B )
26 25 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> 0 < B )
27 lediv1 
 |-  ( ( ( B x. Q ) e. RR /\ A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( B x. Q ) <_ A <-> ( ( B x. Q ) / B ) <_ ( A / B ) ) )
28 20 22 24 26 27 syl112anc 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( B x. Q ) <_ A <-> ( ( B x. Q ) / B ) <_ ( A / B ) ) )
29 19 28 mpbird 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B x. Q ) <_ A )
30 nn0sub2 
 |-  ( ( ( B x. Q ) e. NN0 /\ A e. NN0 /\ ( B x. Q ) <_ A ) -> ( A - ( B x. Q ) ) e. NN0 )
31 7 8 29 30 syl3anc 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( A - ( B x. Q ) ) e. NN0 )
32 2 31 eqeltrid 
 |-  ( ( A e. NN0 /\ B e. NN ) -> R e. NN0 )
33 1 oveq2i 
 |-  ( ( A / B ) - Q ) = ( ( A / B ) - ( |_ ` ( A / B ) ) )
34 fraclt1 
 |-  ( ( A / B ) e. RR -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < 1 )
35 15 34 syl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) - ( |_ ` ( A / B ) ) ) < 1 )
36 33 35 eqbrtrid 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) - Q ) < 1 )
37 2 oveq1i 
 |-  ( R / B ) = ( ( A - ( B x. Q ) ) / B )
38 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
39 38 adantr 
 |-  ( ( A e. NN0 /\ B e. NN ) -> A e. CC )
40 7 nn0cnd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B x. Q ) e. CC )
41 10 12 jca 
 |-  ( B e. NN -> ( B e. CC /\ B =/= 0 ) )
42 41 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B e. CC /\ B =/= 0 ) )
43 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 ) ) )
44 39 40 42 43 syl3anc 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A - ( B x. Q ) ) / B ) = ( ( A / B ) - ( ( B x. Q ) / B ) ) )
45 14 oveq2d 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A / B ) - ( ( B x. Q ) / B ) ) = ( ( A / B ) - Q ) )
46 44 45 eqtrd 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( A - ( B x. Q ) ) / B ) = ( ( A / B ) - Q ) )
47 37 46 eqtrid 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( R / B ) = ( ( A / B ) - Q ) )
48 10 12 dividd 
 |-  ( B e. NN -> ( B / B ) = 1 )
49 48 adantl 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( B / B ) = 1 )
50 36 47 49 3brtr4d 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( R / B ) < ( B / B ) )
51 32 nn0red 
 |-  ( ( A e. NN0 /\ B e. NN ) -> R e. RR )
52 ltdiv1 
 |-  ( ( R e. RR /\ B e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( R < B <-> ( R / B ) < ( B / B ) ) )
53 51 24 24 26 52 syl112anc 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( R < B <-> ( R / B ) < ( B / B ) ) )
54 50 53 mpbird 
 |-  ( ( A e. NN0 /\ B e. NN ) -> R < B )
55 2 oveq2i 
 |-  ( ( B x. Q ) + R ) = ( ( B x. Q ) + ( A - ( B x. Q ) ) )
56 40 39 pncan3d 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( B x. Q ) + ( A - ( B x. Q ) ) ) = A )
57 55 56 eqtr2id 
 |-  ( ( A e. NN0 /\ B e. NN ) -> A = ( ( B x. Q ) + R ) )
58 54 57 jca 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( R < B /\ A = ( ( B x. Q ) + R ) ) )
59 4 32 58 jca31 
 |-  ( ( A e. NN0 /\ B e. NN ) -> ( ( Q e. NN0 /\ R e. NN0 ) /\ ( R < B /\ A = ( ( B x. Q ) + R ) ) ) )