Metamath Proof Explorer

Theorem ddcan

Description: Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion ddcan ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A A B = B

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
2 simprl ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
3 simprr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → B ≠ 0
4 divcan1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ B = A
5 1 2 3 4 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ B = A
6 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
7 1 2 3 6 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
8 divne0 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A B ≠ 0
9 divmul ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A B ∈ ℂ ∧ A B ≠ 0 → A A B = B ↔ A B ⁢ B = A
10 1 2 7 8 9 syl112anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A A B = B ↔ A B ⁢ B = A
11 5 10 mpbird ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → A A B = B