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 / 𝐵 ) = 𝐴 ) ) |