Proof of Theorem dchrptlem1
Step | Hyp | Ref
| Expression |
1 | | fveq2 5888 |
. . . . . . . 8
                   |
2 | 1 | eqeq1d 2464 |
. . . . . . 7
               
                 |
3 | 2 | anbi1d 716 |
. . . . . 6
                                    
        |
4 | 3 | rexbidv 2913 |
. . . . 5
  
                                            |
5 | 4 | iotabidv 5586 |
. . . 4
                   
                        
        |
6 | | dchrpt.5 |
. . . 4
    
              
        |
7 | | iotaex 5582 |
. . . 4
                  
       |
8 | 5, 6, 7 | fvmpt3i 5976 |
. . 3
        
                       |
9 | 8 | ad2antlr 738 |
. 2
    
                                      
        |
10 | | ovex 6343 |
. . 3
     |
11 | | simpr 467 |
. . . . . . . . . . . 12
                      
                                |
12 | | simpllr 774 |
. . . . . . . . . . . . 13
                      
                                  |
13 | 12 | simprd 469 |
. . . . . . . . . . . 12
                      
                                |
14 | 11, 13 | eqtr3d 2498 |
. . . . . . . . . . 11
                      
                              |
15 | | simp-4l 781 |
. . . . . . . . . . . 12
                      
                  |
16 | | simplr 767 |
. . . . . . . . . . . 12
                      
                  |
17 | 12 | simpld 465 |
. . . . . . . . . . . 12
                      
                  |
18 | | dchrpt.n |
. . . . . . . . . . . . . . . . 17
   |
19 | 18 | nnnn0d 10954 |
. . . . . . . . . . . . . . . 16
   |
20 | | dchrpt.z |
. . . . . . . . . . . . . . . . 17
ℤ/nℤ   |
21 | 20 | zncrng 19164 |
. . . . . . . . . . . . . . . 16

  |
22 | | crngring 17840 |
. . . . . . . . . . . . . . . 16

  |
23 | | dchrpt.u |
. . . . . . . . . . . . . . . . 17
Unit   |
24 | | dchrpt.h |
. . . . . . . . . . . . . . . . 17
 mulGrp  ↾s   |
25 | 23, 24 | unitgrp 17944 |
. . . . . . . . . . . . . . . 16

  |
26 | 19, 21, 22, 25 | 4syl 19 |
. . . . . . . . . . . . . . 15
   |
27 | 26 | adantr 471 |
. . . . . . . . . . . . . 14
 
  
  |
28 | | dchrpt.w |
. . . . . . . . . . . . . . . . 17
 Word   |
29 | | wrdf 12709 |
. . . . . . . . . . . . . . . . 17
 Word    ..^         |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
    ..^         |
31 | | dchrpt.i |
. . . . . . . . . . . . . . . . 17
   |
32 | | fdm 5756 |
. . . . . . . . . . . . . . . . . 18
    ..^        ..^       |
33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
  ..^       |
34 | 31, 33 | eleqtrd 2542 |
. . . . . . . . . . . . . . . 16
  ..^       |
35 | 30, 34 | ffvelrnd 6046 |
. . . . . . . . . . . . . . 15
       |
36 | 35 | adantr 471 |
. . . . . . . . . . . . . 14
 
         |
37 | | simprl 769 |
. . . . . . . . . . . . . 14
 
  
  |
38 | | simprr 771 |
. . . . . . . . . . . . . 14
 
  
  |
39 | 23, 24 | unitgrpbas 17943 |
. . . . . . . . . . . . . . 15
     |
40 | | dchrpt.o |
. . . . . . . . . . . . . . 15
     |
41 | | dchrpt.m |
. . . . . . . . . . . . . . 15
.g   |
42 | | eqid 2462 |
. . . . . . . . . . . . . . 15
         |
43 | 39, 40, 41, 42 | odcong 17247 |
. . . . . . . . . . . . . 14
      
 
         
                |
44 | 27, 36, 37, 38, 43 | syl112anc 1280 |
. . . . . . . . . . . . 13
 
             
               |
45 | | dchrpt.t |
. . . . . . . . . . . . . . . . 17
               |
46 | | neg1cn 10741 |
. . . . . . . . . . . . . . . . . 18
  |
47 | | 2re 10707 |
. . . . . . . . . . . . . . . . . . . 20
 |
48 | | dchrpt.b |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
49 | 20, 48 | znfi 19179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
50 | 18, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
51 | 48, 23 | unitss 17937 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
52 | | ssfi 7818 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
  |
53 | 50, 51, 52 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
54 | 39, 40 | odcl2 17265 |
. . . . . . . . . . . . . . . . . . . . . 22
 
               |
55 | 26, 53, 35, 54 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . . . . 21
           |
56 | 55 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . 20
   
 
          
          |
57 | | nndivre 10673 |
. . . . . . . . . . . . . . . . . . . 20
                       |
58 | 47, 56, 57 | sylancr 674 |
. . . . . . . . . . . . . . . . . . 19
   
 
          
            |
