Step | Hyp | Ref
| Expression |
1 | | logf1o 22134 |
. . . 4
         |
2 | | f1of1 5740 |
. . . 4
                   |
3 | 1, 2 | ax-mp 5 |
. . 3
         |
4 | | logcn.d |
. . . 4
  ![(,] (,]](_ioc.gif)    |
5 | 4 | logdmss 22205 |
. . 3

    |
6 | | f1ores 5755 |
. . 3
         

    
           |
7 | 3, 5, 6 | mp2an 672 |
. 2
           |
8 | | f1ofun 5743 |
. . . . . . 7
        
  |
9 | 1, 8 | ax-mp 5 |
. . . . . 6
 |
10 | | f1of 5741 |
. . . . . . . . 9
                
  |
11 | 1, 10 | ax-mp 5 |
. . . . . . . 8
         |
12 | 11 | fdmi 5664 |
. . . . . . 7
     |
13 | 5, 12 | sseqtr4i 3489 |
. . . . . 6
 |
14 | | funimass4 5843 |
. . . . . 6
 
     
         

                 |
15 | 9, 13, 14 | mp2an 672 |
. . . . 5
              

                |
16 | 4 | ellogdm 22202 |
. . . . . . . 8

      |
17 | 16 | simplbi 460 |
. . . . . . 7
   |
18 | 4 | logdmn0 22203 |
. . . . . . 7
   |
19 | 17, 18 | logcld 22140 |
. . . . . 6
       |
20 | 19 | imcld 12788 |
. . . . . . 7
           |
21 | 17, 18 | logimcld 22141 |
. . . . . . . 8
                      |
22 | 21 | simpld 459 |
. . . . . . 7
            |
23 | 4 | logdmnrp 22204 |
. . . . . . . . . 10
    |
24 | | lognegb 22156 |
. . . . . . . . . . . 12
                |
25 | 17, 18, 24 | syl2anc 661 |
. . . . . . . . . . 11
  
           |
26 | 25 | necon3bbid 2695 |
. . . . . . . . . 10
              |
27 | 23, 26 | mpbid 210 |
. . . . . . . . 9
           |
28 | 27 | necomd 2719 |
. . . . . . . 8
           |
29 | | pire 22039 |
. . . . . . . . . 10
 |
30 | 29 | a1i 11 |
. . . . . . . . 9
   |
31 | 21 | simprd 463 |
. . . . . . . . 9
           |
32 | 20, 30, 31 | leltned 9628 |
. . . . . . . 8
         
           |
33 | 28, 32 | mpbird 232 |
. . . . . . 7
           |
34 | 29 | renegcli 9773 |
. . . . . . . . 9
  |
35 | 34 | rexri 9539 |
. . . . . . . 8
  |
36 | 29 | rexri 9539 |
. . . . . . . 8
 |
37 | | elioo2 11444 |
. . . . . . . 8
                 
                              |
38 | 35, 36, 37 | mp2an 672 |
. . . . . . 7
             
         
                   |
39 | 20, 22, 33, 38 | syl3anbrc 1172 |
. . . . . 6
                |
40 | | imf 12706 |
. . . . . . 7
     |
41 | | ffn 5659 |
. . . . . . 7
       |
42 | | elpreima 5924 |
. . . . . . 7
                                      |
43 | 40, 41, 42 | mp2b 10 |
. . . . . 6
              
                     |
44 | 19, 39, 43 | sylanbrc 664 |
. . . . 5
                 |
45 | 15, 44 | mprgbir 2896 |
. . . 4
               |
46 | | elpreima 5924 |
. . . . . . 7
                          |
47 | 40, 41, 46 | mp2b 10 |
. . . . . 6
          
             |
48 | | simpl 457 |
. . . . . . . . 9
           
  |
49 | | eliooord 11458 |
. . . . . . . . . . 11
                       |
50 | 49 | adantl 466 |
. . . . . . . . . 10
                     
   |
51 | 50 | simpld 459 |
. . . . . . . . 9
                   |
52 | 50 | simprd 463 |
. . . . . . . . . 10
               
  |
53 | | imcl 12704 |
. . . . . . . . . . . 12
       |
