MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  log2ublem3 Structured version   Visualization version   GIF version

Theorem log2ublem3 24888
Description: Lemma for log2ub 24889. In decimal, this is a proof that the first four terms of the series for log2 is less than 53056 / 76545. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
Assertion
Ref Expression
log2ublem3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056

Proof of Theorem log2ublem3
StepHypRef Expression
1 0le0 11389 . . . . . . 7 0 ≤ 0
2 risefall0lem 14973 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 14647 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 14671 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2828 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 6881 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 11375 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 11577 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 13097 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 675 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 11380 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 11384 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 10328 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 10328 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 10507 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2828 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 11371 . . . . . . . 8 2 ∈ ℂ
1817mul01i 10507 . . . . . . 7 (2 · 0) = 0
191, 16, 183brtr4i 4874 . . . . . 6 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 0)
20 0nn0 11570 . . . . . 6 0 ∈ ℕ0
21 2nn0 11572 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 11575 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 11770 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 11770 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 11571 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 11770 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 11770 . . . . . 6 25515 ∈ ℕ0
28 eqid 2806 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 11567 . . . . . . 7 25515 ∈ ℂ
3029addid2i 10505 . . . . . 6 (0 + 25515) = 25515
31 3nn0 11573 . . . . . 6 3 ∈ ℕ0
327addid1i 10504 . . . . . 6 (3 + 0) = 3
3329mulid2i 10326 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 6880 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 11410 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2828 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 6880 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 11593 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 11770 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 11579 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 11430 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 11578 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 11413 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 11388 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 13085 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 6880 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 11884 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2828 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 15995 . . . . . . . . . 10 (9↑2) = 81
51 8cn 11386 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 11883 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 10330 . . . . . . . . . 10 (8 · 9) = 72
5444mulid2i 10326 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 40, 53, 54decmul1 11819 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 15995 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 11770 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2806 . . . . . . . . 9 72 = 72
59 eqid 2806 . . . . . . . . 9 31 = 31
60 7t5e35 11867 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 10330 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 11830 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 10509 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 10275 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 11432 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 10509 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 6881 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 11574 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 11865 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 10330 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 11378 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 11433 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 10509 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 11815 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2828 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 6880 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 11770 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 11567 . . . . . . . . . . . 12 35 ∈ ℂ
7978addid1i 10504 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2828 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 11807 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 11777 . . . . . . . . . 10 1 = 01
83 3t2e6 11453 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 6882 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 11435 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2828 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 11855 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 11786 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 11807 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 11808 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 11878 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 10330 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 11831 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 11816 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 11880 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 10330 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 11820 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 11821 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2839 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 24887 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 11770 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 11770 . . . . 5 945 ∈ ℕ0
103 1m1e0 11369 . . . . 5 (1 − 1) = 0
104 eqid 2806 . . . . . 6 25515 = 25515
105 eqid 2806 . . . . . 6 945 = 945
106 6nn0 11576 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 11770 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 11770 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 11434 . . . . . . 7 (5 + 1) = 6
110 eqid 2806 . . . . . . . 8 2551 = 2551
111 eqid 2806 . . . . . . . 8 94 = 94
112 eqid 2806 . . . . . . . . 9 255 = 255
113 eqid 2806 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 11786 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 11845 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 10509 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 11816 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 11809 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 11786 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 11826 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 11811 . . . . 5 (25515 + 945) = 26460
12244sqvali 13162 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 11454 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 6880 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 10332 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2834 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 6881 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 10328 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 10512 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 11770 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2806 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 6882 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 11447 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2828 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addid2i 10505 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 11815 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 11807 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 11815 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 11820 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 11821 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 6881 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2828 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 11361 . . . . . . . 8 3 = (2 + 1)
14417mulid1i 10325 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 6880 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2831 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 6880 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2832 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 24887 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 11770 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 11770 . . . 4 26460 ∈ ℕ0
152106, 31deccl 11770 . . . 4 63 ∈ ℕ0
153 2m1e1 11414 . . . 4 (2 − 1) = 1
154 eqid 2806 . . . . 5 26460 = 26460
155 eqid 2806 . . . . 5 63 = 63
156 eqid 2806 . . . . . 6 2646 = 2646
157 eqid 2806 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 11786 . . . . . 6 (264 + 1) = 265
159 6p6e12 11829 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 11816 . . . . 5 (2646 + 6) = 2652
1617addid2i 10505 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 11809 . . . 4 (26460 + 63) = 26523
163 1p2e3 11431 . . . 4 (1 + 2) = 3
16446oveq2i 6881 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 10332 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 11882 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 10330 . . . . . . 7 (7 · 9) = 63
168167oveq2i 6881 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2828 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 11363 . . . . . . 7 5 = (4 + 1)
171 2t2e4 11451 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 6880 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2831 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 6880 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2832 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 24887 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 11770 . . . . 5 265 ∈ ℕ0
178177, 21deccl 11770 . . . 4 2652 ∈ ℕ0
179178, 31deccl 11770 . . 3 26523 ∈ ℕ0
180 3m1e2 11416 . . 3 (3 − 1) = 2
181 eqid 2806 . . . 4 26523 = 26523
182 5p3e8 11444 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 10509 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 11815 . . 3 (26523 + 5) = 26528
18512, 11mulcli 10328 . . . . 5 (7 · 5) ∈ ℂ
186185mulid1i 10325 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 10329 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 13083 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 6882 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 10330 . . . . . . 7 (2 · 3) = 6
192191oveq1i 6880 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 11365 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2831 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 6880 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2838 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 24887 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2806 . . 3 26528 = 26528
199 eqid 2806 . . . 4 2652 = 2652
200 eqid 2806 . . . . 5 265 = 265
201 00id 10492 . . . . . 6 (0 + 0) = 0
20220dec0h 11777 . . . . . 6 0 = 00
203201, 202eqtri 2828 . . . . 5 (0 + 0) = 00
204 eqid 2806 . . . . . 6 26 = 26
20535, 82eqtri 2828 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 6882 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2828 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 11382 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 11859 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 10330 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 11786 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 11808 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 10330 . . . . . . 7 (2 · 5) = 10
214213oveq1i 6880 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 11798 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2828 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 11808 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 11777 . . . . 5 5 = 05
219172, 72, 2183eqtri 2832 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 11808 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 11870 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 10330 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 11821 . 2 (2 · 26528) = 53056
224197, 223breqtri 4869 1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2156  c0 4116   class class class wbr 4844  (class class class)co 6870  cc 10215  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222  cle 10356  cmin 10547   / cdiv 10965  2c2 11352  3c3 11353  4c4 11354  5c5 11355  6c6 11356  7c7 11357  8c8 11358  9c9 11359  0cn0 11555  cdc 11755  ...cfz 12545  cexp 13079  Σcsu 14635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-oadd 7796  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-sup 8583  df-oi 8650  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-rp 12043  df-fz 12546  df-fzo 12686  df-seq 13021  df-exp 13080  df-hash 13334  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-sum 14636
This theorem is referenced by:  log2ub  24889
  Copyright terms: Public domain W3C validator