elqaa

Description: The set of numbers generated by the roots of polynomials in the rational numbers is the same as the set of algebraic numbers, which by elaa are defined only in terms of polynomials over the integers. (Contributed by Mario Carneiro, 23-Jul-2014) (Proof shortened by AV, 3-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elaa	⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
2		zssq	⊢ ℤ ⊆ ℚ
3		qsscn	⊢ ℚ ⊆ ℂ
4		plyss	⊢ ( ( ℤ ⊆ ℚ ∧ ℚ ⊆ ℂ ) → ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℚ ) )
5	2 3 4	mp2an	⊢ ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℚ )
6		ssdif	⊢ ( ( Poly ‘ ℤ ) ⊆ ( Poly ‘ ℚ ) → ( ( Poly ‘ ℤ ) ∖ { 0_𝑝 } ) ⊆ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) )
7		ssrexv	⊢ ( ( ( Poly ‘ ℤ ) ∖ { 0_𝑝 } ) ⊆ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) → ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
8	5 6 7	mp2b	⊢ ( ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 → ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 )
9	8	anim2i	⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℤ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) → ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
10	1 9	sylbi	⊢ ( 𝐴 ∈ 𝔸 → ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )
11		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℂ )
12		simplr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) )
13		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → ( 𝑓 ‘ 𝐴 ) = 0 )
14		eqid	⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 )
15		fveq2	⊢ ( 𝑚 = 𝑘 → ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) = ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) )
16	15	oveq1d	⊢ ( 𝑚 = 𝑘 → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) = ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑗 ) )
17	16	eleq1d	⊢ ( 𝑚 = 𝑘 → ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ ↔ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑗 ) ∈ ℤ ) )
18	17	rabbidv	⊢ ( 𝑚 = 𝑘 → { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ } = { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑗 ) ∈ ℤ } )
19		oveq2	⊢ ( 𝑗 = 𝑛 → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑗 ) = ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑛 ) )
20	19	eleq1d	⊢ ( 𝑗 = 𝑛 → ( ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑗 ) ∈ ℤ ↔ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑛 ) ∈ ℤ ) )
21	20	cbvrabv	⊢ { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑗 ) ∈ ℤ } = { 𝑛 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑛 ) ∈ ℤ }
22	18 21	eqtrdi	⊢ ( 𝑚 = 𝑘 → { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ } = { 𝑛 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } )
23	22	infeq1d	⊢ ( 𝑚 = 𝑘 → inf ( { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
24	23	cbvmptv	⊢ ( 𝑚 ∈ ℕ₀ ↦ inf ( { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ } , ℝ , < ) ) = ( 𝑘 ∈ ℕ₀ ↦ inf ( { 𝑛 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · 𝑛 ) ∈ ℤ } , ℝ , < ) )
25		eqid	⊢ ( seq 0 ( · , ( 𝑚 ∈ ℕ₀ ↦ inf ( { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ } , ℝ , < ) ) ) ‘ ( deg ‘ 𝑓 ) ) = ( seq 0 ( · , ( 𝑚 ∈ ℕ₀ ↦ inf ( { 𝑗 ∈ ℕ ∣ ( ( ( coeff ‘ 𝑓 ) ‘ 𝑚 ) · 𝑗 ) ∈ ℤ } , ℝ , < ) ) ) ‘ ( deg ‘ 𝑓 ) )
26	11 12 13 14 24 25	elqaalem3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ) ∧ ( 𝑓 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ 𝔸 )
27	26	r19.29an	⊢ ( ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ 𝔸 )
28	10 27	impbii	⊢ ( 𝐴 ∈ 𝔸 ↔ ( 𝐴 ∈ ℂ ∧ ∃ 𝑓 ∈ ( ( Poly ‘ ℚ ) ∖ { 0_𝑝 } ) ( 𝑓 ‘ 𝐴 ) = 0 ) )

Metamath Proof Explorer

Theorem elqaa

Proof