Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . . 4
       |
2 | | gausslemma2d.h |
. . . 4
     |
3 | | gausslemma2d.r |
. . . 4
                      |
4 | | gausslemma2d.m |
. . . 4
       |
5 | 1, 2, 3, 4 | gausslemma2dlem4 15122 |
. . 3
                               |
6 | 5 | oveq1d 5925 |
. 2
         
                         |
7 | | 1zzd 9334 |
. . . . 5
   |
8 | 1 | gausslemma2dlem0a 15107 |
. . . . . . . . 9
   |
9 | 8 | nnzd 9428 |
. . . . . . . 8
   |
10 | | 4nn 9135 |
. . . . . . . 8
 |
11 | | znq 9679 |
. . . . . . . 8
 
     |
12 | 9, 10, 11 | sylancl 413 |
. . . . . . 7
     |
13 | 12 | flqcld 10336 |
. . . . . 6
         |
14 | 4, 13 | eqeltrid 2280 |
. . . . 5
   |
15 | 7, 14 | fzfigd 10492 |
. . . 4
       |
16 | 1, 2, 3, 4 | gausslemma2dlem2 15120 |
. . . . . 6
               |
17 | 16 | adantr 276 |
. . . . 5
 
                   |
18 | | rspa 2542 |
. . . . . . . 8
             
             |
19 | 18 | expcom 116 |
. . . . . . 7
      
                    |
20 | 19 | adantl 277 |
. . . . . 6
 
      
                    |
21 | | elfzelz 10081 |
. . . . . . . . 9
       |
22 | | 2z 9335 |
. . . . . . . . . 10
 |
23 | 22 | a1i 9 |
. . . . . . . . 9
       |
24 | 21, 23 | zmulcld 9435 |
. . . . . . . 8
         |
25 | 24 | adantl 277 |
. . . . . . 7
 
         |
26 | | eleq1 2256 |
. . . . . . 7
           
     |
27 | 25, 26 | syl5ibrcom 157 |
. . . . . 6
 
                   |
28 | 20, 27 | syld 45 |
. . . . 5
 
      
                  |
29 | 17, 28 | mpd 13 |
. . . 4
 
           |
30 | 15, 29 | fprodzcl 11739 |
. . 3
             |
31 | 14 | peano2zd 9432 |
. . . . . 6
     |
32 | 1, 2 | gausslemma2dlem0b 15108 |
. . . . . . 7
   |
33 | 32 | nnzd 9428 |
. . . . . 6
   |
34 | 31, 33 | fzfigd 10492 |
. . . . 5
         |
35 | 1, 2, 3, 4 | gausslemma2dlem3 15121 |
. . . . . . 7
                   |
36 | 35 | adantr 276 |
. . . . . 6
 
                         |
37 | | rspa 2542 |
. . . . . . . . 9
                 
 
               |
38 | 37 | expcom 116 |
. . . . . . . 8
        
                          |
39 | 38 | adantl 277 |
. . . . . . 7
 
        
                          |
40 | | elfzelz 10081 |
. . . . . . . . . 10
         |
41 | 22 | a1i 9 |
. . . . . . . . . 10
         |
42 | 40, 41 | zmulcld 9435 |
. . . . . . . . 9
           |
43 | | zsubcl 9348 |
. . . . . . . . 9
           |
44 | 9, 42, 43 | syl2an 289 |
. . . . . . . 8
 
       
     |
45 | | eleq1 2256 |
. . . . . . . 8
             
       |
46 | 44, 45 | syl5ibrcom 157 |
. . . . . . 7
 
                       |
47 | 39, 46 | syld 45 |
. . . . . 6
 
        
                      |
48 | 36, 47 | mpd 13 |
. . . . 5
 
             |
49 | 34, 48 | fprodzcl 11739 |
. . . 4
               |
50 | | zq 9681 |
. . . 4
                           |
51 | 49, 50 | syl 14 |
. . 3
               |
