Colors of
variables: wff
setvar class |
Syntax hints:
Or wor 5542 ℝcr 10984
< clt 11123 |
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 2709 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663 ax-resscn 11042 ax-pre-lttri 11059 ax-pre-lttrn 11060 |
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 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5529 df-po 5543 df-so 5544 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-er 8582 df-en 8818 df-dom 8819 df-sdom 8820 df-pnf 11125 df-mnf 11126 df-ltxr 11128 |
This theorem is referenced by: gtso
11170 lttri2
11171 lttri3
11172 lttri4
11173 ltnr
11184 ltnsym2
11188 fimaxre
12033 fiminre
12036 lbinf
12042 suprcl
12049 suprub
12050 suprlub
12053 infrecl
12071 infregelb
12073 infrelb
12074 supfirege
12076 suprfinzcl
12550 uzinfi
12782 suprzcl2
12792 suprzub
12793 2resupmax
13036 infmrp1
13192 fseqsupcl
13811 ssnn0fi
13819 fsuppmapnn0fiublem
13824 isercolllem1
15484 isercolllem2
15485 summolem2
15536 zsum
15538 fsumcvg3
15549 mertenslem2
15705 prodmolem2
15753 zprod
15755 cnso
16064 gcdval
16311 dfgcd2
16362 lcmval
16403 lcmgcdlem
16417 odzval
16598 pczpre
16654 prmreclem1
16723 ramz
16832 odval
19249 odf
19252 gexval
19290 gsumval3
19614 retos
20946 mbfsup
24951 mbfinf
24952 itg2monolem1
25038 itg2mono
25041 dvgt0lem2
25290 dvgt0
25291 plyeq0lem
25494 dgrval
25512 dgrcl
25517 dgrub
25518 dgrlb
25520 elqaalem1
25602 elqaalem3
25604 aalioulem2
25616 logccv
25941 ex-po
29178 ssnnssfz
31485 lmdvg
32308 oddpwdc
32728 ballotlemi
32874 ballotlemiex
32875 ballotlemsup
32878 ballotlemimin
32879 ballotlemfrcn0
32903 ballotlemirc
32905 erdszelem3
33561 erdszelem4
33562 erdszelem5
33563 erdszelem6
33564 erdszelem8
33566 erdszelem9
33567 erdszelem11
33569 erdsze2lem1
33571 erdsze2lem2
33572 supfz
34092 inffz
34093 gtinf
34687 ptrecube
35974 poimirlem31
36005 poimirlem32
36006 heicant
36009 mblfinlem3
36013 mblfinlem4
36014 ismblfin
36015 incsequz2
36104 totbndbnd
36144 prdsbnd
36148 aks4d1p4
40432 aks4d1p7
40436 sticksstones1
40450 sticksstones3
40452 pellfundval
41069 dgraaval
41337 dgraaf
41340 fzisoeu
43293 uzublem
43424 infrglb
43586 limsupubuzlem
43708 fourierdlem25
44128 fourierdlem31
44134 fourierdlem36
44139 fourierdlem37
44140 fourierdlem42
44145 fourierdlem79
44181 ioorrnopnlem
44300 hoicvr
44544 hoidmvlelem2
44592 iunhoiioolem
44671 vonioolem1
44676 fsupdm2
44839 finfdm2
44843 prmdvdsfmtnof1lem1
45531 prmdvdsfmtnof
45533 prmdvdsfmtnof1
45534 ssnn0ssfz
46180 rrx2plordso
46565 |