remul01

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

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ A \cdot 0 = 1 \to 2 A \cdot 0 = 2 \cdot 1$
2	1	adantl	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 A \cdot 0 = 2 \cdot 1$
3		2re	$⊢ 2 \in ℝ$
4		ax-1rid	$⊢ 2 \in ℝ \to 2 \cdot 1 = 2$
5	3 4	mp1i	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 \cdot 1 = 2$
6	2 5	eqtrd	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 A \cdot 0 = 2$
7	3	a1i	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 \in ℝ$
8		simpl	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to A \in ℝ$
9		0red	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 0 \in ℝ$
10	8 9	remulcld	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to A \cdot 0 \in ℝ$
11	7 10	remulcld	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 A \cdot 0 \in ℝ$
12		sn-0ne2	$⊢ 0 \neq 2$
13	12	necomi	$⊢ 2 \neq 0$
14	13	a1i	$⊢ 2 A \cdot 0 = 2 \to 2 \neq 0$
15		eqtr2	$⊢ (2 A \cdot 0 = 2 \land 2 A \cdot 0 = 0) \to 2 = 0$
16	14 15	mteqand	$⊢ 2 A \cdot 0 = 2 \to 2 A \cdot 0 \neq 0$
17		ax-rrecex	$⊢ (2 A \cdot 0 \in ℝ \land 2 A \cdot 0 \neq 0) \to \exists x \in ℝ 2 A \cdot 0 x = 1$
18	11 16 17	syl2an	$⊢ ((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \to \exists x \in ℝ 2 A \cdot 0 x = 1$
19		2cnd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 2 \in ℂ$
20		simplll	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A \in ℝ$
21		0red	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 0 \in ℝ$
22	20 21	remulcld	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A \cdot 0 \in ℝ$
23	22	recnd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A \cdot 0 \in ℂ$
24		simprl	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to x \in ℝ$
25	24	recnd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to x \in ℂ$
26	19 23 25	mulassd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 2 A \cdot 0 x = 2 A \cdot 0 x$
27		simprr	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 2 A \cdot 0 x = 1$
28	20	recnd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A \in ℂ$
29		0cnd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 0 \in ℂ$
30	28 29 25	mulassd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A \cdot 0 x = A 0 \cdot x$
31		remul02	$⊢ x \in ℝ \to 0 \cdot x = 0$
32	31	ad2antrl	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 0 \cdot x = 0$
33	32	oveq2d	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A 0 \cdot x = A \cdot 0$
34	30 33	eqtrd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to A \cdot 0 x = A \cdot 0$
35	34	oveq2d	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 2 A \cdot 0 x = 2 A \cdot 0$
36	26 27 35	3eqtr3rd	$⊢ (((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \land (x \in ℝ \land 2 A \cdot 0 x = 1)) \to 2 A \cdot 0 = 1$
37	18 36	rexlimddv	$⊢ ((A \in ℝ \land A \cdot 0 = 1) \land 2 A \cdot 0 = 2) \to 2 A \cdot 0 = 1$
38	6 37	mpdan	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 A \cdot 0 = 1$
39		sn-1ne2	$⊢ 1 \neq 2$
40	39	a1i	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 1 \neq 2$
41	38 40	eqnetrd	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to 2 A \cdot 0 \neq 2$
42	6 41	pm2.21ddne	$⊢ (A \in ℝ \land A \cdot 0 = 1) \to \neg A \cdot 0 = 1$
43	42	ex	$⊢ A \in ℝ \to (A \cdot 0 = 1 \to \neg A \cdot 0 = 1)$
44		pm2.01	$⊢ (A \cdot 0 = 1 \to \neg A \cdot 0 = 1) \to \neg A \cdot 0 = 1$
45	44	neqned	$⊢ (A \cdot 0 = 1 \to \neg A \cdot 0 = 1) \to A \cdot 0 \neq 1$
46	43 45	syl	$⊢ A \in ℝ \to A \cdot 0 \neq 1$
47		id	$⊢ A \in ℝ \to A \in ℝ$
48		elre0re	$⊢ A \in ℝ \to 0 \in ℝ$
49	47 48	remulcld	$⊢ A \in ℝ \to A \cdot 0 \in ℝ$
50		ax-rrecex	$⊢ (A \cdot 0 \in ℝ \land A \cdot 0 \neq 0) \to \exists x \in ℝ A \cdot 0 x = 1$
51	49 50	sylan	$⊢ (A \in ℝ \land A \cdot 0 \neq 0) \to \exists x \in ℝ A \cdot 0 x = 1$
52		simpll	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to A \in ℝ$
53	52	recnd	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to A \in ℂ$
54		0cnd	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to 0 \in ℂ$
55		simprl	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to x \in ℝ$
56	55	recnd	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to x \in ℂ$
57	53 54 56	mulassd	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to A \cdot 0 x = A 0 \cdot x$
58		simprr	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to A \cdot 0 x = 1$
59	31	oveq2d	$⊢ x \in ℝ \to A 0 \cdot x = A \cdot 0$
60	59	ad2antrl	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to A 0 \cdot x = A \cdot 0$
61	57 58 60	3eqtr3rd	$⊢ ((A \in ℝ \land A \cdot 0 \neq 0) \land (x \in ℝ \land A \cdot 0 x = 1)) \to A \cdot 0 = 1$
62	51 61	rexlimddv	$⊢ (A \in ℝ \land A \cdot 0 \neq 0) \to A \cdot 0 = 1$
63	62	ex	$⊢ A \in ℝ \to (A \cdot 0 \neq 0 \to A \cdot 0 = 1)$
64	63	necon1d	$⊢ A \in ℝ \to (A \cdot 0 \neq 1 \to A \cdot 0 = 0)$
65	46 64	mpd	$⊢ A \in ℝ \to A \cdot 0 = 0$

Metamath Proof Explorer

Theorem remul01

Proof