Step | Hyp | Ref
| Expression |
1 | | bposlem2.1 |
. . 3
   |
2 | | bposlem2.2 |
. . 3
   |
3 | | pcbcctr 24197 |
. . 3
 
                                           |
4 | 1, 2, 3 | syl2anc 666 |
. 2
                                           |
5 | | elfznn 11825 |
. . . . . 6
         |
6 | | elnn1uz2 11232 |
. . . . . 6

        |
7 | 5, 6 | sylib 200 |
. . . . 5
               |
8 | | oveq2 6296 |
. . . . . . . . . . . 12
           |
9 | | prmnn 14618 |
. . . . . . . . . . . . . . 15

  |
10 | 2, 9 | syl 17 |
. . . . . . . . . . . . . 14
   |
11 | 10 | nncnd 10622 |
. . . . . . . . . . . . 13
   |
12 | 11 | exp1d 12408 |
. . . . . . . . . . . 12
       |
13 | 8, 12 | sylan9eqr 2506 |
. . . . . . . . . . 11
 
       |
14 | 13 | oveq2d 6304 |
. . . . . . . . . 10
 
               |
15 | 14 | fveq2d 5867 |
. . . . . . . . 9
 
                       |
16 | | 2t1e2 10755 |
. . . . . . . . . . . . 13
   |
17 | 11 | mulid2d 9658 |
. . . . . . . . . . . . . . . 16
     |
18 | | bposlem2.5 |
. . . . . . . . . . . . . . . 16

  |
19 | 17, 18 | eqbrtrd 4422 |
. . . . . . . . . . . . . . 15
  
  |
20 | | 1red 9655 |
. . . . . . . . . . . . . . . 16
   |
21 | 1 | nnred 10621 |
. . . . . . . . . . . . . . . 16
   |
22 | 10 | nnred 10621 |
. . . . . . . . . . . . . . . 16
   |
23 | 10 | nngt0d 10650 |
. . . . . . . . . . . . . . . 16
   |
24 | | lemuldiv 10483 |
. . . . . . . . . . . . . . . 16
 

          |
25 | 20, 21, 22, 23, 24 | syl112anc 1271 |
. . . . . . . . . . . . . . 15
         |
26 | 19, 25 | mpbid 214 |
. . . . . . . . . . . . . 14

    |
27 | 21, 10 | nndivred 10655 |
. . . . . . . . . . . . . . 15
     |
28 | | 1re 9639 |
. . . . . . . . . . . . . . . 16
 |
29 | | 2re 10676 |
. . . . . . . . . . . . . . . . 17
 |
30 | | 2pos 10698 |
. . . . . . . . . . . . . . . . 17
 |
31 | 29, 30 | pm3.2i 457 |
. . . . . . . . . . . . . . . 16
   |
32 | | lemul2 10455 |
. . . . . . . . . . . . . . . 16
  
   
  
         |
33 | 28, 31, 32 | mp3an13 1354 |
. . . . . . . . . . . . . . 15
   
 
         |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . 14
   
         |
35 | 26, 34 | mpbid 214 |
. . . . . . . . . . . . 13
  
      |
36 | 16, 35 | syl5eqbrr 4436 |
. . . . . . . . . . . 12

      |
37 | | 2cnd 10679 |
. . . . . . . . . . . . 13
   |
38 | 1 | nncnd 10622 |
. . . . . . . . . . . . 13
   |
39 | 10 | nnne0d 10651 |
. . . . . . . . . . . . 13
   |
40 | 37, 38, 11, 39 | divassd 10415 |
. . . . . . . . . . . 12
           |
41 | 36, 40 | breqtrrd 4428 |
. . . . . . . . . . 11

      |
42 | | bposlem2.4 |
. . . . . . . . . . . . 13
    
  |
43 | | 2nn 10764 |
. . . . . . . . . . . . . . . 16
 |
44 | | nnmulcl 10629 |
. . . . . . . . . . . . . . . 16
 
     |
45 | 43, 1, 44 | sylancr 668 |
. . . . . . . . . . . . . . 15
     |
