Step | Hyp | Ref
| Expression |
1 | | cnre 6821 |
. . 3
⊢ (A ∈ ℂ →
∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
A = (𝑎 + (i · 𝑏))) |
2 | | recexaplem2 7415 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝑎 + (i · 𝑏)) # 0) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0) |
3 | 2 | 3expia 1105 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) # 0 → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0)) |
4 | | remulcl 6807 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑎 · 𝑎) ∈
ℝ) |
5 | 4 | anidms 377 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ ℝ → (𝑎 · 𝑎) ∈
ℝ) |
6 | | remulcl 6807 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑏 · 𝑏) ∈
ℝ) |
7 | 6 | anidms 377 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ ℝ → (𝑏 · 𝑏) ∈
ℝ) |
8 | | readdcl 6805 |
. . . . . . . . . . 11
⊢ (((𝑎 · 𝑎) ∈ ℝ
∧ (𝑏 · 𝑏) ∈
ℝ) → ((𝑎 ·
𝑎) + (𝑏 · 𝑏)) ∈
ℝ) |
9 | 5, 7, 8 | syl2an 273 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈
ℝ) |
10 | | 0re 6825 |
. . . . . . . . . 10
⊢ 0 ∈ ℝ |
11 | | apreap 7371 |
. . . . . . . . . 10
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈
ℝ ∧ 0 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0 ↔ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0)) |
12 | 9, 10, 11 | sylancl 392 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0 ↔ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0)) |
13 | | recexre 7362 |
. . . . . . . . . . . 12
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈
ℝ ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → ∃y ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1) |
14 | 9, 13 | sylan 267 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → ∃y ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1) |
15 | | recn 6812 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℝ → 𝑎 ∈
ℂ) |
16 | | recn 6812 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℝ → 𝑏 ∈
ℂ) |
17 | | recn 6812 |
. . . . . . . . . . . . . . 15
⊢ (y ∈ ℝ →
y ∈
ℂ) |
18 | | ax-icn 6778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ i ∈ ℂ |
19 | | mulcl 6806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((i ∈ ℂ ∧ 𝑏 ∈ ℂ) → (i · 𝑏) ∈
ℂ) |
20 | 18, 19 | mpan 400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ ℂ → (i · 𝑏) ∈
ℂ) |
21 | | subcl 7007 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℂ ∧ (i
· 𝑏) ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈
ℂ) |
22 | 20, 21 | sylan2 270 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈
ℂ) |
23 | | mulcl 6806 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 − (i · 𝑏)) ∈ ℂ ∧
y ∈
ℂ) → ((𝑎 − (i
· 𝑏)) · y) ∈
ℂ) |
24 | 22, 23 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → ((𝑎 − (i
· 𝑏)) · y) ∈
ℂ) |
25 | 24 | adantr 261 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1) → ((𝑎 − (i · 𝑏)) · y) ∈
ℂ) |
26 | | addcl 6804 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℂ ∧ (i
· 𝑏) ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
27 | 20, 26 | sylan2 270 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈
ℂ) |
28 | 27 | adantr 261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → (𝑎 + (i
· 𝑏)) ∈ ℂ) |
29 | 22 | adantr 261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → (𝑎 − (i
· 𝑏)) ∈ ℂ) |
30 | | simpr 103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → y ∈ ℂ) |
31 | 28, 29, 30 | mulassd 6848 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → (((𝑎 + (i
· 𝑏)) · (𝑎 − (i · 𝑏))) · y) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · y))) |
32 | | recextlem1 7414 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏))) |
33 | 32 | adantr 261 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → ((𝑎 + (i
· 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏))) |
34 | 33 | oveq1d 5470 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → (((𝑎 + (i
· 𝑏)) · (𝑎 − (i · 𝑏))) · y) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y)) |
35 | 31, 34 | eqtr3d 2071 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) → ((𝑎 + (i
· 𝑏)) · ((𝑎 − (i · 𝑏)) · y)) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y)) |
36 | | id 19 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1 → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1) |
37 | 35, 36 | sylan9eq 2089 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · y)) = 1) |
38 | | oveq2 5463 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x = ((𝑎 − (i · 𝑏)) · y) → ((𝑎 + (i · 𝑏)) · x) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · y))) |
39 | 38 | eqeq1d 2045 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = ((𝑎 − (i · 𝑏)) · y) → (((𝑎 + (i · 𝑏)) · x) = 1 ↔ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · y)) = 1)) |
40 | 39 | rspcev 2650 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 − (i · 𝑏)) · y) ∈ ℂ ∧ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · y)) = 1) → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1) |
41 | 25, 37, 40 | syl2anc 391 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧
y ∈
ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1) → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1) |
42 | 41 | exp31 346 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (y ∈ ℂ →
((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1))) |
43 | 17, 42 | syl5 28 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (y ∈ ℝ →
((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1))) |
44 | 43 | rexlimdv 2426 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (∃y ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
45 | 15, 16, 44 | syl2an 273 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃y ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
46 | 45 | adantr 261 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → (∃y ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · y) = 1 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
47 | 14, 46 | mpd 13 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1) |
48 | 47 | ex 108 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
49 | 12, 48 | sylbid 139 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
50 | 3, 49 | syld 40 |
. . . . . . 7
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) # 0 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
51 | 50 | adantr 261 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
A = (𝑎 + (i · 𝑏))) → ((𝑎 + (i · 𝑏)) # 0 → ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
52 | | breq1 3758 |
. . . . . . 7
⊢ (A = (𝑎 + (i · 𝑏)) → (A # 0 ↔ (𝑎 + (i · 𝑏)) # 0)) |
53 | 52 | adantl 262 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
A = (𝑎 + (i · 𝑏))) → (A # 0 ↔ (𝑎 + (i · 𝑏)) # 0)) |
54 | | oveq1 5462 |
. . . . . . . . 9
⊢ (A = (𝑎 + (i · 𝑏)) → (A · x) =
((𝑎 + (i · 𝑏)) · x)) |
55 | 54 | eqeq1d 2045 |
. . . . . . . 8
⊢ (A = (𝑎 + (i · 𝑏)) → ((A · x) =
1 ↔ ((𝑎 + (i ·
𝑏)) · x) = 1)) |
56 | 55 | rexbidv 2321 |
. . . . . . 7
⊢ (A = (𝑎 + (i · 𝑏)) → (∃x ∈ ℂ (A
· x) = 1 ↔ ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
57 | 56 | adantl 262 |
. . . . . 6
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
A = (𝑎 + (i · 𝑏))) → (∃x ∈ ℂ (A
· x) = 1 ↔ ∃x ∈ ℂ ((𝑎 + (i · 𝑏)) · x) = 1)) |
58 | 51, 53, 57 | 3imtr4d 192 |
. . . . 5
⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧
A = (𝑎 + (i · 𝑏))) → (A # 0 → ∃x ∈ ℂ (A
· x) = 1)) |
59 | 58 | ex 108 |
. . . 4
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (A = (𝑎 + (i · 𝑏)) → (A # 0 → ∃x ∈ ℂ (A
· x) = 1))) |
60 | 59 | rexlimivv 2432 |
. . 3
⊢ (∃𝑎 ∈ ℝ
∃𝑏 ∈ ℝ
A = (𝑎 + (i · 𝑏)) → (A # 0 → ∃x ∈ ℂ (A
· x) = 1)) |
61 | 1, 60 | syl 14 |
. 2
⊢ (A ∈ ℂ →
(A # 0 → ∃x ∈ ℂ (A
· x) = 1)) |
62 | 61 | imp 115 |
1
⊢
((A ∈ ℂ ∧
A # 0) → ∃x ∈ ℂ (A
· x) = 1) |