Step | Hyp | Ref
| Expression |
1 | | eluz2nn 9566 |
. . . . 5
    
  |
2 | 1 | nnrpd 9694 |
. . . 4
    
  |
3 | 2 | 3ad2ant2 1019 |
. . 3
               |
4 | | 1red 7972 |
. . . . 5
    
  |
5 | | eluzelre 9538 |
. . . . 5
    
  |
6 | | eluz2gt1 9602 |
. . . . 5
    
  |
7 | 4, 5, 6 | gtapd 8594 |
. . . 4
    
#   |
8 | 7 | 3ad2ant2 1019 |
. . 3
             #   |
9 | | eluz2nn 9566 |
. . . . 5
    
  |
10 | 9 | nnrpd 9694 |
. . . 4
    
  |
11 | 10 | 3ad2ant1 1018 |
. . 3
               |
12 | | rplogbcl 14367 |
. . 3
  #   logb    |
13 | 3, 8, 11, 12 | syl3anc 1238 |
. 2
              logb    |
14 | | eluz2gt1 9602 |
. . . . . . . . . 10
    
  |
15 | 14 | adantr 276 |
. . . . . . . . 9
          
  |
16 | 9 | adantr 276 |
. . . . . . . . . . 11
          
  |
17 | 16 | nnrpd 9694 |
. . . . . . . . . 10
          
  |
18 | 1 | adantl 277 |
. . . . . . . . . . 11
          
  |
19 | 18 | nnrpd 9694 |
. . . . . . . . . 10
          
  |
20 | 6 | adantl 277 |
. . . . . . . . . 10
          
  |
21 | | logbgt0b 14387 |
. . . . . . . . . 10
  
    logb 
   |
22 | 17, 19, 20, 21 | syl12anc 1236 |
. . . . . . . . 9
          
  logb     |
23 | 15, 22 | mpbird 167 |
. . . . . . . 8
          
 logb    |
24 | 23 | anim1ci 341 |
. . . . . . 7
      
     
logb    
logb  
logb     |
25 | | elpq 9648 |
. . . . . . 7
  
logb  
logb      logb      |
26 | 24, 25 | syl 14 |
. . . . . 6
      
     
logb      logb      |
27 | 26 | ex 115 |
. . . . 5
          
  logb     logb       |
28 | | oveq2 5883 |
. . . . . . . . . 10
    logb         
logb     |
29 | 28 | eqcoms 2180 |
. . . . . . . . 9
  logb           
logb     |
30 | 7 | adantl 277 |
. . . . . . . . . . 11
          
#   |
31 | | rpcxplogb 14385 |
. . . . . . . . . . 11
  #     logb     |
32 | 19, 30, 17, 31 | syl3anc 1238 |
. . . . . . . . . 10
          
 
 logb     |
33 | 32 | adantr 276 |
. . . . . . . . 9
      
     
 
 
 logb     |
34 | 29, 33 | sylan9eqr 2232 |
. . . . . . . 8
       
        
logb            |
35 | 34 | ex 115 |
. . . . . . 7
      
     
 
  logb            |
36 | | oveq1 5882 |
. . . . . . . 8
                     |
37 | 19 | adantr 276 |
. . . . . . . . . . . 12
      
     
 
  |
38 | | nnrp 9663 |
. . . . . . . . . . . . . . 15
   |
39 | 38 | ad2antrl 490 |
. . . . . . . . . . . . . 14
      
     
 
  |
40 | | nnrp 9663 |
. . . . . . . . . . . . . . 15
   |
41 | 40 | ad2antll 491 |
. . . . . . . . . . . . . 14
      
     
 
  |
42 | 39, 41 | rpdivcld 9714 |
. . . . . . . . . . . . 13
      
     
 
    |
43 | 42 | rpred 9696 |
. . . . . . . . . . . 12
      
     
 
    |
44 | | nncn 8927 |
. . . . . . . . . . . . 13
   |
45 | 44 | ad2antll 491 |
. . . . . . . . . . . 12
      
     
 
  |
46 | 37, 43, 45 | cxpmuld 14359 |
. . . . . . . . . . 11
      
     
 
 
               |
47 | 39 | rpcnd 9698 |
. . . . . . . . . . . . . 14
      
     
 
  |
48 | 41 | rpap0d 9702 |
. . . . . . . . . . . . . 14
      
     
 
#   |
49 | 47, 45, 48 | divcanap1d 8748 |
. . . . . . . . . . . . 13
      
     
 
      |
50 | 49 | oveq2d 5891 |
. . . . . . . . . . . 12
      
     
 
 
          |
51 | 1 | ad2antlr 489 |
. . . . . . . . . . . . 13
      
     
 
  |
52 | | nnz 9272 |
. . . . . . . . . . . . . 14
   |
