Step | Hyp | Ref
| Expression |
1 | | 1re 9639 |
. 2
 |
2 | | ax-rnegex 9607 |
. 2
      |
3 | | ax-1ne0 9605 |
. . . . . 6
 |
4 | | oveq2 6296 |
. . . . . . . . . 10
       |
5 | 4 | eqeq1d 2452 |
. . . . . . . . 9
         |
6 | 5 | biimpcd 228 |
. . . . . . . 8
         |
7 | | oveq2 6296 |
. . . . . . . . 9
      

               |
8 | | ax-icn 9595 |
. . . . . . . . . . . . . . 15
 |
9 | 8, 8 | mulcli 9645 |
. . . . . . . . . . . . . 14
   |
10 | 9, 9 | mulcli 9645 |
. . . . . . . . . . . . 13
       |
11 | | ax-1cn 9594 |
. . . . . . . . . . . . 13
 |
12 | | 0cn 9632 |
. . . . . . . . . . . . 13
 |
13 | 10, 11, 12 | adddii 9650 |
. . . . . . . . . . . 12
   
                  
      |
14 | 10 | mulid1i 9642 |
. . . . . . . . . . . . 13
   
      
    |
15 | | mul01 9809 |
. . . . . . . . . . . . . . 15
   
  
   
      |
16 | 10, 15 | ax-mp 5 |
. . . . . . . . . . . . . 14
   
     |
17 | | ax-i2m1 9604 |
. . . . . . . . . . . . . 14
     |
18 | 16, 17 | eqtr4i 2475 |
. . . . . . . . . . . . 13
   
      
  |
19 | 14, 18 | oveq12i 6300 |
. . . . . . . . . . . 12
    

               

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

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

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

               
   |
23 | 9 | mulid1i 9642 |
. . . . . . . . . . . . . . 15
       |
24 | 23 | oveq2i 6299 |
. . . . . . . . . . . . . 14
   
     
     

      |
25 | 9, 9, 11 | adddii 9650 |
. . . . . . . . . . . . . . 15
                 
   |
26 | 17 | oveq2i 6299 |
. . . . . . . . . . . . . . . 16
          
  |
27 | | mul01 9809 |
. . . . . . . . . . . . . . . . 17
     
   |
28 | 9, 27 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     |
29 | 26, 28 | eqtri 2472 |
. . . . . . . . . . . . . . 15
         |
30 | 25, 29 | eqtr3i 2474 |
. . . . . . . . . . . . . 14
   
     
   |
31 | 24, 30 | eqtr3i 2474 |
. . . . . . . . . . . . 13
   
       |
32 | 31 | oveq1i 6298 |
. . . . . . . . . . . 12
    

         |
33 | 22, 32 | eqtr3i 2474 |
. . . . . . . . . . 11
   
     
     |
34 | | 00id 9805 |
. . . . . . . . . . . 12
   |
35 | 34 | eqcomi 2459 |
. . . . . . . . . . 11
   |
36 | 33, 35 | eqeq12i 2464 |
. . . . . . . . . 10
    

      
      |
37 | | 0re 9640 |
. . . . . . . . . . 11
 |
38 | | readdcan 9804 |
. . . . . . . . . . 11
 
     
   |
39 | 1, 37, 37, 38 | mp3an 1363 |
. . . . . . . . . 10
    
  |
40 | 21, 36, 39 | 3bitri 275 |
. . . . . . . . 9
    

               |
41 | 7, 40 | sylib 200 |
. . . . . . . 8
     |
42 | 6, 41 | syl6 34 |
. . . . . . 7
       |
43 | 42 | necon3d 2644 |
. . . . . 6
       |
44 | 3, 43 | mpi 20 |
. . . . 5
     |
45 | | ax-rrecex 9608 |
. . . . 5
   
    |
46 | 44, 45 | sylan2 477 |
. . . 4
          |
47 | | simpr 463 |
. . . . . . . . . 10
               |
48 | | simplrl 769 |
. . . . . . . . . . 11
               |
49 | 48 | recnd 9666 |
. . . . . . . . . 10
               |
50 | 47, 49 | mulcld 9660 |
. . . . . . . . 9
             
   |
51 | | simplll 767 |
. . . . . . . . . 10
               |
52 | 51 | recnd 9666 |
. . . . . . . . 9
               |
53 | 12 | a1i 11 |
. . . . . . . . 9
               |
54 | 50, 52, 53 | adddid 9664 |
. . . . . . . 8
                               |
55 | 11 | a1i 11 |
. . . . . . . . . . . . 13
               |
56 | 55, 52, 53 | addassd 9662 |
. . . . . . . . . . . 12
                       |
57 | | simpllr 768 |
. . . . . . . . . . . . 13
                 |
58 | 57 | oveq1d 6303 |
. . . . . . . . . . . 12
                     |
59 | 56, 58 | eqtr3d 2486 |
. . . . . . . . . . 11
                     |
60 | 34, 59, 57 | 3eqtr4a 2510 |
. . . . . . . . . 10
                     |
61 | 37 | a1i 11 |
. . . . . . . . . . . 12
               |
62 | 51, 61 | readdcld 9667 |
. . . . . . . . . . 11
                 |
63 | 1 | a1i 11 |
. . . . . . . . . . 11
               |
64 | | readdcan 9804 |
. . . . . . . . . . 11
   
       
     |
65 | 62, 51, 63, 64 | syl3anc 1267 |
. . . . . . . . . 10
                   
     |
66 | 60, 65 | mpbid 214 |
. . . . . . . . 9
                 |
67 | 66 | oveq2d 6304 |
. . . . . . . 8
                         |
68 | 54, 67 | eqtr3d 2486 |
. . . . . . 7
                             |
69 | | mul31 9798 |
. . . . . . . . . 10
 
           |
70 | 47, 49, 52, 69 | syl3anc 1267 |
. . . . . . . . 9
                       |
71 | | simplrr 770 |
. . . . . . . . . 10
                 |
72 | 71 | oveq1d 6303 |
. . . . . . . . 9
                     |
73 | 47 | mulid2d 9658 |
. . . . . . . . 9
                 |
74 | 70, 72, 73 | 3eqtrd 2488 |
. . . . . . . 8
                   |
75 | | mul01 9809 |
. . . . . . . . 9
         |
76 | 50, 75 | syl 17 |
. . . . . . . 8
                   |
77 | 74, 76 | oveq12d 6306 |
. . . . . . 7
                           |
78 | 68, 77, 74 | 3eqtr3d 2492 |
. . . . . 6
             
   |
79 | 78 | exp42 615 |
. . . . 5
     
   
       |
80 | 79 | rexlimdv 2876 |
. . . 4
         
      |
81 | 46, 80 | mpd 15 |
. . 3
     
     |
82 | 81 | rexlimiva 2874 |
. 2
    
     |
83 | 1, 2, 82 | mp2b 10 |
1
 
   |