Metamath Proof Explorer

Theorem rexdiv

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

Ref Expression
Assertion rexdiv ⊢A∈ℝ∧B∈ℝ∧B≠0→A÷𝑒B=AB

Proof

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