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

Theorem log2cnv 26310
Description: Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypothesis
Ref Expression
log2cnv.1 𝐹 = (𝑛 ∈ β„•0 ↦ (2 / ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛))))
Assertion
Ref Expression
log2cnv seq0( + , 𝐹) ⇝ (logβ€˜2)

Proof of Theorem log2cnv
Dummy variable π‘˜ is distinct from all other variables.
StepHypRef Expression
1 nn0uz 12812 . . . 4 β„•0 = (β„€β‰₯β€˜0)
2 0zd 12518 . . . 4 (⊀ β†’ 0 ∈ β„€)
3 2cn 12235 . . . . . 6 2 ∈ β„‚
4 ax-icn 11117 . . . . . 6 i ∈ β„‚
5 ine0 11597 . . . . . 6 i β‰  0
63, 4, 5divcli 11904 . . . . 5 (2 / i) ∈ β„‚
76a1i 11 . . . 4 (⊀ β†’ (2 / i) ∈ β„‚)
8 3cn 12241 . . . . . . 7 3 ∈ β„‚
9 3ne0 12266 . . . . . . 7 3 β‰  0
104, 8, 9divcli 11904 . . . . . 6 (i / 3) ∈ β„‚
11 absdiv 15187 . . . . . . . . 9 ((i ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ (absβ€˜(i / 3)) = ((absβ€˜i) / (absβ€˜3)))
124, 8, 9, 11mp3an 1462 . . . . . . . 8 (absβ€˜(i / 3)) = ((absβ€˜i) / (absβ€˜3))
13 absi 15178 . . . . . . . . 9 (absβ€˜i) = 1
14 3re 12240 . . . . . . . . . 10 3 ∈ ℝ
15 0re 11164 . . . . . . . . . . 11 0 ∈ ℝ
16 3pos 12265 . . . . . . . . . . 11 0 < 3
1715, 14, 16ltleii 11285 . . . . . . . . . 10 0 ≀ 3
18 absid 15188 . . . . . . . . . 10 ((3 ∈ ℝ ∧ 0 ≀ 3) β†’ (absβ€˜3) = 3)
1914, 17, 18mp2an 691 . . . . . . . . 9 (absβ€˜3) = 3
2013, 19oveq12i 7374 . . . . . . . 8 ((absβ€˜i) / (absβ€˜3)) = (1 / 3)
2112, 20eqtri 2765 . . . . . . 7 (absβ€˜(i / 3)) = (1 / 3)
22 1lt3 12333 . . . . . . . 8 1 < 3
23 recgt1 12058 . . . . . . . . 9 ((3 ∈ ℝ ∧ 0 < 3) β†’ (1 < 3 ↔ (1 / 3) < 1))
2414, 16, 23mp2an 691 . . . . . . . 8 (1 < 3 ↔ (1 / 3) < 1)
2522, 24mpbi 229 . . . . . . 7 (1 / 3) < 1
2621, 25eqbrtri 5131 . . . . . 6 (absβ€˜(i / 3)) < 1
27 eqid 2737 . . . . . . 7 (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1)))) = (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))
2827atantayl3 26305 . . . . . 6 (((i / 3) ∈ β„‚ ∧ (absβ€˜(i / 3)) < 1) β†’ seq0( + , (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))) ⇝ (arctanβ€˜(i / 3)))
2910, 26, 28mp2an 691 . . . . 5 seq0( + , (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))) ⇝ (arctanβ€˜(i / 3))
3029a1i 11 . . . 4 (⊀ β†’ seq0( + , (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))) ⇝ (arctanβ€˜(i / 3)))
31 oveq2 7370 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (-1↑𝑛) = (-1β†‘π‘˜))
32 oveq2 7370 . . . . . . . . . . . 12 (𝑛 = π‘˜ β†’ (2 Β· 𝑛) = (2 Β· π‘˜))
3332oveq1d 7377 . . . . . . . . . . 11 (𝑛 = π‘˜ β†’ ((2 Β· 𝑛) + 1) = ((2 Β· π‘˜) + 1))
3433oveq2d 7378 . . . . . . . . . 10 (𝑛 = π‘˜ β†’ ((i / 3)↑((2 Β· 𝑛) + 1)) = ((i / 3)↑((2 Β· π‘˜) + 1)))
3534, 33oveq12d 7380 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1)) = (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
3631, 35oveq12d 7380 . . . . . . . 8 (𝑛 = π‘˜ β†’ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))) = ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
37 ovex 7395 . . . . . . . 8 ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) ∈ V
3836, 27, 37fvmpt 6953 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) = ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
394a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ i ∈ β„‚)
408a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ 3 ∈ β„‚)
419a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ 3 β‰  0)
42 2nn0 12437 . . . . . . . . . . . . . 14 2 ∈ β„•0
43 nn0mulcl 12456 . . . . . . . . . . . . . 14 ((2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ β„•0)
4442, 43mpan 689 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ β„•0)
45 peano2nn0 12460 . . . . . . . . . . . . 13 ((2 Β· π‘˜) ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
4644, 45syl 17 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
4739, 40, 41, 46expdivd 14072 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((i / 3)↑((2 Β· π‘˜) + 1)) = ((i↑((2 Β· π‘˜) + 1)) / (3↑((2 Β· π‘˜) + 1))))
4847oveq2d 7378 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) = ((-1β†‘π‘˜) Β· ((i↑((2 Β· π‘˜) + 1)) / (3↑((2 Β· π‘˜) + 1)))))
49 neg1cn 12274 . . . . . . . . . . . 12 -1 ∈ β„‚
50 expcl 13992 . . . . . . . . . . . 12 ((-1 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (-1β†‘π‘˜) ∈ β„‚)
5149, 50mpan 689 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (-1β†‘π‘˜) ∈ β„‚)
52 expcl 13992 . . . . . . . . . . . 12 ((i ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (i↑((2 Β· π‘˜) + 1)) ∈ β„‚)
534, 46, 52sylancr 588 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (i↑((2 Β· π‘˜) + 1)) ∈ β„‚)
54 3nn 12239 . . . . . . . . . . . . 13 3 ∈ β„•
55 nnexpcl 13987 . . . . . . . . . . . . 13 ((3 ∈ β„• ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (3↑((2 Β· π‘˜) + 1)) ∈ β„•)
5654, 46, 55sylancr 588 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) ∈ β„•)
5756nncnd 12176 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) ∈ β„‚)
5856nnne0d 12210 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) β‰  0)
5951, 53, 57, 58divassd 11973 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) / (3↑((2 Β· π‘˜) + 1))) = ((-1β†‘π‘˜) Β· ((i↑((2 Β· π‘˜) + 1)) / (3↑((2 Β· π‘˜) + 1)))))
60 expp1 13981 . . . . . . . . . . . . . . 15 ((i ∈ β„‚ ∧ (2 Β· π‘˜) ∈ β„•0) β†’ (i↑((2 Β· π‘˜) + 1)) = ((i↑(2 Β· π‘˜)) Β· i))
614, 44, 60sylancr 588 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (i↑((2 Β· π‘˜) + 1)) = ((i↑(2 Β· π‘˜)) Β· i))
62 expmul 14020 . . . . . . . . . . . . . . . . 17 ((i ∈ β„‚ ∧ 2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (i↑(2 Β· π‘˜)) = ((i↑2)β†‘π‘˜))
634, 42, 62mp3an12 1452 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (i↑(2 Β· π‘˜)) = ((i↑2)β†‘π‘˜))
64 i2 14113 . . . . . . . . . . . . . . . . 17 (i↑2) = -1
6564oveq1i 7372 . . . . . . . . . . . . . . . 16 ((i↑2)β†‘π‘˜) = (-1β†‘π‘˜)
6663, 65eqtrdi 2793 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (i↑(2 Β· π‘˜)) = (-1β†‘π‘˜))
6766oveq1d 7377 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((i↑(2 Β· π‘˜)) Β· i) = ((-1β†‘π‘˜) Β· i))
6861, 67eqtrd 2777 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (i↑((2 Β· π‘˜) + 1)) = ((-1β†‘π‘˜) Β· i))
6968oveq2d 7378 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) = ((-1β†‘π‘˜) Β· ((-1β†‘π‘˜) Β· i)))
7051, 51, 39mulassd 11185 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) Β· i) = ((-1β†‘π‘˜) Β· ((-1β†‘π‘˜) Β· i)))
7149a1i 11 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ -1 ∈ β„‚)
72 id 22 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„•0)
7371, 72, 72expaddd 14060 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (-1↑(π‘˜ + π‘˜)) = ((-1β†‘π‘˜) Β· (-1β†‘π‘˜)))
74 expmul 14020 . . . . . . . . . . . . . . . . . 18 ((-1 ∈ β„‚ ∧ 2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (-1↑(2 Β· π‘˜)) = ((-1↑2)β†‘π‘˜))
7549, 42, 74mp3an12 1452 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = ((-1↑2)β†‘π‘˜))
76 neg1sqe1 14107 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
7776oveq1i 7372 . . . . . . . . . . . . . . . . 17 ((-1↑2)β†‘π‘˜) = (1β†‘π‘˜)
7875, 77eqtrdi 2793 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = (1β†‘π‘˜))
79 nn0cn 12430 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
80792timesd 12403 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) = (π‘˜ + π‘˜))
8180oveq2d 7378 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = (-1↑(π‘˜ + π‘˜)))
82 nn0z 12531 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
83 1exp 14004 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„€ β†’ (1β†‘π‘˜) = 1)
8482, 83syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (1β†‘π‘˜) = 1)
8578, 81, 843eqtr3d 2785 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (-1↑(π‘˜ + π‘˜)) = 1)
8673, 85eqtr3d 2779 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) = 1)
8786oveq1d 7377 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) Β· i) = (1 Β· i))
884mulid2i 11167 . . . . . . . . . . . . 13 (1 Β· i) = i
8987, 88eqtrdi 2793 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) Β· i) = i)
9069, 70, 893eqtr2d 2783 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) = i)
9190oveq1d 7377 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) / (3↑((2 Β· π‘˜) + 1))) = (i / (3↑((2 Β· π‘˜) + 1))))
9248, 59, 913eqtr2d 2783 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) = (i / (3↑((2 Β· π‘˜) + 1))))
9392oveq1d 7377 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = ((i / (3↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)))
94 expcl 13992 . . . . . . . . . 10 (((i / 3) ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ ((i / 3)↑((2 Β· π‘˜) + 1)) ∈ β„‚)
9510, 46, 94sylancr 588 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((i / 3)↑((2 Β· π‘˜) + 1)) ∈ β„‚)
96 nn0p1nn 12459 . . . . . . . . . . 11 ((2 Β· π‘˜) ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
9744, 96syl 17 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
9897nncnd 12176 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„‚)
9997nnne0d 12210 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) β‰  0)
10051, 95, 98, 99divassd 11973 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
10139, 57, 98, 58, 99divdiv1d 11969 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((i / (3↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = (i / ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1))))
10293, 100, 1013eqtr3d 2785 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (i / ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1))))
10357, 98mulcomd 11183 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1)) = (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))))
104103oveq2d 7378 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (i / ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1))) = (i / (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1)))))
10538, 102, 1043eqtrd 2781 . . . . . 6 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) = (i / (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1)))))
10697, 56nnmulcld 12213 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))) ∈ β„•)
107106nncnd 12176 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))) ∈ β„‚)
108106nnne0d 12210 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))) β‰  0)
10939, 107, 108divcld 11938 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (i / (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1)))) ∈ β„‚)
110105, 109eqeltrd 2838 . . . . 5 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) ∈ β„‚)
111110adantl 483 . . . 4 ((⊀ ∧ π‘˜ ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) ∈ β„‚)
11233oveq2d 7378 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (3 Β· ((2 Β· 𝑛) + 1)) = (3 Β· ((2 Β· π‘˜) + 1)))
113 oveq2 7370 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (9↑𝑛) = (9β†‘π‘˜))
114112, 113oveq12d 7380 . . . . . . . 8 (𝑛 = π‘˜ β†’ ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛)) = ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))
115114oveq2d 7378 . . . . . . 7 (𝑛 = π‘˜ β†’ (2 / ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛))) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
116 log2cnv.1 . . . . . . 7 𝐹 = (𝑛 ∈ β„•0 ↦ (2 / ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛))))
117 ovex 7395 . . . . . . 7 (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) ∈ V
118115, 116, 117fvmpt 6953 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (πΉβ€˜π‘˜) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
119 expp1 13981 . . . . . . . . . . . . . . 15 ((3 ∈ β„‚ ∧ (2 Β· π‘˜) ∈ β„•0) β†’ (3↑((2 Β· π‘˜) + 1)) = ((3↑(2 Β· π‘˜)) Β· 3))
1208, 44, 119sylancr 588 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) = ((3↑(2 Β· π‘˜)) Β· 3))
121 expmul 14020 . . . . . . . . . . . . . . . . 17 ((3 ∈ β„‚ ∧ 2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (3↑(2 Β· π‘˜)) = ((3↑2)β†‘π‘˜))
1228, 42, 121mp3an12 1452 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (3↑(2 Β· π‘˜)) = ((3↑2)β†‘π‘˜))
123 sq3 14109 . . . . . . . . . . . . . . . . 17 (3↑2) = 9
124123oveq1i 7372 . . . . . . . . . . . . . . . 16 ((3↑2)β†‘π‘˜) = (9β†‘π‘˜)
125122, 124eqtrdi 2793 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (3↑(2 Β· π‘˜)) = (9β†‘π‘˜))
126125oveq1d 7377 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((3↑(2 Β· π‘˜)) Β· 3) = ((9β†‘π‘˜) Β· 3))
127 9nn 12258 . . . . . . . . . . . . . . . . 17 9 ∈ β„•
128 nnexpcl 13987 . . . . . . . . . . . . . . . . 17 ((9 ∈ β„• ∧ π‘˜ ∈ β„•0) β†’ (9β†‘π‘˜) ∈ β„•)
129127, 128mpan 689 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (9β†‘π‘˜) ∈ β„•)
130129nncnd 12176 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (9β†‘π‘˜) ∈ β„‚)
131 mulcom 11144 . . . . . . . . . . . . . . 15 (((9β†‘π‘˜) ∈ β„‚ ∧ 3 ∈ β„‚) β†’ ((9β†‘π‘˜) Β· 3) = (3 Β· (9β†‘π‘˜)))
132130, 8, 131sylancl 587 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((9β†‘π‘˜) Β· 3) = (3 Β· (9β†‘π‘˜)))
133120, 126, 1323eqtrd 2781 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) = (3 Β· (9β†‘π‘˜)))
13490, 133oveq12d 7380 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) / (3↑((2 Β· π‘˜) + 1))) = (i / (3 Β· (9β†‘π‘˜))))
13548, 59, 1343eqtr2d 2783 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) = (i / (3 Β· (9β†‘π‘˜))))
136135oveq1d 7377 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = ((i / (3 Β· (9β†‘π‘˜))) / ((2 Β· π‘˜) + 1)))
137 nnmulcl 12184 . . . . . . . . . . . . 13 ((3 ∈ β„• ∧ (9β†‘π‘˜) ∈ β„•) β†’ (3 Β· (9β†‘π‘˜)) ∈ β„•)
13854, 129, 137sylancr 588 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (3 Β· (9β†‘π‘˜)) ∈ β„•)
139138nncnd 12176 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3 Β· (9β†‘π‘˜)) ∈ β„‚)
140138nnne0d 12210 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3 Β· (9β†‘π‘˜)) β‰  0)
14139, 139, 98, 140, 99divdiv1d 11969 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((i / (3 Β· (9β†‘π‘˜))) / ((2 Β· π‘˜) + 1)) = (i / ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1))))
142136, 100, 1413eqtr3d 2785 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (i / ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1))))
14340, 130, 98mul32d 11372 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1)) = ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))
144143oveq2d 7378 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (i / ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1))) = (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
14538, 142, 1443eqtrd 2781 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) = (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
146145oveq2d 7378 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)) = ((2 / i) Β· (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))))
147 nnmulcl 12184 . . . . . . . . . . . 12 ((3 ∈ β„• ∧ ((2 Β· π‘˜) + 1) ∈ β„•) β†’ (3 Β· ((2 Β· π‘˜) + 1)) ∈ β„•)
14854, 97, 147sylancr 588 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3 Β· ((2 Β· π‘˜) + 1)) ∈ β„•)
149148, 129nnmulcld 12213 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)) ∈ β„•)
150149nncnd 12176 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)) ∈ β„‚)
151149nnne0d 12210 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)) β‰  0)
15239, 150, 151divcld 11938 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) ∈ β„‚)
153 mulcom 11144 . . . . . . . 8 (((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) ∈ β„‚ ∧ (2 / i) ∈ β„‚) β†’ ((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) Β· (2 / i)) = ((2 / i) Β· (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))))
154152, 6, 153sylancl 587 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) Β· (2 / i)) = ((2 / i) Β· (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))))
1553a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 2 ∈ β„‚)
1565a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ i β‰  0)
157155, 39, 150, 156, 151dmdcand 11967 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) Β· (2 / i)) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
158146, 154, 1573eqtr2d 2783 . . . . . 6 (π‘˜ ∈ β„•0 β†’ ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
159118, 158eqtr4d 2780 . . . . 5 (π‘˜ ∈ β„•0 β†’ (πΉβ€˜π‘˜) = ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)))
160159adantl 483 . . . 4 ((⊀ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜π‘˜) = ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)))
1611, 2, 7, 30, 111, 160isermulc2 15549 . . 3 (⊀ β†’ seq0( + , 𝐹) ⇝ ((2 / i) Β· (arctanβ€˜(i / 3))))
162161mptru 1549 . 2 seq0( + , 𝐹) ⇝ ((2 / i) Β· (arctanβ€˜(i / 3)))
163 bndatandm 26295 . . . . . . . 8 (((i / 3) ∈ β„‚ ∧ (absβ€˜(i / 3)) < 1) β†’ (i / 3) ∈ dom arctan)
16410, 26, 163mp2an 691 . . . . . . 7 (i / 3) ∈ dom arctan
165 atanval 26250 . . . . . . 7 ((i / 3) ∈ dom arctan β†’ (arctanβ€˜(i / 3)) = ((i / 2) Β· ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3)))))))
166164, 165ax-mp 5 . . . . . 6 (arctanβ€˜(i / 3)) = ((i / 2) Β· ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3))))))
167 df-4 12225 . . . . . . . . . . . . 13 4 = (3 + 1)
168167oveq1i 7372 . . . . . . . . . . . 12 (4 / 3) = ((3 + 1) / 3)
169 ax-1cn 11116 . . . . . . . . . . . . 13 1 ∈ β„‚
1708, 169, 8, 9divdiri 11919 . . . . . . . . . . . 12 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
1718, 9dividi 11895 . . . . . . . . . . . . 13 (3 / 3) = 1
172171oveq1i 7372 . . . . . . . . . . . 12 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
173168, 170, 1723eqtri 2769 . . . . . . . . . . 11 (4 / 3) = (1 + (1 / 3))
174169, 8, 9divcli 11904 . . . . . . . . . . . 12 (1 / 3) ∈ β„‚
175169, 174subnegi 11487 . . . . . . . . . . 11 (1 βˆ’ -(1 / 3)) = (1 + (1 / 3))
176 divneg 11854 . . . . . . . . . . . . . 14 ((1 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ -(1 / 3) = (-1 / 3))
177169, 8, 9, 176mp3an 1462 . . . . . . . . . . . . 13 -(1 / 3) = (-1 / 3)
178 ixi 11791 . . . . . . . . . . . . . 14 (i Β· i) = -1
179178oveq1i 7372 . . . . . . . . . . . . 13 ((i Β· i) / 3) = (-1 / 3)
1804, 4, 8, 9divassi 11918 . . . . . . . . . . . . 13 ((i Β· i) / 3) = (i Β· (i / 3))
181177, 179, 1803eqtr2i 2771 . . . . . . . . . . . 12 -(1 / 3) = (i Β· (i / 3))
182181oveq2i 7373 . . . . . . . . . . 11 (1 βˆ’ -(1 / 3)) = (1 βˆ’ (i Β· (i / 3)))
183173, 175, 1823eqtr2ri 2772 . . . . . . . . . 10 (1 βˆ’ (i Β· (i / 3))) = (4 / 3)
184183fveq2i 6850 . . . . . . . . 9 (logβ€˜(1 βˆ’ (i Β· (i / 3)))) = (logβ€˜(4 / 3))
1858, 9pm3.2i 472 . . . . . . . . . . . . 13 (3 ∈ β„‚ ∧ 3 β‰  0)
186 divsubdir 11856 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((3 βˆ’ 1) / 3) = ((3 / 3) βˆ’ (1 / 3)))
1878, 169, 185, 186mp3an 1462 . . . . . . . . . . . 12 ((3 βˆ’ 1) / 3) = ((3 / 3) βˆ’ (1 / 3))
188 3m1e2 12288 . . . . . . . . . . . . 13 (3 βˆ’ 1) = 2
189188oveq1i 7372 . . . . . . . . . . . 12 ((3 βˆ’ 1) / 3) = (2 / 3)
190171oveq1i 7372 . . . . . . . . . . . 12 ((3 / 3) βˆ’ (1 / 3)) = (1 βˆ’ (1 / 3))
191187, 189, 1903eqtr3i 2773 . . . . . . . . . . 11 (2 / 3) = (1 βˆ’ (1 / 3))
192169, 174negsubi 11486 . . . . . . . . . . 11 (1 + -(1 / 3)) = (1 βˆ’ (1 / 3))
193181oveq2i 7373 . . . . . . . . . . 11 (1 + -(1 / 3)) = (1 + (i Β· (i / 3)))
194191, 192, 1933eqtr2ri 2772 . . . . . . . . . 10 (1 + (i Β· (i / 3))) = (2 / 3)
195194fveq2i 6850 . . . . . . . . 9 (logβ€˜(1 + (i Β· (i / 3)))) = (logβ€˜(2 / 3))
196184, 195oveq12i 7374 . . . . . . . 8 ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3))))) = ((logβ€˜(4 / 3)) βˆ’ (logβ€˜(2 / 3)))
197 4re 12244 . . . . . . . . . . 11 4 ∈ ℝ
198 4pos 12267 . . . . . . . . . . 11 0 < 4
199197, 198elrpii 12925 . . . . . . . . . 10 4 ∈ ℝ+
200 3rp 12928 . . . . . . . . . 10 3 ∈ ℝ+
201 rpdivcl 12947 . . . . . . . . . 10 ((4 ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (4 / 3) ∈ ℝ+)
202199, 200, 201mp2an 691 . . . . . . . . 9 (4 / 3) ∈ ℝ+
203 2rp 12927 . . . . . . . . . 10 2 ∈ ℝ+
204 rpdivcl 12947 . . . . . . . . . 10 ((2 ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (2 / 3) ∈ ℝ+)
205203, 200, 204mp2an 691 . . . . . . . . 9 (2 / 3) ∈ ℝ+
206 relogdiv 25964 . . . . . . . . 9 (((4 / 3) ∈ ℝ+ ∧ (2 / 3) ∈ ℝ+) β†’ (logβ€˜((4 / 3) / (2 / 3))) = ((logβ€˜(4 / 3)) βˆ’ (logβ€˜(2 / 3))))
207202, 205, 206mp2an 691 . . . . . . . 8 (logβ€˜((4 / 3) / (2 / 3))) = ((logβ€˜(4 / 3)) βˆ’ (logβ€˜(2 / 3)))
208 4cn 12245 . . . . . . . . . . 11 4 ∈ β„‚
209 2cnne0 12370 . . . . . . . . . . 11 (2 ∈ β„‚ ∧ 2 β‰  0)
210 divcan7 11871 . . . . . . . . . . 11 ((4 ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((4 / 3) / (2 / 3)) = (4 / 2))
211208, 209, 185, 210mp3an 1462 . . . . . . . . . 10 ((4 / 3) / (2 / 3)) = (4 / 2)
212 4d2e2 12330 . . . . . . . . . 10 (4 / 2) = 2
213211, 212eqtri 2765 . . . . . . . . 9 ((4 / 3) / (2 / 3)) = 2
214213fveq2i 6850 . . . . . . . 8 (logβ€˜((4 / 3) / (2 / 3))) = (logβ€˜2)
215196, 207, 2143eqtr2i 2771 . . . . . . 7 ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3))))) = (logβ€˜2)
216215oveq2i 7373 . . . . . 6 ((i / 2) Β· ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3)))))) = ((i / 2) Β· (logβ€˜2))
217166, 216eqtri 2765 . . . . 5 (arctanβ€˜(i / 3)) = ((i / 2) Β· (logβ€˜2))
218217oveq2i 7373 . . . 4 ((2 / i) Β· (arctanβ€˜(i / 3))) = ((2 / i) Β· ((i / 2) Β· (logβ€˜2)))
219 2ne0 12264 . . . . . 6 2 β‰  0
2204, 3, 219divcli 11904 . . . . 5 (i / 2) ∈ β„‚
221 logcl 25940 . . . . . 6 ((2 ∈ β„‚ ∧ 2 β‰  0) β†’ (logβ€˜2) ∈ β„‚)
2223, 219, 221mp2an 691 . . . . 5 (logβ€˜2) ∈ β„‚
2236, 220, 222mulassi 11173 . . . 4 (((2 / i) Β· (i / 2)) Β· (logβ€˜2)) = ((2 / i) Β· ((i / 2) Β· (logβ€˜2)))
224218, 223eqtr4i 2768 . . 3 ((2 / i) Β· (arctanβ€˜(i / 3))) = (((2 / i) Β· (i / 2)) Β· (logβ€˜2))
225 divcan6 11869 . . . . 5 (((2 ∈ β„‚ ∧ 2 β‰  0) ∧ (i ∈ β„‚ ∧ i β‰  0)) β†’ ((2 / i) Β· (i / 2)) = 1)
2263, 219, 4, 5, 225mp4an 692 . . . 4 ((2 / i) Β· (i / 2)) = 1
227226oveq1i 7372 . . 3 (((2 / i) Β· (i / 2)) Β· (logβ€˜2)) = (1 Β· (logβ€˜2))
228222mulid2i 11167 . . 3 (1 Β· (logβ€˜2)) = (logβ€˜2)
229224, 227, 2283eqtri 2769 . 2 ((2 / i) Β· (arctanβ€˜(i / 3))) = (logβ€˜2)
230162, 229breqtri 5135 1 seq0( + , 𝐹) ⇝ (logβ€˜2)
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2944   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059  ici 11060   + caddc 11061   Β· cmul 11063   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  2c2 12215  3c3 12216  4c4 12217  9c9 12222  β„•0cn0 12420  β„€cz 12506  β„+crp 12922  seqcseq 13913  β†‘cexp 13974  abscabs 15126   ⇝ cli 15373  logclog 25926  arctancatan 26230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-tan 15961  df-pi 15962  df-dvds 16144  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-ulm 25752  df-log 25928  df-atan 26233
This theorem is referenced by:  log2tlbnd  26311
  Copyright terms: Public domain W3C validator