Step | Hyp | Ref
| Expression |
1 | | dchrabs.g |
. . . . . . . 8
DChr   |
2 | | eqid 2412 |
. . . . . . . 8
ℤ/nℤ  ℤ/nℤ   |
3 | | dchrabs.d |
. . . . . . . 8
     |
4 | | eqid 2412 |
. . . . . . . 8
       |
5 | | dchrabs.x |
. . . . . . . 8
   |
6 | | cjf 11872 |
. . . . . . . . . 10
     |
7 | | eqid 2412 |
. . . . . . . . . . 11
   ℤ/nℤ      ℤ/nℤ    |
8 | 1, 2, 3, 7, 5 | dchrf 20987 |
. . . . . . . . . 10
      ℤ/nℤ       |
9 | | fco 5567 |
. . . . . . . . . 10
           ℤ/nℤ             ℤ/nℤ       |
10 | 6, 8, 9 | sylancr 645 |
. . . . . . . . 9
        ℤ/nℤ       |
11 | | eqid 2412 |
. . . . . . . . . . . . . . . . . . . . 21
Unit ℤ/nℤ   Unit ℤ/nℤ    |
12 | 1, 3 | dchrrcl 20985 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
13 | 5, 12 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
   |
14 | 1, 2, 7, 11, 13, 3 | dchrelbas3 20983 |
. . . . . . . . . . . . . . . . . . . 20
        ℤ/nℤ       Unit ℤ/nℤ    
Unit ℤ/nℤ            ℤ/nℤ                      ℤ/nℤ    
   ℤ/nℤ        
Unit ℤ/nℤ         |
15 | 5, 14 | mpbid 202 |
. . . . . . . . . . . . . . . . . . 19
       ℤ/nℤ       Unit ℤ/nℤ    
Unit ℤ/nℤ            ℤ/nℤ                      ℤ/nℤ    
   ℤ/nℤ        
Unit ℤ/nℤ        |
16 | 15 | simprd 450 |
. . . . . . . . . . . . . . . . . 18
   Unit ℤ/nℤ    
Unit ℤ/nℤ            ℤ/nℤ                      ℤ/nℤ    
   ℤ/nℤ        
Unit ℤ/nℤ       |
17 | 16 | simp1d 969 |
. . . . . . . . . . . . . . . . 17
  Unit ℤ/nℤ    
Unit ℤ/nℤ            ℤ/nℤ                  |
18 | 17 | r19.21bi 2772 |
. . . . . . . . . . . . . . . 16
 
Unit ℤ/nℤ     Unit ℤ/nℤ            ℤ/nℤ                  |
19 | 18 | r19.21bi 2772 |
. . . . . . . . . . . . . . 15
   Unit ℤ/nℤ    Unit ℤ/nℤ            ℤ/nℤ                  |
20 | 19 | anasss 629 |
. . . . . . . . . . . . . 14
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ             ℤ/nℤ                  |
21 | 20 | fveq2d 5699 |
. . . . . . . . . . . . 13
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ                ℤ/nℤ                       |
22 | 8 | adantr 452 |
. . . . . . . . . . . . . . 15
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ          ℤ/nℤ       |
23 | 7, 11 | unitss 15728 |
. . . . . . . . . . . . . . . 16
Unit ℤ/nℤ      ℤ/nℤ    |
24 | | simprl 733 |
. . . . . . . . . . . . . . . 16
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ     Unit ℤ/nℤ     |
25 | 23, 24 | sseldi 3314 |
. . . . . . . . . . . . . . 15
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ        ℤ/nℤ     |
26 | 22, 25 | ffvelrnd 5838 |
. . . . . . . . . . . . . 14
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ           |
27 | | simprr 734 |
. . . . . . . . . . . . . . . 16
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ     Unit ℤ/nℤ     |
28 | 23, 27 | sseldi 3314 |
. . . . . . . . . . . . . . 15
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ        ℤ/nℤ     |
29 | 22, 28 | ffvelrnd 5838 |
. . . . . . . . . . . . . 14
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ           |
30 | 26, 29 | cjmuld 11989 |
. . . . . . . . . . . . 13
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ                                       |
31 | 21, 30 | eqtrd 2444 |
. . . . . . . . . . . 12
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ                ℤ/nℤ                           |
32 | 13 | nnnn0d 10238 |
. . . . . . . . . . . . . . . 16
   |
