Proof of Theorem quoremnn0ALT
Step | Hyp | Ref
| Expression |
1 | | quorem.1 |
. . 3
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) |
2 | | fldivnn0 13530 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℕ0) |
3 | 1, 2 | eqeltrid 2843 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑄 ∈
ℕ0) |
4 | | quorem.2 |
. . 3
⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) |
5 | | nnnn0 12228 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ0) |
6 | 5 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℕ0) |
7 | 6, 3 | nn0mulcld 12286 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ∈
ℕ0) |
8 | | simpl 483 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 ∈
ℕ0) |
9 | 3 | nn0cnd 12283 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑄 ∈
ℂ) |
10 | | nncn 11969 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
11 | 10 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℂ) |
12 | | nnne0 11995 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
13 | 12 | adantl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ≠
0) |
14 | 9, 11, 13 | divcan3d 11744 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) / 𝐵) = 𝑄) |
15 | | nn0nndivcl 12292 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐴 / 𝐵) ∈
ℝ) |
16 | | flle 13507 |
. . . . . . . 8
⊢ ((𝐴 / 𝐵) ∈ ℝ →
(⌊‘(𝐴 / 𝐵)) ≤ (𝐴 / 𝐵)) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (⌊‘(𝐴 /
𝐵)) ≤ (𝐴 / 𝐵)) |
18 | 1, 17 | eqbrtrid 5109 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑄 ≤ (𝐴 / 𝐵)) |
19 | 14, 18 | eqbrtrd 5096 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) / 𝐵) ≤ (𝐴 / 𝐵)) |
20 | 7 | nn0red 12282 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ∈
ℝ) |
21 | | nn0re 12230 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
22 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 ∈
ℝ) |
23 | | nnre 11968 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
24 | 23 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℝ) |
25 | | nngt0 11992 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 0 <
𝐵) |
26 | 25 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 0 < 𝐵) |
27 | | lediv1 11828 |
. . . . . 6
⊢ (((𝐵 · 𝑄) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐵 · 𝑄) ≤ 𝐴 ↔ ((𝐵 · 𝑄) / 𝐵) ≤ (𝐴 / 𝐵))) |
28 | 20, 22, 24, 26, 27 | syl112anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) ≤ 𝐴 ↔ ((𝐵 · 𝑄) / 𝐵) ≤ (𝐴 / 𝐵))) |
29 | 19, 28 | mpbird 256 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ≤ 𝐴) |
30 | | nn0sub2 12369 |
. . . 4
⊢ (((𝐵 · 𝑄) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0
∧ (𝐵 · 𝑄) ≤ 𝐴) → (𝐴 − (𝐵 · 𝑄)) ∈
ℕ0) |
31 | 7, 8, 29, 30 | syl3anc 1370 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐴 − (𝐵 · 𝑄)) ∈
ℕ0) |
32 | 4, 31 | eqeltrid 2843 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑅 ∈
ℕ0) |
33 | 1 | oveq2i 7279 |
. . . . . 6
⊢ ((𝐴 / 𝐵) − 𝑄) = ((𝐴 / 𝐵) − (⌊‘(𝐴 / 𝐵))) |
34 | | fraclt1 13510 |
. . . . . . 7
⊢ ((𝐴 / 𝐵) ∈ ℝ → ((𝐴 / 𝐵) − (⌊‘(𝐴 / 𝐵))) < 1) |
35 | 15, 34 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 / 𝐵) − (⌊‘(𝐴 / 𝐵))) < 1) |
36 | 33, 35 | eqbrtrid 5109 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 / 𝐵) − 𝑄) < 1) |
37 | 4 | oveq1i 7278 |
. . . . . 6
⊢ (𝑅 / 𝐵) = ((𝐴 − (𝐵 · 𝑄)) / 𝐵) |
38 | | nn0cn 12231 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
39 | 38 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 ∈
ℂ) |
40 | 7 | nn0cnd 12283 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ∈
ℂ) |
41 | 10, 12 | jca 512 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
42 | 41 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 ∈ ℂ
∧ 𝐵 ≠
0)) |
43 | | divsubdir 11657 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 · 𝑄) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 − (𝐵 · 𝑄)) / 𝐵) = ((𝐴 / 𝐵) − ((𝐵 · 𝑄) / 𝐵))) |
44 | 39, 40, 42, 43 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 − (𝐵 · 𝑄)) / 𝐵) = ((𝐴 / 𝐵) − ((𝐵 · 𝑄) / 𝐵))) |
45 | 14 | oveq2d 7284 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 / 𝐵) − ((𝐵 · 𝑄) / 𝐵)) = ((𝐴 / 𝐵) − 𝑄)) |
46 | 44, 45 | eqtrd 2778 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 − (𝐵 · 𝑄)) / 𝐵) = ((𝐴 / 𝐵) − 𝑄)) |
47 | 37, 46 | eqtrid 2790 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 / 𝐵) = ((𝐴 / 𝐵) − 𝑄)) |
48 | 10, 12 | dividd 11737 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → (𝐵 / 𝐵) = 1) |
49 | 48 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 / 𝐵) = 1) |
50 | 36, 47, 49 | 3brtr4d 5106 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 / 𝐵) < (𝐵 / 𝐵)) |
51 | 32 | nn0red 12282 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑅 ∈
ℝ) |
52 | | ltdiv1 11827 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → (𝑅 < 𝐵 ↔ (𝑅 / 𝐵) < (𝐵 / 𝐵))) |
53 | 51, 24, 24, 26, 52 | syl112anc 1373 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 < 𝐵 ↔ (𝑅 / 𝐵) < (𝐵 / 𝐵))) |
54 | 50, 53 | mpbird 256 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑅 < 𝐵) |
55 | 4 | oveq2i 7279 |
. . . 4
⊢ ((𝐵 · 𝑄) + 𝑅) = ((𝐵 · 𝑄) + (𝐴 − (𝐵 · 𝑄))) |
56 | 40, 39 | pncan3d 11323 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) + (𝐴 − (𝐵 · 𝑄))) = 𝐴) |
57 | 55, 56 | eqtr2id 2791 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 = ((𝐵 · 𝑄) + 𝑅)) |
58 | 54, 57 | jca 512 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))) |
59 | 3, 32, 58 | jca31 515 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝑄 ∈
ℕ0 ∧ 𝑅
∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) |