Proof of Theorem recextlem2
Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝐵 = 0 → (i · 𝐵) = (i ·
0)) |
2 | | ax-icn 9874 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
3 | 2 | mul01i 10105 |
. . . . . . . . 9
⊢ (i
· 0) = 0 |
4 | 1, 3 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐵 = 0 → (i · 𝐵) = 0) |
5 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝐴 = 0 ∧ (i · 𝐵) = 0) → (𝐴 + (i · 𝐵)) = (0 + 0)) |
6 | 4, 5 | sylan2 490 |
. . . . . . 7
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 + (i · 𝐵)) = (0 + 0)) |
7 | | 00id 10090 |
. . . . . . 7
⊢ (0 + 0) =
0 |
8 | 6, 7 | syl6eq 2660 |
. . . . . 6
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 + (i · 𝐵)) = 0) |
9 | 8 | necon3ai 2807 |
. . . . 5
⊢ ((𝐴 + (i · 𝐵)) ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
10 | | neorian 2876 |
. . . . 5
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
11 | 9, 10 | sylibr 223 |
. . . 4
⊢ ((𝐴 + (i · 𝐵)) ≠ 0 → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) |
12 | | remulcl 9900 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐴 · 𝐴) ∈ ℝ) |
13 | 12 | anidms 675 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 · 𝐴) ∈ ℝ) |
14 | | remulcl 9900 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 · 𝐵) ∈ ℝ) |
15 | 14 | anidms 675 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 · 𝐵) ∈ ℝ) |
16 | 13, 15 | anim12i 588 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ)) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≠ 0) → ((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ)) |
18 | | msqgt0 10427 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴 · 𝐴)) |
19 | | msqge0 10428 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 0 ≤
(𝐵 · 𝐵)) |
20 | 18, 19 | anim12i 588 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (0 < (𝐴 · 𝐴) ∧ 0 ≤ (𝐵 · 𝐵))) |
21 | 20 | an32s 842 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≠ 0) → (0 < (𝐴 · 𝐴) ∧ 0 ≤ (𝐵 · 𝐵))) |
22 | | addgtge0 10395 |
. . . . . 6
⊢ ((((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ) ∧ (0 < (𝐴 · 𝐴) ∧ 0 ≤ (𝐵 · 𝐵))) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
23 | 17, 21, 22 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
24 | 16 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ)) |
25 | | msqge0 10428 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 0 ≤
(𝐴 · 𝐴)) |
26 | | msqgt0 10427 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 0 < (𝐵 · 𝐵)) |
27 | 25, 26 | anim12i 588 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → (0 ≤ (𝐴 · 𝐴) ∧ 0 < (𝐵 · 𝐵))) |
28 | 27 | anassrs 678 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≠ 0) → (0 ≤ (𝐴 · 𝐴) ∧ 0 < (𝐵 · 𝐵))) |
29 | | addgegt0 10394 |
. . . . . 6
⊢ ((((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐴) ∧ 0 < (𝐵 · 𝐵))) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
30 | 24, 28, 29 | syl2anc 691 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
31 | 23, 30 | jaodan 822 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
32 | 11, 31 | sylan2 490 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 + (i · 𝐵)) ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
33 | 32 | 3impa 1251 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
34 | 33 | gt0ne0d 10471 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) ≠ 0) → ((𝐴 · 𝐴) + (𝐵 · 𝐵)) ≠ 0) |