Step | Hyp | Ref
| Expression |
1 | | cnre 10248 |
. . 3
⊢ (𝐴 ∈ ℂ →
∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
𝐴 = (𝑎 + (i · 𝑏))) |
2 | | recextlem2 10870 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝑎 + (i · 𝑏)) ≠ 0) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) |
3 | 2 | 3expia 1115 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) ≠ 0 → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0)) |
4 | | remulcl 10233 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑎 · 𝑎) ∈ ℝ) |
5 | 4 | anidms 680 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℝ → (𝑎 · 𝑎) ∈ ℝ) |
6 | | remulcl 10233 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑏 · 𝑏) ∈ ℝ) |
7 | 6 | anidms 680 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℝ → (𝑏 · 𝑏) ∈ ℝ) |
8 | | readdcl 10231 |
. . . . . . . . . . . 12
⊢ (((𝑎 · 𝑎) ∈ ℝ ∧ (𝑏 · 𝑏) ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ) |
9 | 5, 7, 8 | syl2an 495 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ) |
10 | | ax-rrecex 10220 |
. . . . . . . . . . 11
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) |
11 | 9, 10 | sylan 489 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) |
12 | | recn 10238 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
13 | | recn 10238 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
14 | | recn 10238 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
15 | | ax-icn 10207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ i ∈
ℂ |
16 | | mulcl 10232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((i
∈ ℂ ∧ 𝑏
∈ ℂ) → (i · 𝑏) ∈ ℂ) |
17 | 15, 16 | mpan 708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ ℂ → (i
· 𝑏) ∈
ℂ) |
18 | | subcl 10492 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℂ ∧ (i
· 𝑏) ∈ ℂ)
→ (𝑎 − (i
· 𝑏)) ∈
ℂ) |
19 | 17, 18 | sylan2 492 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈
ℂ) |
20 | | mulcl 10232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 − (i · 𝑏)) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ) |
21 | 19, 20 | sylan 489 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ) |
22 | 21 | adantr 472 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ) |
23 | | addcl 10230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℂ ∧ (i
· 𝑏) ∈ ℂ)
→ (𝑎 + (i ·
𝑏)) ∈
ℂ) |
24 | 17, 23 | sylan2 492 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
25 | 24 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
26 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈
ℂ) |
27 | | simpr 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
28 | 25, 26, 27 | mulassd 10275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) · 𝑦) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦))) |
29 | | recextlem1 10869 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏))) |
30 | 29 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏))) |
31 | 30 | oveq1d 6829 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) · 𝑦) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦)) |
32 | 28, 31 | eqtr3d 2796 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦)) |
33 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) |
34 | 32, 33 | sylan9eq 2814 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1) |
35 | | oveq2 6822 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((𝑎 − (i · 𝑏)) · 𝑦) → ((𝑎 + (i · 𝑏)) · 𝑥) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦))) |
36 | 35 | eqeq1d 2762 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ((𝑎 − (i · 𝑏)) · 𝑦) → (((𝑎 + (i · 𝑏)) · 𝑥) = 1 ↔ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1)) |
37 | 36 | rspcev 3449 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ ∧ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1) |
38 | 22, 34, 37 | syl2anc 696 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1) |
39 | 38 | exp31 631 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑦 ∈ ℂ → ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))) |
40 | 14, 39 | syl5 34 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑦 ∈ ℝ → ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))) |
41 | 40 | rexlimdv 3168 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) →
(∃𝑦 ∈ ℝ
(((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
42 | 12, 13, 41 | syl2an 495 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(∃𝑦 ∈ ℝ
(((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
43 | 42 | adantr 472 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → (∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
44 | 11, 43 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1) |
45 | 44 | ex 449 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
46 | 3, 45 | syld 47 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) ≠ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
47 | 46 | adantr 472 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → ((𝑎 + (i · 𝑏)) ≠ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
48 | | neeq1 2994 |
. . . . . . 7
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0)) |
49 | 48 | adantl 473 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (𝐴 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0)) |
50 | | oveq1 6821 |
. . . . . . . . 9
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 · 𝑥) = ((𝑎 + (i · 𝑏)) · 𝑥)) |
51 | 50 | eqeq1d 2762 |
. . . . . . . 8
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → ((𝐴 · 𝑥) = 1 ↔ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
52 | 51 | rexbidv 3190 |
. . . . . . 7
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
53 | 52 | adantl 473 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
54 | 47, 49, 53 | 3imtr4d 283 |
. . . . 5
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)) |
55 | 54 | ex 449 |
. . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))) |
56 | 55 | rexlimivv 3174 |
. . 3
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)) |
57 | 1, 56 | syl 17 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)) |
58 | 57 | imp 444 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1) |