Metamath Proof Explorer

Theorem quoremnn0ALT

Description: Alternate proof of quoremnn0 not using quoremz . TODO - Keep either quoremnn0ALT (if we don't keep quoremz ) or quoremnn0 ? (Contributed by NM, 14-Aug-2008) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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