Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 (class class class)co 7362
1c1 11059 · cmul 11063
2c2 12215 |
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-ext 2708 ax-resscn 11115 ax-1cn 11116 ax-icn 11117 ax-addcl 11118 ax-mulcl 11120 ax-mulcom 11122 ax-mulass 11124 ax-distr 11125 ax-1rid 11128 ax-cnre 11131 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-iota 6453 df-fv 6509 df-ov 7365 df-2 12223 |
This theorem is referenced by: decbin2
12766 expubnd
14089 01sqrexlem7
15140 trirecip
15755 bpoly3
15948 fsumcube
15950 ege2le3
15979 cos2tsin
16068 cos2bnd
16077 odd2np1
16230 opoe
16252 flodddiv4
16302 2mulprm
16576 pythagtriplem4
16698 2503lem2
17017 2503lem3
17018 4001lem4
17023 4001prm
17024 htpycc
24359 pco1
24394 pcohtpylem
24398 pcopt
24401 pcorevlem
24405 ovolunlem1a
24876 cos2pi
25849 coskpi
25895 dcubic2
26210 dcubic
26212 basellem3
26448 chtublem
26575 bcp1ctr
26643 bclbnd
26644 bposlem1
26648 bposlem2
26649 bposlem5
26652 2lgslem3d1
26767 2sqreultlem
26811 2sqreunnltlem
26814 chebbnd1lem1
26833 chebbnd1lem3
26835 chebbnd1
26836 frgrregord013
29381 ex-ind-dvds
29447 wrdt2ind
31849 knoppndvlem12
35015 heiborlem6
36304 3lexlogpow5ineq1
40540 aks4d1p1
40562 2np3bcnp1
40581 2ap1caineq
40582 flt4lem7
41026 jm2.23
41349 sumnnodd
43945 wallispilem4
44383 wallispi2lem1
44386 wallispi2lem2
44387 wallispi2
44388 stirlinglem11
44399 dirkertrigeqlem1
44413 fouriersw
44546 fmtnorec4
45815 lighneallem2
45872 lighneallem3
45873 3exp4mod41
45882 opoeALTV
45949 fppr2odd
45997 8exp8mod9
46002 ackval2
46842 ackval2012
46851 |