54 | 53 | adantr 465 |
. . . . . . . . . . 11
                  |
55 | | ltle 9566 |
. . . . . . . . . . 11
               
   |
56 | 54, 29, 55 | sylancl 662 |
. . . . . . . . . 10
                    
   |
57 | 52, 56 | mpd 15 |
. . . . . . . . 9
               
  |
58 | | ellogrn 22129 |
. . . . . . . . 9

     
       |
59 | 48, 51, 57, 58 | syl3anbrc 1172 |
. . . . . . . 8
           
  |
60 | | logef 22148 |
. . . . . . . 8
           |
61 | 59, 60 | syl 16 |
. . . . . . 7
                      |
62 | | efcl 13472 |
. . . . . . . . . 10
       |
63 | 62 | adantr 465 |
. . . . . . . . 9
                  |
64 | 54 | adantr 465 |
. . . . . . . . . . . . . 14
                        |
65 | 64 | recnd 9515 |
. . . . . . . . . . . . 13
                        |
66 | | picn 22040 |
. . . . . . . . . . . . . 14
 |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
                    |
68 | | pipos 22041 |
. . . . . . . . . . . . . . 15
 |
69 | 29, 68 | gt0ne0ii 9979 |
. . . . . . . . . . . . . 14
 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
                    |
71 | 52 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
                        |
72 | 66 | mulid1i 9491 |
. . . . . . . . . . . . . . . . . 18
   |
73 | 71, 72 | syl6breqr 4432 |
. . . . . . . . . . . . . . . . 17
                      
   |
74 | | 1re 9488 |
. . . . . . . . . . . . . . . . . . 19
 |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                    |
76 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                    |
77 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                    |
78 | | ltdivmul 10307 |
. . . . . . . . . . . . . . . . . 18
     
              
    |
79 | 64, 75, 76, 77, 78 | syl112anc 1223 |
. . . . . . . . . . . . . . . . 17
                             
    |
80 | 73, 79 | mpbird 232 |
. . . . . . . . . . . . . . . 16
                       
  |
81 | | 1e0p1 10886 |
. . . . . . . . . . . . . . . 16
   |
82 | 80, 81 | syl6breq 4431 |
. . . . . . . . . . . . . . 15
                       
    |
83 | 64 | recoscld 13532 |
. . . . . . . . . . . . . . . . . . 19
                            |
84 | 64 | resincld 13531 |
. . . . . . . . . . . . . . . . . . 19
                            |
85 | 83, 84 | crimd 12825 |
. . . . . . . . . . . . . . . . . 18
                                                    |
86 | | efeul 13550 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                     |
87 | 86 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
                                                      |
88 | 87 | oveq1d 6207 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                          |
89 | 83 | recnd 9515 |
. . . . . . . . . . . . . . . . . . . . . . 23
                            |
90 | | ax-icn 9444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
91 | 84 | recnd 9515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                            |
92 | | mulcl 9469 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
93 | 90, 91, 92 | sylancr 663 |
. . . . . . . . . . . . . . . . . . . . . . 23
                              |
94 | 89, 93 | addcld 9508 |
. . . . . . . . . . . . . . . . . . . . . 22
                                        |
95 | | recl 12703 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
96 | 95 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                        |
97 | 96 | recnd 9515 |
. . . . . . . . . . . . . . . . . . . . . . 23
                        |
98 | | efcl 13472 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
99 | 97, 98 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
                            |
100 | | efne0 13485 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
101 | 97, 100 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
                            |
102 | 94, 99, 101 | divcan3d 10215 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                |
103 | 88, 102 | eqtrd 2492 |
. . . . . . . . . . . . . . . . . . . 20
                                                      |
104 | | simpr 461 |
. . . . . . . . . . . . . . . . . . . . 21
                        |
105 | 96 | reefcld 13477 |
. . . . . . . . . . . . . . . . . . . . 21
                            |
106 | 104, 105,
101 | redivcld 10262 |
. . . . . . . . . . . . . . . . . . . 20
                                  |
107 | 103, 106 | eqeltrrd 2540 |
. . . . . . . . . . . . . . . . . . 19
                                        |
108 | 107 | reim0d 12818 |
. . . . . . . . . . . . . . . . . 18
                                            |
