![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1red | Unicode version |
Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Ref | Expression |
---|---|
1red |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 6824 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-mp 7 ax-1re 6777 |
This theorem is referenced by: recgt0 7597 ltrec 7630 recp1lt1 7646 peano5nni 7698 peano2nn 7707 nn0p1gt0 7987 nn0ge2m1nn 8018 peano2z 8057 iccf1o 8642 fznatpl1 8708 elfz1b 8722 fzonn0p1p1 8839 elfzom1p1elfzo 8840 ltexp2a 8960 leexp2a 8961 leexp2r 8962 nnlesq 9009 bernneq3 9024 expnbnd 9025 expnlbnd2 9027 |
Copyright terms: Public domain | W3C validator |