mndodcongi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mndodcongi		Structured version Visualization version GIF version

Theorem mndodcongi 19583

Description: If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. For monoids, the reverse implication is false for elements with infinite order. For example, the powers of 2 mod 10 are 1,2,4,8,6,2,4,8,6,... so that the identity 1 never repeats, which is infinite order by our definition, yet other numbers like 6 appear many times in the sequence. (Contributed by Mario Carneiro, 23-Sep-2015.)

**Hypotheses**
Ref	Expression
odcl.1	⊢ 𝑋 = (Base‘𝐺)
odcl.2	⊢ 𝑂 = (od‘𝐺)
odid.3	⊢ · = (._g‘𝐺)
odid.4	⊢ 0 = (0_g‘𝐺)

**Assertion**
Ref	Expression
mndodcongi	⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴)))

**Proof of Theorem mndodcongi**
Step	Hyp	Ref	Expression
1		odcl.1	. . . . . 6 ⊢ 𝑋 = (Base‘𝐺)
2		odcl.2	. . . . . 6 ⊢ 𝑂 = (od‘𝐺)
3		odid.3	. . . . . 6 ⊢ · = (._g‘𝐺)
4		odid.4	. . . . . 6 ⊢ 0 = (0_g‘𝐺)
5	1, 2, 3, 4	mndodcong 19582	. . . . 5 ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) ↔ (𝑀 · 𝐴) = (𝑁 · 𝐴)))
6	5	biimpd 231	. . . 4 ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴)))
7	6	3expia 1134	. . 3 ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑂‘𝐴) ∈ ℕ → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴))))
8	7	3impa 1122	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑂‘𝐴) ∈ ℕ → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴))))
9		nn0z 12592	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℤ)
10		nn0z 12592	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
11		zsubcl 12613	. . . . . . 7 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ)
12	9, 10, 11	syl2an 605	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 − 𝑁) ∈ ℤ)
13	12	3ad2ant3 1148	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑀 − 𝑁) ∈ ℤ)
14		0dvds 16310	. . . . 5 ⊢ ((𝑀 − 𝑁) ∈ ℤ → (0 ∥ (𝑀 − 𝑁) ↔ (𝑀 − 𝑁) = 0))
15	13, 14	syl 17	. . . 4 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (0 ∥ (𝑀 − 𝑁) ↔ (𝑀 − 𝑁) = 0))
16		nn0cn 12491	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℂ)
17		nn0cn 12491	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
18		subeq0 11457	. . . . . . 7 ⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 − 𝑁) = 0 ↔ 𝑀 = 𝑁))
19	16, 17, 18	syl2an 605	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝑀 − 𝑁) = 0 ↔ 𝑀 = 𝑁))
20	19	3ad2ant3 1148	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑀 − 𝑁) = 0 ↔ 𝑀 = 𝑁))
21		oveq1 7403	. . . . 5 ⊢ (𝑀 = 𝑁 → (𝑀 · 𝐴) = (𝑁 · 𝐴))
22	20, 21	biimtrdi 255	. . . 4 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑀 − 𝑁) = 0 → (𝑀 · 𝐴) = (𝑁 · 𝐴)))
23	15, 22	sylbid 242	. . 3 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (0 ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴)))
24		breq1 5103	. . . 4 ⊢ ((𝑂‘𝐴) = 0 → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) ↔ 0 ∥ (𝑀 − 𝑁)))
25	24	imbi1d 343	. . 3 ⊢ ((𝑂‘𝐴) = 0 → (((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴)) ↔ (0 ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴))))
26	23, 25	syl5ibrcom 249	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑂‘𝐴) = 0 → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴))))
27	1, 2	odcl 19576	. . . 4 ⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈ ℕ₀)
28	27	3ad2ant2 1147	. . 3 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → (𝑂‘𝐴) ∈ ℕ₀)
29		elnn0 12483	. . 3 ⊢ ((𝑂‘𝐴) ∈ ℕ₀ ↔ ((𝑂‘𝐴) ∈ ℕ ∨ (𝑂‘𝐴) = 0))
30	28, 29	sylib 220	. 2 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑂‘𝐴) ∈ ℕ ∨ (𝑂‘𝐴) = 0))
31	8, 26, 30	mpjaod 871	1 ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 class class class wbr 5100 ‘cfv 6521 (class class class)co 7396 ℂcc 11071 0cc0 11073 − cmin 11414 ℕcn 12210 ℕ₀cn0 12481 ℤcz 12568 ∥ cdvds 16286 Basecbs 17245 0_gc0g 17468 Mndcmnd 18768 ._gcmg 19109 odcod 19564

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-er 8678 df-en 8928 df-dom 8929 df-sdom 8930 df-sup 9388 df-inf 9389 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-n0 12482 df-z 12569 df-uz 12840 df-rp 12994 df-fz 13513 df-fl 13802 df-mod 13880 df-seq 14015 df-dvds 16287 df-0g 17470 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-mulg 19110 df-od 19568

This theorem is referenced by: (None)

W3C validator