Metamath Proof Explorer

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 ⊢ A ∈ 1 … B
jm2.27dlem2.2 ⊢ C = B + 1
jm2.27dlem2.3 ⊢ B ∈ ℕ
Assertion jm2.27dlem2 ⊢ A ∈ 1 … C

Proof

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