Theorem 2sqreulem2

Description: Lemma 2 for 2sqreu etc. (Contributed by AV, 25-Jun-2023)

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

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢A\in {\mathbb{N}}_0\to A\in ℂ$$
2	1	sqcld	$$⊢A\in {\mathbb{N}}_0\to A^2\in ℂ$$
3	2	3ad2ant1	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to A^2\in ℂ$$
4		nn0cn	$$⊢B\in {\mathbb{N}}_0\to B\in ℂ$$
5	4	sqcld	$$⊢B\in {\mathbb{N}}_0\to B^2\in ℂ$$
6	5	3ad2ant2	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to B^2\in ℂ$$
7		nn0cn	$$⊢C\in {\mathbb{N}}_0\to C\in ℂ$$
8	7	sqcld	$$⊢C\in {\mathbb{N}}_0\to C^2\in ℂ$$
9	8	3ad2ant3	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to C^2\in ℂ$$
10	3 6 9	addcand	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(A^2+B^2=A^2+C^2\leftrightarrow B^2=C^2\right)$$
11		nn0sq11	$$⊢\left(B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(B^2=C^2\leftrightarrow B=C\right)$$
12	11	biimpd	$$⊢\left(B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(B^2=C^2\to B=C\right)$$
13	12	3adant1	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(B^2=C^2\to B=C\right)$$
14	10 13	sylbid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\wedge C\in {\mathbb{N}}_0\right)\to \left(A^2+B^2=A^2+C^2\to B=C\right)$$