Theorem sn-mul01

Description: mul01 without ax-mulcom . (Contributed by SN, 5-May-2024)

	Ref	Expression
Assertion	sn-mul01	|- ( A e. CC -> ( A x. 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( A e. CC -> A e. CC )
2		0cnd	|- ( A e. CC -> 0 e. CC )
3	1 2	mulcld	|- ( A e. CC -> ( A x. 0 ) e. CC )
4	1 2 2	adddid	|- ( A e. CC -> ( A x. ( 0 + 0 ) ) = ( ( A x. 0 ) + ( A x. 0 ) ) )
5		sn-00id	|- ( 0 + 0 ) = 0
6	5	oveq2i	|- ( A x. ( 0 + 0 ) ) = ( A x. 0 )
7	4 6	eqtr3di	|- ( A e. CC -> ( ( A x. 0 ) + ( A x. 0 ) ) = ( A x. 0 ) )
8	3 7	sn-addid0	|- ( A e. CC -> ( A x. 0 ) = 0 )