Step |
Hyp |
Ref |
Expression |
1 |
|
abslt2sqd.a |
|- ( ph -> A e. RR ) |
2 |
|
abslt2sqd.b |
|- ( ph -> B e. RR ) |
3 |
|
abslt2sqd.l |
|- ( ph -> ( abs ` A ) < ( abs ` B ) ) |
4 |
1
|
recnd |
|- ( ph -> A e. CC ) |
5 |
4
|
abscld |
|- ( ph -> ( abs ` A ) e. RR ) |
6 |
4
|
absge0d |
|- ( ph -> 0 <_ ( abs ` A ) ) |
7 |
2
|
recnd |
|- ( ph -> B e. CC ) |
8 |
7
|
abscld |
|- ( ph -> ( abs ` B ) e. RR ) |
9 |
7
|
absge0d |
|- ( ph -> 0 <_ ( abs ` B ) ) |
10 |
|
lt2sq |
|- ( ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) /\ ( ( abs ` B ) e. RR /\ 0 <_ ( abs ` B ) ) ) -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) ) |
11 |
5 6 8 9 10
|
syl22anc |
|- ( ph -> ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) ) |
12 |
3 11
|
mpbid |
|- ( ph -> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) |
13 |
|
absresq |
|- ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) ) |
14 |
1 13
|
syl |
|- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) ) |
15 |
|
absresq |
|- ( B e. RR -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) ) |
16 |
2 15
|
syl |
|- ( ph -> ( ( abs ` B ) ^ 2 ) = ( B ^ 2 ) ) |
17 |
14 16
|
breq12d |
|- ( ph -> ( ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) <-> ( A ^ 2 ) < ( B ^ 2 ) ) ) |
18 |
12 17
|
mpbid |
|- ( ph -> ( A ^ 2 ) < ( B ^ 2 ) ) |