Step |
Hyp |
Ref |
Expression |
1 |
|
intfrac2.1 |
|- Z = ( |_ ` A ) |
2 |
|
intfrac2.2 |
|- F = ( A - Z ) |
3 |
|
fracge0 |
|- ( A e. RR -> 0 <_ ( A - ( |_ ` A ) ) ) |
4 |
1
|
oveq2i |
|- ( A - Z ) = ( A - ( |_ ` A ) ) |
5 |
2 4
|
eqtri |
|- F = ( A - ( |_ ` A ) ) |
6 |
3 5
|
breqtrrdi |
|- ( A e. RR -> 0 <_ F ) |
7 |
|
fraclt1 |
|- ( A e. RR -> ( A - ( |_ ` A ) ) < 1 ) |
8 |
5 7
|
eqbrtrid |
|- ( A e. RR -> F < 1 ) |
9 |
2
|
oveq2i |
|- ( Z + F ) = ( Z + ( A - Z ) ) |
10 |
|
flcl |
|- ( A e. RR -> ( |_ ` A ) e. ZZ ) |
11 |
1 10
|
eqeltrid |
|- ( A e. RR -> Z e. ZZ ) |
12 |
11
|
zcnd |
|- ( A e. RR -> Z e. CC ) |
13 |
|
recn |
|- ( A e. RR -> A e. CC ) |
14 |
12 13
|
pncan3d |
|- ( A e. RR -> ( Z + ( A - Z ) ) = A ) |
15 |
9 14
|
eqtr2id |
|- ( A e. RR -> A = ( Z + F ) ) |
16 |
6 8 15
|
3jca |
|- ( A e. RR -> ( 0 <_ F /\ F < 1 /\ A = ( Z + F ) ) ) |