Description: The sum of the square of a nonzero real number and the square of another real number is a positive real number. (Contributed by AV, 2-May-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | resum2sqcl.q | |- Q = ( ( A ^ 2 ) + ( B ^ 2 ) ) |
|
| Assertion | resum2sqrp | |- ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> Q e. RR+ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | resum2sqcl.q | |- Q = ( ( A ^ 2 ) + ( B ^ 2 ) ) |
|
| 2 | 1 | resum2sqcl | |- ( ( A e. RR /\ B e. RR ) -> Q e. RR ) |
| 3 | 2 | adantlr | |- ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> Q e. RR ) |
| 4 | 1 | resum2sqgt0 | |- ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> 0 < Q ) |
| 5 | 3 4 | elrpd | |- ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> Q e. RR+ ) |