Proof of Theorem gausslemma2dlem4
Step | Hyp | Ref
| Expression |
1 | | gausslemma2d.p |
. . 3
       |
2 | | gausslemma2d.h |
. . 3
     |
3 | | gausslemma2d.r |
. . 3
                      |
4 | 1, 2, 3 | gausslemma2dlem1 15119 |
. 2
                 |
5 | | gausslemma2d.m |
. . . . . 6
       |
6 | | 3lt4 9144 |
. . . . . . . 8
 |
7 | | breq1 4032 |
. . . . . . . 8
 
   |
8 | 6, 7 | mpbiri 168 |
. . . . . . 7
   |
9 | | 3nn0 9248 |
. . . . . . . . 9
 |
10 | | eleq1 2256 |
. . . . . . . . 9
 
   |
11 | 9, 10 | mpbiri 168 |
. . . . . . . 8
   |
12 | | 4nn 9135 |
. . . . . . . 8
 |
13 | | divfl0 10355 |
. . . . . . . 8
 
           |
14 | 11, 12, 13 | sylancl 413 |
. . . . . . 7
 
         |
15 | 8, 14 | mpbid 147 |
. . . . . 6
         |
16 | 5, 15 | eqtrid 2238 |
. . . . 5
   |
17 | | oveq2 5918 |
. . . . . . . . . . . 12
           |
18 | 17 | adantr 276 |
. . . . . . . . . . 11
             |
19 | | fz10 10102 |
. . . . . . . . . . 11
     |
20 | 18, 19 | eqtrdi 2242 |
. . . . . . . . . 10
         |
21 | 20 | prodeq1d 11694 |
. . . . . . . . 9
             
      |
22 | | prod0 11715 |
. . . . . . . . 9
      |
23 | 21, 22 | eqtrdi 2242 |
. . . . . . . 8
               |
24 | | oveq1 5917 |
. . . . . . . . . . . 12
 
     |
25 | 24 | adantr 276 |
. . . . . . . . . . 11
   
     |
26 | | 0p1e1 9086 |
. . . . . . . . . . 11
   |
27 | 25, 26 | eqtrdi 2242 |
. . . . . . . . . 10
   
   |
28 | 27 | oveq1d 5925 |
. . . . . . . . 9
               |
29 | 28 | prodeq1d 11694 |
. . . . . . . 8
               
           |
30 | 23, 29 | oveq12d 5928 |
. . . . . . 7
                                         |
31 | | 1zzd 9334 |
. . . . . . . . . . 11
   |
32 | 1, 2 | gausslemma2dlem0b 15108 |
. . . . . . . . . . . 12
   |
33 | 32 | nnzd 9428 |
. . . . . . . . . . 11
   |
34 | 31, 33 | fzfigd 10492 |
. . . . . . . . . 10
       |
35 | 34 | adantl 277 |
. . . . . . . . 9
         |
36 | | oveq1 5917 |
. . . . . . . . . . . . . . 15
       |
37 | 36 | breq1d 4039 |
. . . . . . . . . . . . . 14
     
       |
38 | 36 | oveq2d 5926 |
. . . . . . . . . . . . . 14
 
         |
39 | 37, 36, 38 | ifbieq12d 3583 |
. . . . . . . . . . . . 13
                                 |
40 | | simpr 110 |
. . . . . . . . . . . . 13
 
           |
41 | 40 | elfzelzd 10082 |
. . . . . . . . . . . . . . 15
 
       |
42 | | 2z 9335 |
. . . . . . . . . . . . . . . 16
 |
43 | 42 | a1i 9 |
. . . . . . . . . . . . . . 15
 
       |
44 | 41, 43 | zmulcld 9435 |
. . . . . . . . . . . . . 14
 
         |
45 | 1 | eldifad 3164 |
. . . . . . . . . . . . . . . . 17
   |
46 | | prmz 12236 |
. . . . . . . . . . . . . . . . 17

  |
47 | 45, 46 | syl 14 |
. . . . . . . . . . . . . . . 16
   |
