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

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 \neq 0$
5		divcl	$⊢ (A \in ℂ \land 3 \in ℂ \land 3 \neq 0) \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 (1 + 3) (\frac{A}{3}) = 1 (\frac{A}{3}) + 3 (\frac{A}{3})$
8		1p3e4	$⊢ 1 + 3 = 4$
9	8	a1i	$⊢ A \in ℂ \to 1 + 3 = 4$
10	9	oveq1d	$⊢ A \in ℂ \to (1 + 3) (\frac{A}{3}) = 4 (\frac{A}{3})$
11	6	mullidd	$⊢ A \in ℂ \to 1 (\frac{A}{3}) = \frac{A}{3}$
12		divcan2	$⊢ (A \in ℂ \land 3 \in ℂ \land 3 \neq 0) \to 3 (\frac{A}{3}) = A$
13	2 4 12	mp3an23	$⊢ A \in ℂ \to 3 (\frac{A}{3}) = A$
14	11 13	oveq12d	$⊢ A \in ℂ \to 1 (\frac{A}{3}) + 3 (\frac{A}{3}) = (\frac{A}{3}) + A$
15	7 10 14	3eqtr3rd	$⊢ A \in ℂ \to (\frac{A}{3}) + A = 4 (\frac{A}{3})$

Metamath Proof Explorer