| Step |
Hyp |
Ref |
Expression |
| 1 |
|
receqid.1 |
|- ( ph -> A e. RR ) |
| 2 |
|
receqid.2 |
|- ( ph -> A =/= 0 ) |
| 3 |
1
|
absred |
|- ( ph -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) ) |
| 4 |
|
sqrt1 |
|- ( sqrt ` 1 ) = 1 |
| 5 |
4
|
a1i |
|- ( ph -> ( sqrt ` 1 ) = 1 ) |
| 6 |
5
|
eqcomd |
|- ( ph -> 1 = ( sqrt ` 1 ) ) |
| 7 |
3 6
|
eqeq12d |
|- ( ph -> ( ( abs ` A ) = 1 <-> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) ) ) |
| 8 |
1
|
resqcld |
|- ( ph -> ( A ^ 2 ) e. RR ) |
| 9 |
1
|
sqge0d |
|- ( ph -> 0 <_ ( A ^ 2 ) ) |
| 10 |
|
1red |
|- ( ph -> 1 e. RR ) |
| 11 |
|
0le1 |
|- 0 <_ 1 |
| 12 |
11
|
a1i |
|- ( ph -> 0 <_ 1 ) |
| 13 |
|
sqrt11 |
|- ( ( ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) <-> ( A ^ 2 ) = 1 ) ) |
| 14 |
8 9 10 12 13
|
syl22anc |
|- ( ph -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) <-> ( A ^ 2 ) = 1 ) ) |
| 15 |
8
|
recnd |
|- ( ph -> ( A ^ 2 ) e. CC ) |
| 16 |
|
1cnd |
|- ( ph -> 1 e. CC ) |
| 17 |
1
|
recnd |
|- ( ph -> A e. CC ) |
| 18 |
|
div11 |
|- ( ( ( A ^ 2 ) e. CC /\ 1 e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( ( A ^ 2 ) / A ) = ( 1 / A ) <-> ( A ^ 2 ) = 1 ) ) |
| 19 |
15 16 17 2 18
|
syl112anc |
|- ( ph -> ( ( ( A ^ 2 ) / A ) = ( 1 / A ) <-> ( A ^ 2 ) = 1 ) ) |
| 20 |
|
sqdivid |
|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^ 2 ) / A ) = A ) |
| 21 |
17 2 20
|
syl2anc |
|- ( ph -> ( ( A ^ 2 ) / A ) = A ) |
| 22 |
21
|
eqeq1d |
|- ( ph -> ( ( ( A ^ 2 ) / A ) = ( 1 / A ) <-> A = ( 1 / A ) ) ) |
| 23 |
14 19 22
|
3bitr2rd |
|- ( ph -> ( A = ( 1 / A ) <-> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) ) ) |
| 24 |
|
eqcom |
|- ( A = ( 1 / A ) <-> ( 1 / A ) = A ) |
| 25 |
24
|
a1i |
|- ( ph -> ( A = ( 1 / A ) <-> ( 1 / A ) = A ) ) |
| 26 |
7 23 25
|
3bitr2rd |
|- ( ph -> ( ( 1 / A ) = A <-> ( abs ` A ) = 1 ) ) |