Theorem mndodconglem 18669

Description: Lemma for mndodcong 18670. (Contributed by Mario Carneiro, 23-Sep-2015.)

Hypotheses

Ref	Expression
odcl.1	⊢ 𝑋 = (Base‘𝐺)
odcl.2	⊢ 𝑂 = (od‘𝐺)
odid.3	⊢ · = (.g‘𝐺)
odid.4	⊢ 0 = (0g‘𝐺)
mndodconglem.1	⊢ (𝜑 → 𝐺 ∈ Mnd)
mndodconglem.2	⊢ (𝜑 → 𝐴 ∈ 𝑋)
mndodconglem.3	⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)
mndodconglem.4	⊢ (𝜑 → 𝑀 ∈ ℕ0)
mndodconglem.5	⊢ (𝜑 → 𝑁 ∈ ℕ0)
mndodconglem.6	⊢ (𝜑 → 𝑀 < (𝑂‘𝐴))
mndodconglem.7	⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))
mndodconglem.8	⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))

Assertion

Ref	Expression
mndodconglem	⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)

Proof of Theorem mndodconglem

Step	Hyp	Ref	Expression
1		mndodconglem.2	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
2		mndodconglem.3	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)
3	2	nnred 11653	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ)
4	3	recnd 10669	. . . . . . . . 9 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℂ)
5		mndodconglem.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
6	5	nn0red 11957	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
7	6	recnd 10669	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
8		mndodconglem.5	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
9	8	nn0red 11957	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
10	9	recnd 10669	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℂ)
11	4, 7, 10	addsubassd 11017	. . . . . . . 8 ⊢ (𝜑 → (((𝑂‘𝐴) + 𝑀) − 𝑁) = ((𝑂‘𝐴) + (𝑀 − 𝑁)))
12	2	nnzd 12087	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℤ)
13	5	nn0zd 12086	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
14	12, 13	zaddcld 12092	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑂‘𝐴) + 𝑀) ∈ ℤ)
15	14	zred 12088	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑂‘𝐴) + 𝑀) ∈ ℝ)
16		mndodconglem.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))
17		nn0addge1 11944	. . . . . . . . . . 11 ⊢ (((𝑂‘𝐴) ∈ ℝ ∧ 𝑀 ∈ ℕ0) → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + 𝑀))
18	3, 5, 17	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + 𝑀))
19	9, 3, 15, 16, 18	ltletrd 10800	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 < ((𝑂‘𝐴) + 𝑀))
20	8	nn0zd 12086	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
21		znnsub 12029	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ((𝑂‘𝐴) + 𝑀) ∈ ℤ) → (𝑁 < ((𝑂‘𝐴) + 𝑀) ↔ (((𝑂‘𝐴) + 𝑀) − 𝑁) ∈ ℕ))
22	20, 14, 21	syl2anc 586	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 < ((𝑂‘𝐴) + 𝑀) ↔ (((𝑂‘𝐴) + 𝑀) − 𝑁) ∈ ℕ))
23	19, 22	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → (((𝑂‘𝐴) + 𝑀) − 𝑁) ∈ ℕ)
24	11, 23	eqeltrrd 2914	. . . . . . 7 ⊢ (𝜑 → ((𝑂‘𝐴) + (𝑀 − 𝑁)) ∈ ℕ)
25	4, 7, 10	addsub12d 11020	. . . . . . . . 9 ⊢ (𝜑 → ((𝑂‘𝐴) + (𝑀 − 𝑁)) = (𝑀 + ((𝑂‘𝐴) − 𝑁)))
26	25	oveq1d 7171	. . . . . . . 8 ⊢ (𝜑 → (((𝑂‘𝐴) + (𝑀 − 𝑁)) · 𝐴) = ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴))
27		mndodconglem.8	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))
28	27	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)) = ((𝑁 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
29		mndodconglem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ Mnd)
30		znnsub 12029	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ (𝑂‘𝐴) ∈ ℤ) → (𝑁 < (𝑂‘𝐴) ↔ ((𝑂‘𝐴) − 𝑁) ∈ ℕ))
31	20, 12, 30	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 < (𝑂‘𝐴) ↔ ((𝑂‘𝐴) − 𝑁) ∈ ℕ))
32	16, 31	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑂‘𝐴) − 𝑁) ∈ ℕ)
33	32	nnnn0d 11956	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑂‘𝐴) − 𝑁) ∈ ℕ0)
34		odcl.1	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝐺)
35		odid.3	. . . . . . . . . . . 12 ⊢ · = (.g‘𝐺)
36		eqid 2821	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
37	34, 35, 36	mulgnn0dir 18257	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ ((𝑂‘𝐴) − 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋)) → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑀 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
38	29, 5, 33, 1, 37	syl13anc 1368	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑀 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
39	34, 35, 36	mulgnn0dir 18257	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑁 ∈ ℕ0 ∧ ((𝑂‘𝐴) − 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋)) → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑁 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
40	29, 8, 33, 1, 39	syl13anc 1368	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑁 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
41	28, 38, 40	3eqtr4d 2866	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴))
42	10, 4	pncan3d 11000	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + ((𝑂‘𝐴) − 𝑁)) = (𝑂‘𝐴))
43	42	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑂‘𝐴) · 𝐴))
44		odcl.2	. . . . . . . . . . . 12 ⊢ 𝑂 = (od‘𝐺)
45		odid.4	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐺)
46	34, 44, 35, 45	odid 18666	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = 0 )
47	1, 46	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑂‘𝐴) · 𝐴) = 0 )
48	43, 47	eqtrd 2856	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = 0 )
49	41, 48	eqtrd 2856	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = 0 )
50	26, 49	eqtrd 2856	. . . . . . 7 ⊢ (𝜑 → (((𝑂‘𝐴) + (𝑀 − 𝑁)) · 𝐴) = 0 )
51	34, 44, 35, 45	odlem2 18667	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ ((𝑂‘𝐴) + (𝑀 − 𝑁)) ∈ ℕ ∧ (((𝑂‘𝐴) + (𝑀 − 𝑁)) · 𝐴) = 0 ) → (𝑂‘𝐴) ∈ (1...((𝑂‘𝐴) + (𝑀 − 𝑁))))
52	1, 24, 50, 51	syl3anc 1367	. . . . . 6 ⊢ (𝜑 → (𝑂‘𝐴) ∈ (1...((𝑂‘𝐴) + (𝑀 − 𝑁))))
53		elfzle2 12912	. . . . . 6 ⊢ ((𝑂‘𝐴) ∈ (1...((𝑂‘𝐴) + (𝑀 − 𝑁))) → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + (𝑀 − 𝑁)))
54	52, 53	syl 17	. . . . 5 ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + (𝑀 − 𝑁)))
55	13, 20	zsubcld 12093	. . . . . . 7 ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℤ)
56	55	zred 12088	. . . . . 6 ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℝ)
57	3, 56	addge01d 11228	. . . . 5 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝑁) ↔ (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + (𝑀 − 𝑁))))
58	54, 57	mpbird 259	. . . 4 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝑁))
59	6, 9	subge0d 11230	. . . 4 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝑁) ↔ 𝑁 ≤ 𝑀))
60	58, 59	mpbid 234	. . 3 ⊢ (𝜑 → 𝑁 ≤ 𝑀)
61	6, 9	letri3d 10782	. . . 4 ⊢ (𝜑 → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
62	61	biimprd 250	. . 3 ⊢ (𝜑 → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁))
63	60, 62	mpan2d 692	. 2 ⊢ (𝜑 → (𝑀 ≤ 𝑁 → 𝑀 = 𝑁))
64	63	imp 409	1 ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114   class class class wbr 5066  ‘cfv 6355  (class class class)co 7156  ℝcr 10536  0cc0 10537  1c1 10538   + caddc 10540   < clt 10675   ≤ cle 10676   − cmin 10870  ℕcn 11638  ℕ₀cn0 11898  ℤcz 11982  ...cfz 12893  Basecbs 16483  +_gcplusg 16565  0_gc0g 16713  Mndcmnd 17911  ._gcmg 18224  odcod 18652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-sup 8906  df-inf 8907  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983  df-uz 12245  df-fz 12894  df-seq 13371  df-0g 16715  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mulg 18225  df-od 18656

This theorem is referenced by:  mndodcong  18670