Theorem nn0sq11

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

	Ref	Expression
Assertion	nn0sq11	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
2		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
3	1 2	jca	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
4		nn0re	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℝ )
5		nn0ge0	⊢ ( 𝐵 ∈ ℕ0 → 0 ≤ 𝐵 )
6	4 5	jca	⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
7		sq11	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ 𝐴 = 𝐵 ) )
8	3 6 7	syl2an	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ 𝐴 = 𝐵 ) )