Theorem bj-inftyexpitaudisj

Description: An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023)

	Ref	Expression
Assertion	bj-inftyexpitaudisj	⊢ ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑥 = 𝐴 → ( {R ‘ ( 1st ‘ 𝑥 ) ) = ( {R ‘ ( 1st ‘ 𝐴 ) ) )
2	1	opeq1d	⊢ ( 𝑥 = 𝐴 → ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ )
3		df-bj-inftyexpitau	⊢ +∞eiτ = ( 𝑥 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st ‘ 𝑥 ) ) , { R } ⟩ )
4		opex	⊢ ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ V
5	2 3 4	fvmpt	⊢ ( 𝐴 ∈ ℝ → ( +∞eiτ ‘ 𝐴 ) = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ )
6		opex	⊢ ⟨ ( {R ‘ ( 1st ‘ 𝑦 ) ) , { R } ⟩ ∈ V
7		df-bj-inftyexpitau	⊢ +∞eiτ = ( 𝑦 ∈ ℝ ↦ ⟨ ( {R ‘ ( 1st ‘ 𝑦 ) ) , { R } ⟩ )
8	6 7	dmmpti	⊢ dom +∞eiτ = ℝ
9	5 8	eleq2s	⊢ ( 𝐴 ∈ dom +∞eiτ → ( +∞eiτ ‘ 𝐴 ) = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ )
10		nrex1	⊢ R ∈ V
11		bj-nsnid	⊢ ( R ∈ V → ¬ { R } ∈ R )
12	10 11	ax-mp	⊢ ¬ { R } ∈ R
13	12	intnan	⊢ ¬ ( ( {R ‘ ( 1st ‘ 𝐴 ) ) ∈ R ∧ { R } ∈ R )
14		opelxp	⊢ ( ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ ( R × R ) ↔ ( ( {R ‘ ( 1st ‘ 𝐴 ) ) ∈ R ∧ { R } ∈ R ) )
15	13 14	mtbir	⊢ ¬ ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ ( R × R )
16		df-c	⊢ ℂ = ( R × R )
17	16	eleq2i	⊢ ( ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ ℂ ↔ ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ ( R × R ) )
18	15 17	mtbir	⊢ ¬ ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ ℂ
19		eqcom	⊢ ( ( +∞eiτ ‘ 𝐴 ) = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ↔ ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ = ( +∞eiτ ‘ 𝐴 ) )
20	19	biimpi	⊢ ( ( +∞eiτ ‘ 𝐴 ) = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ → ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ = ( +∞eiτ ‘ 𝐴 ) )
21	20	eleq1d	⊢ ( ( +∞eiτ ‘ 𝐴 ) = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ → ( ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ ∈ ℂ ↔ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ) )
22	18 21	mtbii	⊢ ( ( +∞eiτ ‘ 𝐴 ) = ⟨ ( {R ‘ ( 1st ‘ 𝐴 ) ) , { R } ⟩ → ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ )
23	9 22	syl	⊢ ( 𝐴 ∈ dom +∞eiτ → ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ )
24		0ncn	⊢ ¬ ∅ ∈ ℂ
25		ndmfv	⊢ ( ¬ 𝐴 ∈ dom +∞eiτ → ( +∞eiτ ‘ 𝐴 ) = ∅ )
26	25	eleq1d	⊢ ( ¬ 𝐴 ∈ dom +∞eiτ → ( ( +∞eiτ ‘ 𝐴 ) ∈ ℂ ↔ ∅ ∈ ℂ ) )
27	24 26	mtbiri	⊢ ( ¬ 𝐴 ∈ dom +∞eiτ → ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ )
28	23 27	pm2.61i	⊢ ¬ ( +∞eiτ ‘ 𝐴 ) ∈ ℂ