Proof of Theorem log2ublem3
Step | Hyp | Ref
| Expression |
1 | | 0le0 10696 |
. . . . . . 7
 |
2 | | 0re 9640 |
. . . . . . . . . . . . 13
 |
3 | | ltm1 10442 |
. . . . . . . . . . . . 13
     |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . 12
   |
5 | | 0z 10945 |
. . . . . . . . . . . . 13
 |
6 | | peano2zm 10977 |
. . . . . . . . . . . . . 14
     |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . . . . . 13
   |
8 | | fzn 11812 |
. . . . . . . . . . . . 13
                 |
9 | 5, 7, 8 | mp2an 677 |
. . . . . . . . . . . 12
  
        |
10 | 4, 9 | mpbi 212 |
. . . . . . . . . . 11
       |
11 | 10 | sumeq1i 13757 |
. . . . . . . . . 10
                                      |
12 | | sum0 13780 |
. . . . . . . . . 10
                |
13 | 11, 12 | eqtri 2472 |
. . . . . . . . 9
                       |
14 | 13 | oveq2i 6299 |
. . . . . . . 8
                                           |
15 | | 3cn 10681 |
. . . . . . . . . . 11
 |
16 | | 7nn0 10888 |
. . . . . . . . . . 11
 |
17 | | expcl 12287 |
. . . . . . . . . . 11
 
       |
18 | 15, 16, 17 | mp2an 677 |
. . . . . . . . . 10
     |
19 | | 5cn 10686 |
. . . . . . . . . . 11
 |
20 | | 7cn 10690 |
. . . . . . . . . . 11
 |
21 | 19, 20 | mulcli 9645 |
. . . . . . . . . 10
   |
22 | 18, 21 | mulcli 9645 |
. . . . . . . . 9
         |
23 | 22 | mul01i 9820 |
. . . . . . . 8
           |
24 | 14, 23 | eqtri 2472 |
. . . . . . 7
                                 |
25 | | 2cn 10677 |
. . . . . . . 8
 |
26 | 25 | mul01i 9820 |
. . . . . . 7
   |
27 | 1, 24, 26 | 3brtr4i 4430 |
. . . . . 6
                                   |
28 | | 0nn0 10881 |
. . . . . 6
 |
29 | | 2nn0 10883 |
. . . . . . . . . 10
 |
30 | | 5nn0 10886 |
. . . . . . . . . 10
 |
31 | 29, 30 | deccl 11062 |
. . . . . . . . 9
;  |
32 | 31, 30 | deccl 11062 |
. . . . . . . 8
;;   |
33 | | 1nn0 10882 |
. . . . . . . 8
 |
34 | 32, 33 | deccl 11062 |
. . . . . . 7
;;;    |
35 | 34, 30 | deccl 11062 |
. . . . . 6
;;;;     |
36 | | eqid 2450 |
. . . . . 6
     |
37 | 35 | nn0cni 10878 |
. . . . . . 7
;;;;     |
38 | 37 | addid2i 9818 |
. . . . . 6
 ;;;;     ;;;;     |
39 | | 3nn0 10884 |
. . . . . 6
 |
40 | 15 | addid1i 9817 |
. . . . . 6
   |
41 | 37 | mulid2i 9643 |
. . . . . . 7
 ;;;;     ;;;;     |
42 | 26 | oveq1i 6298 |
. . . . . . . . 9
       |
43 | | 0p1e1 10718 |
. . . . . . . . 9
   |
44 | 42, 43 | eqtri 2472 |
. . . . . . . 8
     |
45 | 44 | oveq1i 6298 |
. . . . . . 7
     ;;;;      ;;;;      |
46 | 30, 16 | nn0mulcli 10905 |
. . . . . . . 8
   |
47 | 16, 29 | deccl 11062 |
. . . . . . . 8
;  |
48 | | 9nn0 10890 |
. . . . . . . 8
 |
49 | | 2p1e3 10730 |
. . . . . . . . 9
   |
50 | | 8nn0 10889 |
. . . . . . . . . 10
 |
51 | | 1p1e2 10720 |
. . . . . . . . . . 11
   |
52 | | 9cn 10694 |
. . . . . . . . . . . . . 14
 |
53 | | exp1 12275 |
. . . . . . . . . . . . . 14
       |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . 13
     |
55 | 54 | oveq1i 6298 |
. . . . . . . . . . . 12
         |
