mul02lem1

Description: Lemma for mul02 . If any real does not produce 0 when multiplied by 0 , then any complex is equal to double itself. (Contributed by Scott Fenton, 3-Jan-2013)

		Ref	Expression
	Assertion	mul02lem1	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \to B = B + B$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		remulcl	$⊢ (0 \in ℝ \land A \in ℝ) \to 0 \cdot A \in ℝ$
3	1 2	mpan	$⊢ A \in ℝ \to 0 \cdot A \in ℝ$
4		ax-rrecex	$⊢ (0 \cdot A \in ℝ \land 0 \cdot A \neq 0) \to \exists y \in ℝ 0 \cdot A y = 1$
5	3 4	sylan	$⊢ (A \in ℝ \land 0 \cdot A \neq 0) \to \exists y \in ℝ 0 \cdot A y = 1$
6	5	adantr	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \to \exists y \in ℝ 0 \cdot A y = 1$
7		00id	$⊢ 0 + 0 = 0$
8	7	oveq2i	$⊢ y A B (0 + 0) = y A B \cdot 0$
9	8	eqcomi	$⊢ y A B \cdot 0 = y A B (0 + 0)$
10		simprl	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y \in ℝ$
11	10	recnd	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y \in ℂ$
12		simplll	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to A \in ℝ$
13	12	recnd	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to A \in ℂ$
14	11 13	mulcld	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A \in ℂ$
15		simplr	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to B \in ℂ$
16		0cn	$⊢ 0 \in ℂ$
17		mul32	$⊢ (y A \in ℂ \land B \in ℂ \land 0 \in ℂ) \to y A B \cdot 0 = y A \cdot 0 B$
18	16 17	mp3an3	$⊢ (y A \in ℂ \land B \in ℂ) \to y A B \cdot 0 = y A \cdot 0 B$
19	14 15 18	syl2anc	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A B \cdot 0 = y A \cdot 0 B$
20		mul31	$⊢ (y \in ℂ \land A \in ℂ \land 0 \in ℂ) \to y A \cdot 0 = 0 \cdot A y$
21	16 20	mp3an3	$⊢ (y \in ℂ \land A \in ℂ) \to y A \cdot 0 = 0 \cdot A y$
22	11 13 21	syl2anc	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A \cdot 0 = 0 \cdot A y$
23		simprr	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to 0 \cdot A y = 1$
24	22 23	eqtrd	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A \cdot 0 = 1$
25	24	oveq1d	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A \cdot 0 B = 1 B$
26		mulid2	$⊢ B \in ℂ \to 1 B = B$
27	26	ad2antlr	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to 1 B = B$
28	25 27	eqtrd	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A \cdot 0 B = B$
29	19 28	eqtrd	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A B \cdot 0 = B$
30	14 15	mulcld	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A B \in ℂ$
31		adddi	$⊢ (y A B \in ℂ \land 0 \in ℂ \land 0 \in ℂ) \to y A B (0 + 0) = y A B \cdot 0 + y A B \cdot 0$
32	16 16 31	mp3an23	$⊢ y A B \in ℂ \to y A B (0 + 0) = y A B \cdot 0 + y A B \cdot 0$
33	30 32	syl	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A B (0 + 0) = y A B \cdot 0 + y A B \cdot 0$
34	29 29	oveq12d	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A B \cdot 0 + y A B \cdot 0 = B + B$
35	33 34	eqtrd	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to y A B (0 + 0) = B + B$
36	9 29 35	3eqtr3a	$⊢ (((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \land (y \in ℝ \land 0 \cdot A y = 1)) \to B = B + B$
37	6 36	rexlimddv	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land B \in ℂ) \to B = B + B$

Metamath Proof Explorer

Theorem mul02lem1

Proof