109 | 85, 108 | eqtr3d 2494 |
. . . . . . . . . . . . . . . . 17
                            |
110 | | sineq0 22101 |
. . . . . . . . . . . . . . . . . 18
                       |
111 | 65, 110 | syl 16 |
. . . . . . . . . . . . . . . . 17
                                
   |
112 | 109, 111 | mpbid 210 |
. . . . . . . . . . . . . . . 16
                       
  |
113 | | 0z 10760 |
. . . . . . . . . . . . . . . 16
 |
114 | | zleltp1 10798 |
. . . . . . . . . . . . . . . 16
       
       
           |
115 | 112, 113,
114 | sylancl 662 |
. . . . . . . . . . . . . . 15
                              
     |
116 | 82, 115 | mpbird 232 |
. . . . . . . . . . . . . 14
                       
  |
117 | | df-neg 9701 |
. . . . . . . . . . . . . . . 16
    |
118 | 66 | mulm1i 9892 |
. . . . . . . . . . . . . . . . . 18
     |
119 | 51 | adantr 465 |
. . . . . . . . . . . . . . . . . 18
                         |
120 | 118, 119 | syl5eqbr 4425 |
. . . . . . . . . . . . . . . . 17
                           |
121 | 74 | renegcli 9773 |
. . . . . . . . . . . . . . . . . . 19
  |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
                     |
123 | | ltmuldiv 10305 |
. . . . . . . . . . . . . . . . . 18
       
 
       
          |
124 | 122, 64, 76, 77, 123 | syl112anc 1223 |
. . . . . . . . . . . . . . . . 17
                         
          |
125 | 120, 124 | mpbid 210 |
. . . . . . . . . . . . . . . 16
                           |
126 | 117, 125 | syl5eqbrr 4426 |
. . . . . . . . . . . . . . 15
                            |
127 | | zlem1lt 10799 |
. . . . . . . . . . . . . . . 16
       
                   |
128 | 113, 112,
127 | sylancr 663 |
. . . . . . . . . . . . . . 15
                                    |
129 | 126, 128 | mpbird 232 |
. . . . . . . . . . . . . 14
                          |
130 | 64, 76, 70 | redivcld 10262 |
. . . . . . . . . . . . . . 15
                       
  |
131 | | 0re 9489 |
. . . . . . . . . . . . . . 15
 |
132 | | letri3 9563 |
. . . . . . . . . . . . . . 15
       
       
                 |
133 | 130, 131,
132 | sylancl 662 |
. . . . . . . . . . . . . 14
                               
          |
134 | 116, 129,
133 | mpbir2and 913 |
. . . . . . . . . . . . 13
                       
  |
135 | 65, 67, 70, 134 | diveq0d 10217 |
. . . . . . . . . . . 12
                        |
136 | | reim0b 12712 |
. . . . . . . . . . . . 13
 
       |
137 | 136 | ad2antrr 725 |
. . . . . . . . . . . 12
                          |
138 | 135, 137 | mpbird 232 |
. . . . . . . . . . 11
                    |
139 | 138 | rpefcld 13493 |
. . . . . . . . . 10
                        |
140 | 139 | ex 434 |
. . . . . . . . 9
                        |
141 | 4 | ellogdm 22202 |
. . . . . . . . 9
    
                  |
142 | 63, 140, 141 | sylanbrc 664 |
. . . . . . . 8
                  |
143 | | funfvima2 6054 |
. . . . . . . . 9
 
                     |
144 | 9, 13, 143 | mp2an 672 |
. . . . . . . 8
                   |
145 | 142, 144 | syl 16 |
. . . . . . 7
                          |
146 | 61, 145 | eqeltrrd 2540 |
. . . . . 6
           
      |
147 | 47, 146 | sylbi 195 |
. . . . 5
                 |
148 | 147 | ssriv 3460 |
. . . 4
               |
149 | 45, 148 | eqssi 3472 |
. . 3
               |
150 | | f1oeq3 5734 |
. . 3
                
                            |
151 | 149, 150 | ax-mp 5 |
. 2
 
                           |
152 | 7, 151 | mpbi 208 |
1
                 |