Step | Hyp | Ref
| Expression |
1 | | cnre 10860 |
. . 3
⊢ (𝐴 ∈ ℂ →
∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
𝐴 = (𝑎 + (i · 𝑏))) |
2 | | recextlem2 11493 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝑎 + (i · 𝑏)) ≠ 0) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) |
3 | 2 | 3expia 1123 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) ≠ 0 → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0)) |
4 | | remulcl 10844 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑎 · 𝑎) ∈ ℝ) |
5 | 4 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℝ → (𝑎 · 𝑎) ∈ ℝ) |
6 | | remulcl 10844 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑏 · 𝑏) ∈ ℝ) |
7 | 6 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℝ → (𝑏 · 𝑏) ∈ ℝ) |
8 | | readdcl 10842 |
. . . . . . . . . . . 12
⊢ (((𝑎 · 𝑎) ∈ ℝ ∧ (𝑏 · 𝑏) ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ) |
9 | 5, 7, 8 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ) |
10 | | ax-rrecex 10831 |
. . . . . . . . . . 11
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) |
11 | 9, 10 | sylan 583 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → ∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) |
12 | | recn 10849 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
13 | | recn 10849 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
14 | | recn 10849 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
15 | | ax-icn 10818 |
. . . . . . . . . . . . . . . . . . 19
⊢ i ∈
ℂ |
16 | | mulcl 10843 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ 𝑏
∈ ℂ) → (i · 𝑏) ∈ ℂ) |
17 | 15, 16 | mpan 690 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ ℂ → (i
· 𝑏) ∈
ℂ) |
18 | | subcl 11107 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℂ ∧ (i
· 𝑏) ∈ ℂ)
→ (𝑎 − (i
· 𝑏)) ∈
ℂ) |
19 | 17, 18 | sylan2 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈
ℂ) |
20 | | mulcl 10843 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 − (i · 𝑏)) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ) |
21 | 19, 20 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ) |
22 | | addcl 10841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℂ ∧ (i
· 𝑏) ∈ ℂ)
→ (𝑎 + (i ·
𝑏)) ∈
ℂ) |
23 | 17, 22 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
24 | 23 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
25 | 19 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈
ℂ) |
26 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈
ℂ) |
27 | 24, 25, 26 | mulassd 10886 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) · 𝑦) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦))) |
28 | | recextlem1 11492 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏))) |
29 | 28 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏))) |
30 | 29 | oveq1d 7250 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) · 𝑦) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦)) |
31 | 27, 30 | eqtr3d 2781 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦)) |
32 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) |
33 | 31, 32 | sylan9eq 2800 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1) |
34 | | oveq2 7243 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((𝑎 − (i · 𝑏)) · 𝑦) → ((𝑎 + (i · 𝑏)) · 𝑥) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦))) |
35 | 34 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ((𝑎 − (i · 𝑏)) · 𝑦) → (((𝑎 + (i · 𝑏)) · 𝑥) = 1 ↔ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1)) |
36 | 35 | rspcev 3552 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ ∧ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1) |
37 | 21, 33, 36 | syl2an2r 685 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1) |
38 | 37 | exp31 423 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑦 ∈ ℂ → ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))) |
39 | 14, 38 | syl5 34 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑦 ∈ ℝ → ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))) |
40 | 39 | rexlimdv 3212 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) →
(∃𝑦 ∈ ℝ
(((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
41 | 12, 13, 40 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) →
(∃𝑦 ∈ ℝ
(((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
42 | 41 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → (∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
43 | 11, 42 | mpd 15 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1) |
44 | 43 | ex 416 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) ≠ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
45 | 3, 44 | syld 47 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) ≠ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
46 | 45 | adantr 484 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → ((𝑎 + (i · 𝑏)) ≠ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
47 | | neeq1 3006 |
. . . . . . 7
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0)) |
48 | 47 | adantl 485 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (𝐴 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0)) |
49 | | oveq1 7242 |
. . . . . . . . 9
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 · 𝑥) = ((𝑎 + (i · 𝑏)) · 𝑥)) |
50 | 49 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → ((𝐴 · 𝑥) = 1 ↔ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
51 | 50 | rexbidv 3226 |
. . . . . . 7
⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
52 | 51 | adantl 485 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)) |
53 | 46, 48, 52 | 3imtr4d 297 |
. . . . 5
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)) |
54 | 53 | ex 416 |
. . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))) |
55 | 54 | rexlimivv 3221 |
. . 3
⊢
(∃𝑎 ∈
ℝ ∃𝑏 ∈
ℝ 𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)) |
56 | 1, 55 | syl 17 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)) |
57 | 56 | imp 410 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1) |