Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
(class class class)co 7358 ℂcc 11054
ℕ0cn0 12418
↑cexp 13973 |
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 2704 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 ax-cnex 11112 ax-resscn 11113 ax-1cn 11114 ax-icn 11115 ax-addcl 11116 ax-addrcl 11117 ax-mulcl 11118 ax-mulrcl 11119 ax-mulcom 11120 ax-addass 11121 ax-mulass 11122 ax-distr 11123 ax-i2m1 11124 ax-1ne0 11125 ax-1rid 11126 ax-rnegex 11127 ax-rrecex 11128 ax-cnre 11129 ax-pre-lttri 11130 ax-pre-lttrn 11131 ax-pre-ltadd 11132 ax-pre-mulgt0 11133 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3930 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-iun 4957 df-br 5107 df-opab 5169 df-mpt 5190 df-tr 5224 df-id 5532 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6254 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-riota 7314 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7804 df-2nd 7923 df-frecs 8213 df-wrecs 8244 df-recs 8318 df-rdg 8357 df-er 8651 df-en 8887 df-dom 8888 df-sdom 8889 df-pnf 11196 df-mnf 11197 df-xr 11198 df-ltxr 11199 df-le 11200 df-sub 11392 df-neg 11393 df-nn 12159 df-n0 12419 df-z 12505
df-uz 12769 df-seq 13913 df-exp 13974 |
This theorem is referenced by: absexpz
15196 binomlem
15719 incexclem
15726 incexc
15727 incexc2
15728 geoserg
15756 pwdif
15758 pwm1geoser
15759 geolim
15760 geolim2
15761 geo2sum2
15764 geomulcvg
15766 bpolycl
15940 bpolydiflem
15942 efaddlem
15980 oexpneg
16232 pwp1fsum
16278 oddpwp1fsum
16279 cphipval
24623 dvexp3
25358 itgpowd
25430 ply1termlem
25580 dgrcolem2
25651 dvply1
25660 aareccl
25702 aalioulem1
25708 taylfvallem1
25732 tayl0
25737 dvtaylp
25745 taylthlem2
25749 radcnvlem1
25788 pserulm
25797 logtayl
26031 cxpeq
26126 atantayl2
26304 atantayl3
26305 dfef2
26336 ftalem1
26438 ftalem2
26439 ftalem5
26442 basellem4
26449 logexprlim
26589 psgnfzto1st
32003 madjusmdetlem4
32468 oddpwdc
33011 eulerpartlemgs2
33037 signsplypnf
33219 signsply0
33220 breprexplemc
33302 breprexpnat
33304 bcprod
34367 knoppcnlem4
35005 knoppcnlem10
35011 knoppndvlem2
35022 knoppndvlem6
35026 knoppndvlem7
35027 knoppndvlem8
35028 knoppndvlem9
35029 knoppndvlem10
35030 knoppndvlem14
35034 knoppndvlem17
35037 lcmineqlem8
40539 lcmineqlem10
40541 lcmineqlem12
40543 dvrelogpow2b
40571 aks4d1p1p6
40576 aks4d1p1p7
40577 aks4d1p1
40579 2ap1caineq
40599 exp11d
40854 dffltz
41015 fltmul
41016 fltdiv
41017 fltaccoprm
41021 flt4lem6
41039 fltltc
41042 fltnltalem
41043 3cubeslem3l
41052 3cubeslem3r
41053 3cubeslem4
41055 jm2.18
41355 jm2.22
41362 jm2.23
41363 radcnvrat
42682 binomcxplemnn0
42717 binomcxplemnotnn0
42724 expcnfg
43918 fprodexp
43921 climexp
43932 dvsinexp
44238 dvxpaek
44267 dvnxpaek
44269 ibliccsinexp
44278 iblioosinexp
44280 itgsinexplem1
44281 itgsinexp
44282 iblsplit
44293 stoweidlem1
44328 stoweidlem7
44334 wallispi2lem2
44399 wallispi2
44400 stirlinglem3
44403 stirlinglem4
44404 stirlinglem5
44405 stirlinglem7
44407 stirlinglem8
44408 stirlinglem10
44410 stirlinglem11
44411 stirlinglem13
44413 stirlinglem14
44414 stirlinglem15
44415 elaa2lem
44560 etransclem1
44562 etransclem4
44565 etransclem8
44569 etransclem18
44579 etransclem20
44581 etransclem21
44582 etransclem23
44584 etransclem35
44596 etransclem41
44602 etransclem46
44607 etransclem48
44609 2pwp1prm
45867 lighneallem4
45888 oexpnegALTV
45955 fppr2odd
46009 altgsumbcALT
46515 dignn0flhalflem1
46787 nn0sumshdiglemA
46791 nn0sumshdiglemB
46792 |