Metamath Proof Explorer


Theorem resum2sqorgt0

Description: The sum of the square of two real numbers is greater than zero if at least one of the real numbers is nonzero. (Contributed by AV, 26-Feb-2023)

Ref Expression
Hypothesis resum2sqcl.q
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
Assertion resum2sqorgt0
|- ( ( A e. RR /\ B e. RR /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < Q )

Proof

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 )