This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem peano2uz2

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

Ref Expression
Assertion peano2uz2 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } ) → ( 𝐵 + 1 ) ∈ { 𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥 } )

Proof

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