Step |
Hyp |
Ref |
Expression |
1 |
|
binom2.1 |
⊢ 𝐴 ∈ ℂ |
2 |
|
binom2.2 |
⊢ 𝐵 ∈ ℂ |
3 |
1 2
|
subsqi |
⊢ ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) |
4 |
3
|
eqeq1i |
⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = 0 ) |
5 |
1
|
sqcli |
⊢ ( 𝐴 ↑ 2 ) ∈ ℂ |
6 |
2
|
sqcli |
⊢ ( 𝐵 ↑ 2 ) ∈ ℂ |
7 |
5 6
|
subeq0i |
⊢ ( ( ( 𝐴 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ) |
8 |
1 2
|
addcli |
⊢ ( 𝐴 + 𝐵 ) ∈ ℂ |
9 |
1 2
|
subcli |
⊢ ( 𝐴 − 𝐵 ) ∈ ℂ |
10 |
8 9
|
mul0ori |
⊢ ( ( ( 𝐴 + 𝐵 ) · ( 𝐴 − 𝐵 ) ) = 0 ↔ ( ( 𝐴 + 𝐵 ) = 0 ∨ ( 𝐴 − 𝐵 ) = 0 ) ) |
11 |
4 7 10
|
3bitr3i |
⊢ ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( ( 𝐴 + 𝐵 ) = 0 ∨ ( 𝐴 − 𝐵 ) = 0 ) ) |
12 |
|
orcom |
⊢ ( ( ( 𝐴 + 𝐵 ) = 0 ∨ ( 𝐴 − 𝐵 ) = 0 ) ↔ ( ( 𝐴 − 𝐵 ) = 0 ∨ ( 𝐴 + 𝐵 ) = 0 ) ) |
13 |
1 2
|
subeq0i |
⊢ ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) |
14 |
1 2
|
subnegi |
⊢ ( 𝐴 − - 𝐵 ) = ( 𝐴 + 𝐵 ) |
15 |
14
|
eqeq1i |
⊢ ( ( 𝐴 − - 𝐵 ) = 0 ↔ ( 𝐴 + 𝐵 ) = 0 ) |
16 |
2
|
negcli |
⊢ - 𝐵 ∈ ℂ |
17 |
1 16
|
subeq0i |
⊢ ( ( 𝐴 − - 𝐵 ) = 0 ↔ 𝐴 = - 𝐵 ) |
18 |
15 17
|
bitr3i |
⊢ ( ( 𝐴 + 𝐵 ) = 0 ↔ 𝐴 = - 𝐵 ) |
19 |
13 18
|
orbi12i |
⊢ ( ( ( 𝐴 − 𝐵 ) = 0 ∨ ( 𝐴 + 𝐵 ) = 0 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) ) |
20 |
11 12 19
|
3bitri |
⊢ ( ( 𝐴 ↑ 2 ) = ( 𝐵 ↑ 2 ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = - 𝐵 ) ) |