Theorem divdiv32

Description: Swap denominators in a division. (Contributed by NM, 2-Aug-2004)

	Ref	Expression
Assertion	divdiv32	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		reccl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ ℂ )
2		div23	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 / 𝐵 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
3	1 2	syl3an2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · ( 1 / 𝐵 ) ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
4		divrec	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
5	4	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
6	5	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 · ( 1 / 𝐵 ) ) / 𝐶 ) )
8		divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
9	8	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
10		divrec	⊢ ( ( ( 𝐴 / 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐶 ) / 𝐵 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
11	9 10	syl3an1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐶 ) / 𝐵 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
12	11	3expb	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) / 𝐵 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
13	12	3impa	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) / 𝐵 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
14	13	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) / 𝐵 ) = ( ( 𝐴 / 𝐶 ) · ( 1 / 𝐵 ) ) )
15	3 7 14	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) )