Proof of Theorem modid
Step | Hyp | Ref
| Expression |
1 | | modval 12532 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
2 | 1 | adantr 480 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) |
3 | | rerpdivcl 11737 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) |
4 | 3 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 / 𝐵) ∈ ℝ) |
5 | 4 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 / 𝐵) ∈ ℂ) |
6 | | addid2 10098 |
. . . . . . . . 9
⊢ ((𝐴 / 𝐵) ∈ ℂ → (0 + (𝐴 / 𝐵)) = (𝐴 / 𝐵)) |
7 | 6 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝐴 / 𝐵) ∈ ℂ → (⌊‘(0 +
(𝐴 / 𝐵))) = (⌊‘(𝐴 / 𝐵))) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (⌊‘(0 + (𝐴 / 𝐵))) = (⌊‘(𝐴 / 𝐵))) |
9 | | rpregt0 11722 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ+
→ (𝐵 ∈ ℝ
∧ 0 < 𝐵)) |
10 | | divge0 10771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
11 | 9, 10 | sylan2 490 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝐵 ∈ ℝ+) → 0 ≤
(𝐴 / 𝐵)) |
12 | 11 | an32s 842 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ 0 ≤ 𝐴) → 0
≤ (𝐴 / 𝐵)) |
13 | 12 | adantrr 749 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → 0 ≤ (𝐴 / 𝐵)) |
14 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 < 𝐵) → 𝐴 < 𝐵) |
15 | | rpcn 11717 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℂ) |
16 | 15 | mulid1d 9936 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ+
→ (𝐵 · 1) =
𝐵) |
17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 < 𝐵) → (𝐵 · 1) = 𝐵) |
18 | 14, 17 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ+
∧ 𝐴 < 𝐵) → 𝐴 < (𝐵 · 1)) |
19 | 18 | ad2ant2l 778 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → 𝐴 < (𝐵 · 1)) |
20 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → 𝐴 ∈ ℝ) |
21 | 9 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 ∈ ℝ ∧ 0 < 𝐵)) |
22 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
23 | | ltdivmul 10777 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ ∧ (𝐵 ∈
ℝ ∧ 0 < 𝐵))
→ ((𝐴 / 𝐵) < 1 ↔ 𝐴 < (𝐵 · 1))) |
24 | 22, 23 | mp3an2 1404 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 <
𝐵)) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < (𝐵 · 1))) |
25 | 20, 21, 24 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → ((𝐴 / 𝐵) < 1 ↔ 𝐴 < (𝐵 · 1))) |
26 | 19, 25 | mpbird 246 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 / 𝐵) < 1) |
27 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
28 | | flbi2 12480 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (𝐴 /
𝐵) ∈ ℝ) →
((⌊‘(0 + (𝐴 /
𝐵))) = 0 ↔ (0 ≤
(𝐴 / 𝐵) ∧ (𝐴 / 𝐵) < 1))) |
29 | 27, 4, 28 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → ((⌊‘(0 + (𝐴 / 𝐵))) = 0 ↔ (0 ≤ (𝐴 / 𝐵) ∧ (𝐴 / 𝐵) < 1))) |
30 | 13, 26, 29 | mpbir2and 959 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (⌊‘(0 + (𝐴 / 𝐵))) = 0) |
31 | 8, 30 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (⌊‘(𝐴 / 𝐵)) = 0) |
32 | 31 | oveq2d 6565 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 · (⌊‘(𝐴 / 𝐵))) = (𝐵 · 0)) |
33 | 15 | mul01d 10114 |
. . . . . 6
⊢ (𝐵 ∈ ℝ+
→ (𝐵 · 0) =
0) |
34 | 33 | ad2antlr 759 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 · 0) = 0) |
35 | 32, 34 | eqtrd 2644 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐵 · (⌊‘(𝐴 / 𝐵))) = 0) |
36 | 35 | oveq2d 6565 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵)))) = (𝐴 − 0)) |
37 | | recn 9905 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
38 | 37 | subid1d 10260 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴 − 0) = 𝐴) |
39 | 38 | ad2antrr 758 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 − 0) = 𝐴) |
40 | 36, 39 | eqtrd 2644 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵)))) = 𝐴) |
41 | 2, 40 | eqtrd 2644 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵)) → (𝐴 mod 𝐵) = 𝐴) |