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 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
Assertion resum2sqorgt0 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < 𝑄 )

Proof

Step Hyp Ref Expression
1 resum2sqcl.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 1 resum2sqgt0 ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 0 < 𝑄 )
3 2 ex ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℝ → 0 < 𝑄 ) )
4 3 expcom ( 𝐴 ≠ 0 → ( 𝐴 ∈ ℝ → ( 𝐵 ∈ ℝ → 0 < 𝑄 ) ) )
5 4 com23 ( 𝐴 ≠ 0 → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℝ → 0 < 𝑄 ) ) )
6 eqid ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) )
7 6 resum2sqgt0 ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → 0 < ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
8 1 breq2i ( 0 < 𝑄 ↔ 0 < ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
9 resqcl ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )
10 9 adantl ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
11 10 recnd ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
12 resqcl ( 𝐵 ∈ ℝ → ( 𝐵 ↑ 2 ) ∈ ℝ )
13 12 ad2antrr ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℝ )
14 13 recnd ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
15 11 14 addcomd ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) )
16 15 breq2d ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 0 < ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ↔ 0 < ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) ) )
17 8 16 syl5bb ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝑄 ↔ 0 < ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) ) )
18 7 17 mpbird ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐴 ∈ ℝ ) → 0 < 𝑄 )
19 18 ex ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ∈ ℝ → 0 < 𝑄 ) )
20 19 expcom ( 𝐵 ≠ 0 → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℝ → 0 < 𝑄 ) ) )
21 5 20 jaoi ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) → ( 𝐵 ∈ ℝ → ( 𝐴 ∈ ℝ → 0 < 𝑄 ) ) )
22 21 3imp31 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < 𝑄 )