Theorem bj-lineqi

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

	Ref	Expression
Hypotheses	bj-lineqi.a	$$⊢\phi \to A\in ℂ$$
	bj-lineqi.b	$$⊢\phi \to B\in ℂ$$
	bj-lineqi.x	$$⊢\phi \to X\in ℂ$$
	bj-lineqi.y	$$⊢\phi \to Y\in ℂ$$
	bj-lineqi.n0	$$⊢\phi \to A\ne 0$$
	bj-lineqi.1	$$⊢\phi \to AX+B=Y$$
Assertion	bj-lineqi	$$⊢\phi \to X=\frac{Y-B}{A}$$

Proof

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