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 eqtrid ( ( 𝐴 ∈ ℕ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 eqtr2id ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ ) → 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) )
58 54 57 jca ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ ) → ( 𝑅 < 𝐵𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) )
59 4 32 58 jca31 ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℕ0𝑅 ∈ ℕ0 ) ∧ ( 𝑅 < 𝐵𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )