Metamath Proof Explorer

Theorem peano2uz2

Description: Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004)

Ref Expression
Assertion peano2uz2 ⊢ A ∈ ℤ ∧ B ∈ x ∈ ℤ | A ≤ x → B + 1 ∈ x ∈ ℤ | A ≤ x

Proof

Step Hyp Ref Expression
1 peano2z ⊢ B ∈ ℤ → B + 1 ∈ ℤ
2 1 ad2antrl ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A ≤ B → B + 1 ∈ ℤ
3 zre ⊢ A ∈ ℤ → A ∈ ℝ
4 zre ⊢ B ∈ ℤ → B ∈ ℝ
5 lep1 ⊢ B ∈ ℝ → B ≤ B + 1
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ B + 1
7 peano2re ⊢ B ∈ ℝ → B + 1 ∈ ℝ
8 7 ancli ⊢ B ∈ ℝ → B ∈ ℝ ∧ B + 1 ∈ ℝ
9 letr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B + 1 ∈ ℝ → A ≤ B ∧ B ≤ B + 1 → A ≤ B + 1
10 9 3expb ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B + 1 ∈ ℝ → A ≤ B ∧ B ≤ B + 1 → A ≤ B + 1
11 8 10 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∧ B ≤ B + 1 → A ≤ B + 1
12 6 11 mpan2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B → A ≤ B + 1
13 3 4 12 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ≤ B → A ≤ B + 1
14 13 impr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A ≤ B → A ≤ B + 1
15 2 14 jca ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ A ≤ B → B + 1 ∈ ℤ ∧ A ≤ B + 1
16 breq2 ⊢ x = B → A ≤ x ↔ A ≤ B
17 16 elrab ⊢ B ∈ x ∈ ℤ | A ≤ x ↔ B ∈ ℤ ∧ A ≤ B
18 17 anbi2i ⊢ A ∈ ℤ ∧ B ∈ x ∈ ℤ | A ≤ x ↔ A ∈ ℤ ∧ B ∈ ℤ ∧ A ≤ B
19 breq2 ⊢ x = B + 1 → A ≤ x ↔ A ≤ B + 1
20 19 elrab ⊢ B + 1 ∈ x ∈ ℤ | A ≤ x ↔ B + 1 ∈ ℤ ∧ A ≤ B + 1
21 15 18 20 3imtr4i ⊢ A ∈ ℤ ∧ B ∈ x ∈ ℤ | A ≤ x → B + 1 ∈ x ∈ ℤ | A ≤ x