nn0sq11

Description: The square function is one-to-one for nonnegative integers. (Contributed by AV, 25-Jun-2023)

		Ref	Expression
	Assertion	nn0sq11	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} = B^{2} \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
2		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
3	1 2	jca	$⊢ A \in ℕ_{0} \to (A \in ℝ \land 0 \leq A)$
4		nn0re	$⊢ B \in ℕ_{0} \to B \in ℝ$
5		nn0ge0	$⊢ B \in ℕ_{0} \to 0 \leq B$
6	4 5	jca	$⊢ B \in ℕ_{0} \to (B \in ℝ \land 0 \leq B)$
7		sq11	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A^{2} = B^{2} \leftrightarrow A = B)$
8	3 6 7	syl2an	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A^{2} = B^{2} \leftrightarrow A = B)$

Metamath Proof Explorer