Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1539
∈ wcel 2104 (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 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-1cn 11170 ax-addrcl 11173 ax-rnegex 11183 ax-cnre 11185 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-sbc 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-iota 6494 df-fun 6544 df-fv 6550 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
25959 plyco
25990 vieta1
26061 abelthlem9
26188 advlogexp
26399 cxpmul2
26433 nnlogbexp
26522 ftalem5
26817 0sgm
26884 1sgmprm
26938 dchrptlem2
27004 bposlem5
27027 lgsval2lem
27046 lgsmod
27062 lgsdilem2
27072 lgsne0
27074 chebbnd1lem1
27208 dchrisum0flblem1
27247 qabvexp
27365 ostth2lem2
27373 ostth3
27377 rusgrnumwwlk
29496 nexple
33305 faclim
35020 faclim2
35022 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
44956 wallispilem2
45080 etransclem24
45272 etransclem25
45273 etransclem35
45283 lighneallem3
46573 lighneallem4
46576 altgsumbcALT
47117 expnegico01
47286 digexp
47380 dig1
47381 |