Step |
Hyp |
Ref |
Expression |
1 |
|
elfzofz |
|- ( A e. ( M ..^ N ) -> A e. ( M ... N ) ) |
2 |
|
elfzolt2 |
|- ( A e. ( M ..^ N ) -> A < N ) |
3 |
1 2
|
jca |
|- ( A e. ( M ..^ N ) -> ( A e. ( M ... N ) /\ A < N ) ) |
4 |
|
elfzuz |
|- ( A e. ( M ... N ) -> A e. ( ZZ>= ` M ) ) |
5 |
4
|
adantr |
|- ( ( A e. ( M ... N ) /\ A < N ) -> A e. ( ZZ>= ` M ) ) |
6 |
|
elfzel2 |
|- ( A e. ( M ... N ) -> N e. ZZ ) |
7 |
6
|
adantr |
|- ( ( A e. ( M ... N ) /\ A < N ) -> N e. ZZ ) |
8 |
|
simpr |
|- ( ( A e. ( M ... N ) /\ A < N ) -> A < N ) |
9 |
|
elfzo2 |
|- ( A e. ( M ..^ N ) <-> ( A e. ( ZZ>= ` M ) /\ N e. ZZ /\ A < N ) ) |
10 |
5 7 8 9
|
syl3anbrc |
|- ( ( A e. ( M ... N ) /\ A < N ) -> A e. ( M ..^ N ) ) |
11 |
3 10
|
impbii |
|- ( A e. ( M ..^ N ) <-> ( A e. ( M ... N ) /\ A < N ) ) |