52 | | nnq 9688 |
. . . 4
   |
53 | 8, 52 | syl 14 |
. . 3
   |
54 | 8 | nngt0d 9016 |
. . 3
   |
55 | | modqmulmodr 10451 |
. . . 4
                          
 
                              
                         |
56 | 55 | eqcomd 2199 |
. . 3
                          
 
                            
                           |
57 | 30, 51, 53, 54, 56 | syl22anc 1250 |
. 2
                                                         |
58 | | gausslemma2d.n |
. . . . . 6
   |
59 | 1, 2, 3, 4, 58 | gausslemma2dlem5 15124 |
. . . . 5
             
                      |
60 | 59 | oveq2d 5926 |
. . . 4
                                                            |
61 | 60 | oveq1d 5925 |
. . 3
                                                                |
62 | | neg1z 9339 |
. . . . . . 7
  |
63 | 1, 4, 2, 58 | gausslemma2dlem0h 15114 |
. . . . . . 7
   |
64 | | zexpcl 10612 |
. . . . . . 7
           |
65 | 62, 63, 64 | sylancr 414 |
. . . . . 6
        |
66 | 40 | adantl 277 |
. . . . . . . 8
 
         |
67 | 22 | a1i 9 |
. . . . . . . 8
 
         |
68 | 66, 67 | zmulcld 9435 |
. . . . . . 7
 
           |
69 | 34, 68 | fprodzcl 11739 |
. . . . . 6
             |
70 | 65, 69 | zmulcld 9435 |
. . . . 5
                    |
71 | | zq 9681 |
. . . . 5
                                     |
72 | 70, 71 | syl 14 |
. . . 4
                    |
73 | | modqmulmodr 10451 |
. . . 4
                               
 
                                                                  |
74 | 30, 72, 53, 54, 73 | syl22anc 1250 |
. . 3
                                                                   |
75 | 16 | prodeq2d 11695 |
. . . . . . . 8
                     |
76 | 75 | oveq1d 5925 |
. . . . . . 7
                                             |
77 | 7, 33 | fzfigd 10492 |
. . . . . . . . 9
       |
78 | | elfzelz 10081 |
. . . . . . . . . . 11
       |
79 | 78 | zcnd 9430 |
. . . . . . . . . 10
       |
80 | 79 | adantl 277 |
. . . . . . . . 9
 
       |
81 | | 2cnd 9045 |
. . . . . . . . 9
 
       |
82 | 77, 80, 81 | fprodmul 11721 |
. . . . . . . 8
                         |
83 | 1, 4 | gausslemma2dlem0d 15110 |
. . . . . . . . . . . 12
   |
84 | 83 | nn0red 9284 |
. . . . . . . . . . 11
   |
85 | 84 | ltp1d 8939 |
. . . . . . . . . 10
     |
86 | | fzdisj 10108 |
. . . . . . . . . 10
       
 
       |
87 | 85, 86 | syl 14 |
. . . . . . . . 9
               |
88 | | nn0pzuz 9642 |
. . . . . . . . . . 11
 
         |
89 | 83, 7, 88 | syl2anc 411 |
. . . . . . . . . 10
         |
90 | 83 | nn0zd 9427 |
. . . . . . . . . . 11
   |
91 | 1, 4, 2 | gausslemma2dlem0g 15113 |
. . . . . . . . . . 11

  |
92 | | eluz2 9588 |
. . . . . . . . . . 11
         |
93 | 90, 33, 91, 92 | syl3anbrc 1183 |
. . . . . . . . . 10
       |
94 | | fzsplit2 10106 |
. . . . . . . . . 10
            
                  |
95 | 89, 93, 94 | syl2anc 411 |
. . . . . . . . 9
                   |
96 | 22 | a1i 9 |
. . . . . . . . . . . 12
       |
97 | 78, 96 | zmulcld 9435 |
. . . . . . . . . . 11
         |
