jm2.27dlem2

Description: Lemma for rmydioph . This theorem is used along with the next three to efficiently infer steps like 7 e. ( 1 ... ; 1 0 ) . (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Hypotheses	jm2.27dlem2.1	$⊢ A \in (1 \dots B)$
	jm2.27dlem2.2	$⊢ C = B + 1$
	jm2.27dlem2.3	$⊢ B \in ℕ$
Assertion	jm2.27dlem2	$⊢ A \in (1 \dots C)$

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem2.1	$⊢ A \in (1 \dots B)$
2		jm2.27dlem2.2	$⊢ C = B + 1$
3		jm2.27dlem2.3	$⊢ B \in ℕ$
4		elfzelz	$⊢ A \in (1 \dots B) \to A \in ℤ$
5	1 4	ax-mp	$⊢ A \in ℤ$
6		elfzle1	$⊢ A \in (1 \dots B) \to 1 \leq A$
7	1 6	ax-mp	$⊢ 1 \leq A$
8	5	zrei	$⊢ A \in ℝ$
9	3	nnrei	$⊢ B \in ℝ$
10		elfzle2	$⊢ A \in (1 \dots B) \to A \leq B$
11	1 10	ax-mp	$⊢ A \leq B$
12		letrp1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \leq B + 1$
13	8 9 11 12	mp3an	$⊢ A \leq B + 1$
14	13 2	breqtrri	$⊢ A \leq C$
15		1z	$⊢ 1 \in ℤ$
16		nnz	$⊢ B \in ℕ \to B \in ℤ$
17		peano2z	$⊢ B \in ℤ \to B + 1 \in ℤ$
18	3 16 17	mp2b	$⊢ B + 1 \in ℤ$
19	2 18	eqeltri	$⊢ C \in ℤ$
20		elfz1	$⊢ (1 \in ℤ \land C \in ℤ) \to (A \in (1 \dots C) \leftrightarrow (A \in ℤ \land 1 \leq A \land A \leq C))$
21	15 19 20	mp2an	$⊢ A \in (1 \dots C) \leftrightarrow (A \in ℤ \land 1 \leq A \land A \leq C)$
22	5 7 14 21	mpbir3an	$⊢ A \in (1 \dots C)$

Metamath Proof Explorer

Theorem jm2.27dlem2

Proof