Step | Hyp | Ref
| Expression |
1 | | lgseisen.2 |
. . . . 5
       |
2 | | lgseisen.1 |
. . . . 5
       |
3 | | lgseisen.3 |
. . . . . 6
   |
4 | 3 | necomd 2691 |
. . . . 5
   |
5 | | lgsquad.5 |
. . . . 5
     |
6 | | lgsquad.4 |
. . . . 5
     |
7 | | eleq1 2528 |
. . . . . . . . . 10
     
       |
8 | | eleq1 2528 |
. . . . . . . . . 10
     
       |
9 | 7, 8 | bi2anan9 889 |
. . . . . . . . 9
 
      
    
    
        |
10 | | ancom 456 |
. . . . . . . . 9
     
                 |
11 | 9, 10 | syl6bb 269 |
. . . . . . . 8
 
      
    
    
        |
12 | | oveq1 6327 |
. . . . . . . . 9
       |
13 | | oveq1 6327 |
. . . . . . . . 9
       |
14 | 12, 13 | breqan12d 4434 |
. . . . . . . 8
 
       
     |
15 | 11, 14 | anbi12d 722 |
. . . . . . 7
 
                 
     
             |
16 | 15 | ancoms 459 |
. . . . . 6
 
                 
     
             |
17 | 16 | cbvopabv 4488 |
. . . . 5
                        
     
            |
18 | 1, 2, 4, 5, 6, 17 | lgsquadlem2 24339 |
. . . 4
               
                     |
19 | | relopab 4982 |
. . . . . . . 8
                      |
20 | | fzfid 12224 |
. . . . . . . . . 10
       |
21 | | fzfid 12224 |
. . . . . . . . . 10
       |
22 | | xpfi 7873 |
. . . . . . . . . 10
                       |
23 | 20, 21, 22 | syl2anc 671 |
. . . . . . . . 9
             |
24 | | opabssxp 4931 |
. . . . . . . . 9
                                |
25 | | ssfi 7823 |
. . . . . . . . 9
                                               
     
             |
26 | 23, 24, 25 | sylancl 673 |
. . . . . . . 8
    
     
             |
27 | | cnven 7676 |
. . . . . . . 8
                                                
     
               
     
             |
28 | 19, 26, 27 | sylancr 674 |
. . . . . . 7
    
     
               
     
             |
29 | | cnvopab 5259 |
. . . . . . 7
                         
                  |
30 | 28, 29 | syl6breq 4458 |
. . . . . 6
    
     
                    
             |
31 | | hasheni 12569 |
. . . . . 6
                         
                                                      
              |
32 | 30, 31 | syl 17 |
. . . . 5
                                                     |
33 | 32 | oveq2d 6336 |
. . . 4
                                         
                     |
34 | 18, 33 | eqtr4d 2499 |
. . 3
                                     |
35 | | lgsquad.6 |
. . . 4
   
     
            |
36 | 2, 1, 3, 6, 5, 35 | lgsquadlem2 24339 |
. . 3
                |
37 | 34, 36 | oveq12d 6338 |
. 2
                                                      |
38 | | neg1cn 10746 |
. . . 4
  |
39 | 38 | a1i 11 |
. . 3
    |
40 | | opabssxp 4931 |
. . . . . 6
                                |
41 | 35, 40 | eqsstri 3474 |
. . . . 5
           |
42 | | ssfi 7823 |
. . . . 5
                      
  |
43 | 23, 41, 42 | sylancl 673 |
. . . 4
   |
44 | | hashcl 12576 |
. . . 4
       |
45 | 43, 44 | syl 17 |
. . 3
       |
46 | | hashcl 12576 |
. . . 4
                                                 |
47 | 26, 46 | syl 17 |
. . 3
                            |
48 | 39, 45, 47 | expaddd 12456 |
. 2
                                                
     
                         |
49 | 1 | eldifad 3428 |
. . . . . . . . . . . . . . . . 17
   |
50 | 49 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
    
     
  |
51 | | prmnn 14680 |
. . . . . . . . . . . . . . . 16

  |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
 
    
     
  |
53 | | oddprm 14820 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
       |
55 | 5, 54 | syl5eqel 2544 |
. . . . . . . . . . . . . . . . . . . 20
   |
56 | 55 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
 
    
     
  |
57 | 56 | nnzd 11073 |
. . . . . . . . . . . . . . . . . 18
 
    
     
  |
58 | | prmz 14681 |
. . . . . . . . . . . . . . . . . . . 20

  |
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
    
     
  |
60 | | peano2zm 11014 |
. . . . . . . . . . . . . . . . . . 19
 
   |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
    
          |