98 | 97 | adantl 277 |
. . . . . . . . . 10
 
         |
99 | 98 | zcnd 9430 |
. . . . . . . . 9
 
         |
100 | 87, 95, 77, 99 | fprodsplit 11727 |
. . . . . . . 8
                               |
101 | | nnoddn2prm 12385 |
. . . . . . . . . . . . . 14
         |
102 | | nnnn0 9237 |
. . . . . . . . . . . . . . 15
   |
103 | 102 | anim1i 340 |
. . . . . . . . . . . . . 14
 
 
   |
104 | 101, 103 | syl 14 |
. . . . . . . . . . . . 13
         |
105 | | nn0oddm1d2 12037 |
. . . . . . . . . . . . . . 15


 
     |
106 | 105 | biimpa 296 |
. . . . . . . . . . . . . 14
 
       |
107 | 2, 106 | eqeltrid 2280 |
. . . . . . . . . . . . 13
 
   |
108 | 1, 104, 107 | 3syl 17 |
. . . . . . . . . . . 12
   |
109 | | fprodfac 11745 |
. . . . . . . . . . . 12

    
       |
110 | 108, 109 | syl 14 |
. . . . . . . . . . 11
             |
111 | 110 | eqcomd 2199 |
. . . . . . . . . 10
             |
112 | | 2cn 9043 |
. . . . . . . . . . 11
 |
113 | | fprodconst 11750 |
. . . . . . . . . . 11
     
          ♯         |
114 | 77, 112, 113 | sylancl 413 |
. . . . . . . . . 10
          ♯         |
115 | 111, 114 | oveq12d 5928 |
. . . . . . . . 9
                       ♯          |
116 | | hashfz1 10841 |
. . . . . . . . . . . 12

♯        |
117 | 108, 116 | syl 14 |
. . . . . . . . . . 11
 ♯        |
118 | 117 | oveq2d 5926 |
. . . . . . . . . 10
    ♯             |
119 | 118 | oveq2d 5926 |
. . . . . . . . 9
         ♯                    |
120 | 108 | faccld 10794 |
. . . . . . . . . . 11
       |
121 | 120 | nncnd 8986 |
. . . . . . . . . 10
       |
122 | | 2nn0 9247 |
. . . . . . . . . . 11
 |
123 | | nn0expcl 10611 |
. . . . . . . . . . . 12
 
       |
124 | 123 | nn0cnd 9285 |
. . . . . . . . . . 11
 
       |
125 | 122, 108,
124 | sylancr 414 |
. . . . . . . . . 10
       |
126 | 121, 125 | mulcomd 8031 |
. . . . . . . . 9
                       |
127 | 115, 119,
126 | 3eqtrd 2230 |
. . . . . . . 8
                           |
128 | 82, 100, 127 | 3eqtr3d 2234 |
. . . . . . 7
                                 |
129 | 76, 128 | eqtrd 2226 |
. . . . . 6
                                   |
130 | 129 | oveq2d 5926 |
. . . . 5
                                                 |
131 | 30 | zcnd 9430 |
. . . . . 6
             |
132 | | neg1rr 9078 |
. . . . . . . . 9
  |
133 | 132 | a1i 9 |
. . . . . . . 8
    |
134 | 133, 63 | reexpcld 10748 |
. . . . . . 7
        |
135 | 134 | recnd 8038 |
. . . . . 6
        |
136 | 69 | zcnd 9430 |
. . . . . 6
             |
137 | 131, 135,
136 | mul12d 8161 |
. . . . 5
                                                             |
138 | 135, 125,
121 | mulassd 8033 |
. . . . 5
                                     |
139 | 130, 137,
138 | 3eqtr4d 2236 |
. . . 4
                                                 |
140 | 139 | oveq1d 5925 |
. . 3
                                                     |
141 | 61, 74, 140 | 3eqtrd 2230 |
. 2
                                                  |
142 | 6, 57, 141 | 3eqtrd 2230 |
1
                            |