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 ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
2 1 rexbii ⊢ ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃ 𝑞 ∈ ℤ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
3 r19.42v ⊢ ( ∃ 𝑞 ∈ ℤ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
4 2 3 bitri ⊢ ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
5 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝑁 − 𝑟 ) ∈ ℤ )
6 divides ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑁 − 𝑟 ) ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ) )
7 5 6 sylan2 ⊢ ( ( 𝐷 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ) ) → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ) )
8 7 3impb ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ) )
9 8 3com12 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ) )
10 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
11 zcn ⊢ ( 𝑟 ∈ ℤ → 𝑟 ∈ ℂ )
12 zmulcl ⊢ ( ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝑞 · 𝐷 ) ∈ ℤ )
13 12 zcnd ⊢ ( ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝑞 · 𝐷 ) ∈ ℂ )
14 subadd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑟 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( ( 𝑁 − 𝑟 ) = ( 𝑞 · 𝐷 ) ↔ ( 𝑟 + ( 𝑞 · 𝐷 ) ) = 𝑁 ) )
15 10 11 13 14 syl3an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝑁 − 𝑟 ) = ( 𝑞 · 𝐷 ) ↔ ( 𝑟 + ( 𝑞 · 𝐷 ) ) = 𝑁 ) )
16 addcom ⊢ ( ( 𝑟 ∈ ℂ ∧ ( 𝑞 · 𝐷 ) ∈ ℂ ) → ( 𝑟 + ( 𝑞 · 𝐷 ) ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )
17 11 13 16 syl2an ⊢ ( ( 𝑟 ∈ ℤ ∧ ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝑟 + ( 𝑞 · 𝐷 ) ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )
18 17 3adant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝑟 + ( 𝑞 · 𝐷 ) ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )
19 18 eqeq1d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝑟 + ( 𝑞 · 𝐷 ) ) = 𝑁 ↔ ( ( 𝑞 · 𝐷 ) + 𝑟 ) = 𝑁 ) )
20 15 19 bitrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝑁 − 𝑟 ) = ( 𝑞 · 𝐷 ) ↔ ( ( 𝑞 · 𝐷 ) + 𝑟 ) = 𝑁 ) )
21 eqcom ⊢ ( ( 𝑁 − 𝑟 ) = ( 𝑞 · 𝐷 ) ↔ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) )
22 eqcom ⊢ ( ( ( 𝑞 · 𝐷 ) + 𝑟 ) = 𝑁 ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) )
23 20 21 22 3bitr3g ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
24 23 3expia ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( ( 𝑞 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
25 24 expcomd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝐷 ∈ ℤ → ( 𝑞 ∈ ℤ → ( ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) ) )
26 25 3impia ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝑞 ∈ ℤ → ( ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
27 26 imp ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ 𝑞 ∈ ℤ ) → ( ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
28 27 rexbidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑟 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
29 28 3com23 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( ∃ 𝑞 ∈ ℤ ( 𝑞 · 𝐷 ) = ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
30 9 29 bitrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( 𝐷 ∥ ( 𝑁 − 𝑟 ) ↔ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
31 30 anbi2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ ∃ 𝑞 ∈ ℤ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
32 4 31 bitr4id ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )
33 anass ⊢ ( ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )
34 32 33 bitrdi ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝑟 ∈ ℤ ) → ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
35 34 3expa ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ 𝑟 ∈ ℤ ) → ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
36 35 reubidva ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℤ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
37 elnn0z ⊢ ( 𝑟 ∈ ℕ0 ↔ ( 𝑟 ∈ ℤ ∧ 0 ≤ 𝑟 ) )
38 37 anbi1i ⊢ ( ( 𝑟 ∈ ℕ0 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ↔ ( ( 𝑟 ∈ ℤ ∧ 0 ≤ 𝑟 ) ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )
39 anass ⊢ ( ( ( 𝑟 ∈ ℤ ∧ 0 ≤ 𝑟 ) ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ↔ ( 𝑟 ∈ ℤ ∧ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
40 38 39 bitri ⊢ ( ( 𝑟 ∈ ℕ0 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ↔ ( 𝑟 ∈ ℤ ∧ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
41 40 eubii ⊢ ( ∃! 𝑟 ( 𝑟 ∈ ℕ0 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ↔ ∃! 𝑟 ( 𝑟 ∈ ℤ ∧ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
42 df-reu ⊢ ( ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ↔ ∃! 𝑟 ( 𝑟 ∈ ℕ0 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )
43 df-reu ⊢ ( ∃! 𝑟 ∈ ℤ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ↔ ∃! 𝑟 ( 𝑟 ∈ ℤ ∧ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ) )
44 41 42 43 3bitr4ri ⊢ ( ∃! 𝑟 ∈ ℤ ( 0 ≤ 𝑟 ∧ ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) )
45 36 44 bitrdi ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )
46 45 3adant3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℕ0 ( 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝐷 ∥ ( 𝑁 − 𝑟 ) ) ) )