remul02

Description: Real number version of mul02 proven without ax-mulcom . (Contributed by SN, 23-Jan-2024)

		Ref	Expression
	Assertion	remul02	$⊢ A \in ℝ \to 0 \cdot A = 0$

Proof

Step	Hyp	Ref	Expression
1		sn-1ne2	$⊢ 1 \neq 2$
2		elre0re	$⊢ A \in ℝ \to 0 \in ℝ$
3		id	$⊢ A \in ℝ \to A \in ℝ$
4	2 3	remulcld	$⊢ A \in ℝ \to 0 \cdot A \in ℝ$
5		ax-rrecex	$⊢ (0 \cdot A \in ℝ \land 0 \cdot A \neq 0) \to \exists x \in ℝ 0 \cdot A x = 1$
6	4 5	sylan	$⊢ (A \in ℝ \land 0 \cdot A \neq 0) \to \exists x \in ℝ 0 \cdot A x = 1$
7		simprr	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \cdot A x = 1$
8		df-2	$⊢ 2 = 1 + 1$
9	8	oveq1i	$⊢ 2 \cdot 0 = (1 + 1) \cdot 0$
10		re0m0e0	$⊢ 0 -_{ℝ} 0 = 0$
11	10	eqcomi	$⊢ 0 = 0 -_{ℝ} 0$
12	11	oveq2i	$⊢ (1 + 1) \cdot 0 = (1 + 1) (0 -_{ℝ} 0)$
13		1re	$⊢ 1 \in ℝ$
14	13 13	readdcli	$⊢ 1 + 1 \in ℝ$
15		sn-00idlem1	$⊢ 1 + 1 \in ℝ \to (1 + 1) (0 -_{ℝ} 0) = (1 + 1) -_{ℝ} (1 + 1)$
16	14 15	ax-mp	$⊢ (1 + 1) (0 -_{ℝ} 0) = (1 + 1) -_{ℝ} (1 + 1)$
17		repnpcan	$⊢ (1 \in ℝ \land 1 \in ℝ \land 1 \in ℝ) \to (1 + 1) -_{ℝ} (1 + 1) = 1 -_{ℝ} 1$
18	13 13 13 17	mp3an	$⊢ (1 + 1) -_{ℝ} (1 + 1) = 1 -_{ℝ} 1$
19		re1m1e0m0	$⊢ 1 -_{ℝ} 1 = 0 -_{ℝ} 0$
20	18 19 10	3eqtri	$⊢ (1 + 1) -_{ℝ} (1 + 1) = 0$
21	12 16 20	3eqtri	$⊢ (1 + 1) \cdot 0 = 0$
22	9 21	eqtr2i	$⊢ 0 = 2 \cdot 0$
23	22	oveq1i	$⊢ 0 \cdot A = 2 \cdot 0 A$
24	23	oveq1i	$⊢ 0 \cdot A x = 2 \cdot 0 A x$
25	24	a1i	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \cdot A x = 2 \cdot 0 A x$
26		2cnd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 2 \in ℂ$
27		0cnd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \in ℂ$
28		simpll	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to A \in ℝ$
29	28	recnd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to A \in ℂ$
30	26 27 29	mulassd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 2 \cdot 0 A = 2 0 \cdot A$
31	30	oveq1d	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 2 \cdot 0 A x = 2 0 \cdot A x$
32	4	ad2antrr	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \cdot A \in ℝ$
33	32	recnd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \cdot A \in ℂ$
34		simprl	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to x \in ℝ$
35	34	recnd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to x \in ℂ$
36	26 33 35	mulassd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 2 0 \cdot A x = 2 0 \cdot A x$
37	25 31 36	3eqtrd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \cdot A x = 2 0 \cdot A x$
38	7	oveq2d	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 2 0 \cdot A x = 2 \cdot 1$
39		2re	$⊢ 2 \in ℝ$
40		ax-1rid	$⊢ 2 \in ℝ \to 2 \cdot 1 = 2$
41	39 40	mp1i	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 2 \cdot 1 = 2$
42	37 38 41	3eqtrd	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 0 \cdot A x = 2$
43	7 42	eqtr3d	$⊢ ((A \in ℝ \land 0 \cdot A \neq 0) \land (x \in ℝ \land 0 \cdot A x = 1)) \to 1 = 2$
44	6 43	rexlimddv	$⊢ (A \in ℝ \land 0 \cdot A \neq 0) \to 1 = 2$
45	44	ex	$⊢ A \in ℝ \to (0 \cdot A \neq 0 \to 1 = 2)$
46	45	necon1d	$⊢ A \in ℝ \to (1 \neq 2 \to 0 \cdot A = 0)$
47	1 46	mpi	$⊢ A \in ℝ \to 0 \cdot A = 0$

Metamath Proof Explorer

Theorem remul02

Proof