sn-1ticom

Description: Lemma for sn-mullid and sn-it1ei . (Contributed by SN, 27-May-2024)

		Ref	Expression
	Assertion	sn-1ticom	$⊢ 1 i = i \cdot 1$

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2	1 1	mulcli	$⊢ i i \in ℂ$
3	2 2 1	mulassi	$⊢ i i i i i = i i i i i$
4	1 2	mulcli	$⊢ i i i \in ℂ$
5	1 1 4	mulassi	$⊢ i i i i i = i i i i i$
6	1 1 1	mulassi	$⊢ i i i = i i i$
7	6	oveq2i	$⊢ i i i i i = i i i i i$
8	1 1 2	mulassi	$⊢ i i i i = i i i i$
9	8	oveq2i	$⊢ i i i i i = i i i i i$
10	5 7 9	3eqtr4i	$⊢ i i i i i = i i i i i$
11	3 10	eqtri	$⊢ i i i i i = i i i i i$
12		rei4	$⊢ i i i i = 1$
13	12	oveq1i	$⊢ i i i i i = 1 i$
14	12	oveq2i	$⊢ i i i i i = i \cdot 1$
15	11 13 14	3eqtr3i	$⊢ 1 i = i \cdot 1$

Metamath Proof Explorer