46 | 45 | nnred 10621 |
. . . . . . . . . . . . . 14
     |
47 | | 3re 10680 |
. . . . . . . . . . . . . . . 16
 |
48 | | 3pos 10700 |
. . . . . . . . . . . . . . . 16
 |
49 | 47, 48 | pm3.2i 457 |
. . . . . . . . . . . . . . 15
   |
50 | | ltdiv23 10494 |
. . . . . . . . . . . . . . 15
                     |
51 | 49, 50 | mp3an2 1351 |
. . . . . . . . . . . . . 14
    
 
    
       |
52 | 46, 22, 23, 51 | syl12anc 1265 |
. . . . . . . . . . . . 13
             |
53 | 42, 52 | mpbid 214 |
. . . . . . . . . . . 12
    
  |
54 | | df-3 10666 |
. . . . . . . . . . . 12
   |
55 | 53, 54 | syl6breq 4441 |
. . . . . . . . . . 11
    
    |
56 | 46, 10 | nndivred 10655 |
. . . . . . . . . . . 12
       |
57 | | 2z 10966 |
. . . . . . . . . . . 12
 |
58 | | flbi 12048 |
. . . . . . . . . . . 12
     
                         |
59 | 56, 57, 58 | sylancl 667 |
. . . . . . . . . . 11
                         |
60 | 41, 55, 59 | mpbir2and 932 |
. . . . . . . . . 10
           |
61 | 60 | adantr 467 |
. . . . . . . . 9
 
           |
62 | 15, 61 | eqtrd 2484 |
. . . . . . . 8
 
               |
63 | 13 | oveq2d 6304 |
. . . . . . . . . . . 12
 
           |
64 | 63 | fveq2d 5867 |
. . . . . . . . . . 11
 
                   |
65 | | remulcl 9621 |
. . . . . . . . . . . . . . . . . 18
  
        |
66 | 29, 27, 65 | sylancr 668 |
. . . . . . . . . . . . . . . . 17
       |
67 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
68 | | 4re 10683 |
. . . . . . . . . . . . . . . . . 18
 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
70 | 40, 53 | eqbrtrrd 4424 |
. . . . . . . . . . . . . . . . 17
       |
71 | | 3lt4 10776 |
. . . . . . . . . . . . . . . . . 18
 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
73 | 66, 67, 69, 70, 72 | lttrd 9793 |
. . . . . . . . . . . . . . . 16
       |
74 | | 2t2e4 10756 |
. . . . . . . . . . . . . . . 16
   |
75 | 73, 74 | syl6breqr 4442 |
. . . . . . . . . . . . . . 15
         |
76 | | ltmul2 10453 |
. . . . . . . . . . . . . . . . 17
   
               |
77 | 29, 31, 76 | mp3an23 1355 |
. . . . . . . . . . . . . . . 16
     
         |
78 | 27, 77 | syl 17 |
. . . . . . . . . . . . . . 15
             |
79 | 75, 78 | mpbird 236 |
. . . . . . . . . . . . . 14
  
  |
80 | | df-2 10665 |
. . . . . . . . . . . . . 14
   |
81 | 79, 80 | syl6breq 4441 |
. . . . . . . . . . . . 13
  
    |
82 | | 1z 10964 |
. . . . . . . . . . . . . 14
 |
83 | | flbi 12048 |
. . . . . . . . . . . . . 14
   
     
     

      |
84 | 27, 82, 83 | sylancl 667 |
. . . . . . . . . . . . 13
     
     

      |
85 | 26, 81, 84 | mpbir2and 932 |
. . . . . . . . . . . 12
         |
86 | 85 | adantr 467 |
. . . . . . . . . . 11
 
         |
87 | 64, 86 | eqtrd 2484 |
. . . . . . . . . 10
 
             |
88 | 87 | oveq2d 6304 |
. . . . . . . . 9
 
                 |
89 | 88, 16 | syl6eq 2500 |
. . . . . . . 8
 
               |