33 | 2 | zncrng 16788 |
. . . . . . . . . . . . . . . 16

ℤ/nℤ    |
34 | | crngrng 15637 |
. . . . . . . . . . . . . . . 16
 ℤ/nℤ  ℤ/nℤ    |
35 | 32, 33, 34 | 3syl 19 |
. . . . . . . . . . . . . . 15
 ℤ/nℤ    |
36 | 35 | adantr 452 |
. . . . . . . . . . . . . 14
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ     ℤ/nℤ    |
37 | | eqid 2412 |
. . . . . . . . . . . . . . 15
   ℤ/nℤ      ℤ/nℤ    |
38 | 7, 37 | rngcl 15640 |
. . . . . . . . . . . . . 14
  ℤ/nℤ     ℤ/nℤ  
   ℤ/nℤ         ℤ/nℤ        ℤ/nℤ     |
39 | 36, 25, 28, 38 | syl3anc 1184 |
. . . . . . . . . . . . 13
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ          ℤ/nℤ        ℤ/nℤ     |
40 | | fvco3 5767 |
. . . . . . . . . . . . 13
       ℤ/nℤ          ℤ/nℤ        ℤ/nℤ              ℤ/nℤ                 ℤ/nℤ         |
41 | 22, 39, 40 | syl2anc 643 |
. . . . . . . . . . . 12
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ               ℤ/nℤ                 ℤ/nℤ         |
42 | | fvco3 5767 |
. . . . . . . . . . . . . 14
       ℤ/nℤ        ℤ/nℤ                    |
43 | 22, 25, 42 | syl2anc 643 |
. . . . . . . . . . . . 13
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ                     |
44 | | fvco3 5767 |
. . . . . . . . . . . . . 14
       ℤ/nℤ        ℤ/nℤ                    |
45 | 22, 28, 44 | syl2anc 643 |
. . . . . . . . . . . . 13
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ                     |
46 | 43, 45 | oveq12d 6066 |
. . . . . . . . . . . 12
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ                                       |
47 | 31, 41, 46 | 3eqtr4d 2454 |
. . . . . . . . . . 11
 
 Unit ℤ/nℤ  
Unit ℤ/nℤ               ℤ/nℤ                      |
48 | 47 | ralrimivva 2766 |
. . . . . . . . . 10
  Unit ℤ/nℤ    
Unit ℤ/nℤ              ℤ/nℤ                      |
49 | | eqid 2412 |
. . . . . . . . . . . . . 14
   ℤ/nℤ      ℤ/nℤ    |
50 | 7, 49 | rngidcl 15647 |
. . . . . . . . . . . . 13
 ℤ/nℤ     ℤ/nℤ      ℤ/nℤ     |
51 | 35, 50 | syl 16 |
. . . . . . . . . . . 12
    ℤ/nℤ      ℤ/nℤ     |
52 | | fvco3 5767 |
. . . . . . . . . . . 12
       ℤ/nℤ        ℤ/nℤ      ℤ/nℤ            ℤ/nℤ             ℤ/nℤ       |
53 | 8, 51, 52 | syl2anc 643 |
. . . . . . . . . . 11
         ℤ/nℤ             ℤ/nℤ       |
54 | 16 | simp2d 970 |
. . . . . . . . . . . . 13
       ℤ/nℤ      |
55 | 54 | fveq2d 5699 |
. . . . . . . . . . . 12
          ℤ/nℤ           |
56 | | 1re 9054 |
. . . . . . . . . . . . 13
 |
