Theorem lgsdchr

Description: The Legendre symbol function X ( m ) = ( m /L N ) , where N is an odd positive number, is a real Dirichlet character modulo N . (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	lgsdchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	lgsdchr.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	lgsdchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	lgsdchr.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	lgsdchr.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	lgsdchr.x	⊢ 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
Assertion	lgsdchr	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 : 𝐵 ⟶ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		lgsdchr.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		lgsdchr.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		lgsdchr.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		lgsdchr.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		lgsdchr.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
6		lgsdchr.x	⊢ 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) )
7		iotaex	⊢ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ∈ V
8	7	a1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑦 ∈ 𝐵 ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ∈ V )
9	6	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 = ( 𝑦 ∈ 𝐵 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( 𝑦 = ( 𝐿 ‘ 𝑚 ) ∧ ℎ = ( 𝑚 /L 𝑁 ) ) ) ) )
10		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11	10	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ0 )
12	2 4 5	znzrhfo	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ 𝐵 )
13	11 12	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝐿 : ℤ –onto→ 𝐵 )
14		foelrn	⊢ ( ( 𝐿 : ℤ –onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) )
15	13 14	sylan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) )
16	1 2 3 4 5 6	lgsdchrval	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑎 /L 𝑁 ) )
17		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℤ )
18		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
19	18	ad2antrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → 𝑁 ∈ ℤ )
20		lgscl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑎 /L 𝑁 ) ∈ ℤ )
21	17 19 20	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑎 /L 𝑁 ) ∈ ℤ )
22	21	zred	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑎 /L 𝑁 ) ∈ ℝ )
23	16 22	eqeltrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ∈ ℝ )
24		fveq2	⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑋 ‘ 𝑥 ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) )
25	24	eleq1d	⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ∈ ℝ ) )
26	23 25	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) )
27	26	rexlimdva	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ ) )
28	27	imp	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
29	15 28	syldan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℝ )
30	8 9 29	fmpt2d	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 : 𝐵 ⟶ ℝ )
31		ax-resscn	⊢ ℝ ⊆ ℂ
32		fss	⊢ ( ( 𝑋 : 𝐵 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝑋 : 𝐵 ⟶ ℂ )
33	30 31 32	sylancl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 : 𝐵 ⟶ ℂ )
34		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
35	4 34	unitss	⊢ ( Unit ‘ 𝑍 ) ⊆ 𝐵
36		foelrn	⊢ ( ( 𝐿 : ℤ –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) )
37	13 36	sylan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) )
38	15 37	anim12dan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) )
39		reeanv	⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) ↔ ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) )
40	17	adantrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
41		simprr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
42	11	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑁 ∈ ℕ0 )
43		lgsdirnn0	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑎 · 𝑏 ) /L 𝑁 ) = ( ( 𝑎 /L 𝑁 ) · ( 𝑏 /L 𝑁 ) ) )
44	40 41 42 43	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑎 · 𝑏 ) /L 𝑁 ) = ( ( 𝑎 /L 𝑁 ) · ( 𝑏 /L 𝑁 ) ) )
45	2	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
46	11 45	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑍 ∈ CRing )
47		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
48	46 47	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑍 ∈ Ring )
49	48	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑍 ∈ Ring )
50	5	zrhrhm	⊢ ( 𝑍 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
51	49 50	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐿 ∈ ( ℤring RingHom 𝑍 ) )
52		zringbas	⊢ ℤ = ( Base ‘ ℤring )
53		zringmulr	⊢ · = ( .r ‘ ℤring )
54		eqid	⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
55	52 53 54	rhmmul	⊢ ( ( 𝐿 ∈ ( ℤring RingHom 𝑍 ) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) )
56	51 40 41 55	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) = ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) )
57	56	fveq2d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) ) = ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) )
58		zmulcl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
59	1 2 3 4 5 6	lgsdchrval	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 · 𝑏 ) ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) ) = ( ( 𝑎 · 𝑏 ) /L 𝑁 ) )
60	58 59	sylan2	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑎 · 𝑏 ) ) ) = ( ( 𝑎 · 𝑏 ) /L 𝑁 ) )
61	57 60	eqtr3d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑎 · 𝑏 ) /L 𝑁 ) )
62	16	adantrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑎 /L 𝑁 ) )
63	1 2 3 4 5 6	lgsdchrval	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑏 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) = ( 𝑏 /L 𝑁 ) )
64	63	adantrl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) = ( 𝑏 /L 𝑁 ) )
65	62 64	oveq12d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑎 /L 𝑁 ) · ( 𝑏 /L 𝑁 ) ) )
66	44 61 65	3eqtr4d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) )
67		oveq12	⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) = ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) )
68	67	fveq2d	⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) )
69		fveq2	⊢ ( 𝑦 = ( 𝐿 ‘ 𝑏 ) → ( 𝑋 ‘ 𝑦 ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) )
70	24 69	oveqan12d	⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) )
71	68 70	eqeq12d	⊢ ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ↔ ( 𝑋 ‘ ( ( 𝐿 ‘ 𝑎 ) ( .r ‘ 𝑍 ) ( 𝐿 ‘ 𝑏 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑏 ) ) ) ) )
72	66 71	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
73	72	rexlimdvva	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
74	39 73	biimtrrid	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
75	74	imp	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ∧ ∃ 𝑏 ∈ ℤ 𝑦 = ( 𝐿 ‘ 𝑏 ) ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
76	38 75	syldan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
77	76	ralrimivva	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
78		ss2ralv	⊢ ( ( Unit ‘ 𝑍 ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ) )
79	35 77 78	mpsyl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) )
80		1z	⊢ 1 ∈ ℤ
81	1 2 3 4 5 6	lgsdchrval	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 1 ∈ ℤ ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 1 /L 𝑁 ) )
82	80 81	mpan2	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 1 /L 𝑁 ) )
83		eqid	⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
84	5 83	zrh1	⊢ ( 𝑍 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
85	48 84	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
86	85	fveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
87	18	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
88		1lgs	⊢ ( 𝑁 ∈ ℤ → ( 1 /L 𝑁 ) = 1 )
89	87 88	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 1 /L 𝑁 ) = 1 )
90	82 86 89	3eqtr3d	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
91		lgsne0	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑎 /L 𝑁 ) ≠ 0 ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
92	17 19 91	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 /L 𝑁 ) ≠ 0 ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
93	92	biimpd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 /L 𝑁 ) ≠ 0 → ( 𝑎 gcd 𝑁 ) = 1 ) )
94	16	neeq1d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 ↔ ( 𝑎 /L 𝑁 ) ≠ 0 ) )
95	2 34 5	znunit	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑎 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
96	11 95	sylan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝑎 gcd 𝑁 ) = 1 ) )
97	93 94 96	3imtr4d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 → ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ) )
98	24	neeq1d	⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 ) )
99		eleq1	⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( 𝑥 ∈ ( Unit ‘ 𝑍 ) ↔ ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ) )
100	98 99	imbi12d	⊢ ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ↔ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) ≠ 0 → ( 𝐿 ‘ 𝑎 ) ∈ ( Unit ‘ 𝑍 ) ) ) )
101	97 100	syl5ibrcom	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑎 ∈ ℤ ) → ( 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
102	101	rexlimdva	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
103	102	imp	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ ∃ 𝑎 ∈ ℤ 𝑥 = ( 𝐿 ‘ 𝑎 ) ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
104	15 103	syldan	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
105	104	ralrimiva	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
106	79 90 105	3jca	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) )
107		simpl	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
108	1 2 4 34 107 3	dchrelbas3	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 : 𝐵 ⟶ ℂ ∧ ( ∀ 𝑥 ∈ ( Unit ‘ 𝑍 ) ∀ 𝑦 ∈ ( Unit ‘ 𝑍 ) ( 𝑋 ‘ ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑋 ‘ 𝑥 ) · ( 𝑋 ‘ 𝑦 ) ) ∧ ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ ( Unit ‘ 𝑍 ) ) ) ) ) )
109	33 106 108	mpbir2and	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → 𝑋 ∈ 𝐷 )
110	109 30	jca	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 : 𝐵 ⟶ ℝ ) )