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 7027 | . 2 ⊢ 0 ∈ ℝ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 0 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 ℝcr 6888 0cc0 6889 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-1re 6978 ax-addrcl 6981 ax-rnegex 6993 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-cleq 2033 df-clel 2036 df-ral 2311 df-rex 2312 |
This theorem is referenced by: gt0ne0 7422 add20 7469 subge0 7470 lesub0 7474 addgt0d 7512 sublt0d 7561 gt0add 7564 apreap 7578 gt0ap0 7616 ap0gt0 7629 prodgt0 7818 prodge0 7820 lt2msq1 7851 lediv12a 7860 ledivp1 7869 squeeze0 7870 nn2ge 7946 0mnnnnn0 8214 elnn0z 8258 rpgecl 8611 ge0p1rp 8614 ledivge1le 8652 iccf1o 8872 elfz1b 8952 elfz0fzfz0 8983 fz0fzelfz0 8984 fzo1fzo0n0 9039 elfzo0z 9040 fzofzim 9044 elfzodifsumelfzo 9057 btwnzge0 9142 expival 9257 expgt1 9293 ltexp2a 9306 leexp2a 9307 expnbnd 9372 expnlbnd2 9374 resqrexlemcalc3 9614 resqrexlemnm 9616 resqrexlemgt0 9618 sqrtgt0 9632 abs00ap 9660 leabs 9672 ltabs 9683 abslt 9684 absle 9685 absgt0ap 9695 climge0 9845 |
Copyright terms: Public domain | W3C validator |