56 | | 9t9e81 11150 |
. . . . . . . . . . . 12
  ;  |
57 | 55, 56 | eqtri 2472 |
. . . . . . . . . . 11
      ;  |
58 | 48, 33, 51, 57 | numexpp1 15043 |
. . . . . . . . . 10
    ;  |
59 | | 8cn 10692 |
. . . . . . . . . . . . 13
 |
60 | | 9t8e72 11149 |
. . . . . . . . . . . . 13
  ;  |
61 | 52, 59, 60 | mulcomli 9647 |
. . . . . . . . . . . 12
  ;  |
62 | 61 | oveq1i 6298 |
. . . . . . . . . . 11
    ;   |
63 | 47 | nn0cni 10878 |
. . . . . . . . . . . 12
;  |
64 | 63 | addid1i 9817 |
. . . . . . . . . . 11
;  ;  |
65 | 62, 64 | eqtri 2472 |
. . . . . . . . . 10
    ;  |
66 | 52 | mulid2i 9643 |
. . . . . . . . . . 11
   |
67 | 48 | dec0h 11064 |
. . . . . . . . . . 11
;  |
68 | 66, 67 | eqtri 2472 |
. . . . . . . . . 10
  ;  |
69 | 48, 50, 33, 58, 48, 28, 65, 68 | decmul1c 11095 |
. . . . . . . . 9
      ;;   |
70 | 48, 29, 49, 69 | numexpp1 15043 |
. . . . . . . 8
    ;;   |
71 | 39, 33 | deccl 11062 |
. . . . . . . 8
;  |
72 | | eqid 2450 |
. . . . . . . . 9
; ;  |
73 | | eqid 2450 |
. . . . . . . . 9
; ;  |
74 | | 7t5e35 11133 |
. . . . . . . . . . 11
  ;  |
75 | 20, 19, 74 | mulcomli 9647 |
. . . . . . . . . 10
  ;  |
76 | | 7p3e10 10752 |
. . . . . . . . . . . 12
   |
77 | 20, 15, 76 | addcomli 9822 |
. . . . . . . . . . 11
   |
78 | | dec10 11078 |
. . . . . . . . . . 11
;  |
79 | 77, 78 | eqtri 2472 |
. . . . . . . . . 10
  ;  |
80 | | ax-1cn 9594 |
. . . . . . . . . . . . 13
 |
81 | | 3p1e4 10732 |
. . . . . . . . . . . . 13
   |
82 | 15, 80, 81 | addcomli 9822 |
. . . . . . . . . . . 12
   |
83 | 82 | oveq2i 6299 |
. . . . . . . . . . 11
           |
84 | | 4nn0 10885 |
. . . . . . . . . . . 12
 |
85 | | 7t3e21 11131 |
. . . . . . . . . . . . 13
  ;  |
86 | 20, 15, 85 | mulcomli 9647 |
. . . . . . . . . . . 12
  ;  |
87 | | 4cn 10684 |
. . . . . . . . . . . . 13
 |
88 | | 4p1e5 10733 |
. . . . . . . . . . . . 13
   |
89 | 87, 80, 88 | addcomli 9822 |
. . . . . . . . . . . 12
   |
90 | 29, 33, 84, 86, 89 | decaddi 11092 |
. . . . . . . . . . 11
    ;  |
91 | 83, 90 | eqtri 2472 |
. . . . . . . . . 10
      ;  |
92 | 75 | oveq1i 6298 |
. . . . . . . . . . 11
    ;   |
93 | 39, 30 | deccl 11062 |
. . . . . . . . . . . . 13
;  |
94 | 93 | nn0cni 10878 |
. . . . . . . . . . . 12
;  |
95 | 94 | addid1i 9817 |
. . . . . . . . . . 11
;  ;  |
96 | 92, 95 | eqtri 2472 |
. . . . . . . . . 10
    ;  |
97 | 39, 30, 33, 28, 75, 79, 16, 30, 39, 91, 96 | decmac 11087 |
. . . . . . . . 9
        ;;   |
98 | 33 | dec0h 11064 |
. . . . . . . . . 10
;  |
99 | | 3t2e6 10758 |
. . . . . . . . . . . 12
   |
100 | 99, 43 | oveq12i 6300 |
. . . . . . . . . . 11
         |
101 | | 6p1e7 10735 |
. . . . . . . . . . 11
   |
