Theorem 2sqreulem2

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

	Ref	Expression
Assertion	2sqreulem2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) → 𝐵 = 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
2	1	sqcld	⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 ↑ 2 ) ∈ ℂ )
3	2	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
4		nn0cn	⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℂ )
5	4	sqcld	⊢ ( 𝐵 ∈ ℕ0 → ( 𝐵 ↑ 2 ) ∈ ℂ )
6	5	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
7		nn0cn	⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
8	7	sqcld	⊢ ( 𝐶 ∈ ℕ0 → ( 𝐶 ↑ 2 ) ∈ ℂ )
9	8	3ad2ant3	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
10	3 6 9	addcand	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) = ( 𝐶 ↑ 2 ) ) )
11		nn0sq11	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) = ( 𝐶 ↑ 2 ) ↔ 𝐵 = 𝐶 ) )
12	11	biimpd	⊢ ( ( 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) = ( 𝐶 ↑ 2 ) → 𝐵 = 𝐶 ) )
13	12	3adant1	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐵 ↑ 2 ) = ( 𝐶 ↑ 2 ) → 𝐵 = 𝐶 ) )
14	10 13	sylbid	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0 ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) → 𝐵 = 𝐶 ) )