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\in ℂ\to \left(\frac{A}{3}\right)+A=4\left(\frac{A}{3}\right)$$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
2		3cn	$$⊢3\in ℂ$$
3	2	a1i	$$⊢A\in ℂ\to 3\in ℂ$$
4		3ne0	$$⊢3\ne 0$$
5		divcl	$$⊢\left(A\in ℂ\wedge 3\in ℂ\wedge 3\ne 0\right)\to \frac{A}{3}\in ℂ$$
6	2 4 5	mp3an23	$$⊢A\in ℂ\to \frac{A}{3}\in ℂ$$
7	1 3 6	adddird	$$⊢A\in ℂ\to \left(1+3\right)\left(\frac{A}{3}\right)=1\left(\frac{A}{3}\right)+3\left(\frac{A}{3}\right)$$
8		1p3e4	$$⊢1+3=4$$
9	8	a1i	$$⊢A\in ℂ\to 1+3=4$$
10	9	oveq1d	$$⊢A\in ℂ\to \left(1+3\right)\left(\frac{A}{3}\right)=4\left(\frac{A}{3}\right)$$
11	6	mullidd	$$⊢A\in ℂ\to 1\left(\frac{A}{3}\right)=\frac{A}{3}$$
12		divcan2	$$⊢\left(A\in ℂ\wedge 3\in ℂ\wedge 3\ne 0\right)\to 3\left(\frac{A}{3}\right)=A$$
13	2 4 12	mp3an23	$$⊢A\in ℂ\to 3\left(\frac{A}{3}\right)=A$$
14	11 13	oveq12d	$$⊢A\in ℂ\to 1\left(\frac{A}{3}\right)+3\left(\frac{A}{3}\right)=\left(\frac{A}{3}\right)+A$$
15	7 10 14	3eqtr3rd	$$⊢A\in ℂ\to \left(\frac{A}{3}\right)+A=4\left(\frac{A}{3}\right)$$