Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ∧ wa 104
∈ wcel 2148 class class class wbr 4003
ℝcr 7809 0cc0 7810
< clt 7991 ℝ+crp 9652 |
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 2739 df-un 3133 df-in 3135 df-ss 3142 df-sn 3598 df-pr 3599 df-op 3601 df-br 4004 df-rp 9653 |
This theorem is referenced by: reclt1d
9709 recgt1d
9710 ltrecd
9714 lerecd
9715 ltrec1d
9716 lerec2d
9717 lediv2ad
9718 ltdiv2d
9719 lediv2d
9720 ledivdivd
9721 divge0d
9736 ltmul1d
9737 ltmul2d
9738 lemul1d
9739 lemul2d
9740 ltdiv1d
9741 lediv1d
9742 ltmuldivd
9743 ltmuldiv2d
9744 lemuldivd
9745 lemuldiv2d
9746 ltdivmuld
9747 ltdivmul2d
9748 ledivmuld
9749 ledivmul2d
9750 ltdiv23d
9756 lediv23d
9757 lt2mul2divd
9764 mertenslemi1
11542 isprm6
12146 |