![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1lt2 | Unicode version |
Description: 1 is less than 2. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
1lt2 |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7987 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | ltp1i 8893 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-2 9009 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | breqtrri 4045 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: class class
class wbr 4018 (class class class)co 5897
![]() ![]() ![]() ![]() |
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-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4192 ax-pr 4227 ax-un 4451 ax-setind 4554 ax-cnex 7933 ax-resscn 7934 ax-1cn 7935 ax-1re 7936 ax-icn 7937 ax-addcl 7938 ax-addrcl 7939 ax-mulcl 7940 ax-addcom 7942 ax-addass 7944 ax-i2m1 7947 ax-0lt1 7948 ax-0id 7950 ax-rnegex 7951 ax-pre-ltadd 7958 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-rab 2477 df-v 2754 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-br 4019 df-opab 4080 df-xp 4650 df-iota 5196 df-fv 5243 df-ov 5900 df-pnf 8025 df-mnf 8026 df-ltxr 8028 df-2 9009 |
This theorem is referenced by: 1lt3 9121 1lt4 9124 1lt6 9133 1lt7 9139 1lt8 9146 1lt9 9154 1ne2 9156 1ap2 9157 1le2 9158 halflt1 9167 nn0ge2m1nn 9267 nn0n0n1ge2b 9363 halfnz 9380 1lt10 9553 fztpval 10115 ige2m2fzo 10230 sqrt2gt1lt2 11093 ege2le3 11714 cos12dec 11810 ene1 11827 eap1 11828 n2dvds1 11952 2prm 12162 3prm 12163 4nprm 12164 isprm5 12177 basendxltplusgndx 12628 grpstrg 12640 grpbaseg 12641 grpplusgg 12642 rngstrg 12649 lmodstrd 12678 topgrpstrd 12710 reeff1o 14671 cosz12 14678 2logb9irrALT 14869 sqrt2cxp2logb9e3 14870 lgseisenlem1 14928 |
Copyright terms: Public domain | W3C validator |