Theorem 9t11e99OLD

Description: Obsolete version of 9t11e99 as of 10-Jun-2026. (Contributed by AV, 14-Jun-2021) (Revised by AV, 6-Sep-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	9t11e99OLD	⊢ ( 9 · ; 1 1 ) = ; 9 9

Proof

Step	Hyp	Ref	Expression
1		9cn	⊢ 9 ∈ ℂ
2		10nn0	⊢ ; 1 0 ∈ ℕ0
3	2	nn0cni	⊢ ; 1 0 ∈ ℂ
4		ax-1cn	⊢ 1 ∈ ℂ
5	3 4	mulcli	⊢ ( ; 1 0 · 1 ) ∈ ℂ
6	1 5 4	adddii	⊢ ( 9 · ( ( ; 1 0 · 1 ) + 1 ) ) = ( ( 9 · ( ; 1 0 · 1 ) ) + ( 9 · 1 ) )
7	3	mulridi	⊢ ( ; 1 0 · 1 ) = ; 1 0
8	7	oveq2i	⊢ ( 9 · ( ; 1 0 · 1 ) ) = ( 9 · ; 1 0 )
9	1 3	mulcomi	⊢ ( 9 · ; 1 0 ) = ( ; 1 0 · 9 )
10	8 9	eqtri	⊢ ( 9 · ( ; 1 0 · 1 ) ) = ( ; 1 0 · 9 )
11	1	mulridi	⊢ ( 9 · 1 ) = 9
12	10 11	oveq12i	⊢ ( ( 9 · ( ; 1 0 · 1 ) ) + ( 9 · 1 ) ) = ( ( ; 1 0 · 9 ) + 9 )
13	6 12	eqtri	⊢ ( 9 · ( ( ; 1 0 · 1 ) + 1 ) ) = ( ( ; 1 0 · 9 ) + 9 )
14		dfdec10	⊢ ; 1 1 = ( ( ; 1 0 · 1 ) + 1 )
15	14	oveq2i	⊢ ( 9 · ; 1 1 ) = ( 9 · ( ( ; 1 0 · 1 ) + 1 ) )
16		dfdec10	⊢ ; 9 9 = ( ( ; 1 0 · 9 ) + 9 )
17	13 15 16	3eqtr4i	⊢ ( 9 · ; 1 1 ) = ; 9 9