Metamath Proof Explorer

Theorem recex

Description: Existence of reciprocal of nonzero complex number. (Contributed by Eric Schmidt, 22-May-2007)

Ref Expression
Assertion recex ⊢ A ∈ ℂ ∧ A ≠ 0 → ∃ x ∈ ℂ A ⁢ x = 1

Proof

Step Hyp Ref Expression
1 cnre ⊢ A ∈ ℂ → ∃ a ∈ ℝ ∃ b ∈ ℝ A = a + i ⁢ b
2 recextlem2 ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a + i ⁢ b ≠ 0 → a ⁢ a + b ⁢ b ≠ 0
3 2 3expia ⊢ a ∈ ℝ ∧ b ∈ ℝ → a + i ⁢ b ≠ 0 → a ⁢ a + b ⁢ b ≠ 0
4 remulcl ⊢ a ∈ ℝ ∧ a ∈ ℝ → a ⁢ a ∈ ℝ
5 4 anidms ⊢ a ∈ ℝ → a ⁢ a ∈ ℝ
6 remulcl ⊢ b ∈ ℝ ∧ b ∈ ℝ → b ⁢ b ∈ ℝ
7 6 anidms ⊢ b ∈ ℝ → b ⁢ b ∈ ℝ
8 readdcl ⊢ a ⁢ a ∈ ℝ ∧ b ⁢ b ∈ ℝ → a ⁢ a + b ⁢ b ∈ ℝ
9 5 7 8 syl2an ⊢ a ∈ ℝ ∧ b ∈ ℝ → a ⁢ a + b ⁢ b ∈ ℝ
10 ax-rrecex ⊢ a ⁢ a + b ⁢ b ∈ ℝ ∧ a ⁢ a + b ⁢ b ≠ 0 → ∃ y ∈ ℝ a ⁢ a + b ⁢ b ⁢ y = 1
11 9 10 sylan ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a ⁢ a + b ⁢ b ≠ 0 → ∃ y ∈ ℝ a ⁢ a + b ⁢ b ⁢ y = 1
12 recn ⊢ a ∈ ℝ → a ∈ ℂ
13 recn ⊢ b ∈ ℝ → b ∈ ℂ
14 recn ⊢ y ∈ ℝ → y ∈ ℂ
15 ax-icn ⊢ i ∈ ℂ
16 mulcl ⊢ i ∈ ℂ ∧ b ∈ ℂ → i ⁢ b ∈ ℂ
17 15 16 mpan ⊢ b ∈ ℂ → i ⁢ b ∈ ℂ
18 subcl ⊢ a ∈ ℂ ∧ i ⁢ b ∈ ℂ → a − i ⁢ b ∈ ℂ
19 17 18 sylan2 ⊢ a ∈ ℂ ∧ b ∈ ℂ → a − i ⁢ b ∈ ℂ
20 mulcl ⊢ a − i ⁢ b ∈ ℂ ∧ y ∈ ℂ → a − i ⁢ b ⁢ y ∈ ℂ
21 19 20 sylan ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a − i ⁢ b ⁢ y ∈ ℂ
22 addcl ⊢ a ∈ ℂ ∧ i ⁢ b ∈ ℂ → a + i ⁢ b ∈ ℂ
23 17 22 sylan2 ⊢ a ∈ ℂ ∧ b ∈ ℂ → a + i ⁢ b ∈ ℂ
24 23 adantr ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a + i ⁢ b ∈ ℂ
25 19 adantr ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a − i ⁢ b ∈ ℂ
26 simpr ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → y ∈ ℂ
27 24 25 26 mulassd ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a + i ⁢ b ⁢ a − i ⁢ b ⁢ y = a + i ⁢ b ⁢ a − i ⁢ b ⁢ y
28 recextlem1 ⊢ a ∈ ℂ ∧ b ∈ ℂ → a + i ⁢ b ⁢ a − i ⁢ b = a ⁢ a + b ⁢ b
29 28 adantr ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a + i ⁢ b ⁢ a − i ⁢ b = a ⁢ a + b ⁢ b
30 29 oveq1d ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a + i ⁢ b ⁢ a − i ⁢ b ⁢ y = a ⁢ a + b ⁢ b ⁢ y
31 27 30 eqtr3d ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ → a + i ⁢ b ⁢ a − i ⁢ b ⁢ y = a ⁢ a + b ⁢ b ⁢ y
32 id ⊢ a ⁢ a + b ⁢ b ⁢ y = 1 → a ⁢ a + b ⁢ b ⁢ y = 1
33 31 32 sylan9eq ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ ∧ a ⁢ a + b ⁢ b ⁢ y = 1 → a + i ⁢ b ⁢ a − i ⁢ b ⁢ y = 1
34 oveq2 ⊢ x = a − i ⁢ b ⁢ y → a + i ⁢ b ⁢ x = a + i ⁢ b ⁢ a − i ⁢ b ⁢ y
35 34 eqeq1d ⊢ x = a − i ⁢ b ⁢ y → a + i ⁢ b ⁢ x = 1 ↔ a + i ⁢ b ⁢ a − i ⁢ b ⁢ y = 1
36 35 rspcev ⊢ a − i ⁢ b ⁢ y ∈ ℂ ∧ a + i ⁢ b ⁢ a − i ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
37 21 33 36 syl2an2r ⊢ a ∈ ℂ ∧ b ∈ ℂ ∧ y ∈ ℂ ∧ a ⁢ a + b ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
38 37 exp31 ⊢ a ∈ ℂ ∧ b ∈ ℂ → y ∈ ℂ → a ⁢ a + b ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
39 14 38 syl5 ⊢ a ∈ ℂ ∧ b ∈ ℂ → y ∈ ℝ → a ⁢ a + b ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
40 39 rexlimdv ⊢ a ∈ ℂ ∧ b ∈ ℂ → ∃ y ∈ ℝ a ⁢ a + b ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
41 12 13 40 syl2an ⊢ a ∈ ℝ ∧ b ∈ ℝ → ∃ y ∈ ℝ a ⁢ a + b ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
42 41 adantr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a ⁢ a + b ⁢ b ≠ 0 → ∃ y ∈ ℝ a ⁢ a + b ⁢ b ⁢ y = 1 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
43 11 42 mpd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a ⁢ a + b ⁢ b ≠ 0 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
44 43 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ → a ⁢ a + b ⁢ b ≠ 0 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
45 3 44 syld ⊢ a ∈ ℝ ∧ b ∈ ℝ → a + i ⁢ b ≠ 0 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
46 45 adantr ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ A = a + i ⁢ b → a + i ⁢ b ≠ 0 → ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
47 neeq1 ⊢ A = a + i ⁢ b → A ≠ 0 ↔ a + i ⁢ b ≠ 0
48 47 adantl ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ A = a + i ⁢ b → A ≠ 0 ↔ a + i ⁢ b ≠ 0
49 oveq1 ⊢ A = a + i ⁢ b → A ⁢ x = a + i ⁢ b ⁢ x
50 49 eqeq1d ⊢ A = a + i ⁢ b → A ⁢ x = 1 ↔ a + i ⁢ b ⁢ x = 1
51 50 rexbidv ⊢ A = a + i ⁢ b → ∃ x ∈ ℂ A ⁢ x = 1 ↔ ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
52 51 adantl ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ A = a + i ⁢ b → ∃ x ∈ ℂ A ⁢ x = 1 ↔ ∃ x ∈ ℂ a + i ⁢ b ⁢ x = 1
53 46 48 52 3imtr4d ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ A = a + i ⁢ b → A ≠ 0 → ∃ x ∈ ℂ A ⁢ x = 1
54 53 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ → A = a + i ⁢ b → A ≠ 0 → ∃ x ∈ ℂ A ⁢ x = 1
55 54 rexlimivv ⊢ ∃ a ∈ ℝ ∃ b ∈ ℝ A = a + i ⁢ b → A ≠ 0 → ∃ x ∈ ℂ A ⁢ x = 1
56 1 55 syl ⊢ A ∈ ℂ → A ≠ 0 → ∃ x ∈ ℂ A ⁢ x = 1
57 56 imp ⊢ A ∈ ℂ ∧ A ≠ 0 → ∃ x ∈ ℂ A ⁢ x = 1