![]() |
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 4594. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re | ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7955 | . 2 ⊢ 1 ∈ ℝ | |
2 | readdcl 7936 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ) | |
3 | 1, 2 | mpan2 425 | 1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 (class class class)co 5874 ℝcr 7809 1c1 7811 + caddc 7813 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-1re 7904 ax-addrcl 7907 |
This theorem is referenced by: lep1 8801 letrp1 8804 p1le 8805 ledivp1 8859 nnssre 8922 nn1suc 8937 nnge1 8941 div4p1lem1div2 9171 zltp1le 9306 suprzclex 9350 zeo 9357 peano2uz2 9359 uzind 9363 btwnapz 9382 numltc 9408 ge0p1rp 9684 fznatpl1 10075 ubmelm1fzo 10225 qbtwnxr 10257 flhalf 10301 fldiv4p1lem1div2 10304 seq3split 10478 seq3f1olemqsumk 10498 bernneq3 10642 facwordi 10719 faclbnd 10720 expcnvap0 11509 cvgratnnlemfm 11536 cvgratnnlemrate 11537 cvgratz 11539 mertenslemi1 11542 fprodntrivap 11591 divalglemnqt 11924 infssuzex 11949 nonsq 12206 eulerthlema 12229 pcfac 12347 1arith 12364 ennnfonelemkh 12412 tgioo 13982 suplociccreex 14038 reeff1olem 14128 lgsvalmod 14356 |
Copyright terms: Public domain | W3C validator |