Theorem znunit 15104

Description: The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.)

Hypotheses

Ref	Expression
znchr.y	⊢ 𝑌 = (ℤ/nℤ‘𝑁)
znunit.u	⊢ 𝑈 = (Unit‘𝑌)
znunit.l	⊢ 𝐿 = (ℤRHom‘𝑌)

Assertion

Ref	Expression
znunit	⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1))

Proof of Theorem znunit

Dummy variables 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		znchr.y	. . . . 5 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
2	1	zncrng 15090	. . . 4 ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)
3	2	adantr 276	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝑌 ∈ CRing)
4		znunit.u	. . . 4 ⊢ 𝑈 = (Unit‘𝑌)
5		eqid 2238	. . . 4 ⊢ (1r‘𝑌) = (1r‘𝑌)
6		eqid 2238	. . . 4 ⊢ (∥r‘𝑌) = (∥r‘𝑌)
7	4, 5, 6	crngunit 14528	. . 3 ⊢ (𝑌 ∈ CRing → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌)))
8	3, 7	syl 14	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌)))
9		eqidd 2239	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (Base‘𝑌) = (Base‘𝑌))
10		eqidd 2239	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∥r‘𝑌) = (∥r‘𝑌))
11		crngring 14420	. . . 4 ⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring)
12		ringsrg 14460	. . . 4 ⊢ (𝑌 ∈ Ring → 𝑌 ∈ SRing)
13	3, 11, 12	3syl 17	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝑌 ∈ SRing)
14		eqidd 2239	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (.r‘𝑌) = (.r‘𝑌))
15		eqid 2238	. . . . . . 7 ⊢ (Base‘𝑌) = (Base‘𝑌)
16		znunit.l	. . . . . . 7 ⊢ 𝐿 = (ℤRHom‘𝑌)
17	1, 15, 16	znzrhfo 15093	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→(Base‘𝑌))
18	17	adantr 276	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝐿:ℤ–onto→(Base‘𝑌))
19		fof 5618	. . . . 5 ⊢ (𝐿:ℤ–onto→(Base‘𝑌) → 𝐿:ℤ⟶(Base‘𝑌))
20	18, 19	syl 14	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝐿:ℤ⟶(Base‘𝑌))
21		ffvelcdm 5844	. . . 4 ⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) ∈ (Base‘𝑌))
22	20, 21	sylancom 424	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) ∈ (Base‘𝑌))
23	9, 10, 13, 14, 22	dvdsr2d 14512	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌) ↔ ∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
24		forn 5621	. . . . . 6 ⊢ (𝐿:ℤ–onto→(Base‘𝑌) → ran 𝐿 = (Base‘𝑌))
25	18, 24	syl 14	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ran 𝐿 = (Base‘𝑌))
26	25	rexeqdv 2756	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑥 ∈ ran 𝐿(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
27		ffn 5536	. . . . 5 ⊢ (𝐿:ℤ⟶(Base‘𝑌) → 𝐿 Fn ℤ)
28		oveq1 6095	. . . . . . 7 ⊢ (𝑥 = (𝐿‘𝑛) → (𝑥(.r‘𝑌)(𝐿‘𝐴)) = ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)))
29	28	eqeq1d 2247	. . . . . 6 ⊢ (𝑥 = (𝐿‘𝑛) → ((𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
30	29	rexrn 5848	. . . . 5 ⊢ (𝐿 Fn ℤ → (∃𝑥 ∈ ran 𝐿(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
31	20, 27, 30	3syl 17	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑥 ∈ ran 𝐿(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
32	26, 31	bitr3d 190	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
33	16	zrhrhm 15068	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring RingHom 𝑌))
34	3, 11, 33	3syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝐿 ∈ (ℤring RingHom 𝑌))
35	34	adantr 276	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝐿 ∈ (ℤring RingHom 𝑌))
36		simpr 110	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
37		simplr 533	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝐴 ∈ ℤ)
38		zringbas 15041	. . . . . . . 8 ⊢ ℤ = (Base‘ℤring)
39		zringmulr 15044	. . . . . . . 8 ⊢ · = (.r‘ℤring)
40		eqid 2238	. . . . . . . 8 ⊢ (.r‘𝑌) = (.r‘𝑌)
41	38, 39, 40	rhmmul 14581	. . . . . . 7 ⊢ ((𝐿 ∈ (ℤring RingHom 𝑌) ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐿‘(𝑛 · 𝐴)) = ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)))
42	35, 36, 37, 41	syl3anc 1278	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝐿‘(𝑛 · 𝐴)) = ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)))
43	3, 11	syl 14	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝑌 ∈ Ring)
44	43	adantr 276	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑌 ∈ Ring)
45	16, 5	zrh1 15069	. . . . . . 7 ⊢ (𝑌 ∈ Ring → (𝐿‘1) = (1r‘𝑌))
46	44, 45	syl 14	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝐿‘1) = (1r‘𝑌))
47	42, 46	eqeq12d 2253	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝐿‘(𝑛 · 𝐴)) = (𝐿‘1) ↔ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌)))
48		simpll 531	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 𝑁 ∈ ℕ0)
49	36, 37	zmulcld 9786	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (𝑛 · 𝐴) ∈ ℤ)
50		1zzd 9683	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → 1 ∈ ℤ)
51	1, 16	zndvds 15094	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑛 · 𝐴) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝐿‘(𝑛 · 𝐴)) = (𝐿‘1) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
52	48, 49, 50, 51	syl3anc 1278	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → ((𝐿‘(𝑛 · 𝐴)) = (𝐿‘1) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
53	47, 52	bitr3d 190	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
54	53	rexbidva 2547	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
55		simplr 533	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝐴 ∈ ℤ)
56		nn0z 9676	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
57	56	ad2antrr 492	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝑁 ∈ ℤ)
58		gcddvds 12766	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 gcd 𝑁) ∥ 𝐴 ∧ (𝐴 gcd 𝑁) ∥ 𝑁))
59	55, 57, 58	syl2anc 415	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ 𝐴 ∧ (𝐴 gcd 𝑁) ∥ 𝑁))
60	59	simpld 112	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ 𝐴)
61	55, 57	gcdcld 12771	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∈ ℕ0)
62	61	nn0zd 9778	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∈ ℤ)
63	36	adantrr 483	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝑛 ∈ ℤ)
64		dvdsmultr2 12626	. . . . . . . . 9 ⊢ (((𝐴 gcd 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝑁) ∥ 𝐴 → (𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴)))
65	62, 63, 55, 64	syl3anc 1278	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ 𝐴 → (𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴)))
66	60, 65	mpd 13	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴))
67	49	adantrr 483	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝑛 · 𝐴) ∈ ℤ)
68		1zzd 9683	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 1 ∈ ℤ)
69		peano2zm 9694	. . . . . . . . . 10 ⊢ ((𝑛 · 𝐴) ∈ ℤ → ((𝑛 · 𝐴) − 1) ∈ ℤ)
70	67, 69	syl 14	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝑛 · 𝐴) − 1) ∈ ℤ)
71	59	simprd 114	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ 𝑁)
72		simprr 537	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝑁 ∥ ((𝑛 · 𝐴) − 1))
73	62, 57, 70, 71, 72	dvdstrd 12623	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ ((𝑛 · 𝐴) − 1))
74		dvdssub2 12628	. . . . . . . 8 ⊢ ((((𝐴 gcd 𝑁) ∈ ℤ ∧ (𝑛 · 𝐴) ∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 gcd 𝑁) ∥ ((𝑛 · 𝐴) − 1)) → ((𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴) ↔ (𝐴 gcd 𝑁) ∥ 1))
75	62, 67, 68, 73, 74	syl31anc 1281	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴) ↔ (𝐴 gcd 𝑁) ∥ 1))
76	66, 75	mpbid 147	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ 1)
77		dvds1 12646	. . . . . . 7 ⊢ ((𝐴 gcd 𝑁) ∈ ℕ0 → ((𝐴 gcd 𝑁) ∥ 1 ↔ (𝐴 gcd 𝑁) = 1))
78	61, 77	syl 14	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ 1 ↔ (𝐴 gcd 𝑁) = 1))
79	76, 78	mpbid 147	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ (𝑛 ∈ ℤ ∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) = 1)
80	79	rexlimdvaa 2669	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1) → (𝐴 gcd 𝑁) = 1))
81		simpr 110	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝐴 ∈ ℤ)
82	56	adantr 276	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → 𝑁 ∈ ℤ)
83		bezout 12814	. . . . . . 7 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ (𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚)))
84	81, 82, 83	syl2anc 415	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ (𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚)))
85		eqeq1 2245	. . . . . . 7 ⊢ ((𝐴 gcd 𝑁) = 1 → ((𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) ↔ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚))))
86	85	2rexbidv 2575	. . . . . 6 ⊢ ((𝐴 gcd 𝑁) = 1 → (∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ (𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) ↔ ∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚))))
87	84, 86	syl5ibcom 155	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝑁) = 1 → ∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚))))
88	56	ad3antrrr 496	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝑁 ∈ ℤ)
89		dvdsmul1 12606	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑚))
90	88, 89	sylancom 424	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑚))
91		zmulcl 9710	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 · 𝑚) ∈ ℤ)
92	88, 91	sylancom 424	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (𝑁 · 𝑚) ∈ ℤ)
93		dvdsnegb 12601	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ (𝑁 · 𝑚) ∈ ℤ) → (𝑁 ∥ (𝑁 · 𝑚) ↔ 𝑁 ∥ -(𝑁 · 𝑚)))
94	88, 92, 93	syl2anc 415	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (𝑁 ∥ (𝑁 · 𝑚) ↔ 𝑁 ∥ -(𝑁 · 𝑚)))
95	90, 94	mpbid 147	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ -(𝑁 · 𝑚))
96	37	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝐴 ∈ ℤ)
97	96	zcnd 9781	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝐴 ∈ ℂ)
98		zcn 9661	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
99	98	ad2antlr 493	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝑛 ∈ ℂ)
100	97, 99	mulcomd 8354	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (𝐴 · 𝑛) = (𝑛 · 𝐴))
101	100	oveq1d 6103	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → ((𝐴 · 𝑛) + (𝑁 · 𝑚)) = ((𝑛 · 𝐴) + (𝑁 · 𝑚)))
102	99, 97	mulcld 8353	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (𝑛 · 𝐴) ∈ ℂ)
103	92	zcnd 9781	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (𝑁 · 𝑚) ∈ ℂ)
104	102, 103	subnegd 8652	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → ((𝑛 · 𝐴) − -(𝑁 · 𝑚)) = ((𝑛 · 𝐴) + (𝑁 · 𝑚)))
105	101, 104	eqtr4d 2274	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → ((𝐴 · 𝑛) + (𝑁 · 𝑚)) = ((𝑛 · 𝐴) − -(𝑁 · 𝑚)))
106	105	oveq2d 6104	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))) = ((𝑛 · 𝐴) − ((𝑛 · 𝐴) − -(𝑁 · 𝑚))))
107	103	negcld 8632	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → -(𝑁 · 𝑚) ∈ ℂ)
108	102, 107	nncand 8650	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → ((𝑛 · 𝐴) − ((𝑛 · 𝐴) − -(𝑁 · 𝑚))) = -(𝑁 · 𝑚))
109	106, 108	eqtrd 2271	. . . . . . . . 9 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))) = -(𝑁 · 𝑚))
110	95, 109	breqtrrd 4159	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))))
111		oveq2 6096	. . . . . . . . 9 ⊢ (1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) → ((𝑛 · 𝐴) − 1) = ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))))
112	111	breq2d 4143	. . . . . . . 8 ⊢ (1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) → (𝑁 ∥ ((𝑛 · 𝐴) − 1) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚)))))
113	110, 112	syl5ibrcom 157	. . . . . . 7 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) ∧ 𝑚 ∈ ℤ) → (1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) → 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
114	113	rexlimdva 2668	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) ∧ 𝑛 ∈ ℤ) → (∃𝑚 ∈ ℤ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) → 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
115	114	reximdva 2652	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) → ∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
116	87, 115	syld 45	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝑁) = 1 → ∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1)))
117	80, 116	impbid 129	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1) ↔ (𝐴 gcd 𝑁) = 1))
118	32, 54, 117	3bitrd 214	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → (∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ (𝐴 gcd 𝑁) = 1))
119	8, 23, 118	3bitrd 214	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529   class class class wbr 4131  ran crn 4777   Fn wfn 5375  ⟶wf 5376  –onto→wfo 5378  ‘cfv 5380  (class class class)co 6088  ℂcc 8184  1c1 8187   + caddc 8189   · cmul 8191   − cmin 8505   -cneg 8506  ℕ₀cn0 9575  ℤcz 9656   ∥ cdvds 12580   gcd cgcd 12756  Basecbs 13411  ._rcmulr 13492  1_rcur 14370  SRingcsrg 14375  Ringcrg 14408  CRingccrg 14409  ∥_rcdsr 14502  Unitcui 14503   RingHom crh 14567  ℤ_ringczring 15035  ℤRHomczrh 15056  ℤ/nℤczn 15058

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8277  ax-resscn 8278  ax-1cn 8279  ax-1re 8280  ax-icn 8281  ax-addcl 8282  ax-addrcl 8283  ax-mulcl 8284  ax-mulrcl 8285  ax-addcom 8286  ax-mulcom 8287  ax-addass 8288  ax-mulass 8289  ax-distr 8290  ax-i2m1 8291  ax-0lt1 8292  ax-1rid 8293  ax-0id 8294  ax-rnegex 8295  ax-precex 8296  ax-cnre 8297  ax-pre-ltirr 8298  ax-pre-ltwlin 8299  ax-pre-lttrn 8300  ax-pre-apti 8301  ax-pre-ltadd 8302  ax-pre-mulgt0 8303  ax-pre-mulext 8304  ax-arch 8305  ax-caucvg 8306  ax-addf 8308  ax-mulf 8309

