Metamath Proof Explorer


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 ) ) → 𝐵 = 𝐶 ) )