Description: Reciprocal is one-to-one. (Contributed by NM, 16-Sep-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | divclz.1 | ⊢ 𝐴 ∈ ℂ | |
divclz.2 | ⊢ 𝐵 ∈ ℂ | ||
Assertion | rec11i | ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) → ( ( 1 / 𝐴 ) = ( 1 / 𝐵 ) ↔ 𝐴 = 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divclz.1 | ⊢ 𝐴 ∈ ℂ | |
2 | divclz.2 | ⊢ 𝐵 ∈ ℂ | |
3 | rec11 | ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = ( 1 / 𝐵 ) ↔ 𝐴 = 𝐵 ) ) | |
4 | 3 | an4s | ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = ( 1 / 𝐵 ) ↔ 𝐴 = 𝐵 ) ) |
5 | 1 2 4 | mpanl12 | ⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) → ( ( 1 / 𝐴 ) = ( 1 / 𝐵 ) ↔ 𝐴 = 𝐵 ) ) |