Proof of Theorem recextlem2
Step | Hyp | Ref
| Expression |
1 | | oveq2 6698 |
. . . . . . . . 9
⊢ (𝐵 = 0 → (i · 𝐵) = (i ·
0)) |
2 | | ax-icn 10033 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
3 | 2 | mul01i 10264 |
. . . . . . . . 9
⊢ (i
· 0) = 0 |
4 | 1, 3 | syl6eq 2701 |
. . . . . . . 8
⊢ (𝐵 = 0 → (i · 𝐵) = 0) |
5 | | oveq12 6699 |
. . . . . . . 8
⊢ ((𝐴 = 0 ∧ (i · 𝐵) = 0) → (𝐴 + (i · 𝐵)) = (0 + 0)) |
6 | 4, 5 | sylan2 490 |
. . . . . . 7
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 + (i · 𝐵)) = (0 + 0)) |
7 | | 00id 10249 |
. . . . . . 7
⊢ (0 + 0) =
0 |
8 | 6, 7 | syl6eq 2701 |
. . . . . 6
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 + (i · 𝐵)) = 0) |
9 | 8 | necon3ai 2848 |
. . . . 5
⊢ ((𝐴 + (i · 𝐵)) ≠ 0 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
10 | | neorian 2917 |
. . . . 5
⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) ↔ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) |
11 | 9, 10 | sylibr 224 |
. . . 4
⊢ ((𝐴 + (i · 𝐵)) ≠ 0 → (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) |
12 | | remulcl 10059 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐴 · 𝐴) ∈ ℝ) |
13 | 12 | anidms 678 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 · 𝐴) ∈ ℝ) |
14 | | remulcl 10059 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 · 𝐵) ∈ ℝ) |
15 | 14 | anidms 678 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → (𝐵 · 𝐵) ∈ ℝ) |
16 | 13, 15 | anim12i 589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ)) |
17 | 16 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≠ 0) → ((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ)) |
18 | | msqgt0 10586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴 · 𝐴)) |
19 | | msqge0 10587 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 0 ≤
(𝐵 · 𝐵)) |
20 | 18, 19 | anim12i 589 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (0 < (𝐴 · 𝐴) ∧ 0 ≤ (𝐵 · 𝐵))) |
21 | 20 | an32s 863 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≠ 0) → (0 < (𝐴 · 𝐴) ∧ 0 ≤ (𝐵 · 𝐵))) |
22 | | addgtge0 10554 |
. . . . . 6
⊢ ((((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ) ∧ (0 < (𝐴 · 𝐴) ∧ 0 ≤ (𝐵 · 𝐵))) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
23 | 17, 21, 22 | syl2anc 694 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
24 | 16 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ)) |
25 | | msqge0 10587 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 0 ≤
(𝐴 · 𝐴)) |
26 | | msqgt0 10586 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → 0 < (𝐵 · 𝐵)) |
27 | 25, 26 | anim12i 589 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → (0 ≤ (𝐴 · 𝐴) ∧ 0 < (𝐵 · 𝐵))) |
28 | 27 | anassrs 681 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≠ 0) → (0 ≤ (𝐴 · 𝐴) ∧ 0 < (𝐵 · 𝐵))) |
29 | | addgegt0 10553 |
. . . . . 6
⊢ ((((𝐴 · 𝐴) ∈ ℝ ∧ (𝐵 · 𝐵) ∈ ℝ) ∧ (0 ≤ (𝐴 · 𝐴) ∧ 0 < (𝐵 · 𝐵))) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
30 | 24, 28, 29 | syl2anc 694 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
31 | 23, 30 | jaodan 843 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ 0 ∨ 𝐵 ≠ 0)) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
32 | 11, 31 | sylan2 490 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 + (i · 𝐵)) ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
33 | 32 | 3impa 1278 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) ≠ 0) → 0 < ((𝐴 · 𝐴) + (𝐵 · 𝐵))) |
34 | 33 | gt0ne0d 10630 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) ≠ 0) → ((𝐴 · 𝐴) + (𝐵 · 𝐵)) ≠ 0) |