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 x. ; 1 1 ) = ; 9 9

Proof

Step Hyp Ref Expression
1 9cn 
 |-  9 e. CC
2 10nn0 
 |-  ; 1 0 e. NN0
3 2 nn0cni 
 |-  ; 1 0 e. CC
4 ax-1cn 
 |-  1 e. CC
5 3 4 mulcli 
 |-  ( ; 1 0 x. 1 ) e. CC
6 1 5 4 adddii 
 |-  ( 9 x. ( ( ; 1 0 x. 1 ) + 1 ) ) = ( ( 9 x. ( ; 1 0 x. 1 ) ) + ( 9 x. 1 ) )
7 3 mulid1i 
 |-  ( ; 1 0 x. 1 ) = ; 1 0
8 7 oveq2i 
 |-  ( 9 x. ( ; 1 0 x. 1 ) ) = ( 9 x. ; 1 0 )
9 1 3 mulcomi 
 |-  ( 9 x. ; 1 0 ) = ( ; 1 0 x. 9 )
10 8 9 eqtri 
 |-  ( 9 x. ( ; 1 0 x. 1 ) ) = ( ; 1 0 x. 9 )
11 1 mulid1i 
 |-  ( 9 x. 1 ) = 9
12 10 11 oveq12i 
 |-  ( ( 9 x. ( ; 1 0 x. 1 ) ) + ( 9 x. 1 ) ) = ( ( ; 1 0 x. 9 ) + 9 )
13 6 12 eqtri 
 |-  ( 9 x. ( ( ; 1 0 x. 1 ) + 1 ) ) = ( ( ; 1 0 x. 9 ) + 9 )
14 dfdec10 
 |-  ; 1 1 = ( ( ; 1 0 x. 1 ) + 1 )
15 14 oveq2i 
 |-  ( 9 x. ; 1 1 ) = ( 9 x. ( ( ; 1 0 x. 1 ) + 1 ) )
16 dfdec10 
 |-  ; 9 9 = ( ( ; 1 0 x. 9 ) + 9 )
17 13 15 16 3eqtr4i 
 |-  ( 9 x. ; 1 1 ) = ; 9 9