Step |
Hyp |
Ref |
Expression |
1 |
|
binom2.1 |
|- A e. CC |
2 |
|
binom2.2 |
|- B e. CC |
3 |
1 2
|
subsqi |
|- ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) |
4 |
3
|
eqeq1i |
|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( ( A + B ) x. ( A - B ) ) = 0 ) |
5 |
1
|
sqcli |
|- ( A ^ 2 ) e. CC |
6 |
2
|
sqcli |
|- ( B ^ 2 ) e. CC |
7 |
5 6
|
subeq0i |
|- ( ( ( A ^ 2 ) - ( B ^ 2 ) ) = 0 <-> ( A ^ 2 ) = ( B ^ 2 ) ) |
8 |
1 2
|
addcli |
|- ( A + B ) e. CC |
9 |
1 2
|
subcli |
|- ( A - B ) e. CC |
10 |
8 9
|
mul0ori |
|- ( ( ( A + B ) x. ( A - B ) ) = 0 <-> ( ( A + B ) = 0 \/ ( A - B ) = 0 ) ) |
11 |
4 7 10
|
3bitr3i |
|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( ( A + B ) = 0 \/ ( A - B ) = 0 ) ) |
12 |
|
orcom |
|- ( ( ( A + B ) = 0 \/ ( A - B ) = 0 ) <-> ( ( A - B ) = 0 \/ ( A + B ) = 0 ) ) |
13 |
1 2
|
subeq0i |
|- ( ( A - B ) = 0 <-> A = B ) |
14 |
1 2
|
subnegi |
|- ( A - -u B ) = ( A + B ) |
15 |
14
|
eqeq1i |
|- ( ( A - -u B ) = 0 <-> ( A + B ) = 0 ) |
16 |
2
|
negcli |
|- -u B e. CC |
17 |
1 16
|
subeq0i |
|- ( ( A - -u B ) = 0 <-> A = -u B ) |
18 |
15 17
|
bitr3i |
|- ( ( A + B ) = 0 <-> A = -u B ) |
19 |
13 18
|
orbi12i |
|- ( ( ( A - B ) = 0 \/ ( A + B ) = 0 ) <-> ( A = B \/ A = -u B ) ) |
20 |
11 12 19
|
3bitri |
|- ( ( A ^ 2 ) = ( B ^ 2 ) <-> ( A = B \/ A = -u B ) ) |