102 | 100, 101 | eqtri 2472 |
. . . . . . . . . 10
       |
103 | | 5t2e10 10761 |
. . . . . . . . . . . 12
   |
104 | 103, 78 | eqtri 2472 |
. . . . . . . . . . 11
  ;  |
105 | 33, 28, 43, 104 | decsuc 11071 |
. . . . . . . . . 10
    ;  |
106 | 39, 30, 28, 33, 75, 98, 29, 33, 33, 102, 105 | decmac 11087 |
. . . . . . . . 9
      ;  |
107 | 16, 29, 39, 33, 72, 73, 46, 33, 16, 97, 106 | decma2c 11088 |
. . . . . . . 8
    ;  ;  ;;;    |
108 | | 9t3e27 11144 |
. . . . . . . . . . 11
  ;  |
109 | 52, 15, 108 | mulcomli 9647 |
. . . . . . . . . 10
  ;  |
110 | | 7p4e11 11100 |
. . . . . . . . . 10
  ;  |
111 | 29, 16, 84, 109, 49, 33, 110 | decaddci 11093 |
. . . . . . . . 9
    ;  |
112 | | 9t5e45 11146 |
. . . . . . . . . 10
  ;  |
113 | 52, 19, 112 | mulcomli 9647 |
. . . . . . . . 9
  ;  |
114 | 48, 39, 30, 75, 30, 84, 111, 113 | decmul1c 11095 |
. . . . . . . 8
    ;;   |
115 | 46, 47, 48, 70, 30, 71, 107, 114 | decmul2c 11096 |
. . . . . . 7
        ;;;;     |
116 | 41, 45, 115 | 3eqtr4ri 2483 |
. . . . . 6
             ;;;;      |
117 | 27, 28, 35, 28, 36, 38, 39, 40, 116 | log2ublem2 23866 |
. . . . 5
                               ;;;;      |
118 | 48, 84 | deccl 11062 |
. . . . . 6
;  |
119 | 118, 30 | deccl 11062 |
. . . . 5
;;   |
120 | | 1m1e0 10675 |
. . . . 5
   |
121 | | eqid 2450 |
. . . . . 6
;;;;    ;;;;     |
122 | | eqid 2450 |
. . . . . 6
;;  ;;   |
123 | | 6nn0 10887 |
. . . . . . . . 9
 |
124 | 29, 123 | deccl 11062 |
. . . . . . . 8
;  |
125 | 124, 84 | deccl 11062 |
. . . . . . 7
;;   |
126 | | 5p1e6 10734 |
. . . . . . 7
   |
127 | | eqid 2450 |
. . . . . . . 8
;;;   ;;;    |
128 | | eqid 2450 |
. . . . . . . 8
; ;  |
129 | | eqid 2450 |
. . . . . . . . 9
;;  ;;   |
130 | | eqid 2450 |
. . . . . . . . . 10
; ;  |
131 | 29, 30, 126, 130 | decsuc 11071 |
. . . . . . . . 9
;  ;  |
132 | | 9p5e14 11113 |
. . . . . . . . . 10
  ;  |
133 | 52, 19, 132 | addcomli 9822 |
. . . . . . . . 9
  ;  |
134 | 31, 30, 48, 129, 131, 84, 133 | decaddci 11093 |
. . . . . . . 8
;;   ;;   |
135 | 32, 33, 48, 84, 127, 128, 134, 89 | decadd 11089 |
. . . . . . 7
;;;   ;  ;;;    |
136 | 125, 30, 126, 135 | decsuc 11071 |
. . . . . 6
 ;;;   ;   ;;;    |
137 | | 5p5e10 10747 |
. . . . . 6
   |
138 | 34, 30, 118, 30, 121, 122, 136, 137 | decaddc2 11091 |
. . . . 5
;;;;    ;;   ;;;;     |
139 | 52 | sqvali 12351 |
. . . . . . . . 9
       |
140 | | 3t3e9 10759 |
. . . . . . . . . 10
   |
141 | 140 | oveq1i 6298 |
. . . . . . . . 9
       |
142 | 139, 141 | eqtr4i 2475 |
. . . . . . . 8
         |
143 | 15, 15, 52 | mulassi 9649 |
. . . . . . . 8
         |
144 | 142, 143 | eqtri 2472 |
. . . . . . 7
         |
