Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
∈ wcel 2104 class class class wbr 5081
(class class class)co 7307 ℝcr 10920
0cc0 10921 1c1 10922
+ caddc 10924 <
clt 11059 |
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 2707 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-resscn 10978 ax-1cn 10979 ax-icn 10980 ax-addcl 10981 ax-addrcl 10982 ax-mulcl 10983 ax-mulrcl 10984 ax-mulcom 10985 ax-addass 10986 ax-mulass 10987 ax-distr 10988 ax-i2m1 10989 ax-1ne0 10990 ax-1rid 10991 ax-rnegex 10992 ax-rrecex 10993 ax-cnre 10994 ax-pre-lttri 10995 ax-pre-lttrn 10996 ax-pre-ltadd 10997 ax-pre-mulgt0 10998 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-reu 3332 df-rab 3333 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-br 5082 df-opab 5144 df-mpt 5165 df-id 5500 df-po 5514 df-so 5515 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-er 8529 df-en 8765 df-dom 8766 df-sdom 8767 df-pnf 11061 df-mnf 11062 df-xr 11063 df-ltxr 11064 df-le 11065 df-sub 11257 df-neg 11258 |
This theorem is referenced by: lep1
11866 letrp1
11869 recp1lt1
11923 ledivp1
11927 ltp1i
11929 ltp1d
11955 sup2
11981 uzind
12462 ge0p1rp
12811 qbtwnxr
12984 xrsupsslem
13091 supxrunb1
13103 fzp1disj
13365 fzneuz
13387 fzp1nel
13390 fsequb
13745 caubnd
15119 rlim2lt
15255 o1fsum
15574 pcprendvds
16590 pcmpt
16642 iocopnst
24152 bndth
24170 ovolicc2lem3
24732 ioorcl2
24785 itg2const2
24955 reeff1olem
25654 axlowdimlem13
27371 icoreunrn
35578 poimirlem4
35829 poimirlem22
35847 mblfinlem1
35862 aks4d1p1p4
40279 xrpnf
43254 limsupre3lem
43502 fourierdlem25
43902 smfresal
44556 natlocalincr
46755 |