Proof of Theorem modsubdir
Step | Hyp | Ref
| Expression |
1 | | modcl 12672 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℝ) |
2 | 1 | 3adant2 1080 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) ∈
ℝ) |
3 | | modcl 12672 |
. . . 4
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℝ) |
4 | 3 | 3adant1 1079 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) ∈
ℝ) |
5 | 2, 4 | subge0d 10617 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (0 ≤ ((𝐴 mod
𝐶) − (𝐵 mod 𝐶)) ↔ (𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶))) |
6 | | resubcl 10345 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ) |
7 | 6 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 − 𝐵) ∈
ℝ) |
8 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ+) |
9 | | rerpdivcl 11861 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 / 𝐶) ∈
ℝ) |
10 | 9 | flcld 12599 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℤ) |
11 | 10 | 3adant2 1080 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℤ) |
12 | | rerpdivcl 11861 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 / 𝐶) ∈
ℝ) |
13 | 12 | flcld 12599 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℤ) |
14 | 13 | 3adant1 1079 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℤ) |
15 | 11, 14 | zsubcld 11487 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((⌊‘(𝐴 /
𝐶)) −
(⌊‘(𝐵 / 𝐶))) ∈
ℤ) |
16 | | modcyc2 12706 |
. . . . . . 7
⊢ (((𝐴 − 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ∧
((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))) ∈ ℤ) → (((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) mod 𝐶) = ((𝐴 − 𝐵) mod 𝐶)) |
17 | 7, 8, 15, 16 | syl3anc 1326 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) mod 𝐶) = ((𝐴 − 𝐵) mod 𝐶)) |
18 | | recn 10026 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
19 | 18 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐴 ∈
ℂ) |
20 | | recn 10026 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
21 | 20 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐵 ∈
ℂ) |
22 | | rpre 11839 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ℝ+
→ 𝐶 ∈
ℝ) |
23 | 22 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
24 | | refldivcl 12624 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℝ) |
25 | 23, 24 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐴 / 𝐶))) ∈
ℝ) |
26 | 25 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐴 / 𝐶))) ∈
ℂ) |
27 | 26 | 3adant2 1080 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐴 / 𝐶))) ∈
ℂ) |
28 | 22 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
29 | | refldivcl 12624 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℝ) |
30 | 28, 29 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℝ) |
31 | 30 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℂ) |
32 | 31 | 3adant1 1079 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
(⌊‘(𝐵 / 𝐶))) ∈
ℂ) |
33 | 19, 21, 27, 32 | sub4d 10441 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) − ((𝐶 · (⌊‘(𝐴 / 𝐶))) − (𝐶 · (⌊‘(𝐵 / 𝐶))))) = ((𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶)))) − (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
34 | 22 | 3ad2ant3 1084 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℝ) |
35 | 34 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 𝐶 ∈
ℂ) |
36 | 24 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℂ) |
37 | 36 | 3adant2 1080 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐴 /
𝐶)) ∈
ℂ) |
38 | 29 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℂ) |
39 | 38 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (⌊‘(𝐵 /
𝐶)) ∈
ℂ) |
40 | 35, 37, 39 | subdid 10486 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐶 ·
((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶)))) = ((𝐶 · (⌊‘(𝐴 / 𝐶))) − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
41 | 40 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) = ((𝐴 − 𝐵) − ((𝐶 · (⌊‘(𝐴 / 𝐶))) − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
42 | | modval 12670 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) = (𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶))))) |
43 | 42 | 3adant2 1080 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) = (𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶))))) |
44 | | modval 12670 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
45 | 44 | 3adant1 1079 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐵 mod 𝐶) = (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶))))) |
46 | 43, 45 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) = ((𝐴 − (𝐶 · (⌊‘(𝐴 / 𝐶)))) − (𝐵 − (𝐶 · (⌊‘(𝐵 / 𝐶)))))) |
47 | 33, 41, 46 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
48 | 47 | oveq1d 6665 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (((𝐴 − 𝐵) − (𝐶 · ((⌊‘(𝐴 / 𝐶)) − (⌊‘(𝐵 / 𝐶))))) mod 𝐶) = (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶)) |
49 | 17, 48 | eqtr3d 2658 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 − 𝐵) mod 𝐶) = (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶)) |
50 | 49 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 − 𝐵) mod 𝐶) = (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶)) |
51 | 2, 4 | resubcld 10458 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∈ ℝ) |
52 | 51 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∈ ℝ) |
53 | | simpl3 1066 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 𝐶 ∈
ℝ+) |
54 | | simpr 477 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
55 | | modge0 12678 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 0 ≤ (𝐵 mod 𝐶)) |
56 | 55 | 3adant1 1079 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 0 ≤ (𝐵 mod 𝐶)) |
57 | 2, 4 | subge02d 10619 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (0 ≤ (𝐵 mod 𝐶) ↔ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ≤ (𝐴 mod 𝐶))) |
58 | 56, 57 | mpbid 222 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ≤ (𝐴 mod 𝐶)) |
59 | | modlt 12679 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) < 𝐶) |
60 | 59 | 3adant2 1080 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (𝐴 mod 𝐶) < 𝐶) |
61 | 51, 2, 34, 58, 60 | lelttrd 10195 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) < 𝐶) |
62 | 61 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) < 𝐶) |
63 | | modid 12695 |
. . . . 5
⊢
(((((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∈ ℝ ∧ 𝐶 ∈ ℝ+) ∧ (0 ≤
((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) ∧ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) < 𝐶)) → (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
64 | 52, 53, 54, 62, 63 | syl22anc 1327 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → (((𝐴 mod 𝐶) − (𝐵 mod 𝐶)) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
65 | 50, 64 | eqtrd 2656 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
66 | | modge0 12678 |
. . . . . 6
⊢ (((𝐴 − 𝐵) ∈ ℝ ∧ 𝐶 ∈ ℝ+) → 0 ≤
((𝐴 − 𝐵) mod 𝐶)) |
67 | 6, 66 | stoic3 1701 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ 0 ≤ ((𝐴 −
𝐵) mod 𝐶)) |
68 | 67 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 0 ≤ ((𝐴 − 𝐵) mod 𝐶)) |
69 | | simpr 477 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
70 | 68, 69 | breqtrd 4679 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
∧ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) → 0 ≤ ((𝐴 mod 𝐶) − (𝐵 mod 𝐶))) |
71 | 65, 70 | impbida 877 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ (0 ≤ ((𝐴 mod
𝐶) − (𝐵 mod 𝐶)) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)))) |
72 | 5, 71 | bitr3d 270 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+)
→ ((𝐵 mod 𝐶) ≤ (𝐴 mod 𝐶) ↔ ((𝐴 − 𝐵) mod 𝐶) = ((𝐴 mod 𝐶) − (𝐵 mod 𝐶)))) |