Step | Hyp | Ref
| Expression |
1 | | lmrel 17248 |
. 2
      |
2 | | fvex 5701 |
. . . . . . . 8
             |
3 | | rrncms.7 |
. . . . . . . 8
               |
4 | 2, 3 | fnmpti 5532 |
. . . . . . 7
 |
5 | 4 | a1i 11 |
. . . . . 6
   |
6 | | nnuz 10477 |
. . . . . . . 8
     |
7 | | 1z 10267 |
. . . . . . . . 9
 |
8 | 7 | a1i 11 |
. . . . . . . 8
 
   |
9 | | fveq2 5687 |
. . . . . . . . . . . . . . . 16
           |
10 | 9 | fveq1d 5689 |
. . . . . . . . . . . . . . 15
                   |
11 | | eqid 2404 |
. . . . . . . . . . . . . . 15
                     |
12 | | fvex 5701 |
. . . . . . . . . . . . . . 15
         |
13 | 10, 11, 12 | fvmpt 5765 |
. . . . . . . . . . . . . 14
                         |
14 | 13 | adantl 453 |
. . . . . . . . . . . . 13
                             |
15 | | rrncms.6 |
. . . . . . . . . . . . . . . . . 18
       |
16 | 15 | ffvelrnda 5829 |
. . . . . . . . . . . . . . . . 17
 

      |
17 | | rrnval.1 |
. . . . . . . . . . . . . . . . 17
   |
18 | 16, 17 | syl6eleq 2494 |
. . . . . . . . . . . . . . . 16
 

        |
19 | | elmapi 6997 |
. . . . . . . . . . . . . . . 16
                 |
20 | 18, 19 | syl 16 |
. . . . . . . . . . . . . . 15
 

          |
21 | 20 | ffvelrnda 5829 |
. . . . . . . . . . . . . 14
               |
22 | 21 | an32s 780 |
. . . . . . . . . . . . 13
               |
23 | 14, 22 | eqeltrd 2478 |
. . . . . . . . . . . 12
                     |
24 | 23 | recnd 9070 |
. . . . . . . . . . 11
                     |
25 | | rrncms.5 |
. . . . . . . . . . . . . 14
           |
26 | | rrncms.4 |
. . . . . . . . . . . . . . . . 17
   |
27 | 17 | rrnmet 26428 |
. . . . . . . . . . . . . . . . 17
           |
28 | 26, 27 | syl 16 |
. . . . . . . . . . . . . . . 16
           |
29 | | metxmet 18317 |
. . . . . . . . . . . . . . . 16
        
           |
30 | 28, 29 | syl 16 |
. . . . . . . . . . . . . . 15
            |
31 | 7 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
32 | | eqidd 2405 |
. . . . . . . . . . . . . . 15
 

          |
33 | | eqidd 2405 |
. . . . . . . . . . . . . . 15
 

          |
34 | 6, 30, 31, 32, 33, 15 | iscauf 19186 |
. . . . . . . . . . . . . 14
          
                          |
35 | 25, 34 | mpbid 202 |
. . . . . . . . . . . . 13
   
                       |
36 | 35 | adantr 452 |
. . . . . . . . . . . 12
 
                           |
37 | 26 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . 20
   

        |
38 | | simpllr 736 |
. . . . . . . . . . . . . . . . . . . 20
   

        |
39 | 15 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . . 21
   

            |
40 | 6 | uztrn2 10459 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
41 | 40 | adantll 695 |
. . . . . . . . . . . . . . . . . . . . 21
   

        |
42 | 39, 41 | ffvelrnd 5830 |
. . . . . . . . . . . . . . . . . . . 20
   

            |
43 | | simplr 732 |
. . . . . . . . . . . . . . . . . . . . 21
   

        |
44 | 39, 43 | ffvelrnd 5830 |
. . . . . . . . . . . . . . . . . . . 20
   

            |
45 | | rrndstprj1.1 |
. . . . . . . . . . . . . . . . . . . . 21
 
    |
46 | 17, 45 | rrndstprj1 26429 |
. . . . . . . . . . . . . . . . . . . 20
                                  
                  |
47 | 37, 38, 42, 44, 46 | syl22anc 1185 |
. . . . . . . . . . . . . . . . . . 19
   

                                            |
48 | 28 | ad3antrrr 711 |
. . . . . . . . . . . . . . . . . . . 20
   

                |
49 | | metsym 18333 |
. . . . . . . . . . . . . . . . . . . 20
             
                                       |
50 | 48, 42, 44, 49 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . 19
   

                                        |
51 | 47, 50 | breqtrd 4196 |
. . . . . . . . . . . . . . . . . 18
   

                                            |
