Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2106
(class class class)co 7405 ℝcr 11105
1c1 11107 − cmin 11440 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 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 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-ltxr 11249 df-sub 11442 df-neg 11443 |
This theorem is referenced by: lem1
12053 addltmul
12444 div4p1lem1div2
12463 nnunb
12464 suprzcl
12638 zbtwnre
12926 rebtwnz
12927 qbtwnre
13174 qbtwnxr
13175 xnn0lem1lt
13219 xrinfmsslem
13283 xrub
13287 reltre
13315 elfznelfzo
13733 fldiv4p1lem1div2
13796 fldiv4lem1div2uz2
13797 ceile
13810 intfracq
13820 fldiv
13821 m1modnnsub1
13878 expubnd
14138 bernneq2
14189 expnbnd
14191 cshwidxm1
14753 isercolllem1
15607 tgioo
24303 icoopnst
24446 mbfi1fseqlem6
25229 dvfsumlem1
25534 dvfsumlem2
25535 dgreq0
25770 advlog
26153 atanlogsublem
26409 birthdaylem3
26447 wilthlem1
26561 ftalem5
26570 ppiub
26696 chtublem
26703 chtub
26704 logfaclbnd
26714 logfacbnd3
26715 perfectlem2
26722 lgsval2lem
26799 lgsqrlem2
26839 gausslemma2dlem0c
26850 gausslemma2dlem1a
26857 lgseisenlem2
26868 lgseisen
26871 lgsquadlem1
26872 lgsquadlem2
26873 2lgslem1c
26885 2lgsoddprmlem2
26901 rplogsumlem1
26976 selberg2lem
27042 pntrsumo1
27057 pntpbnd1a
27077 colinearalglem4
28156 axlowdimlem16
28204 axeuclidlem
28209 nbusgrvtxm1
28625 pthdlem1
29012 crctcshwlkn0lem1
29053 wwlksm1edg
29124 clwwlkel
29288 clwwlknonex2lem2
29350 numclwwlk7
29633 addltmulALT
31686 cvmliftlem2
34265 cvmliftlem6
34269 cvmliftlem8
34271 cvmliftlem9
34272 cvmliftlem10
34273 gg-dvfsumlem2
35171 irrdiff
36195 iooelexlt
36231 ltflcei
36464 poimirlem12
36488 poimirlem13
36489 poimirlem14
36490 poimirlem31
36507 poimirlem32
36508 itg2addnclem2
36528 itg2addnclem3
36529 monoords
43993 supxrgere
44029 infleinflem2
44067 unb2ltle
44111 limsupre3lem
44434 xlimxrre
44533 xlimmnfv
44536 stoweidlem14
44716 stoweidlem34
44736 fourierdlem11
44820 fourierdlem12
44821 fourierdlem15
44824 fourierdlem42
44851 fourierdlem50
44858 fourierdlem64
44872 fourierdlem79
44887 smfresal
45490 zm1nn
45996 m1mod0mod1
46023 nn0oALTV
46350 perfectALTVlem2
46376 m1modmmod
47160 difmodm1lt
47161 flnn0div2ge
47172 logbpw2m1
47206 fllog2
47207 |