Theorem rr3fv3cld

Description: Third component of a 3-dimensional real coordinate vector is real. (Contributed by Jiamin Zhao, 10-Aug-2026)

	Ref	Expression
Hypothesis	rr3fvd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
Assertion	rr3fv3cld	⊢ ( 𝜑 → ( 𝐴 ‘ 3 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rr3fvd.1	⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) )
2		rr3fvcl	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 3 ) ) → ( ( 𝐴 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) )
3	1 2	syl	⊢ ( 𝜑 → ( ( 𝐴 ‘ 1 ) ∈ ℝ ∧ ( 𝐴 ‘ 2 ) ∈ ℝ ∧ ( 𝐴 ‘ 3 ) ∈ ℝ ) )
4	3	simp3d	⊢ ( 𝜑 → ( 𝐴 ‘ 3 ) ∈ ℝ )