rexdiv

Description: The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016)

		Ref	Expression
	Assertion	rexdiv	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = \frac{A}{B}$

Proof

Step	Hyp	Ref	Expression
1		redivcl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} \in ℝ$
2		recn	$⊢ A \in ℝ \to A \in ℂ$
3		recn	$⊢ B \in ℝ \to B \in ℂ$
4		id	$⊢ B \neq 0 \to B \neq 0$
5	2 3 4	3anim123i	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to (A \in ℂ \land B \in ℂ \land B \neq 0)$
6		divcan2	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B (\frac{A}{B}) = A$
7	5 6	syl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to B (\frac{A}{B}) = A$
8		oveq2	$⊢ x = \frac{A}{B} \to B x = B (\frac{A}{B})$
9	8	eqeq1d	$⊢ x = \frac{A}{B} \to (B x = A \leftrightarrow B (\frac{A}{B}) = A)$
10	9	rspcev	$⊢ (\frac{A}{B} \in ℝ \land B (\frac{A}{B}) = A) \to \exists x \in ℝ B x = A$
11	1 7 10	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \exists x \in ℝ B x = A$
12		receu	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \exists! x \in ℂ B x = A$
13	5 12	syl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \exists! x \in ℂ B x = A$
14		ax-resscn	$⊢ ℝ \subseteq ℂ$
15		id	$⊢ B x = A \to B x = A$
16	15	rgenw	$⊢ \forall x \in ℝ (B x = A \to B x = A)$
17		riotass2	$⊢ ((ℝ \subseteq ℂ \land \forall x \in ℝ (B x = A \to B x = A)) \land (\exists x \in ℝ B x = A \land \exists! x \in ℂ B x = A)) \to (ι x \in ℝ \| B x = A) = (ι x \in ℂ \| B x = A)$
18	14 16 17	mpanl12	$⊢ (\exists x \in ℝ B x = A \land \exists! x \in ℂ B x = A) \to (ι x \in ℝ \| B x = A) = (ι x \in ℂ \| B x = A)$
19	11 13 18	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to (ι x \in ℝ \| B x = A) = (ι x \in ℂ \| B x = A)$
20		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
21		xdivval	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = (ι x \in ℝ^{} \| B \cdot_{𝑒} x = A)$
22	20 21	syl3an1	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = (ι x \in ℝ^{*} \| B \cdot_{𝑒} x = A)$
23		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
24	23	a1i	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to ℝ \subseteq ℝ^{*}$
25		rexmul	$⊢ (B \in ℝ \land x \in ℝ) \to B \cdot_{𝑒} x = B x$
26	25	eqeq1d	$⊢ (B \in ℝ \land x \in ℝ) \to (B \cdot_{𝑒} x = A \leftrightarrow B x = A)$
27	26	biimprd	$⊢ (B \in ℝ \land x \in ℝ) \to (B x = A \to B \cdot_{𝑒} x = A)$
28	27	ralrimiva	$⊢ B \in ℝ \to \forall x \in ℝ (B x = A \to B \cdot_{𝑒} x = A)$
29	28	3ad2ant2	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \forall x \in ℝ (B x = A \to B \cdot_{𝑒} x = A)$
30		xreceu	$⊢ (A \in ℝ^{} \land B \in ℝ \land B \neq 0) \to \exists! x \in ℝ^{} B \cdot_{𝑒} x = A$
31	20 30	syl3an1	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \exists! x \in ℝ^{*} B \cdot_{𝑒} x = A$
32		riotass2	$⊢ ((ℝ \subseteq ℝ^{} \land \forall x \in ℝ (B x = A \to B \cdot_{𝑒} x = A)) \land (\exists x \in ℝ B x = A \land \exists! x \in ℝ^{} B \cdot_{𝑒} x = A)) \to (ι x \in ℝ \| B x = A) = (ι x \in ℝ^{*} \| B \cdot_{𝑒} x = A)$
33	24 29 11 31 32	syl22anc	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to (ι x \in ℝ \| B x = A) = (ι x \in ℝ^{*} \| B \cdot_{𝑒} x = A)$
34	22 33	eqtr4d	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = (ι x \in ℝ \| B x = A)$
35		divval	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = (ι x \in ℂ \| B x = A)$
36	5 35	syl	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to \frac{A}{B} = (ι x \in ℂ \| B x = A)$
37	19 34 36	3eqtr4d	$⊢ (A \in ℝ \land B \in ℝ \land B \neq 0) \to A \div_{𝑒} B = \frac{A}{B}$

Metamath Proof Explorer

Theorem rexdiv

Proof