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 ( 𝐴 ∈ ℂ → ( ( 𝐴 / 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 ) ) )