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
12551 uzinfi
12783 suprzcl2
12793 suprzub
12794 2resupmax
13037 infmrp1
13193 fseqsupcl
13812 ssnn0fi
13820 fsuppmapnn0fiublem
13825 isercolllem1
15485 isercolllem2
15486 summolem2
15537 zsum
15539 fsumcvg3
15550 mertenslem2
15706 prodmolem2
15754 zprod
15756 cnso
16065 gcdval
16312 dfgcd2
16363 lcmval
16404 lcmgcdlem
16418 odzval
16599 pczpre
16655 prmreclem1
16724 ramz
16833 odval
19251 odf
19254 gexval
19295 gsumval3
19619 retos
20951 mbfsup
24956 mbfinf
24957 itg2monolem1
25043 itg2mono
25046 dvgt0lem2
25295 dvgt0
25296 plyeq0lem
25499 dgrval
25517 dgrcl
25522 dgrub
25523 dgrlb
25525 elqaalem1
25607 elqaalem3
25609 aalioulem2
25621 logccv
25946 ex-po
29184 ssnnssfz
31491 lmdvg
32314 oddpwdc
32734 ballotlemi
32880 ballotlemiex
32881 ballotlemsup
32884 ballotlemimin
32885 ballotlemfrcn0
32909 ballotlemirc
32911 erdszelem3
33567 erdszelem4
33568 erdszelem5
33569 erdszelem6
33570 erdszelem8
33572 erdszelem9
33573 erdszelem11
33575 erdsze2lem1
33577 erdsze2lem2
33578 supfz
34095 inffz
34096 gtinf
34722 ptrecube
36009 poimirlem31
36040 poimirlem32
36041 heicant
36044 mblfinlem3
36048 mblfinlem4
36049 ismblfin
36050 incsequz2
36139 totbndbnd
36179 prdsbnd
36183 aks4d1p4
40467 aks4d1p7
40471 sticksstones1
40485 sticksstones3
40487 pellfundval
41105 dgraaval
41373 dgraaf
41376 fzisoeu
43329 uzublem
43460 infrglb
43622 limsupubuzlem
43744 fourierdlem25
44164 fourierdlem31
44170 fourierdlem36
44175 fourierdlem37
44176 fourierdlem42
44181 fourierdlem79
44217 ioorrnopnlem
44336 hoicvr
44580 hoidmvlelem2
44628 iunhoiioolem
44707 vonioolem1
44712 fsupdm2
44875 finfdm2
44879 prmdvdsfmtnof1lem1
45567 prmdvdsfmtnof
45569 prmdvdsfmtnof1
45570 ssnn0ssfz
46216 rrx2plordso
46601 |