Theorem xdivmul

Description: Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016)

	Ref	Expression
Assertion	xdivmul	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 /𝑒 𝐶 ) = 𝐵 ↔ ( 𝐶 ·e 𝐵 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xdivval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ( 𝐴 /𝑒 𝐶 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) )
2	1	3expb	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 /𝑒 𝐶 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) )
3	2	3adant2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 /𝑒 𝐶 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) )
4	3	eqeq1d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 /𝑒 𝐶 ) = 𝐵 ↔ ( ℩ 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) = 𝐵 ) )
5		simp2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℝ* )
6		xreceu	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) → ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 )
7	6	3expb	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 )
8	7	3adant2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 )
9		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐶 ·e 𝑥 ) = ( 𝐶 ·e 𝐵 ) )
10	9	eqeq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ·e 𝑥 ) = 𝐴 ↔ ( 𝐶 ·e 𝐵 ) = 𝐴 ) )
11	10	riota2	⊢ ( ( 𝐵 ∈ ℝ* ∧ ∃! 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) → ( ( 𝐶 ·e 𝐵 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) = 𝐵 ) )
12	5 8 11	syl2anc	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 ·e 𝐵 ) = 𝐴 ↔ ( ℩ 𝑥 ∈ ℝ* ( 𝐶 ·e 𝑥 ) = 𝐴 ) = 𝐵 ) )
13	4 12	bitr4d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐶 ∈ ℝ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 /𝑒 𝐶 ) = 𝐵 ↔ ( 𝐶 ·e 𝐵 ) = 𝐴 ) )