Metamath Proof Explorer

Theorem recex

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

Ref Expression
Assertion recex ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℂ ( 𝐴 · 𝑥 ) = 1 )

Proof

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