![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0red | Unicode version |
Description: ![]() |
Ref | Expression |
---|---|
0red |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 7585 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-1re 7536 ax-addrcl 7539 ax-rnegex 7551 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-cleq 2088 df-clel 2091 df-ral 2375 df-rex 2376 |
This theorem is referenced by: gt0ne0 8002 add20 8049 subge0 8050 lesub0 8054 addgt0d 8095 sublt0d 8144 gt0add 8147 apreap 8161 gt0ap0 8199 ap0gt0 8212 prodgt0 8410 prodge0 8412 lt2msq1 8443 lediv12a 8452 ledivp1 8461 squeeze0 8462 mulle0r 8502 nn2ge 8553 0mnnnnn0 8803 elnn0z 8861 rpgecl 9261 ge0p1rp 9264 ledivge1le 9302 iccf1o 9570 elfz1b 9653 elfz0fzfz0 9686 fz0fzelfz0 9687 fzo1fzo0n0 9743 elfzo0z 9744 fzofzim 9748 elfzodifsumelfzo 9761 btwnzge0 9856 modqid 9905 mulqaddmodid 9920 mulp1mod1 9921 modqltm1p1mod 9932 addmodlteq 9954 expgt1 10124 ltexp2a 10138 leexp2a 10139 expnbnd 10208 expnlbnd2 10210 expcanlem 10255 expcan 10256 resqrexlemcalc3 10580 resqrexlemnm 10582 resqrexlemgt0 10584 sqrtgt0 10598 abs00ap 10626 leabs 10638 ltabs 10651 abslt 10652 absle 10653 absgt0ap 10663 rpmincl 10800 reccn2ap 10872 climge0 10884 fsumrecl 10960 isumlessdc 11055 divcnv 11056 expcnvre 11062 absltap 11068 geolim2 11071 georeclim 11072 geoisumr 11077 cvgratnnlemnexp 11083 cvgratnnlemmn 11084 cvgratnnlemabsle 11086 mertenslem2 11095 dvdslelemd 11287 oddge22np1 11324 divalglemnn 11361 divalglemeuneg 11366 lcmgcdlem 11502 dvdsnprmd 11550 sqrt2irraplemnn 11600 sqrt2irrap 11601 qnumgt0 11619 znnen 11654 mulcncflem 12369 |
Copyright terms: Public domain | W3C validator |