Metamath Proof Explorer


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