This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-tp 3717  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-po 4443  df-iso 4444  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-1st 6378  df-2nd 6379  df-tpos 6520  df-recs 6580  df-frec 6666  df-er 6811  df-ec 6813  df-qs 6817  df-map 6928  df-sup 7331  df-pnf 8369  df-mnf 8370  df-xr 8371  df-ltxr 8372  df-le 8373  df-sub 8507  df-neg 8508  df-reap 8912  df-ap 8919  df-div 9012  df-inn 9315  df-2 9373  df-3 9374  df-4 9375  df-5 9376  df-6 9377  df-7 9378  df-8 9379  df-9 9380  df-n0 9576  df-z 9657  df-dec 9790  df-uz 9939  df-q 10037  df-rp 10073  df-fz 10430  df-fzo 10568  df-fl 10723  df-mod 10782  df-seqfrec 10907  df-exp 10998  df-cj 11630  df-re 11631  df-im 11632  df-rsqrt 11787  df-abs 11788  df-dvds 12581  df-gcd 12757  df-struct 13413  df-ndx 13414  df-slot 13415  df-base 13417  df-sets 13418  df-iress 13419  df-plusg 13504  df-mulr 13505  df-starv 13506  df-sca 13507  df-vsca 13508  df-ip 13509  df-tset 13510  df-ple 13511  df-ds 13513  df-unif 13514  df-0g 13672  df-topgen 13674  df-iimas 13684  df-qus 13685  df-mgm 13736  df-sgrp 13777  df-mnd 13790  df-mhm 13826  df-grp 13868  df-minusg 13869  df-sbg 13870  df-mulg 13983  df-subg 14033  df-nsg 14034  df-eqg 14035  df-ghm 14104  df-cmn 14180  df-abl 14181  df-mgp 14326  df-rng 14340  df-ur 14371  df-srg 14376  df-ring 14410  df-cring 14411  df-oppr 14483  df-dvdsr 14505  df-unit 14506  df-rhm 14569  df-subrg 14637  df-lmod 14735  df-lssm 14800  df-lsp 14834  df-sra 14882  df-rgmod 14883  df-lidl 14916  df-rsp 14917  df-2idl 14947  df-bl 14993  df-mopn 14994  df-fg 14996  df-metu 14997  df-cnfld 15004  df-zring 15036  df-zrh 15059  df-zn 15061

This theorem is used by:  znrrg  15105  lgseisenlem3  16408