Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 (class class class)co 7362
+ caddc 11061 ·
cmul 11063 2c2 12215
4c4 12217 |
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-addass 11123 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 df-3 12224
df-4 12225 |
This theorem is referenced by: 4d2e2
12330 halfpm6th
12381 div4p1lem1div2
12415 3halfnz
12589 decbin0
12765 fldiv4lem1div2uz2
13748 sq2
14108 sq4e2t8
14110 discr
14150 sqoddm1div8
14153 faclbnd2
14198 4bc2eq6
14236 amgm2
15261 bpoly3
15948 sin4lt0
16084 z4even
16261 flodddiv4
16302 flodddiv4t2lthalf
16305 4nprm
16578 2exp4
16964 2exp16
16970 5prm
16988 631prm
17006 1259lem1
17010 1259lem4
17013 2503lem1
17016 2503lem2
17017 2503lem3
17018 4001lem1
17020 4001lem2
17021 4001lem3
17022 4001prm
17024 pcoass
24403 minveclem2
24806 uniioombllem5
24967 uniioombl
24969 dveflem
25359 pilem2
25827 sinhalfpilem
25836 sincosq1lem
25870 tangtx
25878 sincos4thpi
25886 heron
26204 quad2
26205 dquartlem1
26217 dquart
26219 quart1
26222 atan1
26294 log2ublem3
26314 log2ub
26315 chtub
26576 bclbnd
26644 bpos1
26647 bposlem2
26649 bposlem6
26653 bposlem9
26656 gausslemma2dlem3
26732 m1lgs
26752 2lgslem1a2
26754 2lgslem3a
26760 2lgslem3b
26761 2lgslem3c
26762 2lgslem3d
26763 pntibndlem2
26955 pntlemg
26962 pntlemr
26966 ex-fl
29433 minvecolem2
29859 polid2i
30141 quad3
34298 420lcm8e840
40497 3exp7
40539 3lexlogpow5ineq1
40540 3lexlogpow2ineq2
40545 3lexlogpow5ineq5
40546 aks4d1p1p2
40556 aks4d1p1
40562 2ap1caineq
40582 flt4lem
41012 3cubeslem3l
41038 3cubeslem3r
41039 wallispi2lem1
44386 wallispi2lem2
44387 stirlinglem3
44391 stirlinglem10
44398 fmtnorec4
45815 2exp340mod341
45999 8exp8mod9
46002 ackval2012
46851 |