59 | 58 | recnd 9695 |
. . . . . . . . . . . . . . . . . 18
   
 
          
            |
60 | | cxpcl 23668 |
. . . . . . . . . . . . . . . . . 18
                              |
61 | 46, 59, 60 | sylancr 674 |
. . . . . . . . . . . . . . . . 17
   
 
          
  
             |
62 | 45, 61 | syl5eqel 2544 |
. . . . . . . . . . . . . . . 16
   
 
          
  |
63 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   
 
          
   |
64 | | neg1ne0 10743 |
. . . . . . . . . . . . . . . . . . 19
  |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   
 
          
   |
66 | 63, 65, 59 | cxpne0d 23707 |
. . . . . . . . . . . . . . . . 17
   
 
          
  
             |
67 | 45 | neeq1i 2700 |
. . . . . . . . . . . . . . . . 17

  
             |
68 | 66, 67 | sylibr 217 |
. . . . . . . . . . . . . . . 16
   
 
          
  |
69 | | zsubcl 11008 |
. . . . . . . . . . . . . . . . 17
 
     |
70 | 69 | ad2antlr 738 |
. . . . . . . . . . . . . . . 16
   
 
          
    |
71 | 38 | adantr 471 |
. . . . . . . . . . . . . . . 16
   
 
          
  |
72 | | expaddz 12348 |
. . . . . . . . . . . . . . . 16
                               |
73 | 62, 68, 70, 71, 72 | syl22anc 1277 |
. . . . . . . . . . . . . . 15
   
 
          
                      |
74 | 37 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
   
 
          
  |
75 | 74 | zcnd 11070 |
. . . . . . . . . . . . . . . . 17
   
 
          
  |
76 | 71 | zcnd 11070 |
. . . . . . . . . . . . . . . . 17
   
 
          
  |
77 | 75, 76 | npcand 10016 |
. . . . . . . . . . . . . . . 16
   
 
          
      |
78 | 77 | oveq2d 6331 |
. . . . . . . . . . . . . . 15
   
 
          
              |
79 | 45 | oveq1i 6325 |
. . . . . . . . . . . . . . . . . 18
         
                 |
80 | | root1eq1 23744 |
. . . . . . . . . . . . . . . . . . . 20
          
                      
             |
81 | 55, 69, 80 | syl2an 484 |
. . . . . . . . . . . . . . . . . . 19
 
                       
             |
82 | 81 | biimpar 492 |
. . . . . . . . . . . . . . . . . 18
   
 
          
                      |
83 | 79, 82 | syl5eq 2508 |
. . . . . . . . . . . . . . . . 17
   
 
          
        |
84 | 83 | oveq1d 6330 |
. . . . . . . . . . . . . . . 16
   
 
          
                    |
85 | 62, 68, 71 | expclzd 12453 |
. . . . . . . . . . . . . . . . 17
   
 
          
      |
86 | 85 | mulid2d 9687 |
. . . . . . . . . . . . . . . 16
   
 
          
            |
87 | 84, 86 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
   
 
          
                  |
88 | 73, 78, 87 | 3eqtr3d 2504 |
. . . . . . . . . . . . . 14
   
 
          
          |
89 | 88 | ex 440 |
. . . . . . . . . . . . 13
 
                         |
90 | 44, 89 | sylbird 243 |
. . . . . . . . . . . 12
 
                           |
91 | 15, 16, 17, 90 | syl12anc 1274 |
. . . . . . . . . . 11
                      
                            
           |
92 | 14, 91 | mpd 15 |
. . . . . . . . . 10
                      
                          |
93 | 92 | eqeq2d 2472 |
. . . . . . . . 9
                      
                    
       |
94 | 93 | biimpd 212 |
. . . . . . . 8
                      
                    
       |
95 | 94 | expimpd 612 |
. . . . . . 7
   
                                       
       |
96 | 95 | rexlimdva 2891 |
. . . . . 6
    
                                
    
       |
97 | | oveq1 6322 |
. . . . . . . . . . 11
 
             |
98 | 97 | eqeq2d 2472 |
. . . . . . . . . 10
               
                 |
99 | | oveq2 6323 |
. . . . . . . . . . 11
           |
100 | 99 | eqeq2d 2472 |
. . . . . . . . . 10
     
       |
101 | 98, 100 | anbi12d 722 |
. . . . . . . . 9
                                    
        |
102 | 101 | rspcev 3162 |
. . . . . . . 8
                                      
       |
103 | 102 | expr 624 |
. . . . . . 7
                     
               
        |
104 | 103 | adantl 472 |
. . . . . 6
    
                                             |
105 | 96, 104 | impbid 195 |
. . . . 5
    
                                
    
       |
106 | 105 | adantr 471 |
. . . 4
   
                        
                   
       |
107 | 106 | iota5 5585 |
. . 3
   
                                         
            |
108 | 10, 107 | mpan2 682 |
. 2
    
                                  
            |
109 | 9, 108 | eqtrd 2496 |
1
    
                          |