145 | 144 | oveq2i 6299 |
. . . . . 6
                 |
146 | 15, 52 | mulcli 9645 |
. . . . . . . 8
   |
147 | 21, 15, 146 | mul12i 9825 |
. . . . . . 7
                 |
148 | 29, 84 | deccl 11062 |
. . . . . . . . 9
;  |
149 | | eqid 2450 |
. . . . . . . . . 10
; ;  |
150 | 99, 49 | oveq12i 6300 |
. . . . . . . . . . 11
         |
151 | | 6p3e9 10749 |
. . . . . . . . . . 11
   |
152 | 150, 151 | eqtri 2472 |
. . . . . . . . . 10
       |
153 | 87 | addid2i 9818 |
. . . . . . . . . . 11
   |
154 | 33, 28, 84, 104, 153 | decaddi 11092 |
. . . . . . . . . 10
    ;  |
155 | 39, 30, 29, 84, 75, 149, 29, 84, 33, 152, 154 | decmac 11087 |
. . . . . . . . 9
     ;  ;  |
156 | 29, 33, 39, 86, 82 | decaddi 11092 |
. . . . . . . . . 10
    ;  |
157 | 16, 39, 30, 75, 30, 39, 156, 75 | decmul1c 11095 |
. . . . . . . . 9
    ;;   |
158 | 46, 29, 16, 109, 30, 148, 155, 157 | decmul2c 11096 |
. . . . . . . 8
      ;;   |
159 | 158 | oveq2i 6299 |
. . . . . . 7
         ;;    |
160 | 147, 159 | eqtri 2472 |
. . . . . 6
         ;;    |
161 | | df-3 10666 |
. . . . . . . 8
   |
162 | 25 | mulid1i 9642 |
. . . . . . . . 9
   |
163 | 162 | oveq1i 6298 |
. . . . . . . 8
       |
164 | 161, 163 | eqtr4i 2475 |
. . . . . . 7
     |
165 | 164 | oveq1i 6298 |
. . . . . 6
 ;;        ;;    |
166 | 145, 160,
165 | 3eqtri 2476 |
. . . . 5
             ;;    |
167 | 117, 35, 119, 33, 120, 138, 29, 49, 166 | log2ublem2 23866 |
. . . 4
                               ;;;;      |
168 | 125, 123 | deccl 11062 |
. . . . 5
;;;    |
169 | 168, 28 | deccl 11062 |
. . . 4
;;;;     |
170 | 123, 39 | deccl 11062 |
. . . 4
;  |
171 | | 2m1e1 10721 |
. . . 4
   |
172 | | eqid 2450 |
. . . . 5
;;;;    ;;;;     |
173 | | eqid 2450 |
. . . . 5
; ;  |
174 | | eqid 2450 |
. . . . . 6
;;;   ;;;    |
175 | | eqid 2450 |
. . . . . . 7
;;  ;;   |
176 | 124, 84, 88, 175 | decsuc 11071 |
. . . . . 6
;;   ;;   |
177 | | 6p6e12 11099 |
. . . . . 6
  ;  |
178 | 125, 123,
123, 174, 176, 29, 177 | decaddci 11093 |
. . . . 5
;;;    ;;;    |
179 | 15 | addid2i 9818 |
. . . . 5
   |
180 | 168, 28, 123, 39, 172, 173, 178, 179 | decadd 11089 |
. . . 4
;;;;    ;  ;;;;     |
181 | | 1p2e3 10731 |
. . . 4
   |
182 | 54 | oveq2i 6299 |
. . . . 5
             |
183 | 19, 20, 52 | mulassi 9649 |
. . . . . 6
         |
184 | | 9t7e63 11148 |
. . . . . . . 8
  ;  |
185 | 52, 20, 184 | mulcomli 9647 |
. . . . . . 7
  ;  |
186 | 185 | oveq2i 6299 |
. . . . . 6
     ;   |
187 | 183, 186 | eqtri 2472 |
. . . . 5
     ;   |
188 | | df-5 10668 |
. . . . . . 7
   |
189 | | 2t2e4 10756 |
. . . . . . . 8
   |
190 | 189 | oveq1i 6298 |
. . . . . . 7
       |
191 | 188, 190 | eqtr4i 2475 |
. . . . . 6
     |
192 | 191 | oveq1i 6298 |
. . . . 5
 ;       ;   |