57 | | cjre 11907 |
. . . . . . . . . . . . 13
       |
58 | 56, 57 | ax-mp 8 |
. . . . . . . . . . . 12
     |
59 | 55, 58 | syl6eq 2460 |
. . . . . . . . . . 11
          ℤ/nℤ       |
60 | 53, 59 | eqtrd 2444 |
. . . . . . . . . 10
         ℤ/nℤ      |
61 | 16 | simp3d 971 |
. . . . . . . . . . 11
     ℤ/nℤ        
Unit ℤ/nℤ      |
62 | 8, 42 | sylan 458 |
. . . . . . . . . . . . . . . 16
 
   ℤ/nℤ                    |
63 | | cj0 11926 |
. . . . . . . . . . . . . . . . . 18
     |
64 | 63 | eqcomi 2416 |
. . . . . . . . . . . . . . . . 17
     |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
   ℤ/nℤ          |
66 | 62, 65 | eqeq12d 2426 |
. . . . . . . . . . . . . . 15
 
   ℤ/nℤ                          |
67 | 8 | ffvelrnda 5837 |
. . . . . . . . . . . . . . . 16
 
   ℤ/nℤ          |
68 | | 0cn 9048 |
. . . . . . . . . . . . . . . 16
 |
69 | | cj11 11930 |
. . . . . . . . . . . . . . . 16
     
             
       |
70 | 67, 68, 69 | sylancl 644 |
. . . . . . . . . . . . . . 15
 
   ℤ/nℤ                        |
71 | 66, 70 | bitrd 245 |
. . . . . . . . . . . . . 14
 
   ℤ/nℤ                  |
72 | 71 | necon3bid 2610 |
. . . . . . . . . . . . 13
 
   ℤ/nℤ                  |
73 | 72 | imbi1d 309 |
. . . . . . . . . . . 12
 
   ℤ/nℤ           
Unit ℤ/nℤ         Unit ℤ/nℤ       |
74 | 73 | ralbidva 2690 |
. . . . . . . . . . 11
      ℤ/nℤ          
Unit ℤ/nℤ    
   ℤ/nℤ        
Unit ℤ/nℤ       |
75 | 61, 74 | mpbird 224 |
. . . . . . . . . 10
     ℤ/nℤ          
Unit ℤ/nℤ      |
76 | 48, 60, 75 | 3jca 1134 |
. . . . . . . . 9
   Unit ℤ/nℤ    
Unit ℤ/nℤ              ℤ/nℤ                            ℤ/nℤ    
   ℤ/nℤ          
Unit ℤ/nℤ       |
77 | 1, 2, 7, 11, 13, 3 | dchrelbas3 20983 |
. . . . . . . . 9
            ℤ/nℤ       Unit ℤ/nℤ    
Unit ℤ/nℤ              ℤ/nℤ                            ℤ/nℤ    
   ℤ/nℤ          
Unit ℤ/nℤ         |
78 | 10, 76, 77 | mpbir2and 889 |
. . . . . . . 8
     |
79 | 1, 2, 3, 4, 5, 78 | dchrmul 20993 |
. . . . . . 7
           
     |
80 | 79 | adantr 452 |
. . . . . 6
 
Unit ℤ/nℤ               
    |
81 | 80 | fveq1d 5697 |
. . . . 5
 
Unit ℤ/nℤ                            |
82 | 23 | sseli 3312 |
. . . . . . . . 9
 Unit ℤ/nℤ      ℤ/nℤ     |
83 | 82, 62 | sylan2 461 |
. . . . . . . 8
 
Unit ℤ/nℤ                    |
84 | 83 | oveq2d 6064 |
. . . . . . 7
 
Unit ℤ/nℤ                                |
85 | 82, 67 | sylan2 461 |
. . . . . . . 8
 
Unit ℤ/nℤ          |
86 | 85 | absvalsqd 12207 |
. . . . . . 7
 
