Theorem rexdiv

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

	Ref	Expression
Assertion	rexdiv	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( 𝐴 / 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		redivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
2		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
4		id	⊢ ( 𝐵 ≠ 0 → 𝐵 ≠ 0 )
5	2 3 4	3anim123i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
6		divcan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐵 · ( 𝐴 / 𝐵 ) ) = 𝐴 )
7	5 6	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐵 · ( 𝐴 / 𝐵 ) ) = 𝐴 )
8		oveq2	⊢ ( 𝑥 = ( 𝐴 / 𝐵 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( 𝐴 / 𝐵 ) ) )
9	8	eqeq1d	⊢ ( 𝑥 = ( 𝐴 / 𝐵 ) → ( ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( 𝐵 · ( 𝐴 / 𝐵 ) ) = 𝐴 ) )
10	9	rspcev	⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ ( 𝐵 · ( 𝐴 / 𝐵 ) ) = 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )
11	1 7 10	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )
12		receu	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )
13	5 12	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )
14		ax-resscn	⊢ ℝ ⊆ ℂ
15		id	⊢ ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 · 𝑥 ) = 𝐴 )
16	15	rgenw	⊢ ∀ 𝑥 ∈ ℝ ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 · 𝑥 ) = 𝐴 )
17		riotass2	⊢ ( ( ( ℝ ⊆ ℂ ∧ ∀ 𝑥 ∈ ℝ ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 · 𝑥 ) = 𝐴 ) ) ∧ ( ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ∧ ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) ) → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
18	14 16 17	mpanl12	⊢ ( ( ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ∧ ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
19	11 13 18	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
20		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
21		xdivval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
22	20 21	syl3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
23		ressxr	⊢ ℝ ⊆ ℝ*
24	23	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ℝ ⊆ ℝ* )
25		rexmul	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐵 ·e 𝑥 ) = ( 𝐵 · 𝑥 ) )
26	25	eqeq1d	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 ·e 𝑥 ) = 𝐴 ↔ ( 𝐵 · 𝑥 ) = 𝐴 ) )
27	26	biimprd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
28	27	ralrimiva	⊢ ( 𝐵 ∈ ℝ → ∀ 𝑥 ∈ ℝ ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
29	28	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∀ 𝑥 ∈ ℝ ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
30		xreceu	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
31	20 30	syl3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 )
32		riotass2	⊢ ( ( ( ℝ ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ( ( 𝐵 · 𝑥 ) = 𝐴 → ( 𝐵 ·e 𝑥 ) = 𝐴 ) ) ∧ ( ∃ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ∧ ∃! 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) ) → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
33	24 29 11 31 32	syl22anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐵 ·e 𝑥 ) = 𝐴 ) )
34	22 33	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )
35		divval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
36	5 35	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( ℩ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
37	19 34 36	3eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 /𝑒 𝐵 ) = ( 𝐴 / 𝐵 ) )