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 4318. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re | ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 7026 | . 2 ⊢ 1 ∈ ℝ | |
2 | readdcl 7007 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ) | |
3 | 1, 2 | mpan2 401 | 1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 (class class class)co 5512 ℝcr 6888 1c1 6890 + caddc 6892 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 ax-1re 6978 ax-addrcl 6981 |
This theorem is referenced by: lep1 7811 letrp1 7814 p1le 7815 ledivp1 7869 nnssre 7918 nn1suc 7933 nnge1 7937 div4p1lem1div2 8177 zltp1le 8298 zeo 8343 peano2uz2 8345 uzind 8349 numltc 8387 ge0p1rp 8614 fznatpl1 8938 ubmelm1fzo 9082 flhalf 9144 fldiv4p1lem1div2 9147 bernneq3 9371 |
Copyright terms: Public domain | W3C validator |