Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2104
ℝcr 11111 -cneg 11449 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 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 395
df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 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: ltord2
11747 leord2
11748 eqord2
11749 possumd
11843 recgt0
12064 riotaneg
12197 negiso
12198 nn0negleid
12528 difgtsumgt
12529 nnnegz
12565 prodge0rd
13085 modsub12d
13897 monoord2
14003 discr1
14206 discr
14207 recj
15075 reneg
15076 imcj
15083 imneg
15084 abslt
15265 absle
15266 o1lo1
15485 o1lo12
15486 icco1
15488 rlimrege0
15527 lo1sub
15579 iseraltlem2
15633 infcvgaux1i
15807 absefib
16145 efieq1re
16146 moddvds
16212 bitscmp
16383 bitsinv1lem
16386 mulgnegnn
19000 cnsubrg
21205 xrhmeo
24691 pjthlem1
25185 ivth2
25204 ovolshft
25260 shftmbl
25287 volsup2
25354 volivth
25356 mbfmulc2lem
25396 mbfposr
25401 mbfposb
25402 ismbf3d
25403 mbfmulc2
25412 mbfinf
25414 mbfi1fseqlem4
25468 mbfi1fseqlem5
25469 mbfi1fseqlem6
25470 mbfi1flimlem
25472 itg2monolem1
25500 iblposlem
25541 iblre
25543 itgreval
25546 itgneg
25553 i1fibl
25557 itgitg1
25558 itgle
25559 ibladd
25570 itgaddlem2
25573 iblabslem
25577 itgmulc2lem2
25582 itgmulc2
25583 bddiblnc
25591 dvferm2lem
25738 dvferm2
25739 rolle
25742 dvivth
25762 lhop2
25767 dvfsumge
25774 dvfsumlem2
25779 dvfsum2
25786 coseq0negpitopi
26249 tanabsge
26252 tanord
26283 tanregt0
26284 abslogimle
26318 logcj
26350 argimgt0
26356 logdiv2
26361 logcnlem3
26388 logccv
26407 abscxpbnd
26497 logreclem
26503 asinlem3a
26611 asinneg
26627 atanlogsublem
26656 atantan
26664 atans2
26672 birthdaylem3
26694 cxplim
26712 amgmlem
26730 emcllem7
26742 zetacvg
26755 eldmgm
26762 lgamgulmlem2
26770 lgsneg
27060 lgsdilem
27063 lgseisenlem1
27114 pntpbnd1
27325 pntibndlem2
27330 padicabvcxp
27371 ostth3
27377 axsegconlem9
28450 nvabs
30192 pjhthlem1
30911 xlt2addrd
32238 ccfldextdgrr
33035 xrge0iifcnv
33211 xrge0iifiso
33213 xrge0iifhom
33215 dya2ub
33567 sgnmul
33839 signsply0
33860 fdvneggt
33910 fdvnegge
33912 climlec3
35007 gg-dvfsumlem2
35469 poimirlem29
36820 itg2gt0cn
36846 ibladdnc
36848 itgaddnclem2
36850 iblabsnclem
36854 itgmulc2nclem2
36858 itgmulc2nc
36859 ftc1anclem5
36868 dvasin
36875 areacirclem1
36879 areacirclem4
36882 areacirclem5
36883 areacirc
36884 oexpreposd
41514 3cubeslem4
41729 pellexlem6
41874 pell1234qrdich
41901 acongeq
42024 sqrtcval
42694 radcnvrat
43375 binomcxplemdvbinom
43414 binomcxplemnotnn0
43417 infnsuprnmpt
44252 neglt
44292 fperiodmul
44312 supsubc
44361 ltmulneg
44400 rexabslelem
44426 supminfrnmpt
44453 leneg2d
44456 leneg3d
44465 supminfxr
44472 climliminflimsupd
44815 liminfreuzlem
44816 liminfltlem
44818 stoweidlem1
45015 stoweidlem7
45021 stoweidlem13
45027 stoweidlem23
45037 stoweidlem34
45048 stoweidlem42
45056 stoweidlem47
45061 stirlinglem6
45093 stirlinglem10
45097 fourierdlem24
45145 fourierdlem39
45160 fourierdlem40
45161 fourierdlem43
45164 fourierdlem44
45165 fourierdlem46
45166 fourierdlem48
45168 fourierdlem49
45169 fourierdlem58
45178 fourierdlem62
45182 fourierdlem72
45192 fourierdlem78
45198 fourierdlem83
45203 fourierdlem85
45205 fourierdlem88
45208 fourierdlem92
45212 fourierdlem97
45217 fourierdlem103
45223 fourierdlem104
45224 fourierdlem109
45229 fourierdlem111
45231 fourierdlem112
45232 sqwvfoura
45242 etransclem23
45271 etransclem46
45294 hoicvr
45562 hoicvrrex
45570 smfinflem
45831 smfliminflem
45844 finfdm
45860 smfinfdmmbllem
45862 sigaradd
45880 sqrtnegnre
46313 proththd
46580 requad01
46587 requad1
46588 requad2
46589 dignn0flhalflem1
47388 eenglngeehlnmlem1
47510 eenglngeehlnmlem2
47511 line2ylem
47524 itscnhlc0yqe
47532 itsclquadb
47549 itscnhlinecirc02p
47558 amgmwlem
47936 |