Theorem lineq

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

	Ref	Expression
Hypotheses	lineq.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	lineq.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	lineq.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	lineq.y	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
	lineq.n0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion	lineq	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) = 𝑌 ↔ 𝑋 = ( ( 𝑌 − 𝐵 ) / 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lineq.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		lineq.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		lineq.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4		lineq.y	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
5		lineq.n0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
6	1 3	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ℂ )
7	6 2 4	addlsub	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) = 𝑌 ↔ ( 𝐴 · 𝑋 ) = ( 𝑌 − 𝐵 ) ) )
8	4 2	subcld	⊢ ( 𝜑 → ( 𝑌 − 𝐵 ) ∈ ℂ )
9	1 3 8 5	rdiv	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝑌 − 𝐵 ) ↔ 𝑋 = ( ( 𝑌 − 𝐵 ) / 𝐴 ) ) )
10	7 9	bitrd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) + 𝐵 ) = 𝑌 ↔ 𝑋 = ( ( 𝑌 − 𝐵 ) / 𝐴 ) ) )