Metamath Proof Explorer


Theorem sqrecd

Description: Square of reciprocal is reciprocal of square. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses expcld.1 φA
sqrecd.1 φA0
Assertion sqrecd φ1A2=1A2

Proof

Step Hyp Ref Expression
1 expcld.1 φA
2 sqrecd.1 φA0
3 2z 2
4 3 a1i φ2
5 exprec AA021A2=1A2
6 1 2 4 5 syl3anc φ1A2=1A2