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 B A 0 B 0 0 < Q

Proof

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