This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3rdpwhole

Description: A third of a number plus the number is four thirds of the number. (Contributed by SN, 19-Nov-2025)

Ref Expression
Assertion 3rdpwhole 
|- ( A e. CC -> ( ( A / 3 ) + A ) = ( 4 x. ( A / 3 ) ) )

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( A e. CC -> 1 e. CC )
2 3cn 
 |-  3 e. CC
3 2 a1i 
 |-  ( A e. CC -> 3 e. CC )
4 3ne0 
 |-  3 =/= 0
5 divcl 
 |-  ( ( A e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( A / 3 ) e. CC )
6 2 4 5 mp3an23 
 |-  ( A e. CC -> ( A / 3 ) e. CC )
7 1 3 6 adddird 
 |-  ( A e. CC -> ( ( 1 + 3 ) x. ( A / 3 ) ) = ( ( 1 x. ( A / 3 ) ) + ( 3 x. ( A / 3 ) ) ) )
8 1p3e4 
 |-  ( 1 + 3 ) = 4
9 8 a1i 
 |-  ( A e. CC -> ( 1 + 3 ) = 4 )
10 9 oveq1d 
 |-  ( A e. CC -> ( ( 1 + 3 ) x. ( A / 3 ) ) = ( 4 x. ( A / 3 ) ) )
11 6 mullidd 
 |-  ( A e. CC -> ( 1 x. ( A / 3 ) ) = ( A / 3 ) )
12 divcan2 
 |-  ( ( A e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 3 x. ( A / 3 ) ) = A )
13 2 4 12 mp3an23 
 |-  ( A e. CC -> ( 3 x. ( A / 3 ) ) = A )
14 11 13 oveq12d 
 |-  ( A e. CC -> ( ( 1 x. ( A / 3 ) ) + ( 3 x. ( A / 3 ) ) ) = ( ( A / 3 ) + A ) )
15 7 10 14 3eqtr3rd 
 |-  ( A e. CC -> ( ( A / 3 ) + A ) = ( 4 x. ( A / 3 ) ) )