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 e. ( 1 ... B )
jm2.27dlem2.2 
|- C = ( B + 1 )
jm2.27dlem2.3 
|- B e. NN
Assertion jm2.27dlem2 
|- A e. ( 1 ... C )

Proof

Step Hyp Ref Expression
1 jm2.27dlem2.1 
 |-  A e. ( 1 ... B )
2 jm2.27dlem2.2 
 |-  C = ( B + 1 )
3 jm2.27dlem2.3 
 |-  B e. NN
4 elfzelz 
 |-  ( A e. ( 1 ... B ) -> A e. ZZ )
5 1 4 ax-mp 
 |-  A e. ZZ
6 elfzle1 
 |-  ( A e. ( 1 ... B ) -> 1 <_ A )
7 1 6 ax-mp 
 |-  1 <_ A
8 5 zrei 
 |-  A e. RR
9 3 nnrei 
 |-  B e. RR
10 elfzle2 
 |-  ( A e. ( 1 ... B ) -> A <_ B )
11 1 10 ax-mp 
 |-  A <_ B
12 letrp1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ ( B + 1 ) )
13 8 9 11 12 mp3an 
 |-  A <_ ( B + 1 )
14 13 2 breqtrri 
 |-  A <_ C
15 1z 
 |-  1 e. ZZ
16 nnz 
 |-  ( B e. NN -> B e. ZZ )
17 peano2z 
 |-  ( B e. ZZ -> ( B + 1 ) e. ZZ )
18 3 16 17 mp2b 
 |-  ( B + 1 ) e. ZZ
19 2 18 eqeltri 
 |-  C e. ZZ
20 elfz1 
 |-  ( ( 1 e. ZZ /\ C e. ZZ ) -> ( A e. ( 1 ... C ) <-> ( A e. ZZ /\ 1 <_ A /\ A <_ C ) ) )
21 15 19 20 mp2an 
 |-  ( A e. ( 1 ... C ) <-> ( A e. ZZ /\ 1 <_ A /\ A <_ C ) )
22 5 7 14 21 mpbir3an 
 |-  A e. ( 1 ... C )