Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205
∈ wcel 2107 class class class wbr 5110
ℝcr 11057 <
clt 11196 ≤ cle 11197 |
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-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ral 3066 df-rex 3075 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-br 5111 df-opab 5173 df-xp 5644 df-cnv 5646 df-xr 11200 df-le 11202 |
This theorem is referenced by: letrii
11287 nn0ge2m1nn
12489 0nelfz1
13467 fzpreddisj
13497 hashnn0n0nn
14298 hashge2el2dif
14386 divalglem5
16286 divalglem6
16287 sadcadd
16345 htpycc
24359 pco1
24394 pcohtpylem
24398 pcopt
24401 pcopt2
24402 pcoass
24403 pcorevlem
24405 vitalilem5
24992 vieta1lem2
25687 ppiltx
26542 ppiublem1
26566 chtub
26576 axlowdimlem16
27948 axlowdim
27952 lfgrnloop
28118 lfuhgr1v0e
28244 lfgrwlkprop
28677 ballotlem2
33128 subfacp1lem1
33813 subfacp1lem5
33818 bcneg1
34348 poimirlem9
36116 poimirlem16
36123 poimirlem17
36124 poimirlem19
36126 poimirlem20
36127 poimirlem22
36129 fdc
36233 pellexlem6
41186 jm2.23
41349 |