Metamath Proof Explorer

Theorem rec11r

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

Ref Expression
Assertion rec11r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A = B ↔ 1 B = A

Proof

Step Hyp Ref Expression
1 1cnd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 ∈ ℂ
2 simprl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
3 simpll ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
4 simplr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A ≠ 0
5 divmul2 ⊢ 1 ∈ ℂ ∧ B ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → 1 A = B ↔ 1 = A ⁢ B
6 1 2 3 4 5 syl112anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A = B ↔ 1 = A ⁢ B
7 simprr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B ≠ 0
8 divmul3 ⊢ 1 ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 1 B = A ↔ 1 = A ⁢ B
9 1 3 2 7 8 syl112anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 B = A ↔ 1 = A ⁢ B
10 6 9 bitr4d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A = B ↔ 1 B = A