Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
sqrecii
Next ⟩
sqmuli
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqrecii
Description:
Square of reciprocal.
(Contributed by
NM
, 17-Sep-1999)
Ref
Expression
Hypotheses
sqval.1
⊢
A
∈
ℂ
sqreci.1
⊢
A
≠
0
Assertion
sqrecii
⊢
1
A
2
=
1
A
2
Proof
Step
Hyp
Ref
Expression
1
sqval.1
⊢
A
∈
ℂ
2
sqreci.1
⊢
A
≠
0
3
ax-1cn
⊢
1
∈
ℂ
4
3
1
3
1
2
2
divmuldivi
⊢
1
A
⁢
1
A
=
1
⋅
1
A
⁢
A
5
1t1e1
⊢
1
⋅
1
=
1
6
5
oveq1i
⊢
1
⋅
1
A
⁢
A
=
1
A
⁢
A
7
4
6
eqtri
⊢
1
A
⁢
1
A
=
1
A
⁢
A
8
1
2
reccli
⊢
1
A
∈
ℂ
9
8
sqvali
⊢
1
A
2
=
1
A
⁢
1
A
10
1
sqvali
⊢
A
2
=
A
⁢
A
11
10
oveq2i
⊢
1
A
2
=
1
A
⁢
A
12
7
9
11
3eqtr4i
⊢
1
A
2
=
1
A
2