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 ) ∈ { 𝑥 ∈ ℤ ∣ 𝐴𝑥 } )