Metamath Proof Explorer

Theorem divrec

Description: Relationship between division and reciprocal. Theorem I.9 of Apostol p. 18. (Contributed by NM, 2-Aug-2004) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	divrec	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B \in ℂ$
2		simp1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A \in ℂ$
3		reccl	$⊢ (B \in ℂ \land B \neq 0) \to \frac{1}{B} \in ℂ$
4	3	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{1}{B} \in ℂ$
5	1 2 4	mul12d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B A (\frac{1}{B}) = A B (\frac{1}{B})$
6		recid	$⊢ (B \in ℂ \land B \neq 0) \to B (\frac{1}{B}) = 1$
7	6	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B (\frac{1}{B}) = 1$
8	7	oveq2d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A B (\frac{1}{B}) = A \cdot 1$
9	2	mulridd	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A \cdot 1 = A$
10	5 8 9	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B A (\frac{1}{B}) = A$
11	2 4	mulcld	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A (\frac{1}{B}) \in ℂ$
12		3simpc	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (B \in ℂ \land B \neq 0)$
13		divmul	$⊢ (A \in ℂ \land A (\frac{1}{B}) \in ℂ \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{B} = A (\frac{1}{B}) \leftrightarrow B A (\frac{1}{B}) = A)$
14	2 11 12 13	syl3anc	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (\frac{A}{B} = A (\frac{1}{B}) \leftrightarrow B A (\frac{1}{B}) = A)$
15	10 14	mpbird	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$