Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∈ wcel 2105 class class class wbr 5092
(class class class)co 7337 ℝcr 10971
0cc0 10972 < clt 11110
− cmin 11306 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 ax-un 7650 ax-resscn 11029 ax-1cn 11030 ax-icn 11031 ax-addcl 11032 ax-addrcl 11033 ax-mulcl 11034 ax-mulrcl 11035 ax-mulcom 11036 ax-addass 11037 ax-mulass 11038 ax-distr 11039 ax-i2m1 11040 ax-1ne0 11041 ax-1rid 11042 ax-rnegex 11043 ax-rrecex 11044 ax-cnre 11045 ax-pre-lttri 11046 ax-pre-lttrn 11047 ax-pre-ltadd 11048 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-po 5532 df-so 5533 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-iota 6431 df-fun 6481 df-fn 6482 df-f 6483 df-f1 6484 df-fo 6485 df-f1o 6486 df-fv 6487 df-riota 7293 df-ov 7340 df-oprab 7341 df-mpo 7342 df-er 8569 df-en 8805 df-dom 8806 df-sdom 8807 df-pnf 11112 df-mnf 11113 df-ltxr 11115 df-sub 11308 df-neg 11309 |
This theorem is referenced by: possumd
11701 ltmul1a
11925 cshwcsh2id
14640 sqrlem7
15059 fsumlt
15611 bpoly4
15868 sin01gt0
15998 nno
16190 pythagtriplem10
16618 evth
24228 minveclem4
24702 ismbf3d
24924 itg2seq
25013 dvferm1lem
25254 dvferm2lem
25256 mvth
25262 dvlip
25263 dvgt0
25274 dvlt0
25275 dvge0
25276 dvcvx
25290 ftc1lem4
25309 pilem2
25717 cosordlem
25792 lgamgulmlem2
26285 lgsquadlem1
26634 brbtwn2
27562 axpaschlem
27597 axcontlem8
27628 crctcshwlkn0
28474 clwlkclwwlklem2a4
28649 clwwlkext2edg
28708 minvecolem4
29530 cycpmrn
31697 sgnsub
32811 signslema
32841 fdvposlt
32879 tgoldbachgtde
32940 dnibndlem5
34758 unbdqndv2lem2
34786 knoppndvlem2
34789 knoppndvlem21
34808 poimirlem7
35897 itg2addnclem
35941 itg2gt0cn
35945 ftc1cnnclem
35961 areacirclem1
35978 areacirc
35983 sticksstones12a
40378 metakunt29
40418 metakunt30
40419 3cubeslem1
40776 irrapxlem3
40916 pell14qrgt0
40951 rmspecnonsq
40999 rmspecfund
41001 rmspecpos
41009 jm3.1lem1
41110 radcnvrat
42261 supxrgere
43215 supxrgelem
43219 dvbdfbdioolem1
43813 dvbdfbdioolem2
43814 ioodvbdlimc1lem1
43816 ioodvbdlimc1lem2
43817 ioodvbdlimc2lem
43819 dvnxpaek
43827 wallispilem4
43953 wallispi2lem1
43956 stirlinglem11
43969 fourierdlem4
43996 fourierdlem6
43998 fourierdlem7
43999 fourierdlem19
44011 fourierdlem26
44018 fourierdlem41
44033 fourierdlem42
44034 fourierdlem48
44039 fourierdlem49
44040 fourierdlem51
44042 fourierdlem61
44052 fourierdlem63
44054 fourierdlem64
44055 fourierdlem65
44056 fourierdlem71
44062 fourierdlem79
44070 fourierdlem89
44080 fourierdlem90
44081 fourierdlem91
44082 fouriersw
44116 etransclem15
44134 etransclem24
44143 etransclem25
44144 etransclem35
44154 ioorrnopnlem
44189 hoidmvlelem2
44479 hoiqssbllem2
44506 iunhoiioolem
44558 zm1nn
45153 nnoALTV
45506 fllog2
46273 dignn0flhalflem1
46320 eenglngeehlnmlem2
46443 2itscp
46486 |