Theorem mulext1 8240

Description: Left extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)

Assertion

Ref	Expression
mulext1	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))

Proof of Theorem mulext1

Dummy variables 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnre 7634	. . 3 ⊢ (𝐶 ∈ ℂ → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝐶 = (𝑢 + (i · 𝑣)))
2	1	3ad2ant3 972	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝐶 = (𝑢 + (i · 𝑣)))
3		cnre 7634	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → ∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)))
4	3	3ad2ant2 971	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)))
5	4	ad2antrr 475	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) → ∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)))
6		cnre 7634	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
7	6	3ad2ant1 970	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
8	7	adantr 272	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
9	8	ad3antrrr 479	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
10		simplrl 505	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑥 ∈ ℝ)
11	10	recnd 7666	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑥 ∈ ℂ)
12		simprl 501	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → 𝑢 ∈ ℝ)
13	12	ad2antrr 475	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑢 ∈ ℝ)
14	13	ad3antrrr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑢 ∈ ℝ)
15	14	recnd 7666	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑢 ∈ ℂ)
16	11, 15	mulcld 7658	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑥 · 𝑢) ∈ ℂ)
17		simplrr 506	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑦 ∈ ℝ)
18	17	recnd 7666	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑦 ∈ ℂ)
19		simprr 502	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → 𝑣 ∈ ℝ)
20	19	ad2antrr 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑣 ∈ ℝ)
21	20	ad3antrrr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑣 ∈ ℝ)
22	21	recnd 7666	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑣 ∈ ℂ)
23	18, 22	mulcld 7658	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑦 · 𝑣) ∈ ℂ)
24	23	negcld 7931	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑦 · 𝑣) ∈ ℂ)
25		simprl 501	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑧 ∈ ℝ)
26	25	ad3antrrr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℝ)
27	26	recnd 7666	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℂ)
28	27, 15	mulcld 7658	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑧 · 𝑢) ∈ ℂ)
29		simprr 502	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑤 ∈ ℝ)
30	29	ad3antrrr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑤 ∈ ℝ)
31	30	recnd 7666	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑤 ∈ ℂ)
32	31, 22	mulcld 7658	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑤 · 𝑣) ∈ ℂ)
33	32	negcld 7931	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑤 · 𝑣) ∈ ℂ)
34		addext 8238	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 · 𝑢) ∈ ℂ ∧ -(𝑦 · 𝑣) ∈ ℂ) ∧ ((𝑧 · 𝑢) ∈ ℂ ∧ -(𝑤 · 𝑣) ∈ ℂ)) → (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) ∨ -(𝑦 · 𝑣) # -(𝑤 · 𝑣))))
35	16, 24, 28, 33, 34	syl22anc 1185	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) ∨ -(𝑦 · 𝑣) # -(𝑤 · 𝑣))))
36		remulext1 8227	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) → 𝑥 # 𝑧))
37	10, 26, 14, 36	syl3anc 1184	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) → 𝑥 # 𝑧))
38		apneg 8239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 · 𝑣) ∈ ℂ ∧ (𝑤 · 𝑣) ∈ ℂ) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) ↔ -(𝑦 · 𝑣) # -(𝑤 · 𝑣)))
39	23, 32, 38	syl2anc 406	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) ↔ -(𝑦 · 𝑣) # -(𝑤 · 𝑣)))
40		remulext1 8227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) → 𝑦 # 𝑤))
41	17, 30, 21, 40	syl3anc 1184	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) → 𝑦 # 𝑤))
42	39, 41	sylbird 169	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (-(𝑦 · 𝑣) # -(𝑤 · 𝑣) → 𝑦 # 𝑤))
43	37, 42	orim12d 741	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 · 𝑢) # (𝑧 · 𝑢) ∨ -(𝑦 · 𝑣) # -(𝑤 · 𝑣)) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
44	35, 43	syld 45	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
45	15, 18	mulcld 7658	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑦) ∈ ℂ)
46	22, 11	mulcld 7658	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑥) ∈ ℂ)
47	15, 31	mulcld 7658	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑤) ∈ ℂ)
48	22, 27	mulcld 7658	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑧) ∈ ℂ)
49		addext 8238	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑢 · 𝑦) ∈ ℂ ∧ (𝑣 · 𝑥) ∈ ℂ) ∧ ((𝑢 · 𝑤) ∈ ℂ ∧ (𝑣 · 𝑧) ∈ ℂ)) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) ∨ (𝑣 · 𝑥) # (𝑣 · 𝑧))))
50	45, 46, 47, 48, 49	syl22anc 1185	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) ∨ (𝑣 · 𝑥) # (𝑣 · 𝑧))))
51		remulext2 8228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ∈ ℝ) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) → 𝑦 # 𝑤))
52	17, 30, 14, 51	syl3anc 1184	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) → 𝑦 # 𝑤))
53		remulext2 8228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((𝑣 · 𝑥) # (𝑣 · 𝑧) → 𝑥 # 𝑧))
54	10, 26, 21, 53	syl3anc 1184	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑣 · 𝑥) # (𝑣 · 𝑧) → 𝑥 # 𝑧))
55	52, 54	orim12d 741	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) # (𝑢 · 𝑤) ∨ (𝑣 · 𝑥) # (𝑣 · 𝑧)) → (𝑦 # 𝑤 ∨ 𝑥 # 𝑧)))
56	50, 55	syld 45	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → (𝑦 # 𝑤 ∨ 𝑥 # 𝑧)))
57		orcom 688	. . . . . . . . . . . . . 14 ⊢ ((𝑦 # 𝑤 ∨ 𝑥 # 𝑧) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤))
58	56, 57	syl6ib 160	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
59	44, 58	jaod 678	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧))) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
60		simpr 109	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐴 = (𝑥 + (i · 𝑦)))
61		simplr 500	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝐶 = (𝑢 + (i · 𝑣)))
62	61	ad3antrrr 479	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐶 = (𝑢 + (i · 𝑣)))
63	60, 62	oveq12d 5724	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐴 · 𝐶) = ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))))
64		simpllr 504	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐵 = (𝑧 + (i · 𝑤)))
65	64, 62	oveq12d 5724	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐵 · 𝐶) = ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))))
66	63, 65	breq12d 3888	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) ↔ ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) # ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣)))))
67		mulreim 8232	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) = (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))))
68	10, 17, 14, 21, 67	syl22anc 1185	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) = (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))))
69		mulreim 8232	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))) = (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
70	26, 30, 14, 21, 69	syl22anc 1185	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))) = (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
71	68, 70	breq12d 3888	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) # ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))) # (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧))))))
72	10, 14	remulcld 7668	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑥 · 𝑢) ∈ ℝ)
73	17, 21	remulcld 7668	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑦 · 𝑣) ∈ ℝ)
74	73	renegcld 8009	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑦 · 𝑣) ∈ ℝ)
75	72, 74	readdcld 7667	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 · 𝑢) + -(𝑦 · 𝑣)) ∈ ℝ)
76	14, 17	remulcld 7668	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑦) ∈ ℝ)
77	21, 10	remulcld 7668	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑥) ∈ ℝ)
78	76, 77	readdcld 7667	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑢 · 𝑦) + (𝑣 · 𝑥)) ∈ ℝ)
79	26, 14	remulcld 7668	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑧 · 𝑢) ∈ ℝ)
80	30, 21	remulcld 7668	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑤 · 𝑣) ∈ ℝ)
81	80	renegcld 8009	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑤 · 𝑣) ∈ ℝ)
82	79, 81	readdcld 7667	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∈ ℝ)
83	14, 30	remulcld 7668	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑤) ∈ ℝ)
84	21, 26	remulcld 7668	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑧) ∈ ℝ)
85	83, 84	readdcld 7667	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑢 · 𝑤) + (𝑣 · 𝑧)) ∈ ℝ)
86		apreim 8231	. . . . . . . . . . . . . 14 ⊢ (((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) ∈ ℝ ∧ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) ∈ ℝ) ∧ (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∈ ℝ ∧ ((𝑢 · 𝑤) + (𝑣 · 𝑧)) ∈ ℝ)) → ((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))) # (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
87	75, 78, 82, 85, 86	syl22anc 1185	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))) # (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
88	66, 71, 87	3bitrd 213	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
89		apreim 8231	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → ((𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
90	10, 17, 26, 30, 89	syl22anc 1185	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
91	59, 88, 90	3imtr4d 202	. . . . . . . . . . 11 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → (𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤))))
92	60, 64	breq12d 3888	. . . . . . . . . . 11 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐴 # 𝐵 ↔ (𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤))))
93	91, 92	sylibrd 168	. . . . . . . . . 10 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
94	93	ex 114	. . . . . . . . 9 ⊢ (((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
95	94	rexlimdvva 2516	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
96	9, 95	mpd 13	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
97	96	ex 114	. . . . . 6 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → (𝐵 = (𝑧 + (i · 𝑤)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
98	97	rexlimdvva 2516	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) → (∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
99	5, 98	mpd 13	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
100	99	ex 114	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → (𝐶 = (𝑢 + (i · 𝑣)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
101	100	rexlimdvva 2516	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝐶 = (𝑢 + (i · 𝑣)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
102	2, 101	mpd 13	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 670   ∧ w3a 930   = wceq 1299   ∈ wcel 1448  ∃wrex 2376   class class class wbr 3875  (class class class)co 5706  ℂcc 7498  ℝcr 7499  ici 7502   + caddc 7503   · cmul 7505  -cneg 7805   # cap 8209

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-mulrcl 7594  ax-addcom 7595  ax-mulcom 7596  ax-addass 7597  ax-mulass 7598  ax-distr 7599  ax-i2m1 7600  ax-0lt1 7601  ax-1rid 7602  ax-0id 7603  ax-rnegex 7604  ax-precex 7605  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltwlin 7608  ax-pre-lttrn 7609  ax-pre-apti 7610  ax-pre-ltadd 7611  ax-pre-mulgt0 7612  ax-pre-mulext 7613

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-id 4153  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-iota 5024  df-fun 5061  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-pnf 7674  df-mnf 7675  df-ltxr 7677  df-sub 7806  df-neg 7807  df-reap 8203  df-ap 8210

This theorem is referenced by:  mulext2  8241  mulext  8242  mulap0  8276  apmul1  8409