193 | 182, 187,
192 | 3eqtri 2476 |
. . . 4
             ;   |
194 | 167, 169,
170, 29, 171, 180, 33, 181, 193 | log2ublem2 23866 |
. . 3
                               ;;;;      |
195 | 124, 30 | deccl 11062 |
. . . . 5
;;   |
196 | 195, 29 | deccl 11062 |
. . . 4
;;;    |
197 | 196, 39 | deccl 11062 |
. . 3
;;;;     |
198 | | 3m1e2 10723 |
. . 3
   |
199 | | eqid 2450 |
. . . 4
;;;;    ;;;;     |
200 | | 5p3e8 10745 |
. . . . 5
   |
201 | 19, 15, 200 | addcomli 9822 |
. . . 4
   |
202 | 196, 39, 30, 199, 201 | decaddi 11092 |
. . 3
;;;;     ;;;;     |
203 | 20, 19 | mulcli 9645 |
. . . . 5
   |
204 | 203 | mulid1i 9642 |
. . . 4
       |
205 | 19, 20 | mulcomi 9646 |
. . . . 5
     |
206 | | exp0 12273 |
. . . . . 6
       |
207 | 52, 206 | ax-mp 5 |
. . . . 5
     |
208 | 205, 207 | oveq12i 6300 |
. . . 4
             |
209 | 15, 25, 99 | mulcomli 9647 |
. . . . . . 7
   |
210 | 209 | oveq1i 6298 |
. . . . . 6
       |
211 | | df-7 10670 |
. . . . . 6
   |
212 | 210, 211 | eqtr4i 2475 |
. . . . 5
     |
213 | 212 | oveq1i 6298 |
. . . 4
         |
214 | 204, 208,
213 | 3eqtr4i 2482 |
. . 3
               |
215 | 194, 197,
30, 39, 198, 202, 28, 179, 214 | log2ublem2 23866 |
. 2
                               ;;;;      |
216 | | eqid 2450 |
. . 3
;;;;    ;;;;     |
217 | | eqid 2450 |
. . . 4
;;;   ;;;    |
218 | | eqid 2450 |
. . . . 5
;;  ;;   |
219 | | 00id 9805 |
. . . . . 6
   |
220 | 28 | dec0h 11064 |
. . . . . 6
;  |
221 | 219, 220 | eqtri 2472 |
. . . . 5
  ;  |
222 | | eqid 2450 |
. . . . . 6
; ;  |
223 | 43, 98 | eqtri 2472 |
. . . . . 6
  ;  |
224 | 189, 43 | oveq12i 6300 |
. . . . . . 7
         |
225 | 224, 88 | eqtri 2472 |
. . . . . 6
       |
226 | | 6cn 10688 |
. . . . . . . 8
 |
227 | | 6t2e12 11125 |
. . . . . . . 8
  ;  |
228 | 226, 25, 227 | mulcomli 9647 |
. . . . . . 7
  ;  |
229 | 33, 29, 49, 228 | decsuc 11071 |
. . . . . 6
    ;  |
230 | 29, 123, 28, 33, 222, 223, 29, 39, 33, 225, 229 | decma2c 11088 |
. . . . 5
  ;     ;  |
231 | 19, 25, 103 | mulcomli 9647 |
. . . . . . 7
   |
232 | 231 | oveq1i 6298 |
. . . . . 6
       |
233 | | dec10p 11077 |
. . . . . 6
  ;  |
234 | 232, 233 | eqtri 2472 |
. . . . 5
    ;  |
235 | 124, 30, 28, 28, 218, 221, 29, 28, 33, 230, 234 | decma2c 11088 |
. . . 4
  ;;      ;;   |
236 | 30 | dec0h 11064 |
. . . . 5
;  |
237 | 190, 88, 236 | 3eqtri 2476 |
. . . 4
    ;  |
238 | 195, 29, 28, 33, 217, 98, 29, 30, 28, 235, 237 | decma2c 11088 |
. . 3
  ;;;     ;;;    |
239 | | 8t2e16 11136 |
. . . 4
  ;  |
240 | 59, 25, 239 | mulcomli 9647 |
. . 3
  ;  |
241 | 29, 196, 50, 216, 123, 33, 238, 240 | decmul2c 11096 |
. 2
 ;;;;     ;;;;     |
242 | 215, 241 | breqtri 4425 |
1
                              ;;;;     |