Step | Hyp | Ref
| Expression |
1 | | 1re 9660 |
. 2
 |
2 | | ax-rnegex 9628 |
. 2
      |
3 | | ax-1ne0 9626 |
. . . . . 6
 |
4 | | oveq2 6316 |
. . . . . . . . . 10
       |
5 | 4 | eqeq1d 2473 |
. . . . . . . . 9
         |
6 | 5 | biimpcd 232 |
. . . . . . . 8
         |
7 | | oveq2 6316 |
. . . . . . . . 9
      

               |
8 | | ax-icn 9616 |
. . . . . . . . . . . . . . 15
 |
9 | 8, 8 | mulcli 9666 |
. . . . . . . . . . . . . 14
   |
10 | 9, 9 | mulcli 9666 |
. . . . . . . . . . . . 13
       |
11 | | ax-1cn 9615 |
. . . . . . . . . . . . 13
 |
12 | | 0cn 9653 |
. . . . . . . . . . . . 13
 |
13 | 10, 11, 12 | adddii 9671 |
. . . . . . . . . . . 12
   
                  
      |
14 | 10 | mulid1i 9663 |
. . . . . . . . . . . . 13
   
      
    |
15 | | mul01 9830 |
. . . . . . . . . . . . . . 15
   
  
   
      |
16 | 10, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
   
     |
17 | | ax-i2m1 9625 |
. . . . . . . . . . . . . 14
     |
18 | 16, 17 | eqtr4i 2496 |
. . . . . . . . . . . . 13
   
      
  |
19 | 14, 18 | oveq12i 6320 |
. . . . . . . . . . . 12
    

               

        |
20 | 13, 19 | eqtri 2493 |
. . . . . . . . . . 11
   
         

        |
21 | 20, 16 | eqeq12i 2485 |
. . . . . . . . . 10
    

                      
    |
22 | 10, 9, 11 | addassi 9669 |
. . . . . . . . . . . 12
    

               
   |
23 | 9 | mulid1i 9663 |
. . . . . . . . . . . . . . 15
       |
24 | 23 | oveq2i 6319 |
. . . . . . . . . . . . . 14
   
     
     

      |
25 | 9, 9, 11 | adddii 9671 |
. . . . . . . . . . . . . . 15
                 
   |
26 | 17 | oveq2i 6319 |
. . . . . . . . . . . . . . . 16
          
  |
27 | | mul01 9830 |
. . . . . . . . . . . . . . . . 17
     
   |
28 | 9, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     |
29 | 26, 28 | eqtri 2493 |
. . . . . . . . . . . . . . 15
         |
30 | 25, 29 | eqtr3i 2495 |
. . . . . . . . . . . . . 14
   
     
   |
31 | 24, 30 | eqtr3i 2495 |
. . . . . . . . . . . . 13
   
       |
32 | 31 | oveq1i 6318 |
. . . . . . . . . . . 12
    

         |
33 | 22, 32 | eqtr3i 2495 |
. . . . . . . . . . 11
   
     
     |
34 | | 00id 9826 |
. . . . . . . . . . . 12
   |
35 | 34 | eqcomi 2480 |
. . . . . . . . . . 11
   |
36 | 33, 35 | eqeq12i 2485 |
. . . . . . . . . 10
    

      
      |
37 | | 0re 9661 |
. . . . . . . . . . 11
 |
38 | | readdcan 9825 |
. . . . . . . . . . 11
 
     
   |
39 | 1, 37, 37, 38 | mp3an 1390 |
. . . . . . . . . 10
    
  |
40 | 21, 36, 39 | 3bitri 279 |
. . . . . . . . 9
    

               |
41 | 7, 40 | sylib 201 |
. . . . . . . 8
     |
42 | 6, 41 | syl6 33 |
. . . . . . 7
       |
43 | 42 | necon3d 2664 |
. . . . . 6
       |
44 | 3, 43 | mpi 20 |
. . . . 5
     |
45 | | ax-rrecex 9629 |
. . . . 5
   
    |
46 | 44, 45 | sylan2 482 |
. . . 4
          |
47 | | simpr 468 |
. . . . . . . . . 10
               |
48 | | simplrl 778 |
. . . . . . . . . . 11
               |
49 | 48 | recnd 9687 |
. . . . . . . . . 10
               |
50 | 47, 49 | mulcld 9681 |
. . . . . . . . 9
             
   |
51 | | simplll 776 |
. . . . . . . . . 10
               |
52 | 51 | recnd 9687 |
. . . . . . . . 9
               |
53 | 12 | a1i 11 |
. . . . . . . . 9
               |
54 | 50, 52, 53 | adddid 9685 |
. . . . . . . 8
                               |
55 | 11 | a1i 11 |
. . . . . . . . . . . . 13
               |
56 | 55, 52, 53 | addassd 9683 |
. . . . . . . . . . . 12
                       |
57 | | simpllr 777 |
. . . . . . . . . . . . 13
                 |
58 | 57 | oveq1d 6323 |
. . . . . . . . . . . 12
                     |
59 | 56, 58 | eqtr3d 2507 |
. . . . . . . . . . 11
                     |
60 | 34, 59, 57 | 3eqtr4a 2531 |
. . . . . . . . . 10
                     |
61 | 37 | a1i 11 |
. . . . . . . . . . . 12
               |
62 | 51, 61 | readdcld 9688 |
. . . . . . . . . . 11
                 |
63 | 1 | a1i 11 |
. . . . . . . . . . 11
               |
64 | | readdcan 9825 |
. . . . . . . . . . 11
   
       
     |
65 | 62, 51, 63, 64 | syl3anc 1292 |
. . . . . . . . . 10
                   
     |
66 | 60, 65 | mpbid 215 |
. . . . . . . . 9
                 |
67 | 66 | oveq2d 6324 |
. . . . . . . 8
                         |
68 | 54, 67 | eqtr3d 2507 |
. . . . . . 7
                             |
69 | | mul31 9819 |
. . . . . . . . . 10
 
           |
70 | 47, 49, 52, 69 | syl3anc 1292 |
. . . . . . . . 9
                       |
71 | | simplrr 779 |
. . . . . . . . . 10
                 |
72 | 71 | oveq1d 6323 |
. . . . . . . . 9
                     |
73 | 47 | mulid2d 9679 |
. . . . . . . . 9
                 |
74 | 70, 72, 73 | 3eqtrd 2509 |
. . . . . . . 8
                   |
75 | | mul01 9830 |
. . . . . . . . 9
         |
76 | 50, 75 | syl 17 |
. . . . . . . 8
                   |
77 | 74, 76 | oveq12d 6326 |
. . . . . . 7
                           |
78 | 68, 77, 74 | 3eqtr3d 2513 |
. . . . . 6
             
   |
79 | 78 | exp42 622 |
. . . . 5
     
   
       |
80 | 79 | rexlimdv 2870 |
. . . 4
         
      |
81 | 46, 80 | mpd 15 |
. . 3
     
     |
82 | 81 | rexlimiva 2868 |
. 2
    
     |
83 | 1, 2, 82 | mp2b 10 |
1
 
   |