Theorem 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	⊢ 𝐴 ∈ ( 1 ... 𝐵 )
	jm2.27dlem2.2	⊢ 𝐶 = ( 𝐵 + 1 )
	jm2.27dlem2.3	⊢ 𝐵 ∈ ℕ
Assertion	jm2.27dlem2	⊢ 𝐴 ∈ ( 1 ... 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem2.1	⊢ 𝐴 ∈ ( 1 ... 𝐵 )
2		jm2.27dlem2.2	⊢ 𝐶 = ( 𝐵 + 1 )
3		jm2.27dlem2.3	⊢ 𝐵 ∈ ℕ
4		elfzelz	⊢ ( 𝐴 ∈ ( 1 ... 𝐵 ) → 𝐴 ∈ ℤ )
5	1 4	ax-mp	⊢ 𝐴 ∈ ℤ
6		elfzle1	⊢ ( 𝐴 ∈ ( 1 ... 𝐵 ) → 1 ≤ 𝐴 )
7	1 6	ax-mp	⊢ 1 ≤ 𝐴
8	5	zrei	⊢ 𝐴 ∈ ℝ
9	3	nnrei	⊢ 𝐵 ∈ ℝ
10		elfzle2	⊢ ( 𝐴 ∈ ( 1 ... 𝐵 ) → 𝐴 ≤ 𝐵 )
11	1 10	ax-mp	⊢ 𝐴 ≤ 𝐵
12		letrp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ ( 𝐵 + 1 ) )
13	8 9 11 12	mp3an	⊢ 𝐴 ≤ ( 𝐵 + 1 )
14	13 2	breqtrri	⊢ 𝐴 ≤ 𝐶
15		1z	⊢ 1 ∈ ℤ
16		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
17		peano2z	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 + 1 ) ∈ ℤ )
18	3 16 17	mp2b	⊢ ( 𝐵 + 1 ) ∈ ℤ
19	2 18	eqeltri	⊢ 𝐶 ∈ ℤ
20		elfz1	⊢ ( ( 1 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∈ ( 1 ... 𝐶 ) ↔ ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶 ) ) )
21	15 19 20	mp2an	⊢ ( 𝐴 ∈ ( 1 ... 𝐶 ) ↔ ( 𝐴 ∈ ℤ ∧ 1 ≤ 𝐴 ∧ 𝐴 ≤ 𝐶 ) )
22	5 7 14 21	mpbir3an	⊢ 𝐴 ∈ ( 1 ... 𝐶 )