Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
ℝcr 11051 -cneg 11387 |
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 2708 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 ax-resscn 11109 ax-1cn 11110 ax-icn 11111 ax-addcl 11112 ax-addrcl 11113 ax-mulcl 11114 ax-mulrcl 11115 ax-mulcom 11116 ax-addass 11117 ax-mulass 11118 ax-distr 11119 ax-i2m1 11120 ax-1ne0 11121 ax-1rid 11122 ax-rnegex 11123 ax-rrecex 11124 ax-cnre 11125 ax-pre-lttri 11126 ax-pre-lttrn 11127 ax-pre-ltadd 11128 |
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 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3066 df-rex 3075 df-reu 3355 df-rab 3409 df-v 3448 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-po 5546 df-so 5547 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-riota 7314 df-ov 7361 df-oprab 7362 df-mpo 7363 df-er 8649 df-en 8885 df-dom 8886 df-sdom 8887 df-pnf 11192 df-mnf 11193 df-ltxr 11195 df-sub 11388 df-neg 11389 |
This theorem is referenced by: ltord2
11685 leord2
11686 eqord2
11687 possumd
11781 recgt0
12002 riotaneg
12135 negiso
12136 nn0negleid
12466 difgtsumgt
12467 nnnegz
12503 prodge0rd
13023 modsub12d
13834 monoord2
13940 discr1
14143 discr
14144 recj
15010 reneg
15011 imcj
15018 imneg
15019 abslt
15200 absle
15201 o1lo1
15420 o1lo12
15421 icco1
15423 rlimrege0
15462 lo1sub
15514 iseraltlem2
15568 infcvgaux1i
15743 absefib
16081 efieq1re
16082 moddvds
16148 bitscmp
16319 bitsinv1lem
16322 mulgnegnn
18887 cnsubrg
20860 xrhmeo
24312 pjthlem1
24804 ivth2
24822 ovolshft
24878 shftmbl
24905 volsup2
24972 volivth
24974 mbfmulc2lem
25014 mbfposr
25019 mbfposb
25020 ismbf3d
25021 mbfmulc2
25030 mbfinf
25032 mbfi1fseqlem4
25086 mbfi1fseqlem5
25087 mbfi1fseqlem6
25088 mbfi1flimlem
25090 itg2monolem1
25118 iblposlem
25159 iblre
25161 itgreval
25164 itgneg
25171 i1fibl
25175 itgitg1
25176 itgle
25177 ibladd
25188 itgaddlem2
25191 iblabslem
25195 itgmulc2lem2
25200 itgmulc2
25201 bddiblnc
25209 dvferm2lem
25353 dvferm2
25354 rolle
25357 dvivth
25377 lhop2
25382 dvfsumge
25389 dvfsumlem2
25394 dvfsum2
25401 coseq0negpitopi
25863 tanabsge
25866 tanord
25897 tanregt0
25898 abslogimle
25932 logcj
25964 argimgt0
25970 logdiv2
25975 logcnlem3
26002 logccv
26021 abscxpbnd
26109 logreclem
26115 asinlem3a
26223 asinneg
26239 atanlogsublem
26268 atantan
26276 atans2
26284 birthdaylem3
26306 cxplim
26324 amgmlem
26342 emcllem7
26354 zetacvg
26367 eldmgm
26374 lgamgulmlem2
26382 lgsneg
26672 lgsdilem
26675 lgseisenlem1
26726 pntpbnd1
26937 pntibndlem2
26942 padicabvcxp
26983 ostth3
26989 axsegconlem9
27877 nvabs
29617 pjhthlem1
30336 xlt2addrd
31666 ccfldextdgrr
32359 xrge0iifcnv
32517 xrge0iifiso
32519 xrge0iifhom
32521 dya2ub
32873 sgnmul
33145 signsply0
33166 fdvneggt
33216 fdvnegge
33218 climlec3
34309 poimirlem29
36110 itg2gt0cn
36136 ibladdnc
36138 itgaddnclem2
36140 iblabsnclem
36144 itgmulc2nclem2
36148 itgmulc2nc
36149 ftc1anclem5
36158 dvasin
36165 areacirclem1
36169 areacirclem4
36172 areacirclem5
36173 areacirc
36174 oexpreposd
40810 3cubeslem4
41015 pellexlem6
41160 pell1234qrdich
41187 acongeq
41310 sqrtcval
41920 radcnvrat
42601 binomcxplemdvbinom
42640 binomcxplemnotnn0
42643 infnsuprnmpt
43485 neglt
43525 fperiodmul
43545 supsubc
43594 ltmulneg
43634 rexabslelem
43660 supminfrnmpt
43687 leneg2d
43690 leneg3d
43699 supminfxr
43706 climliminflimsupd
44049 liminfreuzlem
44050 liminfltlem
44052 stoweidlem1
44249 stoweidlem7
44255 stoweidlem13
44261 stoweidlem23
44271 stoweidlem34
44282 stoweidlem42
44290 stoweidlem47
44295 stirlinglem6
44327 stirlinglem10
44331 fourierdlem24
44379 fourierdlem39
44394 fourierdlem40
44395 fourierdlem43
44398 fourierdlem44
44399 fourierdlem46
44400 fourierdlem48
44402 fourierdlem49
44403 fourierdlem58
44412 fourierdlem62
44416 fourierdlem72
44426 fourierdlem78
44432 fourierdlem83
44437 fourierdlem85
44439 fourierdlem88
44442 fourierdlem92
44446 fourierdlem97
44451 fourierdlem103
44457 fourierdlem104
44458 fourierdlem109
44463 fourierdlem111
44465 fourierdlem112
44466 sqwvfoura
44476 etransclem23
44505 etransclem46
44528 hoicvr
44796 hoicvrrex
44804 smfinflem
45065 smfliminflem
45078 finfdm
45094 smfinfdmmbllem
45096 sigaradd
45114 sqrtnegnre
45546 proththd
45813 requad01
45820 requad1
45821 requad2
45822 dignn0flhalflem1
46708 eenglngeehlnmlem1
46830 eenglngeehlnmlem2
46831 line2ylem
46844 itscnhlc0yqe
46852 itsclquadb
46869 itscnhlinecirc02p
46878 amgmwlem
47256 |