Colors of
variables: wff set class |
Syntax hints:
∈ wcel 2148 (class class class)co 5875
ℝcr 7810 1c1 7812
+ caddc 7814 6c6 8974
7c7 8975 |
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-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1re 7905 ax-addrcl 7908 |
This theorem depends on definitions:
df-bi 117 df-cleq 2170 df-clel 2173 df-2 8978 df-3 8979
df-4 8980 df-5 8981 df-6 8982
df-7 8983 |
This theorem is referenced by: 7cn
9003 8re
9004 8pos
9022 5lt7
9104 4lt7
9105 3lt7
9106 2lt7
9107 1lt7
9108 7lt8
9109 6lt8
9110 7lt9
9117 6lt9
9118 7lt10
9516 6lt10
9517 lgsdir2lem1
14432 |