62 | 56 | nnred 10657 |
. . . . . . . . . . . . . . . . . . 19
 
    
     
  |
63 | 61 | zred 11074 |
. . . . . . . . . . . . . . . . . . 19
 
    
          |
64 | | prmuz2 14697 |
. . . . . . . . . . . . . . . . . . . . . . . 24

      |
65 | 50, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
    
     
      |
66 | | uz2m1nn 11267 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
    |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 
    
          |
68 | 67 | nnrpd 11373 |
. . . . . . . . . . . . . . . . . . . . 21
 
    
          |
69 | | rphalflt 11363 |
. . . . . . . . . . . . . . . . . . . . 21
  
        |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
    
         
    |
71 | 5, 70 | syl5eqbr 4452 |
. . . . . . . . . . . . . . . . . . 19
 
    
          |
72 | 62, 63, 71 | ltled 9814 |
. . . . . . . . . . . . . . . . . 18
 
    
          |
73 | | eluz2 11199 |
. . . . . . . . . . . . . . . . . 18
               |
74 | 57, 61, 72, 73 | syl3anbrc 1198 |
. . . . . . . . . . . . . . . . 17
 
    
              |
75 | | fzss2 11873 |
. . . . . . . . . . . . . . . . 17
      
       
    |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
         
        |
77 | | simprr 771 |
. . . . . . . . . . . . . . . 16
 
    
            |
78 | 76, 77 | sseldd 3445 |
. . . . . . . . . . . . . . 15
 
    
              |
79 | | fzm1ndvds 14412 |
. . . . . . . . . . . . . . 15
 
      
  |
80 | 52, 78, 79 | syl2anc 671 |
. . . . . . . . . . . . . 14
 
    
     
  |
81 | 4 | adantr 471 |
. . . . . . . . . . . . . . . 16
 
    
        |
82 | 2 | eldifad 3428 |
. . . . . . . . . . . . . . . . . 18
   |
83 | 82 | adantr 471 |
. . . . . . . . . . . . . . . . 17
 
    
     
  |
84 | | prmrp 14713 |
. . . . . . . . . . . . . . . . 17
         |
85 | 50, 83, 84 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
 
    
            |
86 | 81, 85 | mpbird 240 |
. . . . . . . . . . . . . . 15
 
    
          |
87 | | prmz 14681 |
. . . . . . . . . . . . . . . . 17

  |
88 | 83, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
     
  |
89 | | elfzelz 11835 |
. . . . . . . . . . . . . . . . 17
       |
90 | 89 | ad2antll 740 |
. . . . . . . . . . . . . . . 16
 
    
        |
91 | | coprmdvds 14714 |
. . . . . . . . . . . . . . . 16
 
   
       |
92 | 59, 88, 90, 91 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
 
    
        

  
   |
93 | 86, 92 | mpan2d 685 |
. . . . . . . . . . . . . 14
 
    
       
    |
94 | 80, 93 | mtod 182 |
. . . . . . . . . . . . 13
 
    
     
    |
95 | | prmnn 14680 |
. . . . . . . . . . . . . . . . 17

  |
96 | 83, 95 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
     
  |
97 | 96 | nncnd 10658 |
. . . . . . . . . . . . . . 15
 
    
     
  |
98 | | elfznn 11863 |
. . . . . . . . . . . . . . . . 17
       |
99 | 98 | ad2antll 740 |
. . . . . . . . . . . . . . . 16
 
    
        |
100 | 99 | nncnd 10658 |
. . . . . . . . . . . . . . 15
 
    
        |
101 | 97, 100 | mulcomd 9695 |
. . . . . . . . . . . . . 14
 
    
            |
102 | 101 | breq2d 4430 |
. . . . . . . . . . . . 13
 
    
       
      |
103 | 94, 102 | mtbid 306 |
. . . . . . . . . . . 12
 
    
     
    |
104 | | elfzelz 11835 |
. . . . . . . . . . . . . . . 16
       |
105 | 104 | ad2antrl 739 |
. . . . . . . . . . . . . . 15
 
    
     
  |
106 | | dvdsmul2 14380 |
. . . . . . . . . . . . . . 15
 
     |
107 | 105, 59, 106 | syl2anc 671 |
. . . . . . . . . . . . . 14
 
    
          |
108 | | breq2 4422 |
. . . . . . . . . . . . . 14
       
     |
109 | 107, 108 | syl5ibcom 228 |
. . . . . . . . . . . . 13
 
    
                |
110 | 109 | necon3bd 2650 |
. . . . . . . . . . . 12
 
    
        
       |
111 | 103, 110 | mpd 15 |
. . . . . . . . . . 11
 
    
            |
112 | | elfznn 11863 |
. . . . . . . . . . . . . . 15
       |
