Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1541
∈ wcel 2106 (class class class)co 7411
ℂcc 11110 0cc0 11112
1c1 11113 ↑cexp 14031 |
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 2703 ax-sep 5299 ax-nul 5306 ax-pr 5427 ax-1cn 11170 ax-addrcl 11173 ax-rnegex 11183 ax-cnre 11185 |
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 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-iota 6495 df-fun 6545 df-fv 6551 df-ov 7414 df-oprab 7415 df-mpo 7416 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-neg 11451 df-z 12563
df-seq 13971 df-exp 14032 |
This theorem is referenced by: faclbnd4lem3
14259 faclbnd4lem4
14260 faclbnd6
14263 hashmap
14399 absexp
15255 binom
15780 geoser
15817 pwdif
15818 cvgrat
15833 efexp
16048 pwp1fsum
16338 prmdvdsexpr
16658 rpexp1i
16664 phiprm
16714 odzdvds
16732 pclem
16775 pcpre1
16779 pcexp
16796 dvdsprmpweqnn
16822 prmpwdvds
16841 pgp0
19505 sylow2alem2
19527 ablfac1eu
19984 pgpfac1lem3a
19987 plyeq0lem
25948 plyco
25979 vieta1
26049 abelthlem9
26176 advlogexp
26387 cxpmul2
26421 nnlogbexp
26510 ftalem5
26805 0sgm
26872 1sgmprm
26926 dchrptlem2
26992 bposlem5
27015 lgsval2lem
27034 lgsmod
27050 lgsdilem2
27060 lgsne0
27062 chebbnd1lem1
27196 dchrisum0flblem1
27235 qabvexp
27353 ostth2lem2
27361 ostth3
27365 rusgrnumwwlk
29484 nexple
33293 faclim
35008 faclim2
35010 knoppndvlem14
35704 lcmineqlem12
41211 aks4d1p8
41258 nn0rppwr
41526 nn0expgcd
41528 flt0
41681 fltnltalem
41706 mzpexpmpt
41785 pell14qrexpclnn0
41906 pellfund14
41938 rmxy0
41964 jm2.17a
42001 jm2.17b
42002 jm2.18
42029 jm2.23
42037 expdioph
42064 cnsrexpcl
42209 binomcxplemnotnn0
43417 dvnxpaek
44957 wallispilem2
45081 etransclem24
45273 etransclem25
45274 etransclem35
45284 lighneallem3
46574 lighneallem4
46577 altgsumbcALT
47118 expnegico01
47287 digexp
47381 dig1
47382 |