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

Theorem log2ublem3 26298
Description: Lemma for log2ub 26299. 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 12254 . . . . . . 7 0 ≤ 0
2 risefall0lem 15909 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 15583 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 15606 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2764 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 7368 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 12234 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 12435 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 13985 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 690 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 12241 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 12247 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 11162 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 11162 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 11345 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2764 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 12228 . . . . . . . 8 2 ∈ ℂ
1817mul01i 11345 . . . . . . 7 (2 · 0) = 0
191, 16, 183brtr4i 5135 . . . . . 6 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 0)
20 0nn0 12428 . . . . . 6 0 ∈ ℕ0
21 2nn0 12430 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 12433 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 12633 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 12633 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 12429 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 12633 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 12633 . . . . . 6 25515 ∈ ℕ0
28 eqid 2736 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 12425 . . . . . . 7 25515 ∈ ℂ
3029addid2i 11343 . . . . . 6 (0 + 25515) = 25515
31 3nn0 12431 . . . . . 6 3 ∈ ℕ0
327addid1i 11342 . . . . . 6 (3 + 0) = 3
3329mulid2i 11160 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 7367 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 12275 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2764 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 7367 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 12451 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 12633 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 12437 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 12295 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 12436 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 12278 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 12253 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 13973 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 7367 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 12747 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2764 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 16950 . . . . . . . . . 10 (9↑2) = 81
51 8cn 12250 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 12746 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 11164 . . . . . . . . . 10 (8 · 9) = 72
5444mulid2i 11160 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 53, 54decmul1 12682 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 16950 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 12633 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2736 . . . . . . . . 9 72 = 72
59 eqid 2736 . . . . . . . . 9 31 = 31
60 7t5e35 12730 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 11164 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 12693 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 11347 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 12298 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 11347 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 7368 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 12432 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 12728 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 11164 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 12238 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 12299 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 11347 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 12678 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2764 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 7367 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 12633 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 12425 . . . . . . . . . . . 12 35 ∈ ℂ
7978addid1i 11342 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2764 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 12670 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 12640 . . . . . . . . . 10 1 = 01
83 3t2e6 12319 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 7369 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 12301 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2764 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 12718 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 12649 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 12670 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 12671 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 12741 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 11164 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 12694 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 12679 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 12743 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 11164 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 12683 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 12684 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2775 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 26297 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 12633 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 12633 . . . . 5 945 ∈ ℕ0
103 1m1e0 12225 . . . . 5 (1 − 1) = 0
104 eqid 2736 . . . . . 6 25515 = 25515
105 eqid 2736 . . . . . 6 945 = 945
106 6nn0 12434 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 12633 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 12633 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 12300 . . . . . . 7 (5 + 1) = 6
110 eqid 2736 . . . . . . . 8 2551 = 2551
111 eqid 2736 . . . . . . . 8 94 = 94
112 eqid 2736 . . . . . . . . 9 255 = 255
113 eqid 2736 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 12649 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 12708 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 11347 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 12679 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 12672 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 12649 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 12689 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 12674 . . . . 5 (25515 + 945) = 26460
12244sqvali 14084 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 12320 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 7367 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 11166 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2770 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 7368 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 11162 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 11350 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 12633 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2736 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 7369 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 12313 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2764 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addid2i 11343 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 12678 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 12670 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 12678 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 12683 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 12684 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 7368 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2764 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 12217 . . . . . . . 8 3 = (2 + 1)
14417mulid1i 11159 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 7367 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2767 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 7367 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2768 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 26297 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 12633 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 12633 . . . 4 26460 ∈ ℕ0
152106, 31deccl 12633 . . . 4 63 ∈ ℕ0
153 2m1e1 12279 . . . 4 (2 − 1) = 1
154 eqid 2736 . . . . 5 26460 = 26460
155 eqid 2736 . . . . 5 63 = 63
156 eqid 2736 . . . . . 6 2646 = 2646
157 eqid 2736 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 12649 . . . . . 6 (264 + 1) = 265
159 6p6e12 12692 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 12679 . . . . 5 (2646 + 6) = 2652
1617addid2i 11343 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 12672 . . . 4 (26460 + 63) = 26523
163 1p2e3 12296 . . . 4 (1 + 2) = 3
16446oveq2i 7368 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 11166 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 12745 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 11164 . . . . . . 7 (7 · 9) = 63
168167oveq2i 7368 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2764 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 12219 . . . . . . 7 5 = (4 + 1)
171 2t2e4 12317 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 7367 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2767 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 7367 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2768 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 26297 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 12633 . . . . 5 265 ∈ ℕ0
178177, 21deccl 12633 . . . 4 2652 ∈ ℕ0
179178, 31deccl 12633 . . 3 26523 ∈ ℕ0
180 3m1e2 12281 . . 3 (3 − 1) = 2
181 eqid 2736 . . . 4 26523 = 26523
182 5p3e8 12310 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 11347 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 12678 . . 3 (26523 + 5) = 26528
18512, 11mulcli 11162 . . . . 5 (7 · 5) ∈ ℂ
186185mulid1i 11159 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 11163 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 13971 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 7369 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 11164 . . . . . . 7 (2 · 3) = 6
192191oveq1i 7367 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 12221 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2767 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 7367 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2774 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 26297 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2736 . . 3 26528 = 26528
199 eqid 2736 . . . 4 2652 = 2652
200 eqid 2736 . . . . 5 265 = 265
201 00id 11330 . . . . . 6 (0 + 0) = 0
20220dec0h 12640 . . . . . 6 0 = 00
203201, 202eqtri 2764 . . . . 5 (0 + 0) = 00
204 eqid 2736 . . . . . 6 26 = 26
20535, 82eqtri 2764 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 7369 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2764 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 12244 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 12722 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 11164 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 12649 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 12671 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 11164 . . . . . . 7 (2 · 5) = 10
214213oveq1i 7367 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 12661 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2764 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 12671 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 12640 . . . . 5 5 = 05
219172, 72, 2183eqtri 2768 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 12671 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 12733 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 11164 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 12684 . 2 (2 · 26528) = 53056
224197, 223breqtri 5130 1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106  c0 4282   class class class wbr 5105  (class class class)co 7357  cc 11049  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  cle 11190  cmin 11385   / cdiv 11812  2c2 12208  3c3 12209  4c4 12210  5c5 12211  6c6 12212  7c7 12213  8c8 12214  9c9 12215  0cn0 12413  cdc 12618  ...cfz 13424  cexp 13967  Σcsu 15570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571
This theorem is referenced by:  log2ub  26299
  Copyright terms: Public domain W3C validator