Metamath Proof Explorer


Theorem rec11r

Description: Mutual reciprocals. (Contributed by Paul Chapman, 18-Oct-2007)

Ref Expression
Assertion rec11r ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = 𝐵 ↔ ( 1 / 𝐵 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 1cnd ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 1 ∈ ℂ )
2 simprl ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
3 simpll ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
4 simplr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
5 divmul2 ( ( 1 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = 𝐵 ↔ 1 = ( 𝐴 · 𝐵 ) ) )
6 1 2 3 4 5 syl112anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = 𝐵 ↔ 1 = ( 𝐴 · 𝐵 ) ) )
7 simprr ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
8 divmul3 ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐵 ) = 𝐴 ↔ 1 = ( 𝐴 · 𝐵 ) ) )
9 1 3 2 7 8 syl112anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐵 ) = 𝐴 ↔ 1 = ( 𝐴 · 𝐵 ) ) )
10 6 9 bitr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = 𝐵 ↔ ( 1 / 𝐵 ) = 𝐴 ) )