Theorem recexap 8672

Description: Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)

Assertion

Ref	Expression
recexap	⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)

Distinct variable group:   𝑥,𝐴

Proof of Theorem recexap

Dummy variables 𝑦 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnre 8015	. . 3 ⊢ (𝐴 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 𝐴 = (𝑎 + (i · 𝑏)))
2		recexaplem2 8671	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ (𝑎 + (i · 𝑏)) # 0) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0)
3	2	3expia 1207	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) # 0 → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0))
4		remulcl 8000	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑎 · 𝑎) ∈ ℝ)
5	4	anidms 397	. . . . . . . . . . 11 ⊢ (𝑎 ∈ ℝ → (𝑎 · 𝑎) ∈ ℝ)
6		remulcl 8000	. . . . . . . . . . . 12 ⊢ ((𝑏 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑏 · 𝑏) ∈ ℝ)
7	6	anidms 397	. . . . . . . . . . 11 ⊢ (𝑏 ∈ ℝ → (𝑏 · 𝑏) ∈ ℝ)
8		readdcl 7998	. . . . . . . . . . 11 ⊢ (((𝑎 · 𝑎) ∈ ℝ ∧ (𝑏 · 𝑏) ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ)
9	5, 7, 8	syl2an 289	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ)
10		0re 8019	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
11		apreap 8606	. . . . . . . . . 10 ⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ ∧ 0 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0 ↔ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0))
12	9, 10, 11	sylancl 413	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0 ↔ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0))
13		recexre 8597	. . . . . . . . . . . 12 ⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) ∈ ℝ ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → ∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1)
14	9, 13	sylan 283	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → ∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1)
15		recn 8005	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℝ → 𝑎 ∈ ℂ)
16		recn 8005	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ℝ → 𝑏 ∈ ℂ)
17		recn 8005	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
18		ax-icn 7967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ i ∈ ℂ
19		mulcl 7999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((i ∈ ℂ ∧ 𝑏 ∈ ℂ) → (i · 𝑏) ∈ ℂ)
20	18, 19	mpan 424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ ℂ → (i · 𝑏) ∈ ℂ)
21		subcl 8218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℂ ∧ (i · 𝑏) ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈ ℂ)
22	20, 21	sylan2 286	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈ ℂ)
23		mulcl 7999	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎 − (i · 𝑏)) ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ)
24	22, 23	sylan 283	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ)
25	24	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ)
26		addcl 7997	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑎 ∈ ℂ ∧ (i · 𝑏) ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈ ℂ)
27	20, 26	sylan2 286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈ ℂ)
28	27	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (𝑎 + (i · 𝑏)) ∈ ℂ)
29	22	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (𝑎 − (i · 𝑏)) ∈ ℂ)
30		simpr 110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
31	28, 29, 30	mulassd 8043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) · 𝑦) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)))
32		recextlem1 8670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏)))
33	32	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) = ((𝑎 · 𝑎) + (𝑏 · 𝑏)))
34	33	oveq1d 5933	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → (((𝑎 + (i · 𝑏)) · (𝑎 − (i · 𝑏))) · 𝑦) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦))
35	31, 34	eqtr3d 2228	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦))
36		id 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1)
37	35, 36	sylan9eq 2246	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1)
38		oveq2 5926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ((𝑎 − (i · 𝑏)) · 𝑦) → ((𝑎 + (i · 𝑏)) · 𝑥) = ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)))
39	38	eqeq1d 2202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ((𝑎 − (i · 𝑏)) · 𝑦) → (((𝑎 + (i · 𝑏)) · 𝑥) = 1 ↔ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1))
40	39	rspcev 2864	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑎 − (i · 𝑏)) · 𝑦) ∈ ℂ ∧ ((𝑎 + (i · 𝑏)) · ((𝑎 − (i · 𝑏)) · 𝑦)) = 1) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)
41	25, 37, 40	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) ∧ 𝑦 ∈ ℂ) ∧ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)
42	41	exp31 364	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑦 ∈ ℂ → ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)))
43	17, 42	syl5 32	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑦 ∈ ℝ → ((((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)))
44	43	rexlimdv 2610	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
45	15, 16, 44	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
46	45	adantr 276	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → (∃𝑦 ∈ ℝ (((𝑎 · 𝑎) + (𝑏 · 𝑏)) · 𝑦) = 1 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
47	14, 46	mpd 13	. . . . . . . . . 10 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ ((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0) → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1)
48	47	ex 115	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) #ℝ 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
49	12, 48	sylbid 150	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (((𝑎 · 𝑎) + (𝑏 · 𝑏)) # 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
50	3, 49	syld 45	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑎 + (i · 𝑏)) # 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
51	50	adantr 276	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → ((𝑎 + (i · 𝑏)) # 0 → ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
52		breq1 4032	. . . . . . 7 ⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 # 0 ↔ (𝑎 + (i · 𝑏)) # 0))
53	52	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (𝐴 # 0 ↔ (𝑎 + (i · 𝑏)) # 0))
54		oveq1 5925	. . . . . . . . 9 ⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 · 𝑥) = ((𝑎 + (i · 𝑏)) · 𝑥))
55	54	eqeq1d 2202	. . . . . . . 8 ⊢ (𝐴 = (𝑎 + (i · 𝑏)) → ((𝐴 · 𝑥) = 1 ↔ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
56	55	rexbidv 2495	. . . . . . 7 ⊢ (𝐴 = (𝑎 + (i · 𝑏)) → (∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
57	56	adantl 277	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1 ↔ ∃𝑥 ∈ ℂ ((𝑎 + (i · 𝑏)) · 𝑥) = 1))
58	51, 53, 57	3imtr4d 203	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ 𝐴 = (𝑎 + (i · 𝑏))) → (𝐴 # 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))
59	58	ex 115	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 # 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)))
60	59	rexlimivv 2617	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 𝐴 = (𝑎 + (i · 𝑏)) → (𝐴 # 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))
61	1, 60	syl 14	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 # 0 → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))
62	61	imp 124	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2164  ∃wrex 2473   class class class wbr 4029  (class class class)co 5918  ℂcc 7870  ℝcr 7871  0cc0 7872  1c1 7873  ici 7874   + caddc 7875   · cmul 7877   − cmin 8190   #_ℝ creap 8593   # cap 8600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-mulrcl 7971  ax-addcom 7972  ax-mulcom 7973  ax-addass 7974  ax-mulass 7975  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-1rid 7979  ax-0id 7980  ax-rnegex 7981  ax-precex 7982  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987  ax-pre-ltadd 7988  ax-pre-mulgt0 7989  ax-pre-mulext 7990

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-id 4324  df-po 4327  df-iso 4328  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-reap 8594  df-ap 8601

This theorem is referenced by:  mulap0  8673  mulcanapd  8680  receuap  8688  recapb  8690