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