This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znunit

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

Ref Expression
Hypotheses znchr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znunit.u ⊢ 𝑈 = ( Unit ‘ 𝑌 )
znunit.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
Assertion znunit ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) ∈ 𝑈 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 znchr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znunit.u ⊢ 𝑈 = ( Unit ‘ 𝑌 )
3 znunit.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
4 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
5 4 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝑌 ∈ CRing )
6 eqid ⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ 𝑌 )
7 eqid ⊢ ( ∥r ‘ 𝑌 ) = ( ∥r ‘ 𝑌 )
8 2 6 7 crngunit ⊢ ( 𝑌 ∈ CRing → ( ( 𝐿 ‘ 𝐴 ) ∈ 𝑈 ↔ ( 𝐿 ‘ 𝐴 ) ( ∥r ‘ 𝑌 ) ( 1r ‘ 𝑌 ) ) )
9 5 8 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) ∈ 𝑈 ↔ ( 𝐿 ‘ 𝐴 ) ( ∥r ‘ 𝑌 ) ( 1r ‘ 𝑌 ) ) )
10 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
11 1 10 3 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
12 11 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) )
13 fof ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
14 12 13 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) )
15 ffvelcdm ⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑌 ) )
16 14 15 sylancom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑌 ) )
17 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
18 10 7 17 dvdsr2 ⊢ ( ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑌 ) → ( ( 𝐿 ‘ 𝐴 ) ( ∥r ‘ 𝑌 ) ( 1r ‘ 𝑌 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
19 16 18 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) ( ∥r ‘ 𝑌 ) ( 1r ‘ 𝑌 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
20 forn ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑌 ) → ran 𝐿 = ( Base ‘ 𝑌 ) )
21 12 20 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ran 𝐿 = ( Base ‘ 𝑌 ) )
22 21 rexeqdv ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑥 ∈ ran 𝐿 ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ∃ 𝑥 ∈ ( Base ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
23 ffn ⊢ ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑌 ) → 𝐿 Fn ℤ )
24 oveq1 ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑛 ) → ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) )
25 24 eqeq1d ⊢ ( 𝑥 = ( 𝐿 ‘ 𝑛 ) → ( ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
26 25 rexrn ⊢ ( 𝐿 Fn ℤ → ( ∃ 𝑥 ∈ ran 𝐿 ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
27 14 23 26 3syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑥 ∈ ran 𝐿 ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
28 22 27 bitr3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ∃ 𝑛 ∈ ℤ ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
29 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
30 5 29 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝑌 ∈ Ring )
31 3 zrhrhm ⊢ ( 𝑌 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
32 30 31 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
33 32 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝐿 ∈ ( ℤring RingHom 𝑌 ) )
34 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
35 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝐴 ∈ ℤ )
36 zringbas ⊢ ℤ = ( Base ‘ ℤring )
37 zringmulr ⊢ · = ( .r ‘ ℤring )
38 36 37 17 rhmmul ⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑌 ) ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑛 · 𝐴 ) ) = ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) )
39 33 34 35 38 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑛 · 𝐴 ) ) = ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) )
40 30 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑌 ∈ Ring )
41 3 6 zrh1 ⊢ ( 𝑌 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑌 ) )
42 40 41 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑌 ) )
43 39 42 eqeq12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑛 · 𝐴 ) ) = ( 𝐿 ‘ 1 ) ↔ ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ) )
44 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 𝑁 ∈ ℕ0 )
45 34 35 zmulcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝐴 ) ∈ ℤ )
46 1zzd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → 1 ∈ ℤ )
47 1 3 zndvds ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑛 · 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑛 · 𝐴 ) ) = ( 𝐿 ‘ 1 ) ↔ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
48 44 45 46 47 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝐿 ‘ ( 𝑛 · 𝐴 ) ) = ( 𝐿 ‘ 1 ) ↔ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
49 43 48 bitr3d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
50 49 rexbidva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑛 ∈ ℤ ( ( 𝐿 ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ∃ 𝑛 ∈ ℤ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
51 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → 𝐴 ∈ ℤ )
52 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
53 52 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → 𝑁 ∈ ℤ )
54 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 gcd 𝑁 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝑁 ) ∥ 𝑁 ) )
55 51 53 54 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( ( 𝐴 gcd 𝑁 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝑁 ) ∥ 𝑁 ) )
56 55 simpld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∥ 𝐴 )
57 51 53 gcdcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∈ ℕ0 )
58 57 nn0zd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∈ ℤ )
59 34 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → 𝑛 ∈ ℤ )
60 dvdsmultr2 ⊢ ( ( ( 𝐴 gcd 𝑁 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝑁 ) ∥ 𝐴 → ( 𝐴 gcd 𝑁 ) ∥ ( 𝑛 · 𝐴 ) ) )
61 58 59 51 60 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( ( 𝐴 gcd 𝑁 ) ∥ 𝐴 → ( 𝐴 gcd 𝑁 ) ∥ ( 𝑛 · 𝐴 ) ) )
62 56 61 mpd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∥ ( 𝑛 · 𝐴 ) )
63 45 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝑛 · 𝐴 ) ∈ ℤ )
64 1zzd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → 1 ∈ ℤ )
65 peano2zm ⊢ ( ( 𝑛 · 𝐴 ) ∈ ℤ → ( ( 𝑛 · 𝐴 ) − 1 ) ∈ ℤ )
66 63 65 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( ( 𝑛 · 𝐴 ) − 1 ) ∈ ℤ )
67 55 simprd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∥ 𝑁 )
68 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) )
69 58 53 66 67 68 dvdstrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∥ ( ( 𝑛 · 𝐴 ) − 1 ) )
70 dvdssub2 ⊢ ( ( ( ( 𝐴 gcd 𝑁 ) ∈ ℤ ∧ ( 𝑛 · 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 𝐴 gcd 𝑁 ) ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) → ( ( 𝐴 gcd 𝑁 ) ∥ ( 𝑛 · 𝐴 ) ↔ ( 𝐴 gcd 𝑁 ) ∥ 1 ) )
71 58 63 64 69 70 syl31anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( ( 𝐴 gcd 𝑁 ) ∥ ( 𝑛 · 𝐴 ) ↔ ( 𝐴 gcd 𝑁 ) ∥ 1 ) )
72 62 71 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) ∥ 1 )
73 dvds1 ⊢ ( ( 𝐴 gcd 𝑁 ) ∈ ℕ0 → ( ( 𝐴 gcd 𝑁 ) ∥ 1 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
74 57 73 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( ( 𝐴 gcd 𝑁 ) ∥ 1 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
75 72 74 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ ( 𝑛 ∈ ℤ ∧ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) ) → ( 𝐴 gcd 𝑁 ) = 1 )
76 75 rexlimdvaa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑛 ∈ ℤ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) → ( 𝐴 gcd 𝑁 ) = 1 ) )
77 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝐴 ∈ ℤ )
78 52 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → 𝑁 ∈ ℤ )
79 bezout ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ ( 𝐴 gcd 𝑁 ) = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) )
80 77 78 79 syl2anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ ( 𝐴 gcd 𝑁 ) = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) )
81 eqeq1 ⊢ ( ( 𝐴 gcd 𝑁 ) = 1 → ( ( 𝐴 gcd 𝑁 ) = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ↔ 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) )
82 81 2rexbidv ⊢ ( ( 𝐴 gcd 𝑁 ) = 1 → ( ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ ( 𝐴 gcd 𝑁 ) = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ↔ ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) )
83 80 82 syl5ibcom ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝑁 ) = 1 → ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) )
84 52 ad3antrrr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∈ ℤ )
85 dvdsmul1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → 𝑁 ∥ ( 𝑁 · 𝑚 ) )
86 84 85 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∥ ( 𝑁 · 𝑚 ) )
87 zmulcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑁 · 𝑚 ) ∈ ℤ )
88 84 87 sylancom ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( 𝑁 · 𝑚 ) ∈ ℤ )
89 dvdsnegb ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑁 · 𝑚 ) ∈ ℤ ) → ( 𝑁 ∥ ( 𝑁 · 𝑚 ) ↔ 𝑁 ∥ - ( 𝑁 · 𝑚 ) ) )
90 84 88 89 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( 𝑁 ∥ ( 𝑁 · 𝑚 ) ↔ 𝑁 ∥ - ( 𝑁 · 𝑚 ) ) )
91 86 90 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∥ - ( 𝑁 · 𝑚 ) )
92 35 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝐴 ∈ ℤ )
93 92 zcnd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝐴 ∈ ℂ )
94 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
95 94 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝑛 ∈ ℂ )
96 93 95 mulcomd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( 𝐴 · 𝑛 ) = ( 𝑛 · 𝐴 ) )
97 96 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) = ( ( 𝑛 · 𝐴 ) + ( 𝑁 · 𝑚 ) ) )
98 95 93 mulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( 𝑛 · 𝐴 ) ∈ ℂ )
99 88 zcnd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( 𝑁 · 𝑚 ) ∈ ℂ )
100 98 99 subnegd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑛 · 𝐴 ) − - ( 𝑁 · 𝑚 ) ) = ( ( 𝑛 · 𝐴 ) + ( 𝑁 · 𝑚 ) ) )
101 97 100 eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) = ( ( 𝑛 · 𝐴 ) − - ( 𝑁 · 𝑚 ) ) )
102 101 oveq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑛 · 𝐴 ) − ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) = ( ( 𝑛 · 𝐴 ) − ( ( 𝑛 · 𝐴 ) − - ( 𝑁 · 𝑚 ) ) ) )
103 99 negcld ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → - ( 𝑁 · 𝑚 ) ∈ ℂ )
104 98 103 nncand ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑛 · 𝐴 ) − ( ( 𝑛 · 𝐴 ) − - ( 𝑁 · 𝑚 ) ) ) = - ( 𝑁 · 𝑚 ) )
105 102 104 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝑛 · 𝐴 ) − ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) = - ( 𝑁 · 𝑚 ) )
106 91 105 breqtrrd ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) )
107 oveq2 ⊢ ( 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) → ( ( 𝑛 · 𝐴 ) − 1 ) = ( ( 𝑛 · 𝐴 ) − ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) )
108 107 breq2d ⊢ ( 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) → ( 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ↔ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) ) ) )
109 106 108 syl5ibrcom ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ∧ 𝑚 ∈ ℤ ) → ( 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) → 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
110 109 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) → ( ∃ 𝑚 ∈ ℤ 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) → 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
111 110 reximdva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑛 ∈ ℤ ∃ 𝑚 ∈ ℤ 1 = ( ( 𝐴 · 𝑛 ) + ( 𝑁 · 𝑚 ) ) → ∃ 𝑛 ∈ ℤ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
112 83 111 syld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐴 gcd 𝑁 ) = 1 → ∃ 𝑛 ∈ ℤ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ) )
113 76 112 impbid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑛 ∈ ℤ 𝑁 ∥ ( ( 𝑛 · 𝐴 ) − 1 ) ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
114 28 50 113 3bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ∃ 𝑥 ∈ ( Base ‘ 𝑌 ) ( 𝑥 ( .r ‘ 𝑌 ) ( 𝐿 ‘ 𝐴 ) ) = ( 1r ‘ 𝑌 ) ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
115 9 19 114 3bitrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ) → ( ( 𝐿 ‘ 𝐴 ) ∈ 𝑈 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )