Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > peano2re | GIF version |
Description: A theorem for reals analogous the second Peano postulate peano2 4566. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re | ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7889 | . 2 ⊢ 1 ∈ ℝ | |
2 | readdcl 7870 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ) | |
3 | 1, 2 | mpan2 422 | 1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 (class class class)co 5836 ℝcr 7743 1c1 7745 + caddc 7747 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-1re 7838 ax-addrcl 7841 |
This theorem is referenced by: lep1 8731 letrp1 8734 p1le 8735 ledivp1 8789 nnssre 8852 nn1suc 8867 nnge1 8871 div4p1lem1div2 9101 zltp1le 9236 suprzclex 9280 zeo 9287 peano2uz2 9289 uzind 9293 btwnapz 9312 numltc 9338 ge0p1rp 9612 fznatpl1 10001 ubmelm1fzo 10151 qbtwnxr 10183 flhalf 10227 fldiv4p1lem1div2 10230 seq3split 10404 seq3f1olemqsumk 10424 bernneq3 10566 facwordi 10642 faclbnd 10643 expcnvap0 11429 cvgratnnlemfm 11456 cvgratnnlemrate 11457 cvgratz 11459 mertenslemi1 11462 fprodntrivap 11511 divalglemnqt 11842 infssuzex 11867 nonsq 12118 eulerthlema 12141 pcfac 12259 ennnfonelemkh 12288 tgioo 13093 suplociccreex 13149 reeff1olem 13239 |
Copyright terms: Public domain | W3C validator |