This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recextlem2

Description: Lemma for recex . (Contributed by Eric Schmidt, 23-May-2007)

Ref Expression
Assertion recextlem2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) → ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝐵 = 0 → ( i · 𝐵 ) = ( i · 0 ) )
2 ax-icn ⊢ i ∈ ℂ
3 2 mul01i ⊢ ( i · 0 ) = 0
4 1 3 eqtrdi ⊢ ( 𝐵 = 0 → ( i · 𝐵 ) = 0 )
5 oveq12 ⊢ ( ( 𝐴 = 0 ∧ ( i · 𝐵 ) = 0 ) → ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + 0 ) )
6 4 5 sylan2 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 + ( i · 𝐵 ) ) = ( 0 + 0 ) )
7 00id ⊢ ( 0 + 0 ) = 0
8 6 7 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 + ( i · 𝐵 ) ) = 0 )
9 8 necon3ai ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
10 neorian ⊢ ( ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
11 9 10 sylibr ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) )
12 remulcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 · 𝐴 ) ∈ ℝ )
13 12 anidms ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 𝐴 ) ∈ ℝ )
14 remulcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 · 𝐵 ) ∈ ℝ )
15 14 anidms ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 𝐵 ) ∈ ℝ )
16 13 15 anim12i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐴 ) ∈ ℝ ∧ ( 𝐵 · 𝐵 ) ∈ ℝ ) )
17 msqgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · 𝐴 ) )
18 msqge0 ⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐵 · 𝐵 ) )
19 17 18 anim12i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( 0 < ( 𝐴 · 𝐴 ) ∧ 0 ≤ ( 𝐵 · 𝐵 ) ) )
20 19 an32s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( 0 < ( 𝐴 · 𝐴 ) ∧ 0 ≤ ( 𝐵 · 𝐵 ) ) )
21 addgtge0 ⊢ ( ( ( ( 𝐴 · 𝐴 ) ∈ ℝ ∧ ( 𝐵 · 𝐵 ) ∈ ℝ ) ∧ ( 0 < ( 𝐴 · 𝐴 ) ∧ 0 ≤ ( 𝐵 · 𝐵 ) ) ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
22 16 20 21 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
23 msqge0 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 · 𝐴 ) )
24 msqgt0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 0 < ( 𝐵 · 𝐵 ) )
25 23 24 anim12i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( 0 ≤ ( 𝐴 · 𝐴 ) ∧ 0 < ( 𝐵 · 𝐵 ) ) )
26 25 anassrs ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≠ 0 ) → ( 0 ≤ ( 𝐴 · 𝐴 ) ∧ 0 < ( 𝐵 · 𝐵 ) ) )
27 addgegt0 ⊢ ( ( ( ( 𝐴 · 𝐴 ) ∈ ℝ ∧ ( 𝐵 · 𝐵 ) ∈ ℝ ) ∧ ( 0 ≤ ( 𝐴 · 𝐴 ) ∧ 0 < ( 𝐵 · 𝐵 ) ) ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
28 16 26 27 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≠ 0 ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
29 22 28 jaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
30 11 29 sylan2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
31 30 3impa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) → 0 < ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) )
32 31 gt0ne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 + ( i · 𝐵 ) ) ≠ 0 ) → ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) ≠ 0 )