Theorem elaa

Description: Elementhood in the set of algebraic numbers. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	elaa	⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		df-aa	⊢ 𝔸 = ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } )
2	1	eleq2i	⊢ ( 𝐴 ∈ 𝔸 ↔ 𝐴 ∈ ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } ) )
3		eliun	⊢ ( 𝐴 ∈ ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } ) ↔ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) 𝐴 ∈ ( ◡ 𝑓 “ { 0 } ) )
4		eldifi	⊢ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → 𝑓 ∈ ( Poly ‘ ℤ ) )
5		plyf	⊢ ( 𝑓 ∈ ( Poly ‘ ℤ ) → 𝑓 : ℂ ⟶ ℂ )
6		ffn	⊢ ( 𝑓 : ℂ ⟶ ℂ → 𝑓 Fn ℂ )
7		fniniseg	⊢ ( 𝑓 Fn ℂ → ( 𝐴 ∈ ( ◡ 𝑓 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) )
8	4 5 6 7	4syl	⊢ ( 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) → ( 𝐴 ∈ ( ◡ 𝑓 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ) )
9	8	rexbiia	⊢ ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) 𝐴 ∈ ( ◡ 𝑓 “ { 0 } ) ↔ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝐴 ∈ ℂ ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) )
10		r19.42v	⊢ ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝐴 ∈ ℂ ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
11	9 10	bitri	⊢ ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) 𝐴 ∈ ( ◡ 𝑓 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
12	3 11	bitri	⊢ ( 𝐴 ∈ ∪ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( ◡ 𝑓 “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
13	2 12	bitri	⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )