![]() |
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 4261. (Contributed by NM, 5-Jul-2005.) |
Ref | Expression |
---|---|
peano2re | ⊢ (A ∈ ℝ → (A + 1) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re 6824 | . 2 ⊢ 1 ∈ ℝ | |
2 | readdcl 6805 | . 2 ⊢ ((A ∈ ℝ ∧ 1 ∈ ℝ) → (A + 1) ∈ ℝ) | |
3 | 1, 2 | mpan2 401 | 1 ⊢ (A ∈ ℝ → (A + 1) ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1390 (class class class)co 5455 ℝcr 6710 1c1 6712 + caddc 6714 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 ax-1re 6777 ax-addrcl 6780 |
This theorem is referenced by: lep1 7592 letrp1 7595 p1le 7596 ledivp1 7650 nnssre 7699 nn1suc 7714 nnge1 7718 zltp1le 8074 zeo 8119 peano2uz2 8121 uzind 8125 numltc 8163 ge0p1rp 8389 fznatpl1 8708 ubmelm1fzo 8852 bernneq3 9024 |
Copyright terms: Public domain | W3C validator |