113 | 112 | ad2antrl 739 |
. . . . . . . . . . . . . 14
 
    
     
  |
114 | 113, 52 | nnmulcld 10690 |
. . . . . . . . . . . . 13
 
    
          |
115 | 114 | nnred 10657 |
. . . . . . . . . . . 12
 
    
          |
116 | 99, 96 | nnmulcld 10690 |
. . . . . . . . . . . . 13
 
    
          |
117 | 116 | nnred 10657 |
. . . . . . . . . . . 12
 
    
          |
118 | 115, 117 | lttri2d 9805 |
. . . . . . . . . . 11
 
    
                        |
119 | 111, 118 | mpbid 215 |
. . . . . . . . . 10
 
    
                  |
120 | 119 | ex 440 |
. . . . . . . . 9
      
       
          |
121 | 120 | pm4.71rd 645 |
. . . . . . . 8
      
    
   
       
   
         |
122 | | ancom 456 |
. . . . . . . 8
                      
     
                  |
123 | 121, 122 | syl6rbb 270 |
. . . . . . 7
               
                     |
124 | 123 | opabbidv 4482 |
. . . . . 6
    
     
                         
        |
125 | | unopab 4494 |
. . . . . . 7
                                                      
               
             |
126 | 35 | uneq2i 3597 |
. . . . . . 7
                                                                    |
127 | | andi 883 |
. . . . . . . 8
                                             
             |
128 | 127 | opabbii 4483 |
. . . . . . 7
                                     
               
             |
129 | 125, 126,
128 | 3eqtr4i 2494 |
. . . . . 6
                          
     
                  |
130 | | df-xp 4862 |
. . . . . 6
             
    
       |
131 | 124, 129,
130 | 3eqtr4g 2521 |
. . . . 5
                                    |
132 | 131 | fveq2d 5896 |
. . . 4
        
     
                             |
133 | | inopab 4987 |
. . . . . . 7
                                                      
               
             |
134 | 35 | ineq2i 3643 |
. . . . . . 7
                                                                    |
135 | | anandi 842 |
. . . . . . . 8
                                             
             |
136 | 135 | opabbii 4483 |
. . . . . . 7
                                     
               
             |
137 | 133, 134,
136 | 3eqtr4i 2494 |
. . . . . 6
                          
     
         
        |
138 | | ltnsym2 9764 |
. . . . . . . . . . . 12
      
            |
139 | 115, 117,
138 | syl2anc 671 |
. . . . . . . . . . 11
 
    
                  |
140 | 139 | ex 440 |
. . . . . . . . . 10
      
                  |
141 | | imnan 428 |
. . . . . . . . . 10
           
  
             
       
          |
142 | 140, 141 | sylib 201 |
. . . . . . . . 9
              
          |
143 | 142 | nexdv 1793 |
. . . . . . . 8
                           |
144 | 143 | nexdv 1793 |
. . . . . . 7
                  
          |
145 | | opabn0 4749 |
. . . . . . . 8
                  
        
                 
          |
146 | 145 | necon1bbii 2685 |
. . . . . . 7
          
       
           
     
         
         |
147 | 144, 146 | sylib 201 |
. . . . . 6
    
     
         
         |
148 | 137, 147 | syl5eq 2508 |
. . . . 5
                          |
149 | | hashun 12599 |
. . . . 5
     
     
               
     
                                               
     
                   |
150 | 26, 43, 148, 149 | syl3anc 1276 |
. . . 4
        
     
                                              |
151 | | hashxp 12645 |
. . . . . 6
                                             |
152 | 20, 21, 151 | syl2anc 671 |
. . . . 5
                                   |
153 | | oddprm 14820 |
. . . . . . . . . 10
           |
154 | 2, 153 | syl 17 |
. . . . . . . . 9
       |
155 | 6, 154 | syl5eqel 2544 |
. . . . . . . 8
   |
156 | 155 | nnnn0d 10959 |
. . . . . . 7
   |
157 | | hashfz1 12567 |
. . . . . . 7

          |
158 | 156, 157 | syl 17 |
. . . . . 6
           |
159 | 55 | nnnn0d 10959 |
. . . . . . 7
   |
160 | | hashfz1 12567 |
. . . . . . 7

          |
161 | 159, 160 | syl 17 |
. . . . . 6
           |
162 | 158, 161 | oveq12d 6338 |
. . . . 5
                       |
163 | 152, 162 | eqtrd 2496 |
. . . 4
                   |
164 | 132, 150,
163 | 3eqtr3d 2504 |
. . 3
                                    |
165 | 164 | oveq2d 6336 |
. 2
                                              |
166 | 37, 48, 165 | 3eqtr2d 2502 |
1
                    |