Proof of Theorem odmodnn0
Step | Hyp | Ref
| Expression |
1 | | simpl1 1246 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝐺 ∈ Mnd) |
2 | | nnnn0 11633 |
. . . . . 6
⊢ ((𝑂‘𝐴) ∈ ℕ → (𝑂‘𝐴) ∈
ℕ0) |
3 | 2 | adantl 475 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) ∈
ℕ0) |
4 | | simpl3 1250 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝑁 ∈
ℕ0) |
5 | 4 | nn0red 11686 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝑁 ∈ ℝ) |
6 | | nnrp 12132 |
. . . . . . . 8
⊢ ((𝑂‘𝐴) ∈ ℕ → (𝑂‘𝐴) ∈
ℝ+) |
7 | 6 | adantl 475 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) ∈
ℝ+) |
8 | 5, 7 | rerpdivcld 12194 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑁 / (𝑂‘𝐴)) ∈ ℝ) |
9 | 4 | nn0ge0d 11688 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 0 ≤ 𝑁) |
10 | | nnre 11365 |
. . . . . . . 8
⊢ ((𝑂‘𝐴) ∈ ℕ → (𝑂‘𝐴) ∈ ℝ) |
11 | 10 | adantl 475 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) ∈ ℝ) |
12 | | nngt0 11390 |
. . . . . . . 8
⊢ ((𝑂‘𝐴) ∈ ℕ → 0 < (𝑂‘𝐴)) |
13 | 12 | adantl 475 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 0 < (𝑂‘𝐴)) |
14 | | divge0 11229 |
. . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) ∧ ((𝑂‘𝐴) ∈ ℝ ∧ 0 < (𝑂‘𝐴))) → 0 ≤ (𝑁 / (𝑂‘𝐴))) |
15 | 5, 9, 11, 13, 14 | syl22anc 872 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 0 ≤ (𝑁 / (𝑂‘𝐴))) |
16 | | flge0nn0 12923 |
. . . . . 6
⊢ (((𝑁 / (𝑂‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝑁 / (𝑂‘𝐴))) → (⌊‘(𝑁 / (𝑂‘𝐴))) ∈
ℕ0) |
17 | 8, 15, 16 | syl2anc 579 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
(⌊‘(𝑁 / (𝑂‘𝐴))) ∈
ℕ0) |
18 | 3, 17 | nn0mulcld 11690 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) ∈
ℕ0) |
19 | 4 | nn0zd 11815 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝑁 ∈ ℤ) |
20 | | zmodcl 12992 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑁 mod (𝑂‘𝐴)) ∈
ℕ0) |
21 | 19, 20 | sylancom 582 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑁 mod (𝑂‘𝐴)) ∈
ℕ0) |
22 | | simpl2 1248 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝐴 ∈ 𝑋) |
23 | | odcl.1 |
. . . . 5
⊢ 𝑋 = (Base‘𝐺) |
24 | | odid.3 |
. . . . 5
⊢ · =
(.g‘𝐺) |
25 | | eqid 2825 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
26 | 23, 24, 25 | mulgnn0dir 17930 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) ∈ ℕ0 ∧ (𝑁 mod (𝑂‘𝐴)) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋)) → ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 mod (𝑂‘𝐴))) · 𝐴) = ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) · 𝐴)(+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴))) |
27 | 1, 18, 21, 22, 26 | syl13anc 1495 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 mod (𝑂‘𝐴))) · 𝐴) = ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) · 𝐴)(+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴))) |
28 | 11 | recnd 10392 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑂‘𝐴) ∈ ℂ) |
29 | 17 | nn0cnd 11687 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
(⌊‘(𝑁 / (𝑂‘𝐴))) ∈ ℂ) |
30 | 28, 29 | mulcomd 10385 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) = ((⌊‘(𝑁 / (𝑂‘𝐴))) · (𝑂‘𝐴))) |
31 | 30 | oveq1d 6925 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) · 𝐴) = (((⌊‘(𝑁 / (𝑂‘𝐴))) · (𝑂‘𝐴)) · 𝐴)) |
32 | 23, 24 | mulgnn0ass 17936 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧
((⌊‘(𝑁 / (𝑂‘𝐴))) ∈ ℕ0 ∧ (𝑂‘𝐴) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋)) → (((⌊‘(𝑁 / (𝑂‘𝐴))) · (𝑂‘𝐴)) · 𝐴) = ((⌊‘(𝑁 / (𝑂‘𝐴))) · ((𝑂‘𝐴) · 𝐴))) |
33 | 1, 17, 3, 22, 32 | syl13anc 1495 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
(((⌊‘(𝑁 /
(𝑂‘𝐴))) · (𝑂‘𝐴)) · 𝐴) = ((⌊‘(𝑁 / (𝑂‘𝐴))) · ((𝑂‘𝐴) · 𝐴))) |
34 | | odcl.2 |
. . . . . . . . . 10
⊢ 𝑂 = (od‘𝐺) |
35 | | odid.4 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
36 | 23, 34, 24, 35 | odid 18315 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = 0 ) |
37 | 22, 36 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) · 𝐴) = 0 ) |
38 | 37 | oveq2d 6926 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
((⌊‘(𝑁 / (𝑂‘𝐴))) · ((𝑂‘𝐴) · 𝐴)) = ((⌊‘(𝑁 / (𝑂‘𝐴))) · 0 )) |
39 | 23, 24, 35 | mulgnn0z 17927 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧
(⌊‘(𝑁 / (𝑂‘𝐴))) ∈ ℕ0) →
((⌊‘(𝑁 / (𝑂‘𝐴))) · 0 ) = 0 ) |
40 | 1, 17, 39 | syl2anc 579 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
((⌊‘(𝑁 / (𝑂‘𝐴))) · 0 ) = 0 ) |
41 | 38, 40 | eqtrd 2861 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
((⌊‘(𝑁 / (𝑂‘𝐴))) · ((𝑂‘𝐴) · 𝐴)) = 0 ) |
42 | 33, 41 | eqtrd 2861 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) →
(((⌊‘(𝑁 /
(𝑂‘𝐴))) · (𝑂‘𝐴)) · 𝐴) = 0 ) |
43 | 31, 42 | eqtrd 2861 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) · 𝐴) = 0 ) |
44 | 43 | oveq1d 6925 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) · 𝐴)(+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴)) = ( 0 (+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴))) |
45 | 27, 44 | eqtrd 2861 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 mod (𝑂‘𝐴))) · 𝐴) = ( 0 (+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴))) |
46 | | modval 12972 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ (𝑂‘𝐴) ∈ ℝ+) → (𝑁 mod (𝑂‘𝐴)) = (𝑁 − ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))))) |
47 | 5, 7, 46 | syl2anc 579 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑁 mod (𝑂‘𝐴)) = (𝑁 − ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))))) |
48 | 47 | oveq2d 6926 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 mod (𝑂‘𝐴))) = (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 − ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴))))))) |
49 | 18 | nn0cnd 11687 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) ∈ ℂ) |
50 | 4 | nn0cnd 11687 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → 𝑁 ∈ ℂ) |
51 | 49, 50 | pncan3d 10723 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 − ((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))))) = 𝑁) |
52 | 48, 51 | eqtrd 2861 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → (((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 mod (𝑂‘𝐴))) = 𝑁) |
53 | 52 | oveq1d 6925 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((((𝑂‘𝐴) · (⌊‘(𝑁 / (𝑂‘𝐴)))) + (𝑁 mod (𝑂‘𝐴))) · 𝐴) = (𝑁 · 𝐴)) |
54 | 23, 24 | mulgnn0cl 17918 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑁 mod (𝑂‘𝐴)) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋) → ((𝑁 mod (𝑂‘𝐴)) · 𝐴) ∈ 𝑋) |
55 | 1, 21, 22, 54 | syl3anc 1494 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑁 mod (𝑂‘𝐴)) · 𝐴) ∈ 𝑋) |
56 | 23, 25, 35 | mndlid 17671 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ ((𝑁 mod (𝑂‘𝐴)) · 𝐴) ∈ 𝑋) → ( 0 (+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴)) = ((𝑁 mod (𝑂‘𝐴)) · 𝐴)) |
57 | 1, 55, 56 | syl2anc 579 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ( 0
(+g‘𝐺)((𝑁 mod (𝑂‘𝐴)) · 𝐴)) = ((𝑁 mod (𝑂‘𝐴)) · 𝐴)) |
58 | 45, 53, 57 | 3eqtr3rd 2870 |
1
⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑁 mod (𝑂‘𝐴)) · 𝐴) = (𝑁 · 𝐴)) |