Step |
Hyp |
Ref |
Expression |
1 |
|
axsegconlem2.1 |
|- S = sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) |
2 |
1
|
axsegconlem4 |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( sqrt ` S ) e. RR ) |
3 |
2
|
3adant3 |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) e. RR ) |
4 |
1
|
axsegconlem5 |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ ( sqrt ` S ) ) |
5 |
4
|
3adant3 |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 <_ ( sqrt ` S ) ) |
6 |
|
eqeelen |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) = 0 ) ) |
7 |
1
|
eqeq1i |
|- ( S = 0 <-> sum_ p e. ( 1 ... N ) ( ( ( A ` p ) - ( B ` p ) ) ^ 2 ) = 0 ) |
8 |
6 7
|
bitr4di |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> S = 0 ) ) |
9 |
1
|
axsegconlem2 |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> S e. RR ) |
10 |
1
|
axsegconlem3 |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> 0 <_ S ) |
11 |
|
sqrt00 |
|- ( ( S e. RR /\ 0 <_ S ) -> ( ( sqrt ` S ) = 0 <-> S = 0 ) ) |
12 |
9 10 11
|
syl2anc |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( ( sqrt ` S ) = 0 <-> S = 0 ) ) |
13 |
8 12
|
bitr4d |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> ( sqrt ` S ) = 0 ) ) |
14 |
13
|
necon3bid |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A =/= B <-> ( sqrt ` S ) =/= 0 ) ) |
15 |
14
|
biimp3a |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> ( sqrt ` S ) =/= 0 ) |
16 |
3 5 15
|
ne0gt0d |
|- ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) -> 0 < ( sqrt ` S ) ) |