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 )