Theorem lineq

Description: Solution of a (scalar) linear equation. (Contributed by BJ, 6-Jun-2019)

	Ref	Expression
Hypotheses	lineq.a	$$⊢\phi \to A\in ℂ$$
	lineq.b	$$⊢\phi \to B\in ℂ$$
	lineq.x	$$⊢\phi \to X\in ℂ$$
	lineq.y	$$⊢\phi \to Y\in ℂ$$
	lineq.n0	$$⊢\phi \to A\ne 0$$
Assertion	lineq	$$⊢\phi \to \left(AX+B=Y\leftrightarrow X=\frac{Y-B}{A}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lineq.a	$$⊢\phi \to A\in ℂ$$
2		lineq.b	$$⊢\phi \to B\in ℂ$$
3		lineq.x	$$⊢\phi \to X\in ℂ$$
4		lineq.y	$$⊢\phi \to Y\in ℂ$$
5		lineq.n0	$$⊢\phi \to A\ne 0$$
6	1 3	mulcld	$$⊢\phi \to AX\in ℂ$$
7	6 2 4	addlsub	$$⊢\phi \to \left(AX+B=Y\leftrightarrow AX=Y-B\right)$$
8	4 2	subcld	$$⊢\phi \to Y-B\in ℂ$$
9	1 3 8 5	rdiv	$$⊢\phi \to \left(AX=Y-B\leftrightarrow X=\frac{Y-B}{A}\right)$$
10	7 9	bitrd	$$⊢\phi \to \left(AX+B=Y\leftrightarrow X=\frac{Y-B}{A}\right)$$