52 | 51 | adantllr 700 |
. . . . . . . . . . . . . . . . 17
                                                   |
53 | 45 | remet 18774 |
. . . . . . . . . . . . . . . . . . . . 21
     |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   

            |
55 | | simpll 731 |
. . . . . . . . . . . . . . . . . . . . 21
   

      
   |
56 | 55, 41, 22 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . 20
   

                |
57 | 15 | ffvelrnda 5829 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

      |
58 | 57, 17 | syl6eleq 2494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

        |
59 | | elmapi 6997 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
60 | 58, 59 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

          |
61 | 60 | ffvelrnda 5829 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
62 | 61 | an32s 780 |
. . . . . . . . . . . . . . . . . . . . 21
               |
63 | 62 | adantr 452 |
. . . . . . . . . . . . . . . . . . . 20
   

                |
64 | | metcl 18315 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
65 | 54, 56, 63, 64 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . 19
   

                            |
66 | 65 | adantllr 700 |
. . . . . . . . . . . . . . . . . 18
                                   |
67 | | metcl 18315 |
. . . . . . . . . . . . . . . . . . . 20
             
                       |
68 | 48, 44, 42, 67 | syl3anc 1184 |
. . . . . . . . . . . . . . . . . . 19
   

                        |
69 | 68 | adantllr 700 |
. . . . . . . . . . . . . . . . . 18
                               |
70 | | rpre 10574 |
. . . . . . . . . . . . . . . . . . . 20

  |
71 | 70 | adantl 453 |
. . . . . . . . . . . . . . . . . . 19
       |
72 | 71 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . 18
               |
73 | | lelttr 9121 |
. . . . . . . . . . . . . . . . . 18
                                     
                                                                               |
74 | 66, 69, 72, 73 | syl3anc 1184 |
. . . . . . . . . . . . . . . . 17
                                                                                       
   |
75 | 52, 74 | mpand 657 |
. . . . . . . . . . . . . . . 16
                             
                       |
76 | 75 | ralimdva 2744 |
. . . . . . . . . . . . . . 15
   


                        
                            |
77 | 76 | reximdva 2778 |
. . . . . . . . . . . . . 14
      
                     
                          
   |
78 | 77 | ralimdva 2744 |
. . . . . . . . . . . . 13
 
  
                       
                          
   |
79 | 45 | remetdval 18773 |
. . . . . . . . . . . . . . . . . . 19
                                                               |
80 | 56, 63, 79 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
   

                                                  |
81 | 41, 13 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
   

                              |
82 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
83 | 82 | fveq1d 5689 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
84 | | fvex 5701 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
85 | 83, 11, 84 | fvmpt 5765 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
86 | 85 | ad2antlr 708 |
. . . . . . . . . . . . . . . . . . . 20
   

                              |
87 | 81, 86 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . . 19
   

                                                        |
88 | 87 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . 18
   

                                                                |
89 | 80, 88 | eqtr4d 2439 |
. . . . . . . . . . . . . . . . 17
   

                                                              |
90 | 89 | breq1d 4182 |
. . . . . . . . . . . . . . . 16
   

                                                                |
91 | 90 | ralbidva 2682 |
. . . . . . . . . . . . . . 15
      
                        
                                           |
92 | 91 | rexbidva 2683 |
. . . . . . . . . . . . . 14
 
  
                                                                      |
93 | 92 | ralbidv 2686 |
. . . . . . . . . . . . 13
 
  
                          
                                             |
94 | 78, 93 | sylibd 206 |
. . . . . . . . . . . 12
 
  
                       
                                            |
95 | 36, 94 | mpd 15 |
. . . . . . . . . . 11
 
                                             |
96 | | nnex 9962 |
. . . . . . . . . . . . 13
 |
97 | 96 | mptex 5925 |
. . . . . . . . . . . 12
           |
98 | 97 | a1i 11 |
. . . . . . . . . . 11
 
             |
99 | 6, 24, 95, 98 | caucvg 12427 |
. . . . . . . . . 10
 
            |
100 | | climdm 12303 |
. . . . . . . . . 10
          
                        |
101 | 99, 100 | sylib 189 |
. . . . . . . . 9
 
                         |
102 | | fveq2 5687 |
. . . . . . . . . . . . 13
                   |
103 | 102 | mpteq2dv 4256 |
. . . . . . . . . . . 12
                       |
104 | 103 | fveq2d 5691 |
. . . . . . . . . . 11
                           |
105 | | fvex 5701 |
. . . . . . . . . . 11
             |
106 | 104, 3, 105 | fvmpt 5765 |
. . . . . . . . . 10
    
              |
107 | 106 | adantl 453 |
. . . . . . . . 9
 
    
              |
108 | 101, 107 | breqtrrd 4198 |
. . . . . . . 8
 
                 |
109 | 6, 8, 108, 23 | climrecl 12332 |
. . . . . . 7
 
       |
110 | 109 | ralrimiva 2749 |
. . . . . 6
        |
111 | | ffnfv 5853 |
. . . . . 6
    


       |
112 | 5, 110, 111 | sylanbrc 646 |
. . . . 5
       |
113 | | reex 9037 |
. . . . . 6
 |
114 | | elmapg 6990 |
. . . . . 6
 
           |
115 | 113, 26, 114 | sylancr 645 |
. . . . 5
           |
116 | 112, 115 | mpbird 224 |
. . . 4
     |
117 | 116, 17 | syl6eleqr 2495 |
. . 3
   |
118 | | 1nn 9967 |
. . . . . . 7
 |
119 | 26 | ad2antrr 707 |
. . . . . . . . . . . 12
     
   |
120 | 16 | adantlr 696 |
. . . . . . . . . . . 12
     
       |
121 | 117 | ad2antrr 707 |
. . . . . . . . . . . 12
     
   |
122 | 17 | rrnmval 26427 |
. . . . . . . . . . . 12
                      
                     |
123 | 119, 120,
121, 122 | syl3anc 1184 |
. . . . . . . . . . 11
     
                                      |
124 | | simplrr 738 |
. . . . . . . . . . . . . 14
     
   |
125 | 124 | sumeq1d 12450 |
. . . . . . . . . . . . 13
     
                                         |
126 | | sum0 12470 |
. . . . . . . . . . . . 13
                    |
127 | 125, 126 | syl6eq 2452 |
. . . . . . . . . . . 12
     
                      |
128 | 127 | fveq2d 5691 |
. . . . . . . . . . 11
     
    
                         |
129 | 123, 128 | eqtrd 2436 |
. . . . . . . . . 10
     
                   |
130 | | sqr0 12002 |
. . . . . . . . . 10
     |
131 | 129, 130 | syl6eq 2452 |
. . . . . . . . 9
     
               |
132 | | simplrl 737 |
. . . . . . . . . 10
     
   |
133 | 132 | rpgt0d 10607 |
. . . . . . . . 9
     
   |
134 | 131, 133 | eqbrtrd 4192 |
. . . . . . . 8
     
               |
135 | 134 | ralrimiva 2749 |
. . . . . . 7
 
                  |
136 | | fveq2 5687 |
. . . . . . . . . 10
           |
137 | 136, 6 | syl6eqr 2454 |
. . . . . . . . 9
       |
138 | 137 | raleqdv 2870 |
. . . . . . . 8
  
                
                |
139 | 138 | rspcev 3012 |
. . . . . . 7
                
                    |
140 | 118, 135,
139 | sylancr 645 |
. . . . . 6
 
                        |
141 | 140 | expr 599 |
. . . . 5
 


                      |
142 | 7 | a1i 11 |
. . . . . . . . . . 11
     
   |
143 | | simprl 733 |
. . . . . . . . . . . . 13
 
     |
144 | | simprr 734 |
. . . . . . . . . . . . . . . 16
 
     |
145 | 26 | adantr 452 |
. . . . . . . . . . . . . . . . 17
 
     |
146 | | hashnncl 11600 |
. . . . . . . . . . . . . . . . 17
     
   |
147 | 145, 146 | syl 16 |
. . . . . . . . . . . . . . . 16
 
       
   |
148 | 144, 147 | mpbird 224 |
. . . . . . . . . . . . . . 15
 
         |
149 | 148 | nnrpd 10603 |
. . . . . . . . . . . . . 14
 
         |
150 | 149 | rpsqrcld 12169 |
. . . . . . . . . . . . 13
 
             |
151 | 143, 150 | rpdivcld 10621 |
. . . . . . . . . . . 12
 
               |
152 | 151 | adantr 452 |
. . . . . . . . . . 11
     
             |
153 | 13 | adantl 453 |
. . . . . . . . . . 11
    
 

                         |
154 | 108 | adantlr 696 |
. . . . . . . . . . 11
     
                 |
155 | 6, 142, 152, 153, 154 | climi2 12260 |
. . . . . . . . . 10
     
                                      |
156 | 6 | rexuz3 12107 |
. . . . . . . . . . . 12
  
                               
                                    |
157 | 7, 156 | ax-mp 8 |
. . . . . . . . . . 11
  
                              
                                   |
158 | 22 | adantllr 700 |
. . . . . . . . . . . . . . . . 17
    
 

           |
159 | 109 | adantlr 696 |
. . . . . . . . . . . . . . . . . 18
     
       |
160 | 159 | adantr 452 |
. . . . . . . . . . . . . . . . 17
    
 

       |
161 | 45 | remetdval 18773 |
. . . . . . . . . . . . . . . . 17
                                                   |
162 | 158, 160,
161 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
    
 

                                     |
163 | 162 | breq1d 4182 |
. . . . . . . . . . . . . . 15
    
 

                           
                               |
164 | 40, 163 | sylan2 461 |
. . . . . . . . . . . . . 14
    
 
                                  
                               |
165 | 164 | anassrs 630 |
. . . . . . . . . . . . 13
        

    
                                                          |
166 | 165 | ralbidva 2682 |
. . . . . . . . . . . 12
    
 

                                                                       |
167 | 166 | rexbidva 2683 |
. . . . . . . . . . 11
     
                                                                         |
168 | 157, 167 | syl5bbr 251 |
. . . . . . . . . 10
     
                                                                         |
169 | 155, 168 | mpbird 224 |
. . . . . . . . 9
     
                                    |
170 | 169 | ralrimiva 2749 |
. . . . . . . 8
 
   
                                   |
171 | 6 | rexuz3 12107 |
. . . . . . . . . 10
  
      
                         
       
                             |
172 | 7, 171 | ax-mp 8 |
. . . . . . . . 9
  
     
                         
       
                            |
173 | | rexfiuz 12106 |
. . . . . . . . . 10
  
      
                         

                                    |
174 | 145, 173 | syl 16 |
. . . . . . . . 9
 
    
      
                         

                                    |
175 | 172, 174 | syl5bb 249 |
. . . . . . . 8
 
    
      
                         

                                    |
176 | 170, 175 | mpbird 224 |
. . . . . . 7
 
          
                            |
177 | 26 | ad2antrr 707 |
. . . . . . . . . . . . . 14
     
   |
178 | | simplrr 738 |
. . . . . . . . . . . . . 14
     
   |
179 | | eldifsn 3887 |
. . . . . . . . . . . . . 14
    
    |
180 | 177, 178,
179 | sylanbrc 646 |
. . . . . . . . . . . . 13
     
       |
181 | 15 | adantr 452 |
. . . . . . . . . . . . . 14
 
         |
182 | 181 | ffvelrnda 5829 |
. . . . . . . . . . . . 13
     
       |
183 | 117 | ad2antrr 707 |
. . . . . . . . . . . . 13
     
   |
184 | 151 | adantr 452 |
. . . . . . . . . . . . 13
     
             |
185 | 17, 45 | rrndstprj2 26430 |
. . . . . . . . . . . . . 14
                                                   
                                  |
186 | 185 | expr 599 |
. . . . . . . . . . . . 13
                      
 
                         
                                   |
187 | 180, 182,
183, 184, 186 | syl31anc 1187 |
. . . . . . . . . . . 12
     
                                                                |
188 | | simplrl 737 |
. . . . . . . . . . . . . . 15
     
   |
189 | 188 | rpcnd 10606 |
. . . . . . . . . . . . . 14
     
   |
190 | 150 | adantr 452 |
. . . . . . . . . . . . . . 15
     
           |
191 | 190 | rpcnd 10606 |
. . . . . . . . . . . . . 14
     
           |
192 | 190 | rpne0d 10609 |
. . . . . . . . . . . . . 14
     
           |
193 | 189, 191,
192 | divcan1d 9747 |
. . . . . . . . . . . . 13
     
                       |
194 | 193 | breq2d 4184 |
. . . . . . . . . . . 12
     
                                                 |
195 | 187, 194 | sylibd 206 |
. . . . . . . . . . 11
     
                                            |
196 | 40, 195 | sylan2 461 |
. . . . . . . . . 10
              
                                         |
197 | 196 | anassrs 630 |
. . . . . . . . 9
    
 

      
                                         |
198 | 197 | ralimdva 2744 |
. . . . . . . 8
     
        
                         
                     |
199 | 198 | reximdva 2778 |
. . . . . . 7
 
    
      
                          
                     |
200 | 176, 199 | mpd 15 |
. . . . . 6
 
                        |
201 | 200 | expr 599 |
. . . . 5
 


                      |
202 | 141, 201 | pm2.61dne 2644 |
. . . 4
 

                     |
203 | 202 | ralrimiva 2749 |
. . 3
   
                   |
204 | | rrncms.3 |
. . . 4
         |
205 | 204, 30, 6, 31, 32, 15 | lmmbrf 19168 |
. . 3
        

                        |
206 | 117, 203,
205 | mpbir2and 889 |
. 2
          |
207 | | releldm 5061 |
. 2
              
       |
208 | 1, 206, 207 | sylancr 645 |
1
        |