Theorem mndodconglem 18405

Description: Lemma for mndodcong 18406. (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 11506	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ)
4	3	recnd 10520	. . . . . . . . 9 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℂ)
5		mndodconglem.4	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
6	5	nn0red 11809	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ ℝ)
7	6	recnd 10520	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℂ)
8		mndodconglem.5	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
9	8	nn0red 11809	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
10	9	recnd 10520	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℂ)
11	4, 7, 10	addsubassd 10870	. . . . . . . 8 ⊢ (𝜑 → (((𝑂‘𝐴) + 𝑀) − 𝑁) = ((𝑂‘𝐴) + (𝑀 − 𝑁)))
12	2	nnzd 11940	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℤ)
13	5	nn0zd 11939	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ ℤ)
14	12, 13	zaddcld 11945	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑂‘𝐴) + 𝑀) ∈ ℤ)
15	14	zred 11941	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑂‘𝐴) + 𝑀) ∈ ℝ)
16		mndodconglem.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))
17		nn0addge1 11796	. . . . . . . . . . 11 ⊢ (((𝑂‘𝐴) ∈ ℝ ∧ 𝑀 ∈ ℕ0) → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + 𝑀))
18	3, 5, 17	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + 𝑀))
19	9, 3, 15, 16, 18	ltletrd 10652	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 < ((𝑂‘𝐴) + 𝑀))
20	8	nn0zd 11939	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
21		znnsub 11882	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ ((𝑂‘𝐴) + 𝑀) ∈ ℤ) → (𝑁 < ((𝑂‘𝐴) + 𝑀) ↔ (((𝑂‘𝐴) + 𝑀) − 𝑁) ∈ ℕ))
22	20, 14, 21	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 < ((𝑂‘𝐴) + 𝑀) ↔ (((𝑂‘𝐴) + 𝑀) − 𝑁) ∈ ℕ))
23	19, 22	mpbid 233	. . . . . . . 8 ⊢ (𝜑 → (((𝑂‘𝐴) + 𝑀) − 𝑁) ∈ ℕ)
24	11, 23	eqeltrrd 2884	. . . . . . 7 ⊢ (𝜑 → ((𝑂‘𝐴) + (𝑀 − 𝑁)) ∈ ℕ)
25	4, 7, 10	addsub12d 10873	. . . . . . . . 9 ⊢ (𝜑 → ((𝑂‘𝐴) + (𝑀 − 𝑁)) = (𝑀 + ((𝑂‘𝐴) − 𝑁)))
26	25	oveq1d 7036	. . . . . . . 8 ⊢ (𝜑 → (((𝑂‘𝐴) + (𝑀 − 𝑁)) · 𝐴) = ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴))
27		mndodconglem.8	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))
28	27	oveq1d 7036	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)) = ((𝑁 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
29		mndodconglem.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ Mnd)
30		znnsub 11882	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℤ ∧ (𝑂‘𝐴) ∈ ℤ) → (𝑁 < (𝑂‘𝐴) ↔ ((𝑂‘𝐴) − 𝑁) ∈ ℕ))
31	20, 12, 30	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 < (𝑂‘𝐴) ↔ ((𝑂‘𝐴) − 𝑁) ∈ ℕ))
32	16, 31	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑂‘𝐴) − 𝑁) ∈ ℕ)
33	32	nnnn0d 11808	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑂‘𝐴) − 𝑁) ∈ ℕ0)
34		odcl.1	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝐺)
35		odid.3	. . . . . . . . . . . 12 ⊢ · = (.g‘𝐺)
36		eqid 2795	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
37	34, 35, 36	mulgnn0dir 18016	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ ((𝑂‘𝐴) − 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋)) → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑀 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
38	29, 5, 33, 1, 37	syl13anc 1365	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑀 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
39	34, 35, 36	mulgnn0dir 18016	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Mnd ∧ (𝑁 ∈ ℕ0 ∧ ((𝑂‘𝐴) − 𝑁) ∈ ℕ0 ∧ 𝐴 ∈ 𝑋)) → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑁 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
40	29, 8, 33, 1, 39	syl13anc 1365	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑁 · 𝐴)(+g‘𝐺)(((𝑂‘𝐴) − 𝑁) · 𝐴)))
41	28, 38, 40	3eqtr4d 2841	. . . . . . . . 9 ⊢ (𝜑 → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴))
42	10, 4	pncan3d 10853	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + ((𝑂‘𝐴) − 𝑁)) = (𝑂‘𝐴))
43	42	oveq1d 7036	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = ((𝑂‘𝐴) · 𝐴))
44		odcl.2	. . . . . . . . . . . 12 ⊢ 𝑂 = (od‘𝐺)
45		odid.4	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝐺)
46	34, 44, 35, 45	odid 18402	. . . . . . . . . . 11 ⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = 0 )
47	1, 46	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑂‘𝐴) · 𝐴) = 0 )
48	43, 47	eqtrd 2831	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = 0 )
49	41, 48	eqtrd 2831	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 + ((𝑂‘𝐴) − 𝑁)) · 𝐴) = 0 )
50	26, 49	eqtrd 2831	. . . . . . 7 ⊢ (𝜑 → (((𝑂‘𝐴) + (𝑀 − 𝑁)) · 𝐴) = 0 )
51	34, 44, 35, 45	odlem2 18403	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ ((𝑂‘𝐴) + (𝑀 − 𝑁)) ∈ ℕ ∧ (((𝑂‘𝐴) + (𝑀 − 𝑁)) · 𝐴) = 0 ) → (𝑂‘𝐴) ∈ (1...((𝑂‘𝐴) + (𝑀 − 𝑁))))
52	1, 24, 50, 51	syl3anc 1364	. . . . . 6 ⊢ (𝜑 → (𝑂‘𝐴) ∈ (1...((𝑂‘𝐴) + (𝑀 − 𝑁))))
53		elfzle2 12766	. . . . . 6 ⊢ ((𝑂‘𝐴) ∈ (1...((𝑂‘𝐴) + (𝑀 − 𝑁))) → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + (𝑀 − 𝑁)))
54	52, 53	syl 17	. . . . 5 ⊢ (𝜑 → (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + (𝑀 − 𝑁)))
55	13, 20	zsubcld 11946	. . . . . . 7 ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℤ)
56	55	zred 11941	. . . . . 6 ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℝ)
57	3, 56	addge01d 11081	. . . . 5 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝑁) ↔ (𝑂‘𝐴) ≤ ((𝑂‘𝐴) + (𝑀 − 𝑁))))
58	54, 57	mpbird 258	. . . 4 ⊢ (𝜑 → 0 ≤ (𝑀 − 𝑁))
59	6, 9	subge0d 11083	. . . 4 ⊢ (𝜑 → (0 ≤ (𝑀 − 𝑁) ↔ 𝑁 ≤ 𝑀))
60	58, 59	mpbid 233	. . 3 ⊢ (𝜑 → 𝑁 ≤ 𝑀)
61	6, 9	letri3d 10634	. . . 4 ⊢ (𝜑 → (𝑀 = 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀)))
62	61	biimprd 249	. . 3 ⊢ (𝜑 → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≤ 𝑀) → 𝑀 = 𝑁))
63	60, 62	mpan2d 690	. 2 ⊢ (𝜑 → (𝑀 ≤ 𝑁 → 𝑀 = 𝑁))
64	63	imp 407	1 ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081   class class class wbr 4966  ‘cfv 6230  (class class class)co 7021  ℝcr 10387  0cc0 10388  1c1 10389   + caddc 10391   < clt 10526   ≤ cle 10527   − cmin 10722  ℕcn 11491  ℕ₀cn0 11750  ℤcz 11834  ...cfz 12747  Basecbs 16317  +_gcplusg 16399  0_gc0g 16547  Mndcmnd 17738  ._gcmg 17986  odcod 18388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324  ax-cnex 10444  ax-resscn 10445  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-mulcom 10452  ax-addass 10453  ax-mulass 10454  ax-distr 10455  ax-i2m1 10456  ax-1ne0 10457  ax-1rid 10458  ax-rnegex 10459  ax-rrecex 10460  ax-cnre 10461  ax-pre-lttri 10462  ax-pre-lttrn 10463  ax-pre-ltadd 10464  ax-pre-mulgt0 10465

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-iun 4831  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-riota 6982  df-ov 7024  df-oprab 7025  df-mpo 7026  df-om 7442  df-1st 7550  df-2nd 7551  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-er 8144  df-en 8363  df-dom 8364  df-sdom 8365  df-sup 8757  df-inf 8758  df-pnf 10528  df-mnf 10529  df-xr 10530  df-ltxr 10531  df-le 10532  df-sub 10724  df-neg 10725  df-nn 11492  df-n0 11751  df-z 11835  df-uz 12099  df-fz 12748  df-seq 13225  df-0g 16549  df-mgm 17686  df-sgrp 17728  df-mnd 17739  df-mulg 17987  df-od 18392

This theorem is referenced by:  mndodcong  18406