Theorem mulext1 8797

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 8180	. . 3 ⊢ (𝐶 ∈ ℂ → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝐶 = (𝑢 + (i · 𝑣)))
2	1	3ad2ant3 1046	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝐶 = (𝑢 + (i · 𝑣)))
3		cnre 8180	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → ∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)))
4	3	3ad2ant2 1045	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)))
5	4	ad2antrr 488	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) → ∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)))
6		cnre 8180	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
7	6	3ad2ant1 1044	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
8	7	adantr 276	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
9	8	ad3antrrr 492	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)))
10		simplrl 537	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑥 ∈ ℝ)
11	10	recnd 8213	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑥 ∈ ℂ)
12		simprl 531	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → 𝑢 ∈ ℝ)
13	12	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑢 ∈ ℝ)
14	13	ad3antrrr 492	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑢 ∈ ℝ)
15	14	recnd 8213	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑢 ∈ ℂ)
16	11, 15	mulcld 8205	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑥 · 𝑢) ∈ ℂ)
17		simplrr 538	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑦 ∈ ℝ)
18	17	recnd 8213	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑦 ∈ ℂ)
19		simprr 533	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → 𝑣 ∈ ℝ)
20	19	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑣 ∈ ℝ)
21	20	ad3antrrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑣 ∈ ℝ)
22	21	recnd 8213	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑣 ∈ ℂ)
23	18, 22	mulcld 8205	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑦 · 𝑣) ∈ ℂ)
24	23	negcld 8482	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑦 · 𝑣) ∈ ℂ)
25		simprl 531	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑧 ∈ ℝ)
26	25	ad3antrrr 492	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℝ)
27	26	recnd 8213	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑧 ∈ ℂ)
28	27, 15	mulcld 8205	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑧 · 𝑢) ∈ ℂ)
29		simprr 533	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝑤 ∈ ℝ)
30	29	ad3antrrr 492	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑤 ∈ ℝ)
31	30	recnd 8213	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝑤 ∈ ℂ)
32	31, 22	mulcld 8205	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑤 · 𝑣) ∈ ℂ)
33	32	negcld 8482	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑤 · 𝑣) ∈ ℂ)
34		addext 8795	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 · 𝑢) ∈ ℂ ∧ -(𝑦 · 𝑣) ∈ ℂ) ∧ ((𝑧 · 𝑢) ∈ ℂ ∧ -(𝑤 · 𝑣) ∈ ℂ)) → (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) ∨ -(𝑦 · 𝑣) # -(𝑤 · 𝑣))))
35	16, 24, 28, 33, 34	syl22anc 1274	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) ∨ -(𝑦 · 𝑣) # -(𝑤 · 𝑣))))
36		remulext1 8784	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑢 ∈ ℝ) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) → 𝑥 # 𝑧))
37	10, 26, 14, 36	syl3anc 1273	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 · 𝑢) # (𝑧 · 𝑢) → 𝑥 # 𝑧))
38		apneg 8796	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 · 𝑣) ∈ ℂ ∧ (𝑤 · 𝑣) ∈ ℂ) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) ↔ -(𝑦 · 𝑣) # -(𝑤 · 𝑣)))
39	23, 32, 38	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) ↔ -(𝑦 · 𝑣) # -(𝑤 · 𝑣)))
40		remulext1 8784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) → 𝑦 # 𝑤))
41	17, 30, 21, 40	syl3anc 1273	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑦 · 𝑣) # (𝑤 · 𝑣) → 𝑦 # 𝑤))
42	39, 41	sylbird 170	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (-(𝑦 · 𝑣) # -(𝑤 · 𝑣) → 𝑦 # 𝑤))
43	37, 42	orim12d 793	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 · 𝑢) # (𝑧 · 𝑢) ∨ -(𝑦 · 𝑣) # -(𝑤 · 𝑣)) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
44	35, 43	syld 45	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
45	15, 18	mulcld 8205	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑦) ∈ ℂ)
46	22, 11	mulcld 8205	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑥) ∈ ℂ)
47	15, 31	mulcld 8205	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑤) ∈ ℂ)
48	22, 27	mulcld 8205	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑧) ∈ ℂ)
49		addext 8795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑢 · 𝑦) ∈ ℂ ∧ (𝑣 · 𝑥) ∈ ℂ) ∧ ((𝑢 · 𝑤) ∈ ℂ ∧ (𝑣 · 𝑧) ∈ ℂ)) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) ∨ (𝑣 · 𝑥) # (𝑣 · 𝑧))))
50	45, 46, 47, 48, 49	syl22anc 1274	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) ∨ (𝑣 · 𝑥) # (𝑣 · 𝑧))))
51		remulext2 8785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ∈ ℝ) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) → 𝑦 # 𝑤))
52	17, 30, 14, 51	syl3anc 1273	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑢 · 𝑦) # (𝑢 · 𝑤) → 𝑦 # 𝑤))
53		remulext2 8785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑣 ∈ ℝ) → ((𝑣 · 𝑥) # (𝑣 · 𝑧) → 𝑥 # 𝑧))
54	10, 26, 21, 53	syl3anc 1273	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑣 · 𝑥) # (𝑣 · 𝑧) → 𝑥 # 𝑧))
55	52, 54	orim12d 793	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) # (𝑢 · 𝑤) ∨ (𝑣 · 𝑥) # (𝑣 · 𝑧)) → (𝑦 # 𝑤 ∨ 𝑥 # 𝑧)))
56	50, 55	syld 45	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → (𝑦 # 𝑤 ∨ 𝑥 # 𝑧)))
57		orcom 735	. . . . . . . . . . . . . 14 ⊢ ((𝑦 # 𝑤 ∨ 𝑥 # 𝑧) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤))
58	56, 57	imbitrdi 161	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
59	44, 58	jaod 724	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧))) → (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
60		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐴 = (𝑥 + (i · 𝑦)))
61		simplr 529	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → 𝐶 = (𝑢 + (i · 𝑣)))
62	61	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐶 = (𝑢 + (i · 𝑣)))
63	60, 62	oveq12d 6041	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐴 · 𝐶) = ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))))
64		simpllr 536	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → 𝐵 = (𝑧 + (i · 𝑤)))
65	64, 62	oveq12d 6041	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐵 · 𝐶) = ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))))
66	63, 65	breq12d 4102	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) ↔ ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) # ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣)))))
67		mulreim 8789	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) = (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))))
68	10, 17, 14, 21, 67	syl22anc 1274	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) = (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))))
69		mulreim 8789	. . . . . . . . . . . . . . 15 ⊢ (((𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))) = (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
70	26, 30, 14, 21, 69	syl22anc 1274	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))) = (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
71	68, 70	breq12d 4102	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (((𝑥 + (i · 𝑦)) · (𝑢 + (i · 𝑣))) # ((𝑧 + (i · 𝑤)) · (𝑢 + (i · 𝑣))) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))) # (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧))))))
72	10, 14	remulcld 8215	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑥 · 𝑢) ∈ ℝ)
73	17, 21	remulcld 8215	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑦 · 𝑣) ∈ ℝ)
74	73	renegcld 8564	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑦 · 𝑣) ∈ ℝ)
75	72, 74	readdcld 8214	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 · 𝑢) + -(𝑦 · 𝑣)) ∈ ℝ)
76	14, 17	remulcld 8215	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑦) ∈ ℝ)
77	21, 10	remulcld 8215	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑥) ∈ ℝ)
78	76, 77	readdcld 8214	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑢 · 𝑦) + (𝑣 · 𝑥)) ∈ ℝ)
79	26, 14	remulcld 8215	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑧 · 𝑢) ∈ ℝ)
80	30, 21	remulcld 8215	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑤 · 𝑣) ∈ ℝ)
81	80	renegcld 8564	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → -(𝑤 · 𝑣) ∈ ℝ)
82	79, 81	readdcld 8214	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∈ ℝ)
83	14, 30	remulcld 8215	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑢 · 𝑤) ∈ ℝ)
84	21, 26	remulcld 8215	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝑣 · 𝑧) ∈ ℝ)
85	83, 84	readdcld 8214	. . . . . . . . . . . . . 14 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑢 · 𝑤) + (𝑣 · 𝑧)) ∈ ℝ)
86		apreim 8788	. . . . . . . . . . . . . 14 ⊢ (((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) ∈ ℝ ∧ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) ∈ ℝ) ∧ (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∈ ℝ ∧ ((𝑢 · 𝑤) + (𝑣 · 𝑧)) ∈ ℝ)) → ((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))) # (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
87	75, 78, 82, 85, 86	syl22anc 1274	. . . . . . . . . . . . 13 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((((𝑥 · 𝑢) + -(𝑦 · 𝑣)) + (i · ((𝑢 · 𝑦) + (𝑣 · 𝑥)))) # (((𝑧 · 𝑢) + -(𝑤 · 𝑣)) + (i · ((𝑢 · 𝑤) + (𝑣 · 𝑧)))) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
88	66, 71, 87	3bitrd 214	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) ↔ (((𝑥 · 𝑢) + -(𝑦 · 𝑣)) # ((𝑧 · 𝑢) + -(𝑤 · 𝑣)) ∨ ((𝑢 · 𝑦) + (𝑣 · 𝑥)) # ((𝑢 · 𝑤) + (𝑣 · 𝑧)))))
89		apreim 8788	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → ((𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
90	10, 17, 26, 30, 89	syl22anc 1274	. . . . . . . . . . . 12 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤)) ↔ (𝑥 # 𝑧 ∨ 𝑦 # 𝑤)))
91	59, 88, 90	3imtr4d 203	. . . . . . . . . . 11 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → (𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤))))
92	60, 64	breq12d 4102	. . . . . . . . . . 11 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → (𝐴 # 𝐵 ↔ (𝑥 + (i · 𝑦)) # (𝑧 + (i · 𝑤))))
93	91, 92	sylibrd 169	. . . . . . . . . 10 ⊢ ((((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) ∧ 𝐴 = (𝑥 + (i · 𝑦))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
94	93	ex 115	. . . . . . . . 9 ⊢ (((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
95	94	rexlimdvva 2657	. . . . . . . 8 ⊢ ((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝐴 = (𝑥 + (i · 𝑦)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
96	9, 95	mpd 13	. . . . . . 7 ⊢ ((((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) ∧ 𝐵 = (𝑧 + (i · 𝑤))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
97	96	ex 115	. . . . . 6 ⊢ (((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) ∧ (𝑧 ∈ ℝ ∧ 𝑤 ∈ ℝ)) → (𝐵 = (𝑧 + (i · 𝑤)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
98	97	rexlimdvva 2657	. . . . 5 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) → (∃𝑧 ∈ ℝ ∃𝑤 ∈ ℝ 𝐵 = (𝑧 + (i · 𝑤)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
99	5, 98	mpd 13	. . . 4 ⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) ∧ 𝐶 = (𝑢 + (i · 𝑣))) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
100	99	ex 115	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ)) → (𝐶 = (𝑢 + (i · 𝑣)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
101	100	rexlimdvva 2657	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝐶 = (𝑢 + (i · 𝑣)) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵)))
102	2, 101	mpd 13	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 715   ∧ w3a 1004   = wceq 1397   ∈ wcel 2201  ∃wrex 2510   class class class wbr 4089  (class class class)co 6023  ℂcc 8035  ℝcr 8036  ici 8039   + caddc 8040   · cmul 8042  -cneg 8356   # cap 8766

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-cnex 8128  ax-resscn 8129  ax-1cn 8130  ax-1re 8131  ax-icn 8132  ax-addcl 8133  ax-addrcl 8134  ax-mulcl 8135  ax-mulrcl 8136  ax-addcom 8137  ax-mulcom 8138  ax-addass 8139  ax-mulass 8140  ax-distr 8141  ax-i2m1 8142  ax-0lt1 8143  ax-1rid 8144  ax-0id 8145  ax-rnegex 8146  ax-precex 8147  ax-cnre 8148  ax-pre-ltirr 8149  ax-pre-ltwlin 8150  ax-pre-lttrn 8151  ax-pre-apti 8152  ax-pre-ltadd 8153  ax-pre-mulgt0 8154  ax-pre-mulext 8155

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-reu 2516  df-rab 2518  df-v 2803  df-sbc 3031  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-opab 4152  df-id 4392  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-iota 5288  df-fun 5330  df-fv 5336  df-riota 5976  df-ov 6026  df-oprab 6027  df-mpo 6028  df-pnf 8221  df-mnf 8222  df-ltxr 8224  df-sub 8357  df-neg 8358  df-reap 8760  df-ap 8767

This theorem is referenced by:  mulext2  8798  mulext  8799  mulap0  8839  apmul1  8973