Unit ℤ/nℤ                                |
87 | 5 | adantr 452 |
. . . . . . . . . 10
 
Unit ℤ/nℤ      |
88 | | simpr 448 |
. . . . . . . . . 10
 
Unit ℤ/nℤ    Unit ℤ/nℤ     |
89 | 1, 3, 87, 2, 11, 88 | dchrabs 21005 |
. . . . . . . . 9
 
Unit ℤ/nℤ              |
90 | 89 | oveq1d 6063 |
. . . . . . . 8
 
Unit ℤ/nℤ                      |
91 | | sq1 11439 |
. . . . . . . 8
     |
92 | 90, 91 | syl6eq 2460 |
. . . . . . 7
 
Unit ℤ/nℤ                  |
93 | 84, 86, 92 | 3eqtr2d 2450 |
. . . . . 6
 
Unit ℤ/nℤ                  |
94 | 8 | adantr 452 |
. . . . . . . 8
 
Unit ℤ/nℤ         ℤ/nℤ       |
95 | | ffn 5558 |
. . . . . . . 8
      ℤ/nℤ        ℤ/nℤ     |
96 | 94, 95 | syl 16 |
. . . . . . 7
 
Unit ℤ/nℤ       ℤ/nℤ     |
97 | | ffn 5558 |
. . . . . . . . 9
        ℤ/nℤ          ℤ/nℤ     |
98 | 10, 97 | syl 16 |
. . . . . . . 8
      ℤ/nℤ     |
99 | 98 | adantr 452 |
. . . . . . 7
 
Unit ℤ/nℤ         ℤ/nℤ     |
100 | | fvex 5709 |
. . . . . . . 8
   ℤ/nℤ    |
101 | 100 | a1i 11 |
. . . . . . 7
 
Unit ℤ/nℤ       ℤ/nℤ     |
102 | 82 | adantl 453 |
. . . . . . 7
 
Unit ℤ/nℤ       ℤ/nℤ     |
103 | | fnfvof 6284 |
. . . . . . 7
      ℤ/nℤ   
    ℤ/nℤ        ℤ/nℤ  
   ℤ/nℤ    
                       |
104 | 96, 99, 101, 102, 103 | syl22anc 1185 |
. . . . . 6
 
Unit ℤ/nℤ                           |
105 | | eqid 2412 |
. . . . . . 7
         |
106 | 13 | adantr 452 |
. . . . . . 7
 
Unit ℤ/nℤ      |
107 | 1, 2, 105, 11, 106, 88 | dchr1 21002 |
. . . . . 6
 
Unit ℤ/nℤ              |
108 | 93, 104, 107 | 3eqtr4d 2454 |
. . . . 5
 
Unit ℤ/nℤ                       |
109 | 81, 108 | eqtrd 2444 |
. . . 4
 
Unit ℤ/nℤ                           |
110 | 109 | ralrimiva 2757 |
. . 3
  Unit ℤ/nℤ                           |
111 | 1, 2, 3, 4, 5, 78 | dchrmulcl 20994 |
. . . 4
            |
112 | 1 | dchrabl 20999 |
. . . . . 6
   |
113 | | ablgrp 15380 |
. . . . . 6

  |
114 | 13, 112, 113 | 3syl 19 |
. . . . 5
   |
115 | 3, 105 | grpidcl 14796 |
. . . . 5
       |
116 | 114, 115 | syl 16 |
. . . 4
       |
117 | 1, 2, 3, 11, 111, 116 | dchreq 21003 |
. . 3
               
Unit ℤ/nℤ                            |
118 | 110, 117 | mpbird 224 |
. 2
                |
119 | | dchrinv.i |
. . . 4
      |
120 | 3, 4, 105, 119 | grpinvid1 14816 |
. . 3
 

                         |
121 | 114, 5, 78, 120 | syl3anc 1184 |
. 2
                        |
122 | 118, 121 | mpbird 224 |
1
         |