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

Metamath Proof Explorer

Theorem rec11

Description: Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 1cnd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 ∈ ℂ
2 reccl ⊢ B ∈ ℂ ∧ B ≠ 0 → 1 B ∈ ℂ
3 2 adantl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 B ∈ ℂ
4 simpl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ ∧ A ≠ 0
5 divmul ⊢ 1 ∈ ℂ ∧ 1 B ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → 1 A = 1 B ↔ A ⁢ 1 B = 1
6 1 3 4 5 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A = 1 B ↔ A ⁢ 1 B = 1
7 simpll ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
8 simprl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
9 simprr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B ≠ 0
10 divrec ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B
11 7 8 9 10 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B
12 11 eqeq1d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A ⁢ 1 B = 1
13 diveq1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B
14 7 8 9 13 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B
15 6 12 14 3bitr2d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A = 1 B ↔ A = B