53 | 52 | ad2antrl 490 |
. . . . . . . . . . . . 13
      
     
 
  |
54 | | cxpexpnn 14320 |
. . . . . . . . . . . . 13
 
          |
55 | 51, 53, 54 | syl2anc 411 |
. . . . . . . . . . . 12
      
     
 
 
       |
56 | 50, 55 | eqtrd 2210 |
. . . . . . . . . . 11
      
     
 
 
           |
57 | 37, 43 | rpcxpcld 14355 |
. . . . . . . . . . . 12
      
     
 
 
     |
58 | | nnz 9272 |
. . . . . . . . . . . . 13
   |
59 | 58 | ad2antll 491 |
. . . . . . . . . . . 12
      
     
 
  |
60 | | cxpexprp 14319 |
. . . . . . . . . . . 12
                           |
61 | 57, 59, 60 | syl2anc 411 |
. . . . . . . . . . 11
      
     
 
                   |
62 | 46, 56, 61 | 3eqtr3rd 2219 |
. . . . . . . . . 10
      
     
 
               |
63 | 62 | eqeq1d 2186 |
. . . . . . . . 9
      
     
 
             
           |
64 | | simpr 110 |
. . . . . . . . . . . . 13
 
   |
65 | | rplpwr 12028 |
. . . . . . . . . . . . 13
 
             |
66 | 16, 18, 64, 65 | syl2an3an 1298 |
. . . . . . . . . . . 12
      
     
 
  
         |
67 | | oveq1 5882 |
. . . . . . . . . . . . . . . . . 18
             
         |
68 | 67 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . 17
                    
    |
69 | 68 | eqcoms 2180 |
. . . . . . . . . . . . . . . 16
                    
    |
70 | 69 | adantl 277 |
. . . . . . . . . . . . . . 15
       
                                 |
71 | | eluzelz 9537 |
. . . . . . . . . . . . . . . . . . 19
    
  |
72 | 71 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
          
  |
73 | | simpl 109 |
. . . . . . . . . . . . . . . . . 18
 
   |
74 | | rpexp 12153 |
. . . . . . . . . . . . . . . . . 18
 
             |
75 | 72, 72, 73, 74 | syl2an3an 1298 |
. . . . . . . . . . . . . . . . 17
      
     
 
     

     |
76 | | gcdid 11987 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
77 | 71, 76 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
    
        |
78 | | nnnn0 9183 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
79 | | nn0ge0 9201 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
80 | 1, 78, 79 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
81 | 5, 80 | absidd 11176 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
82 | 77, 81 | eqtrd 2210 |
. . . . . . . . . . . . . . . . . . . 20
    
    |
83 | 82 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . . 19
    
  
   |
84 | 83 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
      
     
 
  
   |
85 | 4, 6 | gtned 8070 |
. . . . . . . . . . . . . . . . . . . 20
    
  |
86 | | eqneqall 2357 |
. . . . . . . . . . . . . . . . . . . 20
    |
87 | 85, 86 | syl5com 29 |
. . . . . . . . . . . . . . . . . . 19
    
   |
88 | 87 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . 18
      
     
 
   |
89 | 84, 88 | sylbid 150 |
. . . . . . . . . . . . . . . . 17
      
     
 
  
  |
90 | 75, 89 | sylbid 150 |
. . . . . . . . . . . . . . . 16
      
     
 
     
   |
91 | 90 | adantr 276 |
. . . . . . . . . . . . . . 15
       
                          |
92 | 70, 91 | sylbid 150 |
. . . . . . . . . . . . . 14
       
                          |
93 | 92 | ex 115 |
. . . . . . . . . . . . 13
      
     
 
        
     
    |
94 | 93 | com23 78 |
. . . . . . . . . . . 12
      
     
 
     
             |
95 | 66, 94 | syld 45 |
. . . . . . . . . . 11
      
     
 
  
        
   |
96 | | dfnot 1371 |
. . . . . . . . . . 11
        
        
  |
97 | 95, 96 | imbitrrdi 162 |
. . . . . . . . . 10
      
     
 
  
           |
98 | 97 | con2d 624 |
. . . . . . . . 9
      
     
 
        
     |
99 | 63, 98 | sylbid 150 |
. . . . . . . 8
      
     
 
                   |
100 | 36, 99 | syl5 32 |
. . . . . . 7
      
     
 
      
    |
101 | 35, 100 | syld 45 |
. . . . . 6
      
     
 
  logb   
     |
102 | 101 | rexlimdvva 2602 |
. . . . 5
          
 
  logb    
    |
103 | 27, 102 | syld 45 |
. . . 4
          
  logb       |
104 | 103 | con2d 624 |
. . 3
          
  
 logb     |
105 | 104 | 3impia 1200 |
. 2
            
 logb    |
106 | 13, 105 | eldifd 3140 |
1
              logb      |