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	bitrid	|- ( ( ( 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 )