Proof of Theorem quoremnn0ALT
| Step | Hyp | Ref
| Expression |
| 1 | | quorem.1 |
. . 3
⊢ 𝑄 = (⌊‘(𝐴 / 𝐵)) |
| 2 | | fldivnn0 13862 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℕ0) |
| 3 | 1, 2 | eqeltrid 2845 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑄 ∈
ℕ0) |
| 4 | | quorem.2 |
. . 3
⊢ 𝑅 = (𝐴 − (𝐵 · 𝑄)) |
| 5 | | nnnn0 12533 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ0) |
| 6 | 5 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℕ0) |
| 7 | 6, 3 | nn0mulcld 12592 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ∈
ℕ0) |
| 8 | | simpl 482 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 ∈
ℕ0) |
| 9 | 3 | nn0cnd 12589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑄 ∈
ℂ) |
| 10 | | nncn 12274 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
| 11 | 10 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℂ) |
| 12 | | nnne0 12300 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
| 13 | 12 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ≠
0) |
| 14 | 9, 11, 13 | divcan3d 12048 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) / 𝐵) = 𝑄) |
| 15 | | nn0nndivcl 12598 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐴 / 𝐵) ∈
ℝ) |
| 16 | | flle 13839 |
. . . . . . . 8
⊢ ((𝐴 / 𝐵) ∈ ℝ →
(⌊‘(𝐴 / 𝐵)) ≤ (𝐴 / 𝐵)) |
| 17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (⌊‘(𝐴 /
𝐵)) ≤ (𝐴 / 𝐵)) |
| 18 | 1, 17 | eqbrtrid 5178 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑄 ≤ (𝐴 / 𝐵)) |
| 19 | 14, 18 | eqbrtrd 5165 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) / 𝐵) ≤ (𝐴 / 𝐵)) |
| 20 | 7 | nn0red 12588 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ∈
ℝ) |
| 21 | | nn0re 12535 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℝ) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 ∈
ℝ) |
| 23 | | nnre 12273 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 24 | 23 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐵 ∈
ℝ) |
| 25 | | nngt0 12297 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 0 <
𝐵) |
| 26 | 25 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 0 < 𝐵) |
| 27 | | lediv1 12133 |
. . . . . 6
⊢ (((𝐵 · 𝑄) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐵 · 𝑄) ≤ 𝐴 ↔ ((𝐵 · 𝑄) / 𝐵) ≤ (𝐴 / 𝐵))) |
| 28 | 20, 22, 24, 26, 27 | syl112anc 1376 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) ≤ 𝐴 ↔ ((𝐵 · 𝑄) / 𝐵) ≤ (𝐴 / 𝐵))) |
| 29 | 19, 28 | mpbird 257 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ≤ 𝐴) |
| 30 | | nn0sub2 12679 |
. . . 4
⊢ (((𝐵 · 𝑄) ∈ ℕ0 ∧ 𝐴 ∈ ℕ0
∧ (𝐵 · 𝑄) ≤ 𝐴) → (𝐴 − (𝐵 · 𝑄)) ∈
ℕ0) |
| 31 | 7, 8, 29, 30 | syl3anc 1373 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐴 − (𝐵 · 𝑄)) ∈
ℕ0) |
| 32 | 4, 31 | eqeltrid 2845 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑅 ∈
ℕ0) |
| 33 | 1 | oveq2i 7442 |
. . . . . 6
⊢ ((𝐴 / 𝐵) − 𝑄) = ((𝐴 / 𝐵) − (⌊‘(𝐴 / 𝐵))) |
| 34 | | fraclt1 13842 |
. . . . . . 7
⊢ ((𝐴 / 𝐵) ∈ ℝ → ((𝐴 / 𝐵) − (⌊‘(𝐴 / 𝐵))) < 1) |
| 35 | 15, 34 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 / 𝐵) − (⌊‘(𝐴 / 𝐵))) < 1) |
| 36 | 33, 35 | eqbrtrid 5178 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 / 𝐵) − 𝑄) < 1) |
| 37 | 4 | oveq1i 7441 |
. . . . . 6
⊢ (𝑅 / 𝐵) = ((𝐴 − (𝐵 · 𝑄)) / 𝐵) |
| 38 | | nn0cn 12536 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ0
→ 𝐴 ∈
ℂ) |
| 39 | 38 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 ∈
ℂ) |
| 40 | 7 | nn0cnd 12589 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 · 𝑄) ∈
ℂ) |
| 41 | 10, 12 | jca 511 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
| 42 | 41 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 ∈ ℂ
∧ 𝐵 ≠
0)) |
| 43 | | divsubdir 11961 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 · 𝑄) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 − (𝐵 · 𝑄)) / 𝐵) = ((𝐴 / 𝐵) − ((𝐵 · 𝑄) / 𝐵))) |
| 44 | 39, 40, 42, 43 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 − (𝐵 · 𝑄)) / 𝐵) = ((𝐴 / 𝐵) − ((𝐵 · 𝑄) / 𝐵))) |
| 45 | 14 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 / 𝐵) − ((𝐵 · 𝑄) / 𝐵)) = ((𝐴 / 𝐵) − 𝑄)) |
| 46 | 44, 45 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐴 − (𝐵 · 𝑄)) / 𝐵) = ((𝐴 / 𝐵) − 𝑄)) |
| 47 | 37, 46 | eqtrid 2789 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 / 𝐵) = ((𝐴 / 𝐵) − 𝑄)) |
| 48 | 10, 12 | dividd 12041 |
. . . . . 6
⊢ (𝐵 ∈ ℕ → (𝐵 / 𝐵) = 1) |
| 49 | 48 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝐵 / 𝐵) = 1) |
| 50 | 36, 47, 49 | 3brtr4d 5175 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 / 𝐵) < (𝐵 / 𝐵)) |
| 51 | 32 | nn0red 12588 |
. . . . 5
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑅 ∈
ℝ) |
| 52 | | ltdiv1 12132 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → (𝑅 < 𝐵 ↔ (𝑅 / 𝐵) < (𝐵 / 𝐵))) |
| 53 | 51, 24, 24, 26, 52 | syl112anc 1376 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 < 𝐵 ↔ (𝑅 / 𝐵) < (𝐵 / 𝐵))) |
| 54 | 50, 53 | mpbird 257 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝑅 < 𝐵) |
| 55 | 4 | oveq2i 7442 |
. . . 4
⊢ ((𝐵 · 𝑄) + 𝑅) = ((𝐵 · 𝑄) + (𝐴 − (𝐵 · 𝑄))) |
| 56 | 40, 39 | pncan3d 11623 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝐵 · 𝑄) + (𝐴 − (𝐵 · 𝑄))) = 𝐴) |
| 57 | 55, 56 | eqtr2id 2790 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ 𝐴 = ((𝐵 · 𝑄) + 𝑅)) |
| 58 | 54, 57 | jca 511 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅))) |
| 59 | 3, 32, 58 | jca31 514 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈ ℕ)
→ ((𝑄 ∈
ℕ0 ∧ 𝑅
∈ ℕ0) ∧ (𝑅 < 𝐵 ∧ 𝐴 = ((𝐵 · 𝑄) + 𝑅)))) |