Proof of Theorem modid
Step | Hyp | Ref
| Expression |
1 | | modval 13444 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
2 | 1 | adantr 484 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
3 | | rerpdivcl 12616 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) |
4 | 3 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
5 | 4 | recnd 10861 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 / 𝐵) ∈ ℂ) |
6 | | addid2 11015 |
. . . . . . . . 9
⊢ ((𝐴 / 𝐵) ∈ ℂ → (0 + (𝐴 / 𝐵)) = (𝐴 / 𝐵)) |
7 | 6 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝐴 / 𝐵) ∈ ℂ → (⌊‘(0 +
(𝐴 / 𝐵))) = (⌊‘(𝐴 / 𝐵))) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (⌊‘(0 + (𝐴 / 𝐵))) = (⌊‘(𝐴 / 𝐵))) |
9 | | rpregt0 12600 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ+
→ (𝐵 ∈ ℝ
∧ 0 < 𝐵)) |
10 | | divge0 11701 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
11 | 9, 10 | sylan2 596 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ+) → 0 ≤
(𝐴 / 𝐵)) |
12 | 11 | an32s 652 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 0 ≤ 𝐴) → 0
≤ (𝐴 / 𝐵)) |
13 | 12 | adantrr 717 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
14 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
15 | | rpcn 12596 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℂ) |
16 | 15 | mulid1d 10850 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ+
→ (𝐵 · 1) =
𝐵) |
17 | 16 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 < 𝐵) → (𝐵 · 1) = 𝐵) |
18 | 14, 17 | breqtrrd 5081 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 < 𝐵) → 𝐴 < (𝐵 · 1)) |
19 | 18 | ad2ant2l 746 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → 𝐴 < (𝐵 · 1)) |
20 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → 𝐴 ∈ ℝ) |
21 | 9 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 ∈ ℝ ∧ 0 < 𝐵)) |
22 | | 1re 10833 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
23 | | ltdivmul 11707 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝐵 ∈
ℝ ∧ 0 < 𝐵))
→ ((𝐴 / 𝐵) < 1 ↔ 𝐴 < (𝐵 · 1))) |
24 | 22, 23 | mp3an2 1451 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < (𝐵 · 1))) |
25 | 20, 21, 24 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < (𝐵 · 1))) |
26 | 19, 25 | mpbird 260 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 / 𝐵) < 1) |
27 | | 0z 12187 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
28 | | flbi2 13392 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (𝐴 /
𝐵) ∈ ℝ) →
((⌊‘(0 + (𝐴 /
𝐵))) = 0 ↔ (0 ≤
(𝐴 / 𝐵) ∧ (𝐴 / 𝐵) < 1))) |
29 | 27, 4, 28 | sylancr 590 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → ((⌊‘(0 + (𝐴 / 𝐵))) = 0 ↔ (0 ≤ (𝐴 / 𝐵) ∧ (𝐴 / 𝐵) < 1))) |
30 | 13, 26, 29 | mpbir2and 713 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (⌊‘(0 + (𝐴 / 𝐵))) = 0) |
31 | 8, 30 | eqtr3d 2779 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (⌊‘(𝐴 / 𝐵)) = 0) |
32 | 31 | oveq2d 7229 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 · (⌊‘(𝐴 / 𝐵))) = (𝐵 · 0)) |
33 | 15 | mul01d 11031 |
. . . . . 6
⊢ (𝐵 ∈ ℝ+
→ (𝐵 · 0) =
0) |
34 | 33 | ad2antlr 727 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 · 0) = 0) |
35 | 32, 34 | eqtrd 2777 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 · (⌊‘(𝐴 / 𝐵))) = 0) |
36 | 35 | oveq2d 7229 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵)))) = (𝐴 − 0)) |
37 | | recn 10819 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
38 | 37 | subid1d 11178 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴 − 0) = 𝐴) |
39 | 38 | ad2antrr 726 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 − 0) = 𝐴) |
40 | 36, 39 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵)))) = 𝐴) |
41 | 2, 40 | eqtrd 2777 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴) |