Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∧ wa 104
∈ wcel 2148 class class class wbr 4005
ℝcr 7812 0cc0 7813
< clt 7994 ℝ+crp 9655 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709
ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rab 2464 df-v 2741 df-un 3135 df-in 3137 df-ss 3144 df-sn 3600 df-pr 3601 df-op 3603 df-br 4006 df-rp 9656 |
This theorem is referenced by: reclt1d
9712 recgt1d
9713 ltrecd
9717 lerecd
9718 ltrec1d
9719 lerec2d
9720 lediv2ad
9721 ltdiv2d
9722 lediv2d
9723 ledivdivd
9724 divge0d
9739 ltmul1d
9740 ltmul2d
9741 lemul1d
9742 lemul2d
9743 ltdiv1d
9744 lediv1d
9745 ltmuldivd
9746 ltmuldiv2d
9747 lemuldivd
9748 lemuldiv2d
9749 ltdivmuld
9750 ltdivmul2d
9751 ledivmuld
9752 ledivmul2d
9753 ltdiv23d
9759 lediv23d
9760 lt2mul2divd
9767 mertenslemi1
11545 isprm6
12149 |