Proof of Theorem modcyc
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zre 12619 | . . . . . . . 8
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 2 |  | rpre 13044 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℝ) | 
| 3 |  | remulcl 11241 | . . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑁 · 𝐵) ∈ ℝ) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝑁 · 𝐵) ∈
ℝ) | 
| 5 |  | readdcl 11239 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝑁 · 𝐵) ∈ ℝ) → (𝐴 + (𝑁 · 𝐵)) ∈ ℝ) | 
| 6 | 4, 5 | sylan2 593 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+))
→ (𝐴 + (𝑁 · 𝐵)) ∈ ℝ) | 
| 7 | 6 | 3impb 1114 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 + (𝑁 · 𝐵)) ∈ ℝ) | 
| 8 |  | simp3 1138 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℝ+) | 
| 9 |  | modval 13912 | . . . . 5
⊢ (((𝐴 + (𝑁 · 𝐵)) ∈ ℝ ∧ 𝐵 ∈ ℝ+) → ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = ((𝐴 + (𝑁 · 𝐵)) − (𝐵 · (⌊‘((𝐴 + (𝑁 · 𝐵)) / 𝐵))))) | 
| 10 | 7, 8, 9 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = ((𝐴 + (𝑁 · 𝐵)) − (𝐵 · (⌊‘((𝐴 + (𝑁 · 𝐵)) / 𝐵))))) | 
| 11 |  | recn 11246 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) | 
| 12 | 11 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ 𝐴 ∈
ℂ) | 
| 13 | 4 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝑁 · 𝐵) ∈
ℂ) | 
| 14 | 13 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝑁 · 𝐵) ∈
ℂ) | 
| 15 |  | rpcnne0 13054 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℝ+
→ (𝐵 ∈ ℂ
∧ 𝐵 ≠
0)) | 
| 16 | 15 | 3ad2ant3 1135 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 ∈ ℂ
∧ 𝐵 ≠
0)) | 
| 17 |  | divdir 11948 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 · 𝐵) ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝐴 + (𝑁 · 𝐵)) / 𝐵) = ((𝐴 / 𝐵) + ((𝑁 · 𝐵) / 𝐵))) | 
| 18 | 12, 14, 16, 17 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) / 𝐵) = ((𝐴 / 𝐵) + ((𝑁 · 𝐵) / 𝐵))) | 
| 19 |  | zcn 12620 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 20 |  | divcan4 11950 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝑁 · 𝐵) / 𝐵) = 𝑁) | 
| 21 | 20 | 3expb 1120 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) → ((𝑁 · 𝐵) / 𝐵) = 𝑁) | 
| 22 | 19, 15, 21 | syl2an 596 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝑁 · 𝐵) / 𝐵) = 𝑁) | 
| 23 | 22 | 3adant1 1130 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝑁 · 𝐵) / 𝐵) = 𝑁) | 
| 24 | 23 | oveq2d 7448 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 / 𝐵) + ((𝑁 · 𝐵) / 𝐵)) = ((𝐴 / 𝐵) + 𝑁)) | 
| 25 | 18, 24 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) / 𝐵) = ((𝐴 / 𝐵) + 𝑁)) | 
| 26 | 25 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘((𝐴 +
(𝑁 · 𝐵)) / 𝐵)) = (⌊‘((𝐴 / 𝐵) + 𝑁))) | 
| 27 |  | rerpdivcl 13066 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) | 
| 28 | 27 | 3adant2 1131 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 / 𝐵) ∈
ℝ) | 
| 29 |  | simp2 1137 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ 𝑁 ∈
ℤ) | 
| 30 |  | fladdz 13866 | . . . . . . . . 9
⊢ (((𝐴 / 𝐵) ∈ ℝ ∧ 𝑁 ∈ ℤ) →
(⌊‘((𝐴 / 𝐵) + 𝑁)) = ((⌊‘(𝐴 / 𝐵)) + 𝑁)) | 
| 31 | 28, 29, 30 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘((𝐴 /
𝐵) + 𝑁)) = ((⌊‘(𝐴 / 𝐵)) + 𝑁)) | 
| 32 | 26, 31 | eqtrd 2776 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘((𝐴 +
(𝑁 · 𝐵)) / 𝐵)) = ((⌊‘(𝐴 / 𝐵)) + 𝑁)) | 
| 33 | 32 | oveq2d 7448 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 ·
(⌊‘((𝐴 + (𝑁 · 𝐵)) / 𝐵))) = (𝐵 · ((⌊‘(𝐴 / 𝐵)) + 𝑁))) | 
| 34 |  | rpcn 13046 | . . . . . . . 8
⊢ (𝐵 ∈ ℝ+
→ 𝐵 ∈
ℂ) | 
| 35 | 34 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℂ) | 
| 36 |  | reflcl 13837 | . . . . . . . . . 10
⊢ ((𝐴 / 𝐵) ∈ ℝ →
(⌊‘(𝐴 / 𝐵)) ∈
ℝ) | 
| 37 | 36 | recnd 11290 | . . . . . . . . 9
⊢ ((𝐴 / 𝐵) ∈ ℝ →
(⌊‘(𝐴 / 𝐵)) ∈
ℂ) | 
| 38 | 27, 37 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℂ) | 
| 39 | 38 | 3adant2 1131 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐵)) ∈
ℂ) | 
| 40 | 19 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ 𝑁 ∈
ℂ) | 
| 41 | 35, 39, 40 | adddid 11286 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 ·
((⌊‘(𝐴 / 𝐵)) + 𝑁)) = ((𝐵 · (⌊‘(𝐴 / 𝐵))) + (𝐵 · 𝑁))) | 
| 42 |  | mulcom 11242 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝑁 · 𝐵) = (𝐵 · 𝑁)) | 
| 43 | 19, 34, 42 | syl2an 596 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝑁 · 𝐵) = (𝐵 · 𝑁)) | 
| 44 | 43 | 3adant1 1130 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝑁 · 𝐵) = (𝐵 · 𝑁)) | 
| 45 | 44 | eqcomd 2742 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 · 𝑁) = (𝑁 · 𝐵)) | 
| 46 | 45 | oveq2d 7448 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐵 ·
(⌊‘(𝐴 / 𝐵))) + (𝐵 · 𝑁)) = ((𝐵 · (⌊‘(𝐴 / 𝐵))) + (𝑁 · 𝐵))) | 
| 47 | 33, 41, 46 | 3eqtrd 2780 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 ·
(⌊‘((𝐴 + (𝑁 · 𝐵)) / 𝐵))) = ((𝐵 · (⌊‘(𝐴 / 𝐵))) + (𝑁 · 𝐵))) | 
| 48 | 47 | oveq2d 7448 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) − (𝐵 · (⌊‘((𝐴 + (𝑁 · 𝐵)) / 𝐵)))) = ((𝐴 + (𝑁 · 𝐵)) − ((𝐵 · (⌊‘(𝐴 / 𝐵))) + (𝑁 · 𝐵)))) | 
| 49 | 34 | adantl 481 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ 𝐵 ∈
ℂ) | 
| 50 | 49, 38 | mulcld 11282 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 ·
(⌊‘(𝐴 / 𝐵))) ∈
ℂ) | 
| 51 | 50 | 3adant2 1131 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐵 ·
(⌊‘(𝐴 / 𝐵))) ∈
ℂ) | 
| 52 | 12, 51, 14 | pnpcan2d 11659 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) − ((𝐵 · (⌊‘(𝐴 / 𝐵))) + (𝑁 · 𝐵))) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | 
| 53 | 10, 48, 52 | 3eqtrd 2780 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | 
| 54 |  | modval 13912 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | 
| 55 | 54 | 3adant2 1131 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ (𝐴 mod 𝐵) = (𝐴 − (𝐵 · (⌊‘(𝐴 / 𝐵))))) | 
| 56 | 53, 55 | eqtr4d 2779 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 𝐵 ∈ ℝ+)
→ ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵)) | 
| 57 | 56 | 3com23 1126 | 1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+
∧ 𝑁 ∈ ℤ)
→ ((𝐴 + (𝑁 · 𝐵)) mod 𝐵) = (𝐴 mod 𝐵)) |