Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 ≠ wne 2941
class class class wbr 5149 (class class class)co 7409
ℝcr 11109 0cc0 11110
1c1 11111 · cmul 11115
< clt 11248 |
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 ax-pre-mulgt0 11187 |
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-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 |
This theorem is referenced by: 0le1
11737 eqneg
11934 elimgt0
12052 ltp1
12054 ltm1
12056 recgt0
12060 mulgt1
12073 reclt1
12109 recgt1
12110 recgt1i
12111 recp1lt1
12112 recreclt
12113 recgt0ii
12120 inelr
12202 nnge1
12240 nngt0
12243 0nnnALT
12249 nnrecgt0
12255 2pos
12315 3pos
12317 4pos
12319 5pos
12321 6pos
12322 7pos
12323 8pos
12324 9pos
12325 neg1lt0
12329 halflt1
12430 nn0p1gt0
12501 elnnnn0c
12517 elnnz1
12588 nn0lt10b
12624 recnz
12637 1rp
12978 divlt1lt
13043 divle1le
13044 ledivge1le
13045 nnledivrp
13086 xmulrid
13258 0nelfz1
13520 fz10
13522 fzpreddisj
13550 elfznelfzob
13738 1mod
13868 expgt1
14066 ltexp2a
14131 expcan
14134 ltexp2
14135 leexp2
14136 leexp2a
14137 expnbnd
14195 expnlbnd
14196 expnlbnd2
14197 expmulnbnd
14198 discr1
14202 bcn1
14273 hashnn0n0nn
14351 s2fv0
14838 swrd2lsw
14903 2swrd2eqwrdeq
14904 sgn1
15039 resqrex
15197 mulcn2
15540 cvgrat
15829 bpoly4
16003 cos1bnd
16130 sin01gt0
16133 sincos1sgn
16136 ruclem8
16180 p1modz1
16204 nnoddm1d2
16329 sadcadd
16399 dvdsnprmd
16627 isprm7
16645 divdenle
16685 43prm
17055 plendxnocndx
17329 ipostr
18482 srgbinomlem4
20052 abvtrivd
20448 gzrngunit
21011 znidomb
21117 psgnodpmr
21143 thlleOLD
21252 leordtval2
22716 mopnex
24028 dscopn
24082 metnrmlem1a
24374 xrhmph
24463 evth
24475 xlebnum
24481 vitalilem5
25129 vitali
25130 ply1remlem
25680 plyremlem
25817 plyrem
25818 vieta1lem2
25824 reeff1olem
25958 sinhalfpilem
25973 rplogcl
26112 logtayllem
26167 cxplt
26202 cxple
26203 atanlogaddlem
26418 ressatans
26439 rlimcnp
26470 rlimcnp2
26471 cxp2limlem
26480 cxp2lim
26481 cxploglim2
26483 amgmlem
26494 emcllem2
26501 harmonicubnd
26514 fsumharmonic
26516 zetacvg
26519 ftalem1
26577 ftalem2
26578 chpchtsum
26722 chpub
26723 mersenne
26730 perfectlem2
26733 efexple
26784 chebbnd1
26975 dchrmusumlema
26996 dchrvmasumlem2
27001 dchrvmasumiflem1
27004 dchrisum0flblem2
27012 dchrisum0lema
27017 dchrisum0lem1
27019 dchrisum0lem2a
27020 mulog2sumlem1
27037 chpdifbndlem1
27056 chpdifbnd
27058 selberg3lem1
27060 pntrmax
27067 pntrsumo1
27068 pntpbnd1a
27088 pntpbnd2
27090 pntibndlem1
27092 pntlem3
27112 pnt
27117 ostth2lem1
27121 ostth2lem3
27138 ostth2lem4
27139 axcontlem2
28223 wwlksn0s
29115 clwwlkf1
29302 esumcst
33061 hasheuni
33083 ballotlemi1
33501 ballotlemic
33505 sgnnbi
33544 sgnpbi
33545 sgnmulsgp
33549 signsply0
33562 signswch
33572 hgt750lem
33663 unblimceq0
35383 knoppndvlem1
35388 knoppndvlem2
35389 knoppndvlem7
35394 knoppndvlem13
35400 knoppndvlem14
35401 knoppndvlem15
35402 knoppndvlem17
35404 knoppndvlem20
35407 irrdiff
36207 poimirlem22
36510 poimirlem31
36519 asindmre
36571 areacirclem4
36579 60gcd7e1
40870 3lexlogpow5ineq2
40920 aks4d1p1p2
40935 aks4d1p7
40948 aks4d1p8d2
40950 aks4d1p8d3
40951 aks4d1p8
40952 aks4d1p9
40953 sticksstones11
40972 2xp3dxp2ge1d
41022 3cubeslem1
41422 pellexlem2
41568 pellexlem6
41572 pell14qrgt0
41597 elpell1qr2
41610 pellfundex
41624 pellfundrp
41626 rmxypos
41686 relexp01min
42464 imo72b2
42924 radcnvrat
43073 reclt0d
44097 sqrlearg
44266 sumnnodd
44346 liminf10ex
44490 liminfltlimsupex
44497 dvnmul
44659 stoweidlem7
44723 stoweidlem36
44752 stoweidlem38
44754 stoweidlem42
44758 stoweidlem51
44767 stoweidlem59
44775 stirlinglem5
44794 stirlinglem7
44796 stirlinglem10
44799 stirlinglem11
44800 stirlinglem12
44801 stirlinglem15
44804 dirkeritg
44818 fourierdlem11
44834 fourierdlem30
44853 fourierdlem47
44869 fourierdlem79
44901 fourierdlem103
44925 fourierdlem104
44926 fouriersw
44947 etransclem4
44954 etransclem31
44981 etransclem32
44982 etransclem35
44985 etransclem41
44991 salexct2
45055 hoidmvlelem1
45311 tworepnotupword
45600 m1mod0mod1
46037 nfermltl2rev
46411 m1modmmod
47207 regt1loggt0
47222 rege1logbrege0
47244 nnlog2ge0lt1
47252 eenglngeehlnmlem2
47424 amgmwlem
47849 |