Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2105
(class class class)co 7337 ℂcc 10970
1c1 10973 + caddc 10975 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-1cn 11030 ax-addcl 11032 |
This theorem depends on definitions:
df-bi 206 df-an 397 |
This theorem is referenced by: nnsscn
12079 xp1d2m1eqxm1d2
12328 nneo
12505 zeo
12507 zeo2
12508 zesq
14042 facndiv
14103 faclbnd
14105 faclbnd6
14114 iseralt
15495 bcxmas
15646 trireciplem
15673 fallfacfwd
15845 bpolydiflem
15863 fsumcube
15869 odd2np1
16149 srgbinomlem3
19873 srgbinomlem4
19874 pcoass
24293 dvfsumabs
25293 ply1divex
25407 qaa
25589 aaliou3lem2
25609 abssinper
25783 advlogexp
25916 atantayl2
26194 basellem3
26338 basellem8
26343 lgseisenlem1
26629 lgsquadlem1
26634 pntrsumo1
26819 crctcshwlkn0lem6
28468 clwlkclwwlklem3
28653 fwddifnp1
34563 ltflcei
35870 itg2addnclem3
35935 pell14qrgapw
40960 binomcxplemrat
42289 sumnnodd
43507 dirkertrigeqlem1
43975 dirkertrigeqlem3
43977 dirkertrigeq
43978 fourierswlem
44107 fmtnorec4
45352 lighneallem4b
45412 ackval1
46378 ackval2
46379 |