Theorem div2sub

Description: Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013)

	Ref	Expression
Assertion	div2sub	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐷 − 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
2		subcl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
3	2	3adant3	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → ( 𝐶 − 𝐷 ) ∈ ℂ )
4		subeq0	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) = 0 ↔ 𝐶 = 𝐷 ) )
5	4	necon3bid	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) ≠ 0 ↔ 𝐶 ≠ 𝐷 ) )
6	5	biimp3ar	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → ( 𝐶 − 𝐷 ) ≠ 0 )
7	3 6	jca	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → ( ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ≠ 0 ) )
8		div2neg	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ≠ 0 ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) )
9	8	3expb	⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℂ ∧ ( ( 𝐶 − 𝐷 ) ∈ ℂ ∧ ( 𝐶 − 𝐷 ) ≠ 0 ) ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) )
10	1 7 9	syl2an	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) )
11		negsubdi2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → - ( 𝐴 − 𝐵 ) = ( 𝐵 − 𝐴 ) )
12		negsubdi2	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
13	12	3adant3	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) → - ( 𝐶 − 𝐷 ) = ( 𝐷 − 𝐶 ) )
14	11 13	oveqan12d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( - ( 𝐴 − 𝐵 ) / - ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐷 − 𝐶 ) ) )
15	10 14	eqtr3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 ≠ 𝐷 ) ) → ( ( 𝐴 − 𝐵 ) / ( 𝐶 − 𝐷 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐷 − 𝐶 ) ) )