48 | 47 | adantr 276 |
. . . . . . . . . . . . . . 15
 
       |
49 | 48, 44 | zsubcld 9434 |
. . . . . . . . . . . . . 14
 
     
     |
50 | | zq 9681 |
. . . . . . . . . . . . . . . 16
       |
51 | 44, 50 | syl 14 |
. . . . . . . . . . . . . . 15
 
         |
52 | | 2nn 9133 |
. . . . . . . . . . . . . . . . 17
 |
53 | | znq 9679 |
. . . . . . . . . . . . . . . . 17
 
     |
54 | 47, 52, 53 | sylancl 413 |
. . . . . . . . . . . . . . . 16
     |
55 | 54 | adantr 276 |
. . . . . . . . . . . . . . 15
 
         |
56 | | qdclt 10305 |
. . . . . . . . . . . . . . 15
    
  DECID       |
57 | 51, 55, 56 | syl2anc 411 |
. . . . . . . . . . . . . 14
 
    
DECID       |
58 | 44, 49, 57 | ifcldcd 3593 |
. . . . . . . . . . . . 13
 
                      |
59 | 3, 39, 40, 58 | fvmptd3 5643 |
. . . . . . . . . . . 12
 
                          |
60 | 59, 58 | eqeltrd 2270 |
. . . . . . . . . . 11
 
           |
61 | 60 | zcnd 9430 |
. . . . . . . . . 10
 
           |
62 | 61 | adantll 476 |
. . . . . . . . 9
   
           |
63 | 35, 62 | fprodcl 11737 |
. . . . . . . 8
               |
64 | 63 | mullidd 8027 |
. . . . . . 7
               
           |
65 | 30, 64 | eqtr2d 2227 |
. . . . . 6
                                       |
66 | 65 | ex 115 |
. . . . 5
                                       |
67 | 16, 66 | syl 14 |
. . . 4
                                       |
68 | 67 | impcom 125 |
. . 3
 
                                     |
69 | 1, 5 | gausslemma2dlem0d 15110 |
. . . . . . . . 9
   |
70 | 69 | nn0red 9284 |
. . . . . . . 8
   |
71 | 70 | ltp1d 8939 |
. . . . . . 7
     |
72 | | fzdisj 10108 |
. . . . . . 7
       
 
       |
73 | 71, 72 | syl 14 |
. . . . . 6
               |
74 | 73 | adantl 277 |
. . . . 5
                     |
75 | | eluzelz 9591 |
. . . . . . . . . . . . . . 15
    
  |
76 | | znq 9679 |
. . . . . . . . . . . . . . 15
 
     |
77 | 75, 12, 76 | sylancl 413 |
. . . . . . . . . . . . . 14
    
    |
78 | 77 | flqcld 10336 |
. . . . . . . . . . . . 13
    
        |
79 | | nnrp 9719 |
. . . . . . . . . . . . . . . 16
   |
80 | 12, 79 | ax-mp 5 |
. . . . . . . . . . . . . . 15
 |
81 | | eluzelre 9592 |
. . . . . . . . . . . . . . 15
    
  |
82 | | eluz2 9588 |
. . . . . . . . . . . . . . . 16
         |
83 | | 4lt5 9147 |
. . . . . . . . . . . . . . . . . 18
 |
84 | | 4re 9049 |
. . . . . . . . . . . . . . . . . . 19
 |
85 | | 5re 9051 |
. . . . . . . . . . . . . . . . . . . 20
 |
86 | 85 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
 
   |
87 | | zre 9311 |
. . . . . . . . . . . . . . . . . . . 20
   |
88 | 87 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
 
   |
89 | | ltleletr 8091 |
. . . . . . . . . . . . . . . . . . 19
 
  
    |
90 | 84, 86, 88, 89 | mp3an2i 1353 |
. . . . . . . . . . . . . . . . . 18
 
       |
91 | 83, 90 | mpani 430 |
. . . . . . . . . . . . . . . . 17
 
 
   |
