Step |
Hyp |
Ref |
Expression |
1 |
|
divccncf.1 |
|- F = ( x e. CC |-> ( x / A ) ) |
2 |
|
divrec2 |
|- ( ( x e. CC /\ A e. CC /\ A =/= 0 ) -> ( x / A ) = ( ( 1 / A ) x. x ) ) |
3 |
2
|
3expb |
|- ( ( x e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( x / A ) = ( ( 1 / A ) x. x ) ) |
4 |
3
|
ancoms |
|- ( ( ( A e. CC /\ A =/= 0 ) /\ x e. CC ) -> ( x / A ) = ( ( 1 / A ) x. x ) ) |
5 |
4
|
mpteq2dva |
|- ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) = ( x e. CC |-> ( ( 1 / A ) x. x ) ) ) |
6 |
1 5
|
syl5eq |
|- ( ( A e. CC /\ A =/= 0 ) -> F = ( x e. CC |-> ( ( 1 / A ) x. x ) ) ) |
7 |
|
reccl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC ) |
8 |
|
eqid |
|- ( x e. CC |-> ( ( 1 / A ) x. x ) ) = ( x e. CC |-> ( ( 1 / A ) x. x ) ) |
9 |
8
|
mulc1cncf |
|- ( ( 1 / A ) e. CC -> ( x e. CC |-> ( ( 1 / A ) x. x ) ) e. ( CC -cn-> CC ) ) |
10 |
7 9
|
syl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( ( 1 / A ) x. x ) ) e. ( CC -cn-> CC ) ) |
11 |
6 10
|
eqeltrd |
|- ( ( A e. CC /\ A =/= 0 ) -> F e. ( CC -cn-> CC ) ) |