![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0re | GIF version |
Description: 0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
0re | ⊢ 0 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7973 | . 2 ⊢ 1 ∈ ℝ | |
2 | ax-rnegex 7937 | . 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0) | |
3 | readdcl 7954 | . . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ) | |
4 | 1, 3 | mpan 424 | . . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ) |
5 | eleq1 2251 | . . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ)) | |
6 | 4, 5 | syl5ibcom 155 | . . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ)) |
7 | 6 | rexlimiv 2600 | . 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ) |
8 | 1, 2, 7 | mp2b 8 | 1 ⊢ 0 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: = wceq 1363 ∈ wcel 2159 ∃wrex 2468 (class class class)co 5890 ℝcr 7827 0cc0 7828 1c1 7829 + caddc 7831 |
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-5 1457 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-4 1520 ax-17 1536 ax-ial 1544 ax-i5r 1545 ax-ext 2170 ax-1re 7922 ax-addrcl 7925 ax-rnegex 7937 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-cleq 2181 df-clel 2184 df-ral 2472 df-rex 2473 |
This theorem is referenced by: 0red 7975 0xr 8021 axmulgt0 8046 gtso 8053 0lt1 8101 ine0 8368 ltaddneg 8398 addgt0 8422 addgegt0 8423 addgtge0 8424 addge0 8425 ltaddpos 8426 ltneg 8436 leneg 8439 lt0neg1 8442 lt0neg2 8443 le0neg1 8444 le0neg2 8445 addge01 8446 suble0 8450 0le1 8455 gt0ne0i 8460 gt0ne0d 8486 lt0ne0d 8487 recexre 8552 recexgt0 8554 inelr 8558 rimul 8559 1ap0 8564 reapmul1 8569 apsqgt0 8575 msqge0 8590 mulge0 8593 recexaplem2 8626 recexap 8627 rerecclap 8704 ltm1 8820 recgt0 8824 ltmul12a 8834 lemul12a 8836 mulgt1 8837 gt0div 8844 ge0div 8845 recgt1i 8872 recreclt 8874 sup3exmid 8931 crap0 8932 nnge1 8959 nngt0 8961 nnrecgt0 8974 0ne1 9003 0le0 9025 neg1lt0 9044 halfge0 9152 iap0 9159 nn0ssre 9197 nn0ge0 9218 nn0nlt0 9219 nn0le0eq0 9221 0mnnnnn0 9225 elnnnn0b 9237 elnnnn0c 9238 elnnz 9280 0z 9281 elnnz1 9293 nn0lt10b 9350 recnz 9363 gtndiv 9365 fnn0ind 9386 rpge0 9683 rpnegap 9703 0nrp 9706 0ltpnf 9799 mnflt0 9801 xneg0 9848 xaddid1 9879 xnn0xadd0 9884 xposdif 9899 elrege0 9993 0e0icopnf 9996 0elunit 10003 1elunit 10004 divelunit 10019 lincmb01cmp 10020 iccf1o 10021 unitssre 10022 fz0to4untppr 10141 modqelico 10351 modqmuladdim 10384 addmodid 10389 expubnd 10594 le2sq2 10613 bernneq2 10659 expnbnd 10661 expnlbnd 10662 faclbnd 10738 faclbnd3 10740 faclbnd6 10741 bcval4 10749 bcpasc 10763 reim0 10887 re0 10921 im0 10922 rei 10925 imi 10926 cj0 10927 caucvgre 11007 rennim 11028 sqrt0rlem 11029 sqrt0 11030 resqrexlemdecn 11038 resqrexlemnm 11044 resqrexlemgt0 11046 sqrt00 11066 sqrt9 11074 sqrt2gt1lt2 11075 leabs 11100 ltabs 11113 sqrtpclii 11156 max0addsup 11245 fimaxre2 11252 climge0 11350 iserge0 11368 fsum00 11487 arisum2 11524 0.999... 11546 fprodge0 11662 cos0 11755 ef01bndlem 11781 sin01bnd 11782 cos01bnd 11783 cos2bnd 11785 sin01gt0 11786 cos01gt0 11787 sincos2sgn 11790 sin4lt0 11791 absef 11794 absefib 11795 efieq1re 11796 epos 11805 flodddiv4 11956 gcdn0gt0 11996 nn0seqcvgd 12058 algcvgblem 12066 algcvga 12068 pythagtriplem12 12292 pythagtriplem13 12293 pythagtriplem14 12294 pythagtriplem16 12296 mulgnegnn 13037 ssblps 14308 ssbl 14309 xmeter 14319 cnbl0 14417 reeff1olem 14575 pilem3 14587 pipos 14592 sinhalfpilem 14595 sincosq1sgn 14630 sincosq2sgn 14631 sinq34lt0t 14635 coseq0q4123 14638 coseq00topi 14639 coseq0negpitopi 14640 tangtx 14642 sincos4thpi 14644 sincos6thpi 14646 cosordlem 14653 cosq34lt1 14654 cos02pilt1 14655 cos0pilt1 14656 cos11 14657 ioocosf1o 14658 log1 14670 logrpap0b 14680 logdivlti 14685 rpabscxpbnd 14742 lgsval2lem 14794 lgsval4a 14806 lgsneg 14808 lgsdilem 14811 lgsdir2lem1 14812 ex-gcd 14866 trilpolemclim 15168 trilpolemcl 15169 trilpolemisumle 15170 trilpolemeq1 15172 trilpolemlt1 15173 trirec0 15176 apdiff 15180 redc0 15189 reap0 15190 dceqnconst 15192 dcapnconst 15193 nconstwlpolemgt0 15196 neap0mkv 15201 |
Copyright terms: Public domain | W3C validator |