Metamath Proof Explorer

Theorem quoremz

Description: Quotient and remainder of an integer divided by a positive integer. TODO - is this really needed for anything? Should we use mod to simplify it? Remark (AV): This is a special case of divalg . (Contributed by NM, 14-Aug-2008)

Ref Expression
Hypotheses quorem.1 ⊢ 𝑄 = ( ⌊ ‘ ( 𝐴 / 𝐵 ) )
quorem.2 ⊢ 𝑅 = ( 𝐴 − ( 𝐵 · 𝑄 ) )
Assertion quoremz ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0 ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 quorem.1 ⊢ 𝑄 = ( ⌊ ‘ ( 𝐴 / 𝐵 ) )
2 quorem.2 ⊢ 𝑅 = ( 𝐴 − ( 𝐵 · 𝑄 ) )
3 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℝ )
5 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
6 5 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ )
7 nnne0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
8 7 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ≠ 0 )
9 4 6 8 redivcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
10 9 flcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℤ )
11 1 10 eqeltrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝑄 ∈ ℤ )
12 11 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝑄 ∈ ℂ )
13 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
14 13 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℂ )
15 12 14 8 divcan3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 · 𝑄 ) / 𝐵 ) = 𝑄 )
16 flle ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ≤ ( 𝐴 / 𝐵 ) )
17 9 16 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ≤ ( 𝐴 / 𝐵 ) )
18 1 17 eqbrtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝑄 ≤ ( 𝐴 / 𝐵 ) )
19 15 18 eqbrtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 · 𝑄 ) / 𝐵 ) ≤ ( 𝐴 / 𝐵 ) )
20 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
21 20 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℤ )
22 21 11 zmulcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · 𝑄 ) ∈ ℤ )
23 22 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · 𝑄 ) ∈ ℝ )
24 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
25 24 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 0 < 𝐵 )
26 lediv1 ⊢ ( ( ( 𝐵 · 𝑄 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐵 · 𝑄 ) ≤ 𝐴 ↔ ( ( 𝐵 · 𝑄 ) / 𝐵 ) ≤ ( 𝐴 / 𝐵 ) ) )
27 23 4 6 25 26 syl112anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 · 𝑄 ) ≤ 𝐴 ↔ ( ( 𝐵 · 𝑄 ) / 𝐵 ) ≤ ( 𝐴 / 𝐵 ) ) )
28 19 27 mpbird ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · 𝑄 ) ≤ 𝐴 )
29 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℤ )
30 znn0sub ⊢ ( ( ( 𝐵 · 𝑄 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐵 · 𝑄 ) ≤ 𝐴 ↔ ( 𝐴 − ( 𝐵 · 𝑄 ) ) ∈ ℕ0 ) )
31 22 29 30 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 · 𝑄 ) ≤ 𝐴 ↔ ( 𝐴 − ( 𝐵 · 𝑄 ) ) ∈ ℕ0 ) )
32 28 31 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 − ( 𝐵 · 𝑄 ) ) ∈ ℕ0 )
33 2 32 eqeltrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝑅 ∈ ℕ0 )
34 1 oveq2i ⊢ ( ( 𝐴 / 𝐵 ) − 𝑄 ) = ( ( 𝐴 / 𝐵 ) − ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) )
35 fraclt1 ⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( ( 𝐴 / 𝐵 ) − ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) < 1 )
36 9 35 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / 𝐵 ) − ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ) < 1 )
37 34 36 eqbrtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / 𝐵 ) − 𝑄 ) < 1 )
38 2 oveq1i ⊢ ( 𝑅 / 𝐵 ) = ( ( 𝐴 − ( 𝐵 · 𝑄 ) ) / 𝐵 )
39 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
40 39 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐴 ∈ ℂ )
41 22 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · 𝑄 ) ∈ ℂ )
42 13 7 jca ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
43 42 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
44 divsubdir ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 · 𝑄 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 − ( 𝐵 · 𝑄 ) ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) − ( ( 𝐵 · 𝑄 ) / 𝐵 ) ) )
45 40 41 43 44 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 − ( 𝐵 · 𝑄 ) ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) − ( ( 𝐵 · 𝑄 ) / 𝐵 ) ) )
46 15 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / 𝐵 ) − ( ( 𝐵 · 𝑄 ) / 𝐵 ) ) = ( ( 𝐴 / 𝐵 ) − 𝑄 ) )
47 45 46 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 − ( 𝐵 · 𝑄 ) ) / 𝐵 ) = ( ( 𝐴 / 𝐵 ) − 𝑄 ) )
48 38 47 eqtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝑅 / 𝐵 ) = ( ( 𝐴 / 𝐵 ) − 𝑄 ) )
49 13 7 dividd ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 / 𝐵 ) = 1 )
50 49 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 / 𝐵 ) = 1 )
51 37 48 50 3brtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝑅 / 𝐵 ) < ( 𝐵 / 𝐵 ) )
52 33 nn0red ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝑅 ∈ ℝ )
53 ltdiv1 ⊢ ( ( 𝑅 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝑅 < 𝐵 ↔ ( 𝑅 / 𝐵 ) < ( 𝐵 / 𝐵 ) ) )
54 52 6 6 25 53 syl112anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝑅 < 𝐵 ↔ ( 𝑅 / 𝐵 ) < ( 𝐵 / 𝐵 ) ) )
55 51 54 mpbird ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝑅 < 𝐵 )
56 2 oveq2i ⊢ ( ( 𝐵 · 𝑄 ) + 𝑅 ) = ( ( 𝐵 · 𝑄 ) + ( 𝐴 − ( 𝐵 · 𝑄 ) ) )
57 41 40 pncan3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 · 𝑄 ) + ( 𝐴 − ( 𝐵 · 𝑄 ) ) ) = 𝐴 )
58 56 57 eqtr2id ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) )
59 55 58 jca ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) )
60 11 33 59 jca31 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ0 ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )