This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recrecnq

Description: Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 29-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion recrecnq ⊢ A ∈ 𝑸 → * 𝑸 ⁡ * 𝑸 ⁡ A = A

Proof

Step Hyp Ref Expression
1 2fveq3 ⊢ x = A → * 𝑸 ⁡ * 𝑸 ⁡ x = * 𝑸 ⁡ * 𝑸 ⁡ A
2 id ⊢ x = A → x = A
3 1 2 eqeq12d ⊢ x = A → * 𝑸 ⁡ * 𝑸 ⁡ x = x ↔ * 𝑸 ⁡ * 𝑸 ⁡ A = A
4 mulcomnq ⊢ * 𝑸 ⁡ x ⋅ 𝑸 x = x ⋅ 𝑸 * 𝑸 ⁡ x
5 recidnq ⊢ x ∈ 𝑸 → x ⋅ 𝑸 * 𝑸 ⁡ x = 1 𝑸
6 4 5 eqtrid ⊢ x ∈ 𝑸 → * 𝑸 ⁡ x ⋅ 𝑸 x = 1 𝑸
7 recclnq ⊢ x ∈ 𝑸 → * 𝑸 ⁡ x ∈ 𝑸
8 recmulnq ⊢ * 𝑸 ⁡ x ∈ 𝑸 → * 𝑸 ⁡ * 𝑸 ⁡ x = x ↔ * 𝑸 ⁡ x ⋅ 𝑸 x = 1 𝑸
9 7 8 syl ⊢ x ∈ 𝑸 → * 𝑸 ⁡ * 𝑸 ⁡ x = x ↔ * 𝑸 ⁡ x ⋅ 𝑸 x = 1 𝑸
10 6 9 mpbird ⊢ x ∈ 𝑸 → * 𝑸 ⁡ * 𝑸 ⁡ x = x
11 3 10 vtoclga ⊢ A ∈ 𝑸 → * 𝑸 ⁡ * 𝑸 ⁡ A = A