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 Q
Assertion quoremnn0ALT A 0 B Q 0 R 0 R < B A = B Q + R

Proof

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