Step |
Hyp |
Ref |
Expression |
1 |
|
flval |
|- ( A e. RR -> ( |_ ` A ) = ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) ) |
2 |
1
|
eqcomd |
|- ( A e. RR -> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` A ) ) |
3 |
|
flcl |
|- ( A e. RR -> ( |_ ` A ) e. ZZ ) |
4 |
|
rebtwnz |
|- ( A e. RR -> E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) |
5 |
|
breq1 |
|- ( x = ( |_ ` A ) -> ( x <_ A <-> ( |_ ` A ) <_ A ) ) |
6 |
|
oveq1 |
|- ( x = ( |_ ` A ) -> ( x + 1 ) = ( ( |_ ` A ) + 1 ) ) |
7 |
6
|
breq2d |
|- ( x = ( |_ ` A ) -> ( A < ( x + 1 ) <-> A < ( ( |_ ` A ) + 1 ) ) ) |
8 |
5 7
|
anbi12d |
|- ( x = ( |_ ` A ) -> ( ( x <_ A /\ A < ( x + 1 ) ) <-> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) ) ) |
9 |
8
|
riota2 |
|- ( ( ( |_ ` A ) e. ZZ /\ E! x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) -> ( ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` A ) ) ) |
10 |
3 4 9
|
syl2anc |
|- ( A e. RR -> ( ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) <-> ( iota_ x e. ZZ ( x <_ A /\ A < ( x + 1 ) ) ) = ( |_ ` A ) ) ) |
11 |
2 10
|
mpbird |
|- ( A e. RR -> ( ( |_ ` A ) <_ A /\ A < ( ( |_ ` A ) + 1 ) ) ) |