xdivrec

Description: Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017)

		Ref	Expression
	Assertion	xdivrec	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = A \cdot_{𝑒} (1 \div_{𝑒} B)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to B \in ℝ$
2	1	rexrd	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to B \in ℝ^{}$
3		simp1	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to A \in ℝ^{}$
4		1xr	$⊢ 1 \in ℝ^{*}$
5	4	a1i	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to 1 \in ℝ^{}$
6		simp3	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to B \neq 0$
7	5 1 6	xdivcld	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to 1 \div_{𝑒} B \in ℝ^{}$
8	3 7	xmulcld	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to A \cdot_{𝑒} (1 \div_{𝑒} B) \in ℝ^{}$
9		xmulcom	$⊢ (B \in ℝ^{} \land A \cdot_{𝑒} (1 \div_{𝑒} B) \in ℝ^{}) \to B \cdot_{𝑒} (A \cdot_{𝑒} (1 \div_{𝑒} B)) = (A \cdot_{𝑒} (1 \div_{𝑒} B)) \cdot_{𝑒} B$
10	2 8 9	syl2anc	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to B \cdot_{𝑒} (A \cdot_{𝑒} (1 \div_{𝑒} B)) = (A \cdot_{𝑒} (1 \div_{𝑒} B)) \cdot_{𝑒} B$
11		xmulass	$⊢ (A \in ℝ^{} \land 1 \div_{𝑒} B \in ℝ^{} \land B \in ℝ^{*}) \to (A \cdot_{𝑒} (1 \div_{𝑒} B)) \cdot_{𝑒} B = A \cdot_{𝑒} ((1 \div_{𝑒} B) \cdot_{𝑒} B)$
12	3 7 2 11	syl3anc	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to (A \cdot_{𝑒} (1 \div_{𝑒} B)) \cdot_{𝑒} B = A \cdot_{𝑒} ((1 \div_{𝑒} B) \cdot_{𝑒} B)$
13		xmulcom	$⊢ (1 \div_{𝑒} B \in ℝ^{} \land B \in ℝ^{}) \to (1 \div_{𝑒} B) \cdot_{𝑒} B = B \cdot_{𝑒} (1 \div_{𝑒} B)$
14	7 2 13	syl2anc	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to (1 \div_{𝑒} B) \cdot_{𝑒} B = B \cdot_{𝑒} (1 \div_{𝑒} B)$
15		eqid	$⊢ 1 \div_{𝑒} B = 1 \div_{𝑒} B$
16		xdivmul	$⊢ (1 \in ℝ^{} \land 1 \div_{𝑒} B \in ℝ^{} \land (B \in ℝ \land B \neq 0)) \to (1 \div_{𝑒} B = 1 \div_{𝑒} B \leftrightarrow B \cdot_{𝑒} (1 \div_{𝑒} B) = 1)$
17	5 7 1 6 16	syl112anc	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to (1 \div_{𝑒} B = 1 \div_{𝑒} B \leftrightarrow B \cdot_{𝑒} (1 \div_{𝑒} B) = 1)$
18	15 17	mpbii	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to B \cdot_{𝑒} (1 \div_{𝑒} B) = 1$
19	14 18	eqtrd	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to (1 \div_{𝑒} B) \cdot_{𝑒} B = 1$
20	19	oveq2d	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to A \cdot_{𝑒} ((1 \div_{𝑒} B) \cdot_{𝑒} B) = A \cdot_{𝑒} 1$
21	10 12 20	3eqtrd	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to B \cdot_{𝑒} (A \cdot_{𝑒} (1 \div_{𝑒} B)) = A \cdot_{𝑒} 1$
22		xmulid1	$⊢ A \in ℝ^{*} \to A \cdot_{𝑒} 1 = A$
23	3 22	syl	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to A \cdot_{𝑒} 1 = A$
24	21 23	eqtrd	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to B \cdot_{𝑒} (A \cdot_{𝑒} (1 \div_{𝑒} B)) = A$
25		xdivmul	$⊢ (A \in ℝ^{} \land A \cdot_{𝑒} (1 \div_{𝑒} B) \in ℝ^{} \land (B \in ℝ \land B \neq 0)) \to (A \div_{𝑒} B = A \cdot_{𝑒} (1 \div_{𝑒} B) \leftrightarrow B \cdot_{𝑒} (A \cdot_{𝑒} (1 \div_{𝑒} B)) = A)$
26	3 8 1 6 25	syl112anc	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to (A \div_{𝑒} B = A \cdot_{𝑒} (1 \div_{𝑒} B) \leftrightarrow B \cdot_{𝑒} (A \cdot_{𝑒} (1 \div_{𝑒} B)) = A)$
27	24 26	mpbird	$⊢ (A \in ℝ^{*} \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = A \cdot_{𝑒} (1 \div_{𝑒} B)$

Metamath Proof Explorer

Theorem xdivrec

Proof