90 | 62, 89 | oveq12d 6306 |
. . . . . . 7
 
                  
            |
91 | | 2cn 10677 |
. . . . . . . 8
 |
92 | 91 | subidi 9942 |
. . . . . . 7
   |
93 | 90, 92 | syl6eq 2500 |
. . . . . 6
 
                  
          |
94 | 45 | nnrpd 11336 |
. . . . . . . . . . . 12
     |
95 | 94 | adantr 467 |
. . . . . . . . . . 11
 
    
    |
96 | | eluzge2nn0 11195 |
. . . . . . . . . . . . 13
    
  |
97 | | nnexpcl 12282 |
. . . . . . . . . . . . 13
 
       |
98 | 10, 96, 97 | syl2an 480 |
. . . . . . . . . . . 12
 
    
      |
99 | 98 | nnrpd 11336 |
. . . . . . . . . . 11
 
    
      |
100 | 95, 99 | rpdivcld 11355 |
. . . . . . . . . 10
 
    
          |
101 | 100 | rpge0d 11342 |
. . . . . . . . 9
 
    
          |
102 | 46 | adantr 467 |
. . . . . . . . . . . . 13
 
    
    |
103 | | remulcl 9621 |
. . . . . . . . . . . . . . 15
 
     |
104 | 47, 22, 103 | sylancr 668 |
. . . . . . . . . . . . . 14
     |
105 | 104 | adantr 467 |
. . . . . . . . . . . . 13
 
    
    |
106 | 98 | nnred 10621 |
. . . . . . . . . . . . 13
 
    
      |
107 | | ltdivmul 10477 |
. . . . . . . . . . . . . . . . 17
   
               |
108 | 49, 107 | mp3an3 1352 |
. . . . . . . . . . . . . . . 16
   
             |
109 | 46, 22, 108 | syl2anc 666 |
. . . . . . . . . . . . . . 15
             |
110 | 42, 109 | mpbid 214 |
. . . . . . . . . . . . . 14
  
    |
111 | 110 | adantr 467 |
. . . . . . . . . . . . 13
 
    
      |
112 | 22, 22 | remulcld 9668 |
. . . . . . . . . . . . . . 15
     |
113 | 112 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
    |
114 | | bposlem2.3 |
. . . . . . . . . . . . . . . . . 18
   |
115 | | nnltp1le 10989 |
. . . . . . . . . . . . . . . . . . 19
 
       |
116 | 43, 10, 115 | sylancr 668 |
. . . . . . . . . . . . . . . . . 18
       |
117 | 114, 116 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
  
  |
118 | 54, 117 | syl5eqbr 4435 |
. . . . . . . . . . . . . . . 16

  |
119 | | lemul1 10454 |
. . . . . . . . . . . . . . . . . 18
 

          |
120 | 47, 119 | mp3an1 1350 |
. . . . . . . . . . . . . . . . 17
  
 

       |
121 | 22, 22, 23, 120 | syl12anc 1265 |
. . . . . . . . . . . . . . . 16
         |
122 | 118, 121 | mpbid 214 |
. . . . . . . . . . . . . . 15
  
    |
123 | 122 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
      |
124 | 11 | sqvald 12410 |
. . . . . . . . . . . . . . . 16
         |
125 | 124 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
        |
126 | 22 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
  |
127 | 10 | nnge1d 10649 |
. . . . . . . . . . . . . . . . 17

  |
128 | 127 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
  |
129 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
    
      |
130 | 126, 128,
129 | leexp2ad 12445 |
. . . . . . . . . . . . . . 15
 
    
          |
131 | 125, 130 | eqbrtrrd 4424 |
. . . . . . . . . . . . . 14
 
    
        |
132 | 105, 113,
106, 123, 131 | letrd 9789 |
. . . . . . . . . . . . 13
 
    
        |
133 | 102, 105,
106, 111, 132 | ltletrd 9792 |
. . . . . . . . . . . 12
 
    
        |
134 | 98 | nncnd 10622 |
. . . . . . . . . . . . 13
 
    
      |
