Step |
Hyp |
Ref |
Expression |
1 |
|
resum2sqcl.q |
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) ) |
2 |
1
|
resum2sqgt0 |
|- ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> 0 < Q ) |
3 |
2
|
ex |
|- ( ( A e. RR /\ A =/= 0 ) -> ( B e. RR -> 0 < Q ) ) |
4 |
3
|
expcom |
|- ( A =/= 0 -> ( A e. RR -> ( B e. RR -> 0 < Q ) ) ) |
5 |
4
|
com23 |
|- ( A =/= 0 -> ( B e. RR -> ( A e. RR -> 0 < Q ) ) ) |
6 |
|
eqid |
|- ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) |
7 |
6
|
resum2sqgt0 |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> 0 < ( ( B ^ 2 ) + ( A ^ 2 ) ) ) |
8 |
1
|
breq2i |
|- ( 0 < Q <-> 0 < ( ( A ^ 2 ) + ( B ^ 2 ) ) ) |
9 |
|
resqcl |
|- ( A e. RR -> ( A ^ 2 ) e. RR ) |
10 |
9
|
adantl |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( A ^ 2 ) e. RR ) |
11 |
10
|
recnd |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( A ^ 2 ) e. CC ) |
12 |
|
resqcl |
|- ( B e. RR -> ( B ^ 2 ) e. RR ) |
13 |
12
|
ad2antrr |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( B ^ 2 ) e. RR ) |
14 |
13
|
recnd |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( B ^ 2 ) e. CC ) |
15 |
11 14
|
addcomd |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) ) |
16 |
15
|
breq2d |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( 0 < ( ( A ^ 2 ) + ( B ^ 2 ) ) <-> 0 < ( ( B ^ 2 ) + ( A ^ 2 ) ) ) ) |
17 |
8 16
|
syl5bb |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> ( 0 < Q <-> 0 < ( ( B ^ 2 ) + ( A ^ 2 ) ) ) ) |
18 |
7 17
|
mpbird |
|- ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> 0 < Q ) |
19 |
18
|
ex |
|- ( ( B e. RR /\ B =/= 0 ) -> ( A e. RR -> 0 < Q ) ) |
20 |
19
|
expcom |
|- ( B =/= 0 -> ( B e. RR -> ( A e. RR -> 0 < Q ) ) ) |
21 |
5 20
|
jaoi |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( B e. RR -> ( A e. RR -> 0 < Q ) ) ) |
22 |
21
|
3imp31 |
|- ( ( A e. RR /\ B e. RR /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < Q ) |