92 | 91 | 3impia 1202 |
. . . . . . . . . . . . . . . 16
 
   |
93 | 82, 92 | sylbi 121 |
. . . . . . . . . . . . . . 15
    
  |
94 | | divge1 9779 |
. . . . . . . . . . . . . . 15
       |
95 | 80, 81, 93, 94 | mp3an2i 1353 |
. . . . . . . . . . . . . 14
    
    |
96 | | 1zzd 9334 |
. . . . . . . . . . . . . . 15
    
  |
97 | | flqge 10341 |
. . . . . . . . . . . . . . 15
   
   
         |
98 | 77, 96, 97 | syl2anc 411 |
. . . . . . . . . . . . . 14
    
  
         |
99 | 95, 98 | mpbid 147 |
. . . . . . . . . . . . 13
    
        |
100 | | elnnz1 9330 |
. . . . . . . . . . . . 13
      
                |
101 | 78, 99, 100 | sylanbrc 417 |
. . . . . . . . . . . 12
    
        |
102 | 101 | adantl 277 |
. . . . . . . . . . 11
              
    |
103 | | oddprm 12384 |
. . . . . . . . . . . 12
           |
104 | 103 | adantr 276 |
. . . . . . . . . . 11
                 |
105 | | eldifi 3281 |
. . . . . . . . . . . . . 14
    
  |
106 | | prmuz2 12256 |
. . . . . . . . . . . . . 14

      |
107 | 105, 106 | syl 14 |
. . . . . . . . . . . . 13
    
      |
108 | 107 | adantr 276 |
. . . . . . . . . . . 12
                 |
109 | | fldiv4lem1div2uz2 10365 |
. . . . . . . . . . . 12
    
            |
110 | 108, 109 | syl 14 |
. . . . . . . . . . 11
              
        |
111 | 102, 104,
110 | 3jca 1179 |
. . . . . . . . . 10
                                   |
112 | 111 | ex 115 |
. . . . . . . . 9
              
                    |
113 | 1, 112 | syl 14 |
. . . . . . . 8
          
                    |
114 | 113 | impcom 125 |
. . . . . . 7
                               |
115 | 2 | oveq2i 5921 |
. . . . . . . . 9
             |
116 | 5, 115 | eleq12i 2261 |
. . . . . . . 8
    
                |
117 | | elfz1b 10146 |
. . . . . . . 8
              
                        |
118 | 116, 117 | bitri 184 |
. . . . . . 7
    
                        |
119 | 114, 118 | sylibr 134 |
. . . . . 6
             |
120 | | fzsplit 10107 |
. . . . . 6
                       |
121 | 119, 120 | syl 14 |
. . . . 5
                         |
122 | 34 | adantl 277 |
. . . . 5
             |
123 | 61 | adantll 476 |
. . . . 5
                   |
124 | 74, 121, 122, 123 | fprodsplit 11727 |
. . . 4
                                           |
125 | 124 | ancoms 268 |
. . 3
 
    
           
                        |
126 | | 2re 9042 |
. . . . . . 7
 |
127 | 126 | a1i 9 |
. . . . . 6
   |
128 | | oddprmgt2 12259 |
. . . . . . 7
    
  |
129 | 1, 128 | syl 14 |
. . . . . 6
   |
130 | 127, 129 | gtned 8122 |
. . . . 5
   |
131 | 130 | neneqd 2385 |
. . . 4
   |
132 | | prm23ge5 12389 |
. . . . . . 7

        |
133 | 45, 132 | syl 14 |
. . . . . 6
         |
134 | | 3orass 983 |
. . . . . 6
      
 
        |
135 | 133, 134 | sylib 122 |
. . . . 5
           |
136 | 135 | ord 725 |
. . . 4
 
         |
137 | 131, 136 | mpd 13 |
. . 3
         |
138 | 68, 125, 137 | mpjaodan 799 |
. 2
                                     |
139 | 4, 138 | eqtrd 2226 |
1
                               |