135 | 134 | mulid1d 9657 |
. . . . . . . . . . . 12
 
    
            |
136 | 133, 135 | breqtrrd 4428 |
. . . . . . . . . . 11
 
    
          |
137 | | 1red 9655 |
. . . . . . . . . . . 12
 
    
  |
138 | 102, 137,
99 | ltdivmuld 11386 |
. . . . . . . . . . 11
 
    
        
           |
139 | 136, 138 | mpbird 236 |
. . . . . . . . . 10
 
    
          |
140 | | 1e0p1 11076 |
. . . . . . . . . 10
   |
141 | 139, 140 | syl6breq 4441 |
. . . . . . . . 9
 
    
            |
142 | 100 | rpred 11338 |
. . . . . . . . . 10
 
    
          |
143 | | 0z 10945 |
. . . . . . . . . 10
 |
144 | | flbi 12048 |
. . . . . . . . . 10
                        
                      |
145 | 142, 143,
144 | sylancl 667 |
. . . . . . . . 9
 
    
                                    |
146 | 101, 141,
145 | mpbir2and 932 |
. . . . . . . 8
 
    
              |
147 | 1 | nnrpd 11336 |
. . . . . . . . . . . . . 14
   |
148 | 147 | adantr 467 |
. . . . . . . . . . . . 13
 
    
  |
149 | 148, 99 | rpdivcld 11355 |
. . . . . . . . . . . 12
 
    
        |
150 | 149 | rpge0d 11342 |
. . . . . . . . . . 11
 
    
        |
151 | 21 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
  |
152 | 21, 147 | ltaddrpd 11368 |
. . . . . . . . . . . . . . . . 17
     |
153 | 38 | 2timesd 10852 |
. . . . . . . . . . . . . . . . 17
       |
154 | 152, 153 | breqtrrd 4428 |
. . . . . . . . . . . . . . . 16
     |
155 | 154 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
    |
156 | 151, 102,
106, 155, 133 | lttrd 9793 |
. . . . . . . . . . . . . 14
 
    
      |
157 | 156, 135 | breqtrrd 4428 |
. . . . . . . . . . . . 13
 
    
        |
158 | 151, 137,
99 | ltdivmuld 11386 |
. . . . . . . . . . . . 13
 
    
      
         |
159 | 157, 158 | mpbird 236 |
. . . . . . . . . . . 12
 
    
        |
160 | 159, 140 | syl6breq 4441 |
. . . . . . . . . . 11
 
    
          |
161 | 149 | rpred 11338 |
. . . . . . . . . . . 12
 
    
        |
162 | | flbi 12048 |
. . . . . . . . . . . 12
                   
                   |
163 | 161, 143,
162 | sylancl 667 |
. . . . . . . . . . 11
 
    
                              |
164 | 150, 160,
163 | mpbir2and 932 |
. . . . . . . . . 10
 
    
            |
165 | 164 | oveq2d 6304 |
. . . . . . . . 9
 
    
    
           |
166 | | 2t0e0 10762 |
. . . . . . . . 9
   |
167 | 165, 166 | syl6eq 2500 |
. . . . . . . 8
 
    
    
         |
168 | 146, 167 | oveq12d 6306 |
. . . . . . 7
 
    
                              |
169 | | 0m0e0 10716 |
. . . . . . 7
   |
170 | 168, 169 | syl6eq 2500 |
. . . . . 6
 
    
                            |
171 | 93, 170 | jaodan 793 |
. . . . 5
 
                        
          |
172 | 7, 171 | sylan2 477 |
. . . 4
 
                        
          |
173 | 172 | sumeq2dv 13762 |
. . 3
                          
                  |
174 | | fzfid 12183 |
. . . 4
         |
175 | | sumz 13781 |
. . . . 5
       
                     |
176 | 175 | olcs 397 |
. . . 4
                 |
177 | 174, 176 | syl 17 |
. . 3
           |
178 | 173, 177 | eqtrd 2484 |
. 2
                          
          |
179 | 4, 178 | eqtrd 2484 |
1
         |