Proof of Theorem geolimilem
| Step | Hyp | Ref
| Expression |
| 1 | | ax1cn 6422 |
. . . . . . . . . . 11
 |
| 2 | | geoser.2 |
. . . . . . . . . . 11
 |
| 3 | 1, 2 | subcli 6523 |
. . . . . . . . . 10
   |
| 4 | | 1re 6598 |
. . . . . . . . . . 11
 |
| 5 | | geolimilem.3 |
. . . . . . . . . . 11
     |
| 6 | | abssubne0 8134 |
. . . . . . . . . . 11
           |
| 7 | 2, 4, 5, 6 | mp3an 1191 |
. . . . . . . . . 10
   |
| 8 | 3, 7 | reccli 6902 |
. . . . . . . . 9
     |
| 9 | 8 | negcli 6526 |
. . . . . . . 8
      |
| 10 | 9, 2 | mulcli 6474 |
. . . . . . 7
      
 |
| 11 | | nnnn0 7315 |
. . . . . . . . . 10

  |
| 12 | | opreq2 4890 |
. . . . . . . . . . 11
           |
| 13 | | geoser.1 |
. . . . . . . . . . 11
            |
| 14 | | oprex 4907 |
. . . . . . . . . . 11
     |
| 15 | 12, 13, 14 | fvopab4 4743 |
. . . . . . . . . 10

          |
| 16 | 11, 15 | syl 12 |
. . . . . . . . 9

          |
| 17 | 16 | rgen 2159 |
. . . . . . . 8

         |
| 18 | | nn0ex 7314 |
. . . . . . . . . 10
 |
| 19 | 18, 13 | fopabex2 4541 |
. . . . . . . . 9
 |
| 20 | 19 | expcnv 8494 |
. . . . . . . 8
                  |
| 21 | 2, 17, 5, 20 | mp3an 1191 |
. . . . . . 7
 |
| 22 | 10, 21 | pm3.2i 307 |
. . . . . 6
          |
| 23 | | 0z 7355 |
. . . . . . 7
 |
| 24 | | elnn0uz 7610 |
. . . . . . . . 9

      |
| 25 | | expcl 7824 |
. . . . . . . . . . . . 13
  
      |
| 26 | 2, 25 | mpan 759 |
. . . . . . . . . . . 12
       |
| 27 | 13, 26 | fopab 4800 |
. . . . . . . . . . 11
     |
| 28 | 27 | ffvelrni 4788 |
. . . . . . . . . 10

   
  |
| 29 | | geolimilem.5 |
. . . . . . . . . . 11

                 |
| 30 | 2 | negcli 6526 |
. . . . . . . . . . . . . 14
  |
| 31 | 3, 7 | pm3.2i 307 |
. . . . . . . . . . . . . 14
  
 
  |
| 32 | | div23 6925 |
. . . . . . . . . . . . . 14
                
                     |
| 33 | 30, 31, 32 | mp3an13 1182 |
. . . . . . . . . . . . 13
    
                        |
| 34 | 28, 33 | syl 12 |
. . . . . . . . . . . 12

                        |
| 35 | | mulneg1 6615 |
. . . . . . . . . . . . . 14
        
              |
| 36 | 35, 2, 28 | sylancr 526 |
. . . . . . . . . . . . 13

        
       |
| 37 | 36 | opreq1d 4897 |
. . . . . . . . . . . 12

                        |
| 38 | | mulneg12 6617 |
. . . . . . . . . . . . . . . . 17
                       |
| 39 | 8, 2, 38 | mp2an 761 |
. . . . . . . . . . . . . . . 16
               |
| 40 | | divrec2 6923 |
. . . . . . . . . . . . . . . . 17
         
            |
| 41 | 30, 3, 7, 40 | mp3an 1191 |
. . . . . . . . . . . . . . . 16
 
           |
| 42 | 39, 41 | eqtr4i 1911 |
. . . . . . . . . . . . . . 15
        
    |
| 43 | 42 | opreq1i 4892 |
. . . . . . . . . . . . . 14
               
         |
| 44 | 43 | eqcomi 1888 |
. . . . . . . . . . . . 13
                  
      |
| 45 | 44 | a1i 8 |
. . . . . . . . . . . 12

                          |
| 46 | 34, 37, 45 | 3eqtr3d 1934 |
. . . . . . . . . . 11

                  
       |
| 47 | 29, 46 | eqtrd 1925 |
. . . . . . . . . 10

           
       |
| 48 | 28, 47 | jca 310 |
. . . . . . . . 9

                         |
| 49 | 24, 48 | sylbir 218 |
. . . . . . . 8

        
           
        |
| 50 | 49 | rgen 2159 |
. . . . . . 7
                              |
| 51 | 23, 50 | pm3.2i 307 |
. . . . . 6
                                |
| 52 | | geolimilem.4 |
. . . . . . . 8
 |
| 53 | | fnex 4535 |
. . . . . . . 8
     |
| 54 | 52, 18, 53 | mp2an 761 |
. . . . . . 7
 |
| 55 | 23 | elisseti 2301 |
. . . . . . 7
 |
| 56 | 19, 54, 55 | climmulc2 8389 |
. . . . . 6
                                                  
   |
| 57 | 22, 51, 56 | mp2an 761 |
. . . . 5
          |
| 58 | 10 | mul01i 6594 |
. . . . 5
          |
| 59 | 57, 58 | breqtri 3360 |
. . . 4
 |
| 60 | 59, 8 | pm3.2i 307 |
. . 3

      |
| 61 | | mulcl 6456 |
. . . . . . . . . . 11
               |
| 62 | 61, 2, 28 | sylancr 526 |
. . . . . . . . . 10

        |
| 63 | | negcl 6525 |
. . . . . . . . . 10
                |
| 64 | 62, 63 | syl 12 |
. . . . . . . . 9

         |
| 65 | | divcl 6901 |
. . . . . . . . . 10
                           |
| 66 | 3, 7, 65 | mp3an23 1183 |
. . . . . . . . 9
          
          |
| 67 | 64, 66 | syl 12 |
. . . . . . . 8

             |
| 68 | 29, 67 | eqeltrd 1971 |
. . . . . . 7

   
  |
| 69 | | mulcom 6459 |
. . . . . . . . . . . . . 14
                     |
| 70 | | expcl 7824 |
. . . . . . . . . . . . . . 15
  
      |
| 71 | 2, 70 | mpan 759 |
. . . . . . . . . . . . . 14

   
  |
| 72 | 69, 2, 71 | sylancr 526 |
. . . . . . . . . . . . 13

              |
| 73 | 15 | opreq2d 4898 |
. . . . . . . . . . . . 13

              |
| 74 | | expp1 7817 |
. . . . . . . . . . . . . 14
  
              |
| 75 | 2, 74 | mpan 759 |
. . . . . . . . . . . . 13

              |
| 76 | 72, 73, 75 | 3eqtr4rd 1939 |
. . . . . . . . . . . 12

              |
| 77 | 76 | opreq2d 4898 |
. . . . . . . . . . 11

                  |
| 78 | | negsub 6540 |
. . . . . . . . . . . 12
                            |
| 79 | 78, 1, 62 | sylancr 526 |
. . . . . . . . . . 11

                   |
| 80 | 77, 79 | eqtr4d 1928 |
. . . . . . . . . 10

                   |
| 81 | 80 | opreq1d 4897 |
. . . . . . . . 9

               
           |
| 82 | | divdir 6933 |
. . . . . . . . . . 11
                                                |
| 83 | 1, 31, 82 | mp3an13 1182 |
. . . . . . . . . 10
                                        |
| 84 | 64, 83 | syl 12 |
. . . . . . . . 9

                                |
| 85 | 81, 84 | eqtrd 1925 |
. . . . . . . 8

                   
           |
| 86 | 1, 2 | subeq0i 6565 |
. . . . . . . . . . . 12
     |
| 87 | 86 | necon3bii 2032 |
. . . . . . . . . . 11
  
  |
| 88 | 7, 87 | mpbi 206 |
. . . . . . . . . 10
 |
| 89 | | necom 2094 |
. . . . . . . . . 10
   |
| 90 | 88, 89 | mpbi 206 |
. . . . . . . . 9
 |
| 91 | 13, 2 | geoseri 8496 |
. . . . . . . . 9
 
                    |
| 92 | 90, 91 | mpan2 760 |
. . . . . . . 8

                   |
| 93 | 29 | opreq2d 4898 |
. . . . . . . 8

                 
           |
| 94 | 85, 92, 93 | 3eqtr4d 1937 |
. . . . . . 7

                 |
| 95 | 68, 94 | jca 310 |
. . . . . 6

                       |
| 96 | 24, 95 | sylbir 218 |
. . . . 5

        
                  |
| 97 | 96 | rgen 2159 |
. . . 4
                            |
| 98 | 23, 97 | pm3.2i 307 |
. . 3
                              |
| 99 | | oprex 4907 |
. . . 4
  |
| 100 | | oprex 4907 |
. . . 4
     |
| 101 | 54, 99, 55, 100 | climaddc2 8379 |
. . 3
                                               |
| 102 | 60, 98, 101 | mp2an 761 |
. 2
        |
| 103 | 8 | addid1i 6483 |
. 2
           |
| 104 | 102, 103 | breqtri 3360 |
1
      |