peano2uz2

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

		Ref	Expression
	Assertion	peano2uz2	$⊢ (A \in ℤ \land B \in \{x \in ℤ \| A \leq x\}) \to B + 1 \in \{x \in ℤ \| A \leq x\}$

Proof

Step	Hyp	Ref	Expression
1		peano2z	$⊢ B \in ℤ \to B + 1 \in ℤ$
2	1	ad2antrl	$⊢ (A \in ℤ \land (B \in ℤ \land A \leq B)) \to B + 1 \in ℤ$
3		zre	$⊢ A \in ℤ \to A \in ℝ$
4		zre	$⊢ B \in ℤ \to B \in ℝ$
5		lep1	$⊢ B \in ℝ \to B \leq B + 1$
6	5	adantl	$⊢ (A \in ℝ \land B \in ℝ) \to B \leq B + 1$
7		peano2re	$⊢ B \in ℝ \to B + 1 \in ℝ$
8	7	ancli	$⊢ B \in ℝ \to (B \in ℝ \land B + 1 \in ℝ)$
9		letr	$⊢ (A \in ℝ \land B \in ℝ \land B + 1 \in ℝ) \to ((A \leq B \land B \leq B + 1) \to A \leq B + 1)$
10	9	3expb	$⊢ (A \in ℝ \land (B \in ℝ \land B + 1 \in ℝ)) \to ((A \leq B \land B \leq B + 1) \to A \leq B + 1)$
11	8 10	sylan2	$⊢ (A \in ℝ \land B \in ℝ) \to ((A \leq B \land B \leq B + 1) \to A \leq B + 1)$
12	6 11	mpan2d	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \to A \leq B + 1)$
13	3 4 12	syl2an	$⊢ (A \in ℤ \land B \in ℤ) \to (A \leq B \to A \leq B + 1)$
14	13	impr	$⊢ (A \in ℤ \land (B \in ℤ \land A \leq B)) \to A \leq B + 1$
15	2 14	jca	$⊢ (A \in ℤ \land (B \in ℤ \land A \leq B)) \to (B + 1 \in ℤ \land A \leq B + 1)$
16		breq2	$⊢ x = B \to (A \leq x \leftrightarrow A \leq B)$
17	16	elrab	$⊢ B \in \{x \in ℤ \| A \leq x\} \leftrightarrow (B \in ℤ \land A \leq B)$
18	17	anbi2i	$⊢ (A \in ℤ \land B \in \{x \in ℤ \| A \leq x\}) \leftrightarrow (A \in ℤ \land (B \in ℤ \land A \leq B))$
19		breq2	$⊢ x = B + 1 \to (A \leq x \leftrightarrow A \leq B + 1)$
20	19	elrab	$⊢ B + 1 \in \{x \in ℤ \| A \leq x\} \leftrightarrow (B + 1 \in ℤ \land A \leq B + 1)$
21	15 18 20	3imtr4i	$⊢ (A \in ℤ \land B \in \{x \in ℤ \| A \leq x\}) \to B + 1 \in \{x \in ℤ \| A \leq x\}$

Metamath Proof Explorer

Theorem peano2uz2

Proof