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 bitrid ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 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 < 𝑄 )