lineq

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

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

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

Metamath Proof Explorer