Colors of
variables: wff set class |
Syntax hints:
= wceq 1353 ∈ wcel 2148
(class class class)co 5875 ℂcc 7809
0cc0 7811 + caddc 7814 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1cn 7904 ax-icn 7906 ax-addcl 7907 ax-mulcl 7909 ax-addcom 7911 ax-i2m1 7916 ax-0id 7919 |
This theorem depends on definitions:
df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: ine0
8351 inelr
8541 muleqadd
8625 0p1e1
9033 iap0
9142 num0h
9395 nummul1c
9432 decrmac
9441 decmul1
9447 fz0tp
10122 fz0to4untppr
10124 fzo0to3tp
10219 rei
10908 imi
10909 resqrexlemover
11019 ef01bndlem
11764 efhalfpi
14223 sinq34lt0t
14255 ex-fac
14483 |