Proof of Theorem expmulz
Step | Hyp | Ref
| Expression |
1 | | elznn0nn 10770 |
. . 3

       |
2 | | elznn0nn 10770 |
. . . 4

       |
3 | | expmul 12025 |
. . . . . . . 8
 
                 |
4 | 3 | 3expia 1190 |
. . . . . . 7
 
     
             |
5 | 4 | adantlr 714 |
. . . . . 6
                       |
6 | | simp2l 1014 |
. . . . . . . . . . . . . 14
          |
7 | 6 | recnd 9522 |
. . . . . . . . . . . . 13
          |
8 | | simp3 990 |
. . . . . . . . . . . . . 14
          |
9 | 8 | nn0cnd 10748 |
. . . . . . . . . . . . 13
          |
10 | 7, 9 | mulneg1d 9907 |
. . . . . . . . . . . 12
                |
11 | 10 | oveq2d 6215 |
. . . . . . . . . . 11
                   
    |
12 | | simp1l 1012 |
. . . . . . . . . . . 12
          |
13 | | simp2r 1015 |
. . . . . . . . . . . . 13
           |
14 | 13 | nnnn0d 10746 |
. . . . . . . . . . . 12
           |
15 | | expmul 12025 |
. . . . . . . . . . . 12
  
                   |
16 | 12, 14, 8, 15 | syl3anc 1219 |
. . . . . . . . . . 11
                          |
17 | 11, 16 | eqtr3d 2497 |
. . . . . . . . . 10
                          |
18 | 17 | oveq2d 6215 |
. . . . . . . . 9
                              |
19 | | expcl 11999 |
. . . . . . . . . . 11
           |
20 | 12, 14, 19 | syl2anc 661 |
. . . . . . . . . 10
               |
21 | | simp1r 1013 |
. . . . . . . . . . 11
          |
22 | 13 | nnzd 10856 |
. . . . . . . . . . 11
           |
23 | | expne0i 12012 |
. . . . . . . . . . 11
           |
24 | 12, 21, 22, 23 | syl3anc 1219 |
. . . . . . . . . 10
               |
25 | 8 | nn0zd 10855 |
. . . . . . . . . 10
          |
26 | | exprec 12021 |
. . . . . . . . . 10
                                     |
27 | 20, 24, 25, 26 | syl3anc 1219 |
. . . . . . . . 9
                                |
28 | 18, 27 | eqtr4d 2498 |
. . . . . . . 8
                              |
29 | 7, 9 | mulcld 9516 |
. . . . . . . . 9
        
   |
30 | 14, 8 | nn0mulcld 10751 |
. . . . . . . . . 10
             |
31 | 10, 30 | eqeltrrd 2543 |
. . . . . . . . 9
         
   |
32 | | expneg2 11990 |
. . . . . . . . 9
  
        
             |
33 | 12, 29, 31, 32 | syl3anc 1219 |
. . . . . . . 8
                         |
34 | | expneg2 11990 |
. . . . . . . . . 10
 
               |
35 | 12, 7, 14, 34 | syl3anc 1219 |
. . . . . . . . 9
                     |
36 | 35 | oveq1d 6214 |
. . . . . . . 8
                             |
37 | 28, 33, 36 | 3eqtr4d 2505 |
. . . . . . 7
                        |
38 | 37 | 3expia 1190 |
. . . . . 6
            
             |
39 | 5, 38 | jaodan 783 |
. . . . 5
    
                       |
40 | | simp2 989 |
. . . . . . . . . . . . 13
     
    |
41 | 40 | nn0cnd 10748 |
. . . . . . . . . . . 12
     
    |
42 | | simp3l 1016 |
. . . . . . . . . . . . 13
     
    |
43 | 42 | recnd 9522 |
. . . . . . . . . . . 12
     
    |
44 | 41, 43 | mulneg2d 9908 |
. . . . . . . . . . 11
     
  
       |
45 | 44 | oveq2d 6215 |
. . . . . . . . . 10
     
             
    |
46 | | simp1l 1012 |
. . . . . . . . . . 11
     
    |
47 | | simp3r 1017 |
. . . . . . . . . . . 12
     
     |
48 | 47 | nnnn0d 10746 |
. . . . . . . . . . 11
     
     |
49 | | expmul 12025 |
. . . . . . . . . . 11
 
                    |
50 | 46, 40, 48, 49 | syl3anc 1219 |
. . . . . . . . . 10
     
                    |
51 | 45, 50 | eqtr3d 2497 |
. . . . . . . . 9
     
                    |
52 | 51 | oveq2d 6215 |
. . . . . . . 8
     
                        |
53 | 41, 43 | mulcld 9516 |
. . . . . . . . 9
     
  
   |
54 | 40, 48 | nn0mulcld 10751 |
. . . . . . . . . 10
     
  
    |
55 | 44, 54 | eqeltrrd 2543 |
. . . . . . . . 9
     
   
   |
56 | 46, 53, 55, 32 | syl3anc 1219 |
. . . . . . . 8
     
                   |
57 | | expcl 11999 |
. . . . . . . . . 10
 
       |
58 | 46, 40, 57 | syl2anc 661 |
. . . . . . . . 9
     
        |
59 | | expneg2 11990 |
. . . . . . . . 9
     
                       |
60 | 58, 43, 48, 59 | syl3anc 1219 |
. . . . . . . 8
     
                       |
61 | 52, 56, 60 | 3eqtr4d 2505 |
. . . . . . 7
     
                  |
62 | 61 | 3expia 1190 |
. . . . . 6
                          |
63 | | simp1l 1012 |
. . . . . . . . . 10
       
  
  |
64 | | simp2l 1014 |
. . . . . . . . . . 11
       
  
  |
65 | 64 | recnd 9522 |
. . . . . . . . . 10
       
  
  |
66 | | simp2r 1015 |
. . . . . . . . . . 11
       
      |
67 | 66 | nnnn0d 10746 |
. . . . . . . . . 10
       
      |
68 | 63, 65, 67, 34 | syl3anc 1219 |
. . . . . . . . 9
       
                |
69 | 68 | oveq1d 6214 |
. . . . . . . 8
       
                        |
70 | 63, 67, 19 | syl2anc 661 |
. . . . . . . . . 10
       
          |
71 | | simp1r 1013 |
. . . . . . . . . . 11
       
     |
72 | 66 | nnzd 10856 |
. . . . . . . . . . 11
       
      |
73 | 63, 71, 72, 23 | syl3anc 1219 |
. . . . . . . . . 10
       
          |
74 | 70, 73 | reccld 10210 |
. . . . . . . . 9
       
            |
75 | | simp3l 1016 |
. . . . . . . . . 10
       
  
  |
76 | 75 | recnd 9522 |
. . . . . . . . 9
       
  
  |
77 | | simp3r 1017 |
. . . . . . . . . 10
       
      |
78 | 77 | nnnn0d 10746 |
. . . . . . . . 9
       
      |
79 | | expneg2 11990 |
. . . . . . . . 9
        
                             |
80 | 74, 76, 78, 79 | syl3anc 1219 |
. . . . . . . 8
       
                              |
81 | 77 | nnzd 10856 |
. . . . . . . . . . 11
       
      |
82 | | exprec 12021 |
. . . . . . . . . . 11
            
                           |
83 | 70, 73, 81, 82 | syl3anc 1219 |
. . . . . . . . . 10
       
                             |
84 | 83 | oveq2d 6215 |
. . . . . . . . 9
       
                                 |
85 | | expcl 11999 |
. . . . . . . . . . 11
                     |
86 | 70, 78, 85 | syl2anc 661 |
. . . . . . . . . 10
       
               |
87 | | expne0i 12012 |
. . . . . . . . . . 11
            
             |
88 | 70, 73, 81, 87 | syl3anc 1219 |
. . . . . . . . . 10
       
               |
89 | 86, 88 | recrecd 10214 |
. . . . . . . . 9
       
                             |
90 | | expmul 12025 |
. . . . . . . . . . 11
                         |
91 | 63, 67, 78, 90 | syl3anc 1219 |
. . . . . . . . . 10
       
                       |
92 | 65, 76 | mul2negd 9909 |
. . . . . . . . . . 11
       
           |
93 | 92 | oveq2d 6215 |
. . . . . . . . . 10
       
                   |
94 | 91, 93 | eqtr3d 2497 |
. . . . . . . . 9
       
                     |
95 | 84, 89, 94 | 3eqtrd 2499 |
. . . . . . . 8
       
                         |
96 | 69, 80, 95 | 3eqtrrd 2500 |
. . . . . . 7
       
      
            |
97 | 96 | 3expia 1190 |
. . . . . 6
                             |
98 | 62, 97 | jaodan 783 |
. . . . 5
    
                          |
99 | 39, 98 | jaod 380 |
. . . 4
    
      

      
             |
100 | 2, 99 | sylan2b 475 |
. . 3
      

      
             |
101 | 1, 100 | syl5bi 217 |
. 2
     
                 |
102 | 101 | impr 619 |
1
          
            |