Theorem zringunit

Description: The units of ZZ are the integers with norm 1 , i.e. 1 and -u 1 . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Assertion	zringunit	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) ↔ ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		zringbas	⊢ ℤ = ( Base ‘ ℤring )
2		eqid	⊢ ( Unit ‘ ℤring ) = ( Unit ‘ ℤring )
3	1 2	unitcl	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) → 𝐴 ∈ ℤ )
4		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
5		zgz	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℤ[i] )
6	5	ssriv	⊢ ℤ ⊆ ℤ[i]
7		gzsubrg	⊢ ℤ[i] ∈ ( SubRing ‘ ℂfld )
8		eqid	⊢ ( ℂfld ↾s ℤ[i] ) = ( ℂfld ↾s ℤ[i] )
9	8	subsubrg	⊢ ( ℤ[i] ∈ ( SubRing ‘ ℂfld ) → ( ℤ ∈ ( SubRing ‘ ( ℂfld ↾s ℤ[i] ) ) ↔ ( ℤ ∈ ( SubRing ‘ ℂfld ) ∧ ℤ ⊆ ℤ[i] ) ) )
10	7 9	ax-mp	⊢ ( ℤ ∈ ( SubRing ‘ ( ℂfld ↾s ℤ[i] ) ) ↔ ( ℤ ∈ ( SubRing ‘ ℂfld ) ∧ ℤ ⊆ ℤ[i] ) )
11	4 6 10	mpbir2an	⊢ ℤ ∈ ( SubRing ‘ ( ℂfld ↾s ℤ[i] ) )
12		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
13		ressabs	⊢ ( ( ℤ[i] ∈ ( SubRing ‘ ℂfld ) ∧ ℤ ⊆ ℤ[i] ) → ( ( ℂfld ↾s ℤ[i] ) ↾s ℤ ) = ( ℂfld ↾s ℤ ) )
14	7 6 13	mp2an	⊢ ( ( ℂfld ↾s ℤ[i] ) ↾s ℤ ) = ( ℂfld ↾s ℤ )
15	12 14	eqtr4i	⊢ ℤring = ( ( ℂfld ↾s ℤ[i] ) ↾s ℤ )
16		eqid	⊢ ( Unit ‘ ( ℂfld ↾s ℤ[i] ) ) = ( Unit ‘ ( ℂfld ↾s ℤ[i] ) )
17	15 16 2	subrguss	⊢ ( ℤ ∈ ( SubRing ‘ ( ℂfld ↾s ℤ[i] ) ) → ( Unit ‘ ℤring ) ⊆ ( Unit ‘ ( ℂfld ↾s ℤ[i] ) ) )
18	11 17	ax-mp	⊢ ( Unit ‘ ℤring ) ⊆ ( Unit ‘ ( ℂfld ↾s ℤ[i] ) )
19	18	sseli	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) → 𝐴 ∈ ( Unit ‘ ( ℂfld ↾s ℤ[i] ) ) )
20	8	gzrngunit	⊢ ( 𝐴 ∈ ( Unit ‘ ( ℂfld ↾s ℤ[i] ) ) ↔ ( 𝐴 ∈ ℤ[i] ∧ ( abs ‘ 𝐴 ) = 1 ) )
21	20	simprbi	⊢ ( 𝐴 ∈ ( Unit ‘ ( ℂfld ↾s ℤ[i] ) ) → ( abs ‘ 𝐴 ) = 1 )
22	19 21	syl	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) → ( abs ‘ 𝐴 ) = 1 )
23	3 22	jca	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) → ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) )
24		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
25	24	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 𝐴 ∈ ℂ )
26		simpr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( abs ‘ 𝐴 ) = 1 )
27		ax-1ne0	⊢ 1 ≠ 0
28	27	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 1 ≠ 0 )
29	26 28	eqnetrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( abs ‘ 𝐴 ) ≠ 0 )
30		fveq2	⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
31		abs0	⊢ ( abs ‘ 0 ) = 0
32	30 31	eqtrdi	⊢ ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
33	32	necon3i	⊢ ( ( abs ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ 0 )
34	29 33	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 𝐴 ≠ 0 )
35		eldifsn	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
36	25 34 35	sylanbrc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
37		simpl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 𝐴 ∈ ℤ )
38		cnfldinv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( invr ‘ ℂfld ) ‘ 𝐴 ) = ( 1 / 𝐴 ) )
39	25 34 38	syl2anc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( invr ‘ ℂfld ) ‘ 𝐴 ) = ( 1 / 𝐴 ) )
40		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
41	40	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 𝐴 ∈ ℝ )
42		absresq	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
43	41 42	syl	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
44	26	oveq1d	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 1 ↑ 2 ) )
45		sq1	⊢ ( 1 ↑ 2 ) = 1
46	44 45	eqtrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = 1 )
47	25	sqvald	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
48	43 46 47	3eqtr3rd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( 𝐴 · 𝐴 ) = 1 )
49		1cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 1 ∈ ℂ )
50	49 25 25 34	divmuld	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( 1 / 𝐴 ) = 𝐴 ↔ ( 𝐴 · 𝐴 ) = 1 ) )
51	48 50	mpbird	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( 1 / 𝐴 ) = 𝐴 )
52	39 51	eqtrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( invr ‘ ℂfld ) ‘ 𝐴 ) = 𝐴 )
53	52 37	eqeltrd	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( invr ‘ ℂfld ) ‘ 𝐴 ) ∈ ℤ )
54		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
55		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
56		cndrng	⊢ ℂfld ∈ DivRing
57	54 55 56	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
58		eqid	⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
59	12 57 2 58	subrgunit	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ( 𝐴 ∈ ( Unit ‘ ℤring ) ↔ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐴 ∈ ℤ ∧ ( ( invr ‘ ℂfld ) ‘ 𝐴 ) ∈ ℤ ) ) )
60	4 59	ax-mp	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) ↔ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐴 ∈ ℤ ∧ ( ( invr ‘ ℂfld ) ‘ 𝐴 ) ∈ ℤ ) )
61	36 37 53 60	syl3anbrc	⊢ ( ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) → 𝐴 ∈ ( Unit ‘ ℤring ) )
62	23 61	impbii	⊢ ( 𝐴 ∈ ( Unit ‘ ℤring ) ↔ ( 𝐴 ∈ ℤ ∧ ( abs ‘ 𝐴 ) = 1 ) )