Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 (class class class)co 7409
0cc0 11110 1c1 11111
− cmin 11444 |
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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-ltxr 11253 df-sub 11446 |
This theorem is referenced by: nnm1nn0
12513 xov1plusxeqvd
13475 fseq1p1m1
13575 elfzp1b
13578 elfzm1b
13579 elfznelfzo
13737 fldiv4lem1div2
13802 fzennn
13933 faclbnd4lem4
14256 lsw1
14517 ccat2s1p2
14580 revs1
14715 arisum
15806 pwdif
15814 geo2sum
15819 bpoly1
15995 nn0o
16326 exprmfct
16641 phiprmpw
16709 phiprm
16710 odzdvds
16728 prmpwdvds
16837 prmreclem4
16852 vdwapun
16907 sylow1lem1
19466 efgs1b
19604 efgsfo
19607 efgredlema
19608 efgredeu
19620 imasdsf1olem
23879 htpycom
24492 htpycc
24496 reparphti
24513 pcoval2
24532 pcocn
24533 pcohtpylem
24535 pcopt
24538 pcorevcl
24541 pcorevlem
24542 pi1xfrcnv
24573 dvexp
25470 dvlipcn
25511 dvply1
25797 vieta1
25825 pserdvlem2
25940 abelthlem2
25944 coseq1
26034 advlogexp
26163 logtayl
26168 cxpaddlelem
26259 isosctrlem2
26324 asin1
26399 leibpilem2
26446 log2ublem3
26453 scvxcvx
26490 1sgmprm
26702 dchrfi
26758 lgslem4
26803 lgsne0
26838 lgsquad2lem2
26888 2lgsoddprmlem3a
26913 rpvmasumlem
26990 selberg2lem
27053 logdivbnd
27059 pntrsumo1
27068 pntrlog2bndlem4
27083 pntrlog2bndlem5
27084 pntpbnd2
27090 ostth2lem2
27137 axpaschlem
28198 elntg2
28243 wwlksn0s
29115 clwwlkn1
29294 hst1h
31480 st0
31502 archirngz
32335 drngdimgt0
32703 lmatfval
32794 lmat22e11
32798 fib2
33401 ballotlem4
33497 ballotlemi1
33501 ballotlemii
33502 ballotlemic
33505 ballotlem1c
33506 ballotlemfrceq
33527 signsvtn0
33581 signstfveq0a
33587 subfacp1lem6
34176 cvxpconn
34233 cvxsconn
34234 cvmliftlem10
34285 cvmliftlem13
34287 bcprod
34708 gg-reparphti
35172 poimirlem3
36491 poimirlem4
36492 poimirlem13
36501 poimirlem19
36507 lcmfunnnd
40877 lcm1un
40878 lcmineqlem10
40903 lcmineqlem12
40905 lcmineqlem18
40911 metakunt30
41014 mapfzcons
41454 irrapxlem3
41562 2nn0ind
41684 jm2.18
41727 jm2.23
41735 dvnmul
44659 stoweidlem1
44717 stoweidlem11
44727 stoweidlem26
44742 stoweidlem34
44750 stoweidlem45
44761 wallispilem3
44783 wallispi
44786 stirlinglem5
44794 sqwvfourb
44945 upwordsing
45598 proththdlem
46281 341fppr2
46402 nnsgrpnmnd
46588 pzriprng1ALT
46820 blen1b
47274 nn0sumshdiglem1
47307 |