Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2104
class class class wbr 5149 (class class class)co 7413
ℝcr 11113 1c1 11115
< clt 11254 −
cmin 11450 |
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 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7729 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191 |
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 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 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-er 8707 df-en 8944 df-dom 8945 df-sdom 8946 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11452 df-neg 11453 |
This theorem is referenced by: suprzcl
12648 fzsuc2
13565 fzm1
13587 m1modnnsub1
13888 cshwidxm1
14763 fsumm1
15703 isumsplit
15792 climcndslem1
15801 bitsfzolem
16381 fldivp1
16836 4sqlem12
16895 ram0
16961 sylow1lem1
19509 dgreq0
26013 atanlogsublem
26654 birthdaylem3
26692 wilthlem1
26806 ftalem5
26815 basellem5
26823 lgsval2lem
27044 lgsqrlem2
27084 gausslemma2dlem0c
27095 lgsquadlem1
27117 lgsquadlem2
27118 pntrsumbnd2
27304 axlowdimlem16
28480 pthdlem1
29288 clwwlkel
29564 clwwlknonex2lem2
29626 xlt2addrd
32236 cycpmco2lem6
32558 cvmliftlem6
34577 cvmliftlem8
34579 cvmliftlem9
34580 cvmliftlem10
34581 bcprod
35010 iooelexlt
36548 poimirlem1
36794 poimirlem2
36795 poimirlem6
36799 poimirlem7
36800 poimirlem8
36801 poimirlem12
36805 poimirlem15
36808 poimirlem16
36809 poimirlem17
36810 poimirlem19
36812 poimirlem20
36813 poimirlem21
36814 poimirlem22
36815 poimirlem23
36816 poimirlem26
36819 mettrifi
36930 aks4d1p1
41249 sticksstones10
41279 sticksstones12a
41281 metakunt18
41310 metakunt20
41312 metakunt24
41316 irrapxlem1
41864 rmspecsqrtnq
41948 acongeq
42026 monoords
44307 fzisoeu
44310 fzdifsuc2
44320 infleinflem2
44381 unb2ltle
44425 limsupre3lem
44748 xlimxrre
44847 xlimmnfv
44850 iblspltprt
44989 itgspltprt
44995 stoweidlem11
45027 stoweidlem14
45030 fourierdlem11
45134 fourierdlem12
45135 fourierdlem15
45138 fourierdlem41
45164 fourierdlem48
45170 fourierdlem49
45171 fourierdlem50
45172 fourierdlem79
45201 ioorrnopnxrlem
45322 iundjiun
45476 lswn0
46412 bgoldbtbndlem4
46776 m1modmmod
47296 logbpw2m1
47342 |