Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 ≠ wne 2944
class class class wbr 5110 (class class class)co 7362
ℝcr 11057 0cc0 11058
1c1 11059 · cmul 11063
< clt 11196 |
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 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-resscn 11115 ax-1cn 11116 ax-icn 11117 ax-addcl 11118 ax-addrcl 11119 ax-mulcl 11120 ax-mulrcl 11121 ax-mulcom 11122 ax-addass 11123 ax-mulass 11124 ax-distr 11125 ax-i2m1 11126 ax-1ne0 11127 ax-1rid 11128 ax-rnegex 11129 ax-rrecex 11130 ax-cnre 11131 ax-pre-lttri 11132 ax-pre-lttrn 11133 ax-pre-ltadd 11134 ax-pre-mulgt0 11135 |
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 3357 df-rab 3411 df-v 3450 df-sbc 3745 df-csb 3861 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-po 5550 df-so 5551 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11198 df-mnf 11199 df-xr 11200 df-ltxr 11201 df-le 11202 df-sub 11394 df-neg 11395 |
This theorem is referenced by: 0le1
11685 eqneg
11882 elimgt0
12000 ltp1
12002 ltm1
12004 recgt0
12008 mulgt1
12021 reclt1
12057 recgt1
12058 recgt1i
12059 recp1lt1
12060 recreclt
12061 recgt0ii
12068 inelr
12150 nnge1
12188 nngt0
12191 0nnnALT
12197 nnrecgt0
12203 2pos
12263 3pos
12265 4pos
12267 5pos
12269 6pos
12270 7pos
12271 8pos
12272 9pos
12273 neg1lt0
12277 halflt1
12378 nn0p1gt0
12449 elnnnn0c
12465 elnnz1
12536 nn0lt10b
12572 recnz
12585 1rp
12926 divlt1lt
12991 divle1le
12992 ledivge1le
12993 nnledivrp
13034 xmulid1
13205 0nelfz1
13467 fz10
13469 fzpreddisj
13497 elfznelfzob
13685 1mod
13815 expgt1
14013 ltexp2a
14078 expcan
14081 ltexp2
14082 leexp2
14083 leexp2a
14084 expnbnd
14142 expnlbnd
14143 expnlbnd2
14144 expmulnbnd
14145 discr1
14149 bcn1
14220 hashnn0n0nn
14298 s2fv0
14783 swrd2lsw
14848 2swrd2eqwrdeq
14849 sgn1
14984 resqrex
15142 mulcn2
15485 cvgrat
15775 bpoly4
15949 cos1bnd
16076 sin01gt0
16079 sincos1sgn
16082 ruclem8
16126 p1modz1
16150 nnoddm1d2
16275 sadcadd
16345 dvdsnprmd
16573 isprm7
16591 divdenle
16631 43prm
17001 plendxnocndx
17272 ipostr
18425 srgbinomlem4
19967 abvtrivd
20315 gzrngunit
20879 znidomb
20984 psgnodpmr
21010 thlleOLD
21119 leordtval2
22579 mopnex
23891 dscopn
23945 metnrmlem1a
24237 xrhmph
24326 evth
24338 xlebnum
24344 vitalilem5
24992 vitali
24993 ply1remlem
25543 plyremlem
25680 plyrem
25681 vieta1lem2
25687 reeff1olem
25821 sinhalfpilem
25836 rplogcl
25975 logtayllem
26030 cxplt
26065 cxple
26066 atanlogaddlem
26279 ressatans
26300 rlimcnp
26331 rlimcnp2
26332 cxp2limlem
26341 cxp2lim
26342 cxploglim2
26344 amgmlem
26355 emcllem2
26362 harmonicubnd
26375 fsumharmonic
26377 zetacvg
26380 ftalem1
26438 ftalem2
26439 chpchtsum
26583 chpub
26584 mersenne
26591 perfectlem2
26594 efexple
26645 chebbnd1
26836 dchrmusumlema
26857 dchrvmasumlem2
26862 dchrvmasumiflem1
26865 dchrisum0flblem2
26873 dchrisum0lema
26878 dchrisum0lem1
26880 dchrisum0lem2a
26881 mulog2sumlem1
26898 chpdifbndlem1
26917 chpdifbnd
26919 selberg3lem1
26921 pntrmax
26928 pntrsumo1
26929 pntpbnd1a
26949 pntpbnd2
26951 pntibndlem1
26953 pntlem3
26973 pnt
26978 ostth2lem1
26982 ostth2lem3
26999 ostth2lem4
27000 axcontlem2
27956 wwlksn0s
28848 clwwlkf1
29035 esumcst
32702 hasheuni
32724 ballotlemi1
33142 ballotlemic
33146 sgnnbi
33185 sgnpbi
33186 sgnmulsgp
33190 signsply0
33203 signswch
33213 hgt750lem
33304 unblimceq0
34999 knoppndvlem1
35004 knoppndvlem2
35005 knoppndvlem7
35010 knoppndvlem13
35016 knoppndvlem14
35017 knoppndvlem15
35018 knoppndvlem17
35020 knoppndvlem20
35023 irrdiff
35826 poimirlem22
36129 poimirlem31
36138 asindmre
36190 areacirclem4
36198 60gcd7e1
40491 3lexlogpow5ineq2
40541 aks4d1p1p2
40556 aks4d1p7
40569 aks4d1p8d2
40571 aks4d1p8d3
40572 aks4d1p8
40573 aks4d1p9
40574 sticksstones11
40593 2xp3dxp2ge1d
40643 3cubeslem1
41036 pellexlem2
41182 pellexlem6
41186 pell14qrgt0
41211 elpell1qr2
41224 pellfundex
41238 pellfundrp
41240 rmxypos
41300 relexp01min
42059 imo72b2
42519 radcnvrat
42668 reclt0d
43695 sqrlearg
43865 sumnnodd
43945 liminf10ex
44089 liminfltlimsupex
44096 dvnmul
44258 stoweidlem7
44322 stoweidlem36
44351 stoweidlem38
44353 stoweidlem42
44357 stoweidlem51
44366 stoweidlem59
44374 stirlinglem5
44393 stirlinglem7
44395 stirlinglem10
44398 stirlinglem11
44399 stirlinglem12
44400 stirlinglem15
44403 dirkeritg
44417 fourierdlem11
44433 fourierdlem30
44452 fourierdlem47
44468 fourierdlem79
44500 fourierdlem103
44524 fourierdlem104
44525 fouriersw
44546 etransclem4
44553 etransclem31
44580 etransclem32
44581 etransclem35
44584 etransclem41
44590 salexct2
44654 hoidmvlelem1
44910 tworepnotupword
45199 m1mod0mod1
45635 nfermltl2rev
46009 m1modmmod
46681 regt1loggt0
46696 rege1logbrege0
46718 nnlog2ge0lt1
46726 eenglngeehlnmlem2
46898 amgmwlem
47323 |