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	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 3 ) + 𝐴 ) = ( 4 · ( 𝐴 / 3 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1cnd	⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
2		3cn	⊢ 3 ∈ ℂ
3	2	a1i	⊢ ( 𝐴 ∈ ℂ → 3 ∈ ℂ )
4		3ne0	⊢ 3 ≠ 0
5		divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( 𝐴 / 3 ) ∈ ℂ )
6	2 4 5	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 3 ) ∈ ℂ )
7	1 3 6	adddird	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 3 ) · ( 𝐴 / 3 ) ) = ( ( 1 · ( 𝐴 / 3 ) ) + ( 3 · ( 𝐴 / 3 ) ) ) )
8		1p3e4	⊢ ( 1 + 3 ) = 4
9	8	a1i	⊢ ( 𝐴 ∈ ℂ → ( 1 + 3 ) = 4 )
10	9	oveq1d	⊢ ( 𝐴 ∈ ℂ → ( ( 1 + 3 ) · ( 𝐴 / 3 ) ) = ( 4 · ( 𝐴 / 3 ) ) )
11	6	mullidd	⊢ ( 𝐴 ∈ ℂ → ( 1 · ( 𝐴 / 3 ) ) = ( 𝐴 / 3 ) )
12		divcan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℂ ∧ 3 ≠ 0 ) → ( 3 · ( 𝐴 / 3 ) ) = 𝐴 )
13	2 4 12	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 3 · ( 𝐴 / 3 ) ) = 𝐴 )
14	11 13	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( 1 · ( 𝐴 / 3 ) ) + ( 3 · ( 𝐴 / 3 ) ) ) = ( ( 𝐴 / 3 ) + 𝐴 ) )
15	7 10 14	3eqtr3rd	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 3 ) + 𝐴 ) = ( 4 · ( 𝐴 / 3 ) ) )