Metamath Proof Explorer


Theorem divalg

Description: The division algorithm (theorem). Dividing an integer N by a nonzero integer D produces a (unique) quotient q and a unique remainder 0 <_ r < ( absD ) . Theorem 1.14 in ApostolNT p. 19. The proof does not use / or |_ or mod . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion divalg NDD0∃!rq0rr<DN=qD+r

Proof

Step Hyp Ref Expression
1 eqeq1 N=ifNN1N=qD+rifNN1=qD+r
2 1 3anbi3d N=ifNN10rr<DN=qD+r0rr<DifNN1=qD+r
3 2 rexbidv N=ifNN1q0rr<DN=qD+rq0rr<DifNN1=qD+r
4 3 reubidv N=ifNN1∃!rq0rr<DN=qD+r∃!rq0rr<DifNN1=qD+r
5 fveq2 D=ifDD0D1D=ifDD0D1
6 5 breq2d D=ifDD0D1r<Dr<ifDD0D1
7 oveq2 D=ifDD0D1qD=qifDD0D1
8 7 oveq1d D=ifDD0D1qD+r=qifDD0D1+r
9 8 eqeq2d D=ifDD0D1ifNN1=qD+rifNN1=qifDD0D1+r
10 6 9 3anbi23d D=ifDD0D10rr<DifNN1=qD+r0rr<ifDD0D1ifNN1=qifDD0D1+r
11 10 rexbidv D=ifDD0D1q0rr<DifNN1=qD+rq0rr<ifDD0D1ifNN1=qifDD0D1+r
12 11 reubidv D=ifDD0D1∃!rq0rr<DifNN1=qD+r∃!rq0rr<ifDD0D1ifNN1=qifDD0D1+r
13 1z 1
14 13 elimel ifNN1
15 simpl DD0D
16 eleq1 D=ifDD0D1DifDD0D1
17 eleq1 1=ifDD0D11ifDD0D1
18 15 16 17 13 elimdhyp ifDD0D1
19 simpr DD0D0
20 neeq1 D=ifDD0D1D0ifDD0D10
21 neeq1 1=ifDD0D110ifDD0D10
22 ax-1ne0 10
23 19 20 21 22 elimdhyp ifDD0D10
24 eqid r0|ifDD0D1ifNN1r=r0|ifDD0D1ifNN1r
25 14 18 23 24 divalglem10 ∃!rq0rr<ifDD0D1ifNN1=qifDD0D1+r
26 4 12 25 dedth2h NDD0∃!rq0rr<DN=qD+r
27 26 3impb NDD0∃!rq0rr<DN=qD+r