Proof of Theorem moddi
| Step | Hyp | Ref
| Expression |
| 1 | | rpcn 13045 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℂ) |
| 2 | 1 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → 𝐴 ∈ ℂ) |
| 3 | | recn 11245 |
. . . . 5
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
| 4 | 3 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → 𝐵 ∈ ℂ) |
| 5 | | rpre 13043 |
. . . . . . . 8
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
| 7 | | refldivcl 13863 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℝ) |
| 8 | 6, 7 | remulcld 11291 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℝ) |
| 9 | 8 | recnd 11289 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℂ) |
| 10 | 9 | 3adant1 1131 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐶 · (⌊‘(𝐵 / 𝐶))) ∈ ℂ) |
| 11 | 2, 4, 10 | subdid 11719 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 · (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 · 𝐵) − (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
| 12 | | rpcnne0 13053 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℝ+
→ (𝐶 ∈ ℂ
∧ 𝐶 ≠
0)) |
| 13 | 12 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) |
| 14 | | rpcnne0 13053 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ+
→ (𝐴 ∈ ℂ
∧ 𝐴 ≠
0)) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) |
| 16 | | divcan5 11969 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0) ∧ (𝐴 ∈ ℂ ∧ 𝐴 ≠ 0)) → ((𝐴 · 𝐵) / (𝐴 · 𝐶)) = (𝐵 / 𝐶)) |
| 17 | 4, 13, 15, 16 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → ((𝐴 · 𝐵) / (𝐴 · 𝐶)) = (𝐵 / 𝐶)) |
| 18 | 17 | fveq2d 6910 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶))) = (⌊‘(𝐵 / 𝐶))) |
| 19 | 18 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))) = ((𝐴 · 𝐶) · (⌊‘(𝐵 / 𝐶)))) |
| 20 | | rpcn 13045 |
. . . . . . 7
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℂ) |
| 21 | 20 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → 𝐶 ∈ ℂ) |
| 22 | | rerpdivcl 13065 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 / 𝐶) ∈
ℝ) |
| 23 | | reflcl 13836 |
. . . . . . . . 9
⊢ ((𝐵 / 𝐶) ∈ ℝ →
(⌊‘(𝐵 / 𝐶)) ∈
ℝ) |
| 24 | 23 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐵 / 𝐶) ∈ ℝ →
(⌊‘(𝐵 / 𝐶)) ∈
ℂ) |
| 25 | 22, 24 | syl 17 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℂ) |
| 26 | 25 | 3adant1 1131 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (⌊‘(𝐵 / 𝐶)) ∈ ℂ) |
| 27 | 2, 21, 26 | mulassd 11284 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → ((𝐴 · 𝐶) · (⌊‘(𝐵 / 𝐶))) = (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
| 28 | 19, 27 | eqtr2d 2778 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶)))) = ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶))))) |
| 29 | 28 | oveq2d 7447 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → ((𝐴 · 𝐵) − (𝐴 · (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
| 30 | 11, 29 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 · (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
| 31 | | modval 13911 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
| 32 | 31 | 3adant1 1131 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
| 33 | 32 | oveq2d 7447 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 · (𝐵 mod 𝐶)) = (𝐴 · (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
| 34 | | rpre 13043 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
| 35 | | remulcl 11240 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
| 36 | 34, 35 | sylan 580 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ)
→ (𝐴 · 𝐵) ∈
ℝ) |
| 37 | 36 | 3adant3 1133 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 · 𝐵) ∈ ℝ) |
| 38 | | rpmulcl 13058 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐶 ∈
ℝ+) → (𝐴 · 𝐶) ∈
ℝ+) |
| 39 | | modval 13911 |
. . 3
⊢ (((𝐴 · 𝐵) ∈ ℝ ∧ (𝐴 · 𝐶) ∈ ℝ+) → ((𝐴 · 𝐵) mod (𝐴 · 𝐶)) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
| 40 | 37, 38, 39 | 3imp3i2an 1346 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → ((𝐴 · 𝐵) mod (𝐴 · 𝐶)) = ((𝐴 · 𝐵) − ((𝐴 · 𝐶) · (⌊‘((𝐴 · 𝐵) / (𝐴 · 𝐶)))))) |
| 41 | 30, 33, 40 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℝ
∧ 𝐶 ∈
ℝ+) → (𝐴 · (𝐵 mod 𝐶)) = ((𝐴 · 𝐵) mod (𝐴 · 𝐶))) |