![]() |
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 7637 | . 2 ⊢ 1 ∈ ℝ | |
2 | ax-rnegex 7604 | . 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0) | |
3 | readdcl 7618 | . . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ) | |
4 | 1, 3 | mpan 418 | . . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ) |
5 | eleq1 2162 | . . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ)) | |
6 | 4, 5 | syl5ibcom 154 | . . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ)) |
7 | 6 | rexlimiv 2502 | . 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ) |
8 | 1, 2, 7 | mp2b 8 | 1 ⊢ 0 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: = wceq 1299 ∈ wcel 1448 ∃wrex 2376 (class class class)co 5706 ℝcr 7499 0cc0 7500 1c1 7501 + caddc 7503 |
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 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 ax-17 1474 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-1re 7589 ax-addrcl 7592 ax-rnegex 7604 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-cleq 2093 df-clel 2096 df-ral 2380 df-rex 2381 |
This theorem is referenced by: 0red 7639 0xr 7684 axmulgt0 7708 gtso 7714 0lt1 7760 ine0 8023 ltaddneg 8053 addgt0 8077 addgegt0 8078 addgtge0 8079 addge0 8080 ltaddpos 8081 ltneg 8091 leneg 8094 lt0neg1 8097 lt0neg2 8098 le0neg1 8099 le0neg2 8100 addge01 8101 suble0 8105 0le1 8110 gt0ne0i 8115 gt0ne0d 8141 lt0ne0d 8142 recexre 8206 recexgt0 8208 inelr 8212 rimul 8213 1ap0 8218 reapmul1 8223 apsqgt0 8229 msqge0 8244 mulge0 8247 recexaplem2 8274 recexap 8275 rerecclap 8351 ltm1 8462 recgt0 8466 ltmul12a 8476 lemul12a 8478 mulgt1 8479 gt0div 8486 ge0div 8487 recgt1i 8514 recreclt 8516 sup3exmid 8573 crap0 8574 nnge1 8601 nngt0 8603 nnrecgt0 8616 0ne1 8645 0le0 8667 neg1lt0 8686 halfge0 8788 iap0 8795 nn0ssre 8833 nn0ge0 8854 nn0nlt0 8855 nn0le0eq0 8857 0mnnnnn0 8861 elnnnn0b 8873 elnnnn0c 8874 elnnz 8916 0z 8917 elnnz1 8929 nn0lt10b 8983 recnz 8996 gtndiv 8998 fnn0ind 9019 rpge0 9303 rpnegap 9323 0nrp 9324 0ltpnf 9409 mnflt0 9411 xneg0 9455 xaddid1 9486 xnn0xadd0 9491 xposdif 9506 elrege0 9600 0e0icopnf 9603 0elunit 9610 1elunit 9611 divelunit 9626 lincmb01cmp 9627 iccf1o 9628 unitssre 9629 modqelico 9948 modqmuladdim 9981 addmodid 9986 expubnd 10191 le2sq2 10209 bernneq2 10254 expnbnd 10256 expnlbnd 10257 faclbnd 10328 faclbnd3 10330 faclbnd6 10331 bcval4 10339 bcpasc 10353 reim0 10474 re0 10508 im0 10509 rei 10512 imi 10513 cj0 10514 caucvgre 10593 rennim 10614 sqrt0rlem 10615 sqrt0 10616 resqrexlemdecn 10624 resqrexlemnm 10630 resqrexlemgt0 10632 sqrt00 10652 sqrt9 10660 sqrt2gt1lt2 10661 leabs 10686 ltabs 10699 sqrtpclii 10742 max0addsup 10831 fimaxre2 10837 climge0 10933 iserge0 10951 fsum00 11070 arisum2 11107 0.999... 11129 cos0 11235 ef01bndlem 11261 sin01bnd 11262 cos01bnd 11263 cos2bnd 11265 sin01gt0 11266 cos01gt0 11267 sincos2sgn 11270 sin4lt0 11271 absef 11273 absefib 11274 efieq1re 11275 epos 11282 flodddiv4 11426 gcdn0gt0 11461 nn0seqcvgd 11515 algcvgblem 11523 algcvga 11525 ssblps 12353 ssbl 12354 xmeter 12364 cnbl0 12456 ex-gcd 12546 trilpolemclim 12813 trilpolemcl 12814 trilpolemisumle 12815 trilpolemeq1 12817 trilpolemlt1 12818 |
Copyright terms: Public domain | W3C validator |