Step | Hyp | Ref
| Expression |
1 | | iotaex 6329 |
. . . . . 6
⊢
(℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) ∈ V |
2 | 1 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑦 ∈ 𝐵) → (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))) ∈ V) |
3 | | lgsdchr.x |
. . . . . 6
⊢ 𝑋 = (𝑦 ∈ 𝐵 ↦ (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁)))) |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑋 = (𝑦 ∈ 𝐵 ↦ (℩ℎ∃𝑚 ∈ ℤ (𝑦 = (𝐿‘𝑚) ∧ ℎ = (𝑚 /L 𝑁))))) |
5 | | nnnn0 11995 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
6 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℕ0) |
7 | | lgsdchr.z |
. . . . . . . . 9
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
8 | | lgsdchr.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑍) |
9 | | lgsdchr.l |
. . . . . . . . 9
⊢ 𝐿 = (ℤRHom‘𝑍) |
10 | 7, 8, 9 | znzrhfo 20378 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→𝐵) |
11 | 6, 10 | syl 17 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝐿:ℤ–onto→𝐵) |
12 | | foelrn 6894 |
. . . . . . 7
⊢ ((𝐿:ℤ–onto→𝐵 ∧ 𝑥 ∈ 𝐵) → ∃𝑎 ∈ ℤ 𝑥 = (𝐿‘𝑎)) |
13 | 11, 12 | sylan 583 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑥 ∈ 𝐵) → ∃𝑎 ∈ ℤ 𝑥 = (𝐿‘𝑎)) |
14 | | lgsdchr.g |
. . . . . . . . . . 11
⊢ 𝐺 = (DChr‘𝑁) |
15 | | lgsdchr.d |
. . . . . . . . . . 11
⊢ 𝐷 = (Base‘𝐺) |
16 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26102 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → (𝑋‘(𝐿‘𝑎)) = (𝑎 /L 𝑁)) |
17 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → 𝑎 ∈
ℤ) |
18 | | nnz 12097 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
19 | 18 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → 𝑁 ∈
ℤ) |
20 | | lgscl 26059 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑎 /L 𝑁) ∈
ℤ) |
21 | 17, 19, 20 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → (𝑎 /L 𝑁) ∈
ℤ) |
22 | 21 | zred 12180 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → (𝑎 /L 𝑁) ∈
ℝ) |
23 | 16, 22 | eqeltrd 2834 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → (𝑋‘(𝐿‘𝑎)) ∈ ℝ) |
24 | | fveq2 6686 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐿‘𝑎) → (𝑋‘𝑥) = (𝑋‘(𝐿‘𝑎))) |
25 | 24 | eleq1d 2818 |
. . . . . . . . 9
⊢ (𝑥 = (𝐿‘𝑎) → ((𝑋‘𝑥) ∈ ℝ ↔ (𝑋‘(𝐿‘𝑎)) ∈ ℝ)) |
26 | 23, 25 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → (𝑥 = (𝐿‘𝑎) → (𝑋‘𝑥) ∈ ℝ)) |
27 | 26 | rexlimdva 3195 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
(∃𝑎 ∈ ℤ
𝑥 = (𝐿‘𝑎) → (𝑋‘𝑥) ∈ ℝ)) |
28 | 27 | imp 410 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧
∃𝑎 ∈ ℤ
𝑥 = (𝐿‘𝑎)) → (𝑋‘𝑥) ∈ ℝ) |
29 | 13, 28 | syldan 594 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑥 ∈ 𝐵) → (𝑋‘𝑥) ∈ ℝ) |
30 | 2, 4, 29 | fmpt2d 6909 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑋:𝐵⟶ℝ) |
31 | | ax-resscn 10684 |
. . . 4
⊢ ℝ
⊆ ℂ |
32 | | fss 6531 |
. . . 4
⊢ ((𝑋:𝐵⟶ℝ ∧ ℝ ⊆
ℂ) → 𝑋:𝐵⟶ℂ) |
33 | 30, 31, 32 | sylancl 589 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑋:𝐵⟶ℂ) |
34 | | eqid 2739 |
. . . . . 6
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
35 | 8, 34 | unitss 19544 |
. . . . 5
⊢
(Unit‘𝑍)
⊆ 𝐵 |
36 | | foelrn 6894 |
. . . . . . . . 9
⊢ ((𝐿:ℤ–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑏 ∈ ℤ 𝑦 = (𝐿‘𝑏)) |
37 | 11, 36 | sylan 583 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑦 ∈ 𝐵) → ∃𝑏 ∈ ℤ 𝑦 = (𝐿‘𝑏)) |
38 | 13, 37 | anim12dan 622 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∃𝑎 ∈ ℤ 𝑥 = (𝐿‘𝑎) ∧ ∃𝑏 ∈ ℤ 𝑦 = (𝐿‘𝑏))) |
39 | | reeanv 3271 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
ℤ ∃𝑏 ∈
ℤ (𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) ↔ (∃𝑎 ∈ ℤ 𝑥 = (𝐿‘𝑎) ∧ ∃𝑏 ∈ ℤ 𝑦 = (𝐿‘𝑏))) |
40 | 17 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑎 ∈
ℤ) |
41 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑏 ∈
ℤ) |
42 | 6 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑁 ∈
ℕ0) |
43 | | lgsdirnn0 26092 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ ((𝑎 · 𝑏) /L 𝑁) = ((𝑎 /L 𝑁) · (𝑏 /L 𝑁))) |
44 | 40, 41, 42, 43 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑎 · 𝑏) /L 𝑁) = ((𝑎 /L 𝑁) · (𝑏 /L 𝑁))) |
45 | 7 | zncrng 20375 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 𝑍 ∈
CRing) |
46 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑍 ∈ CRing) |
47 | | crngring 19440 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑍 ∈ Ring) |
49 | 48 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝑍 ∈ Ring) |
50 | 9 | zrhrhm 20344 |
. . . . . . . . . . . . . . . 16
⊢ (𝑍 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑍)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → 𝐿 ∈ (ℤring
RingHom 𝑍)) |
52 | | zringbas 20307 |
. . . . . . . . . . . . . . . 16
⊢ ℤ =
(Base‘ℤring) |
53 | | zringmulr 20310 |
. . . . . . . . . . . . . . . 16
⊢ ·
= (.r‘ℤring) |
54 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢
(.r‘𝑍) = (.r‘𝑍) |
55 | 52, 53, 54 | rhmmul 19613 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑍) ∧ 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝐿‘(𝑎 · 𝑏)) = ((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏))) |
56 | 51, 40, 41, 55 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝐿‘(𝑎 · 𝑏)) = ((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏))) |
57 | 56 | fveq2d 6690 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑋‘(𝐿‘(𝑎 · 𝑏))) = (𝑋‘((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏)))) |
58 | | zmulcl 12124 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ) |
59 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26102 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 · 𝑏) ∈ ℤ) → (𝑋‘(𝐿‘(𝑎 · 𝑏))) = ((𝑎 · 𝑏) /L 𝑁)) |
60 | 58, 59 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑋‘(𝐿‘(𝑎 · 𝑏))) = ((𝑎 · 𝑏) /L 𝑁)) |
61 | 57, 60 | eqtr3d 2776 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑋‘((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏))) = ((𝑎 · 𝑏) /L 𝑁)) |
62 | 16 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑋‘(𝐿‘𝑎)) = (𝑎 /L 𝑁)) |
63 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26102 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑏 ∈ ℤ) → (𝑋‘(𝐿‘𝑏)) = (𝑏 /L 𝑁)) |
64 | 63 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑋‘(𝐿‘𝑏)) = (𝑏 /L 𝑁)) |
65 | 62, 64 | oveq12d 7200 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑋‘(𝐿‘𝑎)) · (𝑋‘(𝐿‘𝑏))) = ((𝑎 /L 𝑁) · (𝑏 /L 𝑁))) |
66 | 44, 61, 65 | 3eqtr4d 2784 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑋‘((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏))) = ((𝑋‘(𝐿‘𝑎)) · (𝑋‘(𝐿‘𝑏)))) |
67 | | oveq12 7191 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) → (𝑥(.r‘𝑍)𝑦) = ((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏))) |
68 | 67 | fveq2d 6690 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = (𝑋‘((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏)))) |
69 | | fveq2 6686 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐿‘𝑏) → (𝑋‘𝑦) = (𝑋‘(𝐿‘𝑏))) |
70 | 24, 69 | oveqan12d 7201 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) → ((𝑋‘𝑥) · (𝑋‘𝑦)) = ((𝑋‘(𝐿‘𝑎)) · (𝑋‘(𝐿‘𝑏)))) |
71 | 68, 70 | eqeq12d 2755 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) → ((𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ↔ (𝑋‘((𝐿‘𝑎)(.r‘𝑍)(𝐿‘𝑏))) = ((𝑋‘(𝐿‘𝑎)) · (𝑋‘(𝐿‘𝑏))))) |
72 | 66, 71 | syl5ibrcom 250 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → ((𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
73 | 72 | rexlimdvva 3205 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
(∃𝑎 ∈ ℤ
∃𝑏 ∈ ℤ
(𝑥 = (𝐿‘𝑎) ∧ 𝑦 = (𝐿‘𝑏)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
74 | 39, 73 | syl5bir 246 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
((∃𝑎 ∈ ℤ
𝑥 = (𝐿‘𝑎) ∧ ∃𝑏 ∈ ℤ 𝑦 = (𝐿‘𝑏)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
75 | 74 | imp 410 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧
(∃𝑎 ∈ ℤ
𝑥 = (𝐿‘𝑎) ∧ ∃𝑏 ∈ ℤ 𝑦 = (𝐿‘𝑏))) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
76 | 38, 75 | syldan 594 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
77 | 76 | ralrimivva 3104 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
78 | | ss2ralv 3955 |
. . . . 5
⊢
((Unit‘𝑍)
⊆ 𝐵 →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) → ∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)(𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)))) |
79 | 35, 77, 78 | mpsyl 68 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∀𝑥 ∈
(Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)(𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦))) |
80 | | 1z 12105 |
. . . . . 6
⊢ 1 ∈
ℤ |
81 | 14, 7, 15, 8, 9, 3 | lgsdchrval 26102 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 1 ∈
ℤ) → (𝑋‘(𝐿‘1)) = (1 /L 𝑁)) |
82 | 80, 81 | mpan2 691 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑋‘(𝐿‘1)) = (1 /L 𝑁)) |
83 | | eqid 2739 |
. . . . . . . 8
⊢
(1r‘𝑍) = (1r‘𝑍) |
84 | 9, 83 | zrh1 20345 |
. . . . . . 7
⊢ (𝑍 ∈ Ring → (𝐿‘1) =
(1r‘𝑍)) |
85 | 48, 84 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝐿‘1) =
(1r‘𝑍)) |
86 | 85 | fveq2d 6690 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑋‘(𝐿‘1)) = (𝑋‘(1r‘𝑍))) |
87 | 18 | adantr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℤ) |
88 | | 1lgs 26088 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (1
/L 𝑁) =
1) |
89 | 87, 88 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (1
/L 𝑁) =
1) |
90 | 82, 86, 89 | 3eqtr3d 2782 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑋‘(1r‘𝑍)) = 1) |
91 | | lgsne0 26083 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑎 /L 𝑁) ≠ 0 ↔ (𝑎 gcd 𝑁) = 1)) |
92 | 17, 19, 91 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → ((𝑎 /L 𝑁) ≠ 0 ↔ (𝑎 gcd 𝑁) = 1)) |
93 | 92 | biimpd 232 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → ((𝑎 /L 𝑁) ≠ 0 → (𝑎 gcd 𝑁) = 1)) |
94 | 16 | neeq1d 2994 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → ((𝑋‘(𝐿‘𝑎)) ≠ 0 ↔ (𝑎 /L 𝑁) ≠ 0)) |
95 | 7, 34, 9 | znunit 20394 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑎 ∈ ℤ)
→ ((𝐿‘𝑎) ∈ (Unit‘𝑍) ↔ (𝑎 gcd 𝑁) = 1)) |
96 | 6, 95 | sylan 583 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → ((𝐿‘𝑎) ∈ (Unit‘𝑍) ↔ (𝑎 gcd 𝑁) = 1)) |
97 | 93, 94, 96 | 3imtr4d 297 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → ((𝑋‘(𝐿‘𝑎)) ≠ 0 → (𝐿‘𝑎) ∈ (Unit‘𝑍))) |
98 | 24 | neeq1d 2994 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐿‘𝑎) → ((𝑋‘𝑥) ≠ 0 ↔ (𝑋‘(𝐿‘𝑎)) ≠ 0)) |
99 | | eleq1 2821 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐿‘𝑎) → (𝑥 ∈ (Unit‘𝑍) ↔ (𝐿‘𝑎) ∈ (Unit‘𝑍))) |
100 | 98, 99 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑥 = (𝐿‘𝑎) → (((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)) ↔ ((𝑋‘(𝐿‘𝑎)) ≠ 0 → (𝐿‘𝑎) ∈ (Unit‘𝑍)))) |
101 | 97, 100 | syl5ibrcom 250 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑎 ∈ ℤ) → (𝑥 = (𝐿‘𝑎) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
102 | 101 | rexlimdva 3195 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
(∃𝑎 ∈ ℤ
𝑥 = (𝐿‘𝑎) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
103 | 102 | imp 410 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧
∃𝑎 ∈ ℤ
𝑥 = (𝐿‘𝑎)) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
104 | 13, 103 | syldan 594 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) ∧ 𝑥 ∈ 𝐵) → ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
105 | 104 | ralrimiva 3097 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍))) |
106 | 79, 90, 105 | 3jca 1129 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) →
(∀𝑥 ∈
(Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)(𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))) |
107 | | simpl 486 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑁 ∈
ℕ) |
108 | 14, 7, 8, 34, 107, 15 | dchrelbas3 25986 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑋 ∈ 𝐷 ↔ (𝑋:𝐵⟶ℂ ∧ (∀𝑥 ∈ (Unit‘𝑍)∀𝑦 ∈ (Unit‘𝑍)(𝑋‘(𝑥(.r‘𝑍)𝑦)) = ((𝑋‘𝑥) · (𝑋‘𝑦)) ∧ (𝑋‘(1r‘𝑍)) = 1 ∧ ∀𝑥 ∈ 𝐵 ((𝑋‘𝑥) ≠ 0 → 𝑥 ∈ (Unit‘𝑍)))))) |
109 | 33, 106, 108 | mpbir2and 713 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → 𝑋 ∈ 𝐷) |
110 | 109, 30 | jca 515 |
1
⊢ ((𝑁 ∈ ℕ ∧ ¬ 2
∥ 𝑁) → (𝑋 ∈ 𝐷 ∧ 𝑋:𝐵⟶ℝ)) |