Metamath Proof Explorer

Theorem 9t11e99

Description: 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion 9t11e99 ( 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 mulid1i ⊢ ( 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 mulid1i ⊢ ( 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