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 ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ N = if N ∈ ℤ N 1 → N = q ⁢ D + r ↔ if N ∈ ℤ N 1 = q ⁢ D + r
2 1 3anbi3d ⊢ N = if N ∈ ℤ N 1 → 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r ↔ 0 ≤ r ∧ r < D ∧ if N ∈ ℤ N 1 = q ⁢ D + r
3 2 rexbidv ⊢ N = if N ∈ ℤ N 1 → ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r ↔ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ if N ∈ ℤ N 1 = q ⁢ D + r
4 3 reubidv ⊢ N = if N ∈ ℤ N 1 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r ↔ ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ if N ∈ ℤ N 1 = q ⁢ D + r
5 fveq2 ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → D = if D ∈ ℤ ∧ D ≠ 0 D 1
6 5 breq2d ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → r < D ↔ r < if D ∈ ℤ ∧ D ≠ 0 D 1
7 oveq2 ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → q ⁢ D = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1
8 7 oveq1d ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → q ⁢ D + r = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1 + r
9 8 eqeq2d ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → if N ∈ ℤ N 1 = q ⁢ D + r ↔ if N ∈ ℤ N 1 = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1 + r
10 6 9 3anbi23d ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → 0 ≤ r ∧ r < D ∧ if N ∈ ℤ N 1 = q ⁢ D + r ↔ 0 ≤ r ∧ r < if D ∈ ℤ ∧ D ≠ 0 D 1 ∧ if N ∈ ℤ N 1 = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1 + r
11 10 rexbidv ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ if N ∈ ℤ N 1 = q ⁢ D + r ↔ ∃ q ∈ ℤ 0 ≤ r ∧ r < if D ∈ ℤ ∧ D ≠ 0 D 1 ∧ if N ∈ ℤ N 1 = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1 + r
12 11 reubidv ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ if N ∈ ℤ N 1 = q ⁢ D + r ↔ ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < if D ∈ ℤ ∧ D ≠ 0 D 1 ∧ if N ∈ ℤ N 1 = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1 + r
13 1z ⊢ 1 ∈ ℤ
14 13 elimel ⊢ if N ∈ ℤ N 1 ∈ ℤ
15 simpl ⊢ D ∈ ℤ ∧ D ≠ 0 → D ∈ ℤ
16 eleq1 ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → D ∈ ℤ ↔ if D ∈ ℤ ∧ D ≠ 0 D 1 ∈ ℤ
17 eleq1 ⊢ 1 = if D ∈ ℤ ∧ D ≠ 0 D 1 → 1 ∈ ℤ ↔ if D ∈ ℤ ∧ D ≠ 0 D 1 ∈ ℤ
18 15 16 17 13 elimdhyp ⊢ if D ∈ ℤ ∧ D ≠ 0 D 1 ∈ ℤ
19 simpr ⊢ D ∈ ℤ ∧ D ≠ 0 → D ≠ 0
20 neeq1 ⊢ D = if D ∈ ℤ ∧ D ≠ 0 D 1 → D ≠ 0 ↔ if D ∈ ℤ ∧ D ≠ 0 D 1 ≠ 0
21 neeq1 ⊢ 1 = if D ∈ ℤ ∧ D ≠ 0 D 1 → 1 ≠ 0 ↔ if D ∈ ℤ ∧ D ≠ 0 D 1 ≠ 0
22 ax-1ne0 ⊢ 1 ≠ 0
23 19 20 21 22 elimdhyp ⊢ if D ∈ ℤ ∧ D ≠ 0 D 1 ≠ 0
24 eqid ⊢ r ∈ ℕ 0 | if D ∈ ℤ ∧ D ≠ 0 D 1 ∥ if N ∈ ℤ N 1 − r = r ∈ ℕ 0 | if D ∈ ℤ ∧ D ≠ 0 D 1 ∥ if N ∈ ℤ N 1 − r
25 14 18 23 24 divalglem10 ⊢ ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < if D ∈ ℤ ∧ D ≠ 0 D 1 ∧ if N ∈ ℤ N 1 = q ⁢ if D ∈ ℤ ∧ D ≠ 0 D 1 + r
26 4 12 25 dedth2h ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r
27 26 3impb ⊢ N ∈ ℤ ∧ D ∈ ℤ ∧ D ≠ 0 → ∃! r ∈ ℤ ∃ q ∈ ℤ 0 ≤ r ∧ r < D ∧ N = q ⁢ D + r