Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∈ wcel 2106 class class class wbr 5148
(class class class)co 7411 ℝcr 11111
0cc0 11112 < clt 11252
− cmin 11448 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11254 df-mnf 11255 df-ltxr 11257 df-sub 11450 df-neg 11451 |
This theorem is referenced by: possumd
11843 ltmul1a
12067 cshwcsh2id
14783 01sqrexlem7
15199 fsumlt
15750 bpoly4
16007 sin01gt0
16137 nno
16329 pythagtriplem10
16757 evth
24699 minveclem4
25173 ismbf3d
25395 itg2seq
25484 dvferm1lem
25725 dvferm2lem
25727 mvth
25733 dvlip
25734 dvgt0
25745 dvlt0
25746 dvge0
25747 dvcvx
25761 ftc1lem4
25780 pilem2
26188 cosordlem
26263 lgamgulmlem2
26758 lgsquadlem1
27107 brbtwn2
28418 axpaschlem
28453 axcontlem8
28484 crctcshwlkn0
29330 clwlkclwwlklem2a4
29505 clwwlkext2edg
29564 minvecolem4
30388 cycpmrn
32560 sgnsub
33829 signslema
33859 fdvposlt
33897 tgoldbachgtde
33958 dnibndlem5
35661 unbdqndv2lem2
35689 knoppndvlem2
35692 knoppndvlem21
35711 poimirlem7
36798 itg2addnclem
36842 itg2gt0cn
36846 ftc1cnnclem
36862 areacirclem1
36879 areacirc
36884 sticksstones12a
41279 metakunt29
41319 metakunt30
41320 3cubeslem1
41724 irrapxlem3
41864 pell14qrgt0
41899 rmspecnonsq
41947 rmspecfund
41949 rmspecpos
41957 jm3.1lem1
42058 radcnvrat
43375 supxrgere
44342 supxrgelem
44346 dvbdfbdioolem1
44943 dvbdfbdioolem2
44944 ioodvbdlimc1lem1
44946 ioodvbdlimc1lem2
44947 ioodvbdlimc2lem
44949 dvnxpaek
44957 wallispilem4
45083 wallispi2lem1
45086 stirlinglem11
45099 fourierdlem4
45126 fourierdlem6
45128 fourierdlem7
45129 fourierdlem19
45141 fourierdlem26
45148 fourierdlem41
45163 fourierdlem42
45164 fourierdlem48
45169 fourierdlem49
45170 fourierdlem51
45172 fourierdlem61
45182 fourierdlem63
45184 fourierdlem64
45185 fourierdlem65
45186 fourierdlem71
45192 fourierdlem79
45200 fourierdlem89
45210 fourierdlem90
45211 fourierdlem91
45212 fouriersw
45246 etransclem15
45264 etransclem24
45273 etransclem25
45274 etransclem35
45284 ioorrnopnlem
45319 hoidmvlelem2
45611 hoiqssbllem2
45638 iunhoiioolem
45690 zm1nn
46309 nnoALTV
46662 fllog2
47342 dignn0flhalflem1
47389 eenglngeehlnmlem2
47512 2itscp
47555 |