Colors of
variables: wff set class |
Syntax hints:
∈ wcel 2148 (class class class)co 5874
ℝcr 7809 1c1 7811
+ caddc 7813 6c6 8973
7c7 8974 |
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 7904 ax-addrcl 7907 |
This theorem depends on definitions:
df-bi 117 df-cleq 2170 df-clel 2173 df-2 8977 df-3 8978
df-4 8979 df-5 8980 df-6 8981
df-7 8982 |
This theorem is referenced by: 7cn
9002 8re
9003 8pos
9021 5lt7
9103 4lt7
9104 3lt7
9105 2lt7
9106 1lt7
9107 7lt8
9108 6lt8
9109 7lt9
9116 6lt9
9117 7lt10
9515 6lt10
9516 lgsdir2lem1
14399 |