Proof of Theorem modsubdir
Step | Hyp | Ref
| Expression |
1 | | modcl 13477 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℝ) |
2 | 1 | 3adant2 1133 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℝ) |
3 | | modcl 13477 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℝ) |
4 | 3 | 3adant1 1132 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℝ) |
5 | 2, 4 | subge0d 11451 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (0 ≤ ((𝐴 mod
𝐶) − (𝐵 mod 𝐶)) ↔ (𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶))) |
6 | | resubcl 11171 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) |
7 | 6 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 − 𝐵) ∈
ℝ) |
8 | | simp3 1140 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ+) |
9 | | rerpdivcl 12645 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 / 𝐶) ∈
ℝ) |
10 | 9 | flcld 13402 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℤ) |
11 | 10 | 3adant2 1133 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℤ) |
12 | | rerpdivcl 12645 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 / 𝐶) ∈
ℝ) |
13 | 12 | flcld 13402 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℤ) |
14 | 13 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℤ) |
15 | 11, 14 | zsubcld 12316 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((⌊‘(𝐴 /
𝐶)) −
(⌊‘(𝐵 / 𝐶))) ∈
ℤ) |
16 | | modcyc2 13511 |
. . . . . . 7
⊢ (((𝐴 − 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ∧
((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))) ∈ ℤ) → (((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) mod 𝐶) = ((𝐴 − 𝐵) mod 𝐶)) |
17 | 7, 8, 15, 16 | syl3anc 1373 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) mod 𝐶) = ((𝐴 − 𝐵) mod 𝐶)) |
18 | | recn 10848 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
19 | 18 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐴 ∈
ℂ) |
20 | | recn 10848 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
21 | 20 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
22 | | rpre 12623 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ) |
23 | 22 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
24 | | refldivcl 13427 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℝ) |
25 | 23, 24 | remulcld 10892 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐴 / 𝐶))) ∈
ℝ) |
26 | 25 | recnd 10890 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐴 / 𝐶))) ∈
ℂ) |
27 | 26 | 3adant2 1133 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐴 / 𝐶))) ∈
ℂ) |
28 | 22 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
29 | | refldivcl 13427 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℝ) |
30 | 28, 29 | remulcld 10892 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℝ) |
31 | 30 | recnd 10890 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℂ) |
32 | 31 | 3adant1 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℂ) |
33 | 19, 21, 27, 32 | sub4d 11267 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) − ((𝐶 · (⌊‘(𝐴 / 𝐶))) − (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶)))) − (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
34 | 22 | 3ad2ant3 1137 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
35 | 34 | recnd 10890 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℂ) |
36 | 24 | recnd 10890 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℂ) |
37 | 36 | 3adant2 1133 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℂ) |
38 | 29 | recnd 10890 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℂ) |
39 | 38 | 3adant1 1132 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℂ) |
40 | 35, 37, 39 | subdid 11317 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶)))) = ((𝐶 · (⌊‘(𝐴 / 𝐶))) − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
41 | 40 | oveq2d 7250 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) = ((𝐴 − 𝐵) − ((𝐶 · (⌊‘(𝐴 / 𝐶))) − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
42 | | modval 13475 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) = (𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶))))) |
43 | 42 | 3adant2 1133 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) = (𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶))))) |
44 | | modval 13475 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
45 | 44 | 3adant1 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
46 | 43, 45 | oveq12d 7252 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) = ((𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶)))) − (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
47 | 33, 41, 46 | 3eqtr4d 2789 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
48 | 47 | oveq1d 7249 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) mod 𝐶) = (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶)) |
49 | 17, 48 | eqtr3d 2781 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) mod 𝐶) = (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶)) |
50 | 49 | adantr 484 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 − 𝐵) mod 𝐶) = (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶)) |
51 | 2, 4 | resubcld 11289 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∈ ℝ) |
52 | 51 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∈ ℝ) |
53 | | simpl3 1195 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 𝐶 ∈
ℝ+) |
54 | | simpr 488 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
55 | | modge0 13483 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 0 ≤ (𝐵 mod 𝐶)) |
56 | 55 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 0 ≤ (𝐵 mod 𝐶)) |
57 | 2, 4 | subge02d 11453 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (0 ≤ (𝐵 mod 𝐶) ↔ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ≤ (𝐴 mod 𝐶))) |
58 | 56, 57 | mpbid 235 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ≤ (𝐴 mod 𝐶)) |
59 | | modlt 13484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) < 𝐶) |
60 | 59 | 3adant2 1133 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) < 𝐶) |
61 | 51, 2, 34, 58, 60 | lelttrd 11019 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) < 𝐶) |
62 | 61 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) < 𝐶) |
63 | | modid 13500 |
. . . . 5
⊢
(((((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∈ ℝ ∧ 𝐶 ∈ ℝ+) ∧ (0 ≤
((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∧ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) < 𝐶)) → (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
64 | 52, 53, 54, 62, 63 | syl22anc 839 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
65 | 50, 64 | eqtrd 2779 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
66 | | modge0 13483 |
. . . . . 6
⊢ (((𝐴 − 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ+) → 0 ≤
((𝐴 − 𝐵) mod 𝐶)) |
67 | 6, 66 | stoic3 1784 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 0 ≤ ((𝐴 −
𝐵) mod 𝐶)) |
68 | 67 | adantr 484 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 0 ≤ ((𝐴 − 𝐵) mod 𝐶)) |
69 | | simpr 488 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
70 | 68, 69 | breqtrd 5095 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
71 | 65, 70 | impbida 801 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (0 ≤ ((𝐴 mod
𝐶) − (𝐵 mod 𝐶)) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)))) |
72 | 5, 71 | bitr3d 284 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)))) |