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