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

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ↔ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
2 1 3anbi3d ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
3 2 rexbidv ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
4 3 reubidv ⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ) )
5 fveq2 ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( abs ‘ 𝐷 ) = ( abs ‘ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) )
6 5 breq2d ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( 𝑟 < ( abs ‘ 𝐷 ) ↔ 𝑟 < ( abs ‘ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) ) )
7 oveq2 ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( 𝑞 · 𝐷 ) = ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) )
8 7 oveq1d ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( ( 𝑞 · 𝐷 ) + 𝑟 ) = ( ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) + 𝑟 ) )
9 8 eqeq2d ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ↔ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) + 𝑟 ) ) )
10 6 9 3anbi23d ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) + 𝑟 ) ) ) )
11 10 rexbidv ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) + 𝑟 ) ) ) )
12 11 reubidv ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) ↔ ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) + 𝑟 ) ) ) )
13 1z ⊢ 1 ∈ ℤ
14 13 elimel ⊢ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) ∈ ℤ
15 simpl ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → 𝐷 ∈ ℤ )
16 eleq1 ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( 𝐷 ∈ ℤ ↔ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ∈ ℤ ) )
17 eleq1 ⊢ ( 1 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( 1 ∈ ℤ ↔ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ∈ ℤ ) )
18 15 16 17 13 elimdhyp ⊢ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ∈ ℤ
19 simpr ⊢ ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → 𝐷 ≠ 0 )
20 neeq1 ⊢ ( 𝐷 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( 𝐷 ≠ 0 ↔ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ≠ 0 ) )
21 neeq1 ⊢ ( 1 = if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) → ( 1 ≠ 0 ↔ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ≠ 0 ) )
22 ax-1ne0 ⊢ 1 ≠ 0
23 19 20 21 22 elimdhyp ⊢ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ≠ 0
24 eqid ⊢ { 𝑟 ∈ ℕ0 ∣ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ∥ ( if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) − 𝑟 ) } = { 𝑟 ∈ ℕ0 ∣ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ∥ ( if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) − 𝑟 ) }
25 14 18 23 24 divalglem10 ⊢ ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) ∧ if ( 𝑁 ∈ ℤ , 𝑁 , 1 ) = ( ( 𝑞 · if ( ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) , 𝐷 , 1 ) ) + 𝑟 ) )
26 4 12 25 dedth2h ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) ) → ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )
27 26 3impb ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ) → ∃! 𝑟 ∈ ℤ ∃ 𝑞 ∈ ℤ ( 0 ≤ 𝑟 ∧ 𝑟 < ( abs ‘ 𝐷 ) ∧ 𝑁 = ( ( 𝑞 · 𝐷 ) + 𝑟 ) ) )