Theorem nn0sq11

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

	Ref	Expression
Assertion	nn0sq11	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
2		nn0ge0	$$⊢A\in {\mathbb{N}}_0\to 0\le A$$
3	1 2	jca	$$⊢A\in {\mathbb{N}}_0\to \left(A\in ℝ\wedge 0\le A\right)$$
4		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
5		nn0ge0	$$⊢B\in {\mathbb{N}}_0\to 0\le B$$
6	4 5	jca	$$⊢B\in {\mathbb{N}}_0\to \left(B\in ℝ\wedge 0\le B\right)$$
7		sq11	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$
8	3 6 7	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$