![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0red | GIF version |
Description: 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Ref | Expression |
---|---|
0red | ⊢ (𝜑 → 0 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 7409 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 0 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1436 ℝcr 7270 0cc0 7271 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1379 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-4 1443 ax-17 1462 ax-ial 1470 ax-i5r 1471 ax-ext 2067 ax-1re 7360 ax-addrcl 7363 ax-rnegex 7375 |
This theorem depends on definitions: df-bi 115 df-nf 1393 df-cleq 2078 df-clel 2081 df-ral 2360 df-rex 2361 |
This theorem is referenced by: gt0ne0 7826 add20 7873 subge0 7874 lesub0 7878 addgt0d 7916 sublt0d 7965 gt0add 7968 apreap 7982 gt0ap0 8020 ap0gt0 8033 prodgt0 8225 prodge0 8227 lt2msq1 8258 lediv12a 8267 ledivp1 8276 squeeze0 8277 mulle0r 8317 nn2ge 8366 0mnnnnn0 8615 elnn0z 8673 rpgecl 9071 ge0p1rp 9074 ledivge1le 9112 iccf1o 9330 elfz1b 9411 elfz0fzfz0 9442 fz0fzelfz0 9443 fzo1fzo0n0 9497 elfzo0z 9498 fzofzim 9502 elfzodifsumelfzo 9515 btwnzge0 9610 modqid 9659 mulqaddmodid 9674 mulp1mod1 9675 modqltm1p1mod 9686 addmodlteq 9708 expival 9808 expgt1 9844 ltexp2a 9858 leexp2a 9859 expnbnd 9926 expnlbnd2 9928 expcanlem 9973 expcan 9974 resqrexlemcalc3 10290 resqrexlemnm 10292 resqrexlemgt0 10294 sqrtgt0 10308 abs00ap 10336 leabs 10348 ltabs 10361 abslt 10362 absle 10363 absgt0ap 10373 climge0 10551 dvdslelemd 10638 oddge22np1 10675 divalglemnn 10712 divalglemeuneg 10717 lcmgcdlem 10853 dvdsnprmd 10901 sqrt2irraplemnn 10951 sqrt2irrap 10952 qnumgt0 10970 znnen 11005 |
Copyright terms: Public domain | W3C validator |