This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqdivid

Description: The square of a nonzero complex number divided by itself equals that number. (Contributed by AV, 19-Jul-2021)

		Ref	Expression
	Assertion	sqdivid	$⊢ (A \in ℂ \land A \neq 0) \to \frac{A^{2}}{A} = A$

Step	Hyp	Ref	Expression
1		sqval	$⊢ A \in ℂ \to A^{2} = A A$
2	1	adantr	$⊢ (A \in ℂ \land A \neq 0) \to A^{2} = A A$
3	2	oveq1d	$⊢ (A \in ℂ \land A \neq 0) \to \frac{A^{2}}{A} = \frac{A A}{A}$
4		divcan3	$⊢ (A \in ℂ \land A \in ℂ \land A \neq 0) \to \frac{A A}{A} = A$
5	4	3anidm12	$⊢ (A \in ℂ \land A \neq 0) \to \frac{A A}{A} = A$
6	3 5	eqtrd	$⊢ (A \in ℂ \land A \neq 0) \to \frac{A^{2}}{A} = A$