Metamath Proof Explorer


Theorem divalgb

Description: Express the division algorithm as stated in divalg in terms of || . (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion divalgb NDD0∃!rq0rr<DN=qD+r∃!r0r<DDNr

Proof

Step Hyp Ref Expression
1 df-3an 0rr<DN=qD+r0rr<DN=qD+r
2 1 rexbii q0rr<DN=qD+rq0rr<DN=qD+r
3 r19.42v q0rr<DN=qD+r0rr<DqN=qD+r
4 2 3 bitri q0rr<DN=qD+r0rr<DqN=qD+r
5 zsubcl NrNr
6 divides DNrDNrqqD=Nr
7 5 6 sylan2 DNrDNrqqD=Nr
8 7 3impb DNrDNrqqD=Nr
9 8 3com12 NDrDNrqqD=Nr
10 zcn NN
11 zcn rr
12 zmulcl qDqD
13 12 zcnd qDqD
14 subadd NrqDNr=qDr+qD=N
15 10 11 13 14 syl3an NrqDNr=qDr+qD=N
16 addcom rqDr+qD=qD+r
17 11 13 16 syl2an rqDr+qD=qD+r
18 17 3adant1 NrqDr+qD=qD+r
19 18 eqeq1d NrqDr+qD=NqD+r=N
20 15 19 bitrd NrqDNr=qDqD+r=N
21 eqcom Nr=qDqD=Nr
22 eqcom qD+r=NN=qD+r
23 20 21 22 3bitr3g NrqDqD=NrN=qD+r
24 23 3expia NrqDqD=NrN=qD+r
25 24 expcomd NrDqqD=NrN=qD+r
26 25 3impia NrDqqD=NrN=qD+r
27 26 imp NrDqqD=NrN=qD+r
28 27 rexbidva NrDqqD=NrqN=qD+r
29 28 3com23 NDrqqD=NrqN=qD+r
30 9 29 bitrd NDrDNrqN=qD+r
31 30 anbi2d NDr0rr<DDNr0rr<DqN=qD+r
32 4 31 bitr4id NDrq0rr<DN=qD+r0rr<DDNr
33 anass 0rr<DDNr0rr<DDNr
34 32 33 bitrdi NDrq0rr<DN=qD+r0rr<DDNr
35 34 3expa NDrq0rr<DN=qD+r0rr<DDNr
36 35 reubidva ND∃!rq0rr<DN=qD+r∃!r0rr<DDNr
37 elnn0z r0r0r
38 37 anbi1i r0r<DDNrr0rr<DDNr
39 anass r0rr<DDNrr0rr<DDNr
40 38 39 bitri r0r<DDNrr0rr<DDNr
41 40 eubii ∃!rr0r<DDNr∃!rr0rr<DDNr
42 df-reu ∃!r0r<DDNr∃!rr0r<DDNr
43 df-reu ∃!r0rr<DDNr∃!rr0rr<DDNr
44 41 42 43 3bitr4ri ∃!r0rr<DDNr∃!r0r<DDNr
45 36 44 bitrdi ND∃!rq0rr<DN=qD+r∃!r0r<DDNr
46 45 3adant3 NDD0∃!rq0rr<DN=qD+r∃!r0r<DDNr