Metamath Proof Explorer

Theorem aaitgo

Description: The standard algebraic numbers AA are generated by IntgOver . (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion aaitgo ⊢𝔸=IntgOver⁡ℚ

Proof

Step Hyp Ref Expression
1 rabid ⊢a∈a∈ℂ|∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1↔a∈ℂ∧∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
2 qsscn ⊢ℚ⊆ℂ
3 itgoval ⊢ℚ⊆ℂ→IntgOver⁡ℚ=a∈ℂ|∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
4 2 3 ax-mp ⊢IntgOver⁡ℚ=a∈ℂ|∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
5 4 eleq2i ⊢a∈IntgOver⁡ℚ↔a∈a∈ℂ|∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
6 aacn ⊢a∈𝔸→a∈ℂ
7 mpaacl ⊢a∈𝔸→minPoly𝔸⁡a∈Poly⁡ℚ
8 mpaaroot ⊢a∈𝔸→minPoly𝔸⁡a⁡a=0
9 mpaadgr ⊢a∈𝔸→deg⁡minPoly𝔸⁡a=deg𝔸⁡a
10 9 fveq2d ⊢a∈𝔸→coeff⁡minPoly𝔸⁡a⁡deg⁡minPoly𝔸⁡a=coeff⁡minPoly𝔸⁡a⁡deg𝔸⁡a
11 mpaamn ⊢a∈𝔸→coeff⁡minPoly𝔸⁡a⁡deg𝔸⁡a=1
12 10 11 eqtrd ⊢a∈𝔸→coeff⁡minPoly𝔸⁡a⁡deg⁡minPoly𝔸⁡a=1
13 fveq1 ⊢b=minPoly𝔸⁡a→b⁡a=minPoly𝔸⁡a⁡a
14 13 eqeq1d ⊢b=minPoly𝔸⁡a→b⁡a=0↔minPoly𝔸⁡a⁡a=0
15 fveq2 ⊢b=minPoly𝔸⁡a→coeff⁡b=coeff⁡minPoly𝔸⁡a
16 fveq2 ⊢b=minPoly𝔸⁡a→deg⁡b=deg⁡minPoly𝔸⁡a
17 15 16 fveq12d ⊢b=minPoly𝔸⁡a→coeff⁡b⁡deg⁡b=coeff⁡minPoly𝔸⁡a⁡deg⁡minPoly𝔸⁡a
18 17 eqeq1d ⊢b=minPoly𝔸⁡a→coeff⁡b⁡deg⁡b=1↔coeff⁡minPoly𝔸⁡a⁡deg⁡minPoly𝔸⁡a=1
19 14 18 anbi12d ⊢b=minPoly𝔸⁡a→b⁡a=0∧coeff⁡b⁡deg⁡b=1↔minPoly𝔸⁡a⁡a=0∧coeff⁡minPoly𝔸⁡a⁡deg⁡minPoly𝔸⁡a=1
20 19 rspcev ⊢minPoly𝔸⁡a∈Poly⁡ℚ∧minPoly𝔸⁡a⁡a=0∧coeff⁡minPoly𝔸⁡a⁡deg⁡minPoly𝔸⁡a=1→∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
21 7 8 12 20 syl12anc ⊢a∈𝔸→∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
22 6 21 jca ⊢a∈𝔸→a∈ℂ∧∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
23 simpl ⊢b∈Poly⁡ℚ∧b⁡a=0∧coeff⁡b⁡deg⁡b=1→b∈Poly⁡ℚ
24 coe0 ⊢coeff⁡0𝑝=ℕ0×0
25 24 fveq1i ⊢coeff⁡0𝑝⁡deg⁡0𝑝=ℕ0×0⁡deg⁡0𝑝
26 dgr0 ⊢deg⁡0𝑝=0
27 0nn0 ⊢0∈ℕ0
28 26 27 eqeltri ⊢deg⁡0𝑝∈ℕ0
29 c0ex ⊢0∈V
30 29 fvconst2 ⊢deg⁡0𝑝∈ℕ0→ℕ0×0⁡deg⁡0𝑝=0
31 28 30 ax-mp ⊢ℕ0×0⁡deg⁡0𝑝=0
32 25 31 eqtri ⊢coeff⁡0𝑝⁡deg⁡0𝑝=0
33 0ne1 ⊢0≠1
34 32 33 eqnetri ⊢coeff⁡0𝑝⁡deg⁡0𝑝≠1
35 fveq2 ⊢b=0𝑝→coeff⁡b=coeff⁡0𝑝
36 fveq2 ⊢b=0𝑝→deg⁡b=deg⁡0𝑝
37 35 36 fveq12d ⊢b=0𝑝→coeff⁡b⁡deg⁡b=coeff⁡0𝑝⁡deg⁡0𝑝
38 37 neeq1d ⊢b=0𝑝→coeff⁡b⁡deg⁡b≠1↔coeff⁡0𝑝⁡deg⁡0𝑝≠1
39 34 38 mpbiri ⊢b=0𝑝→coeff⁡b⁡deg⁡b≠1
40 39 necon2i ⊢coeff⁡b⁡deg⁡b=1→b≠0𝑝
41 40 ad2antll ⊢b∈Poly⁡ℚ∧b⁡a=0∧coeff⁡b⁡deg⁡b=1→b≠0𝑝
42 eldifsn ⊢b∈Poly⁡ℚ∖0𝑝↔b∈Poly⁡ℚ∧b≠0𝑝
43 23 41 42 sylanbrc ⊢b∈Poly⁡ℚ∧b⁡a=0∧coeff⁡b⁡deg⁡b=1→b∈Poly⁡ℚ∖0𝑝
44 simprl ⊢b∈Poly⁡ℚ∧b⁡a=0∧coeff⁡b⁡deg⁡b=1→b⁡a=0
45 43 44 jca ⊢b∈Poly⁡ℚ∧b⁡a=0∧coeff⁡b⁡deg⁡b=1→b∈Poly⁡ℚ∖0𝑝∧b⁡a=0
46 45 reximi2 ⊢∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1→∃b∈Poly⁡ℚ∖0𝑝b⁡a=0
47 46 anim2i ⊢a∈ℂ∧∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1→a∈ℂ∧∃b∈Poly⁡ℚ∖0𝑝b⁡a=0
48 elqaa ⊢a∈𝔸↔a∈ℂ∧∃b∈Poly⁡ℚ∖0𝑝b⁡a=0
49 47 48 sylibr ⊢a∈ℂ∧∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1→a∈𝔸
50 22 49 impbii ⊢a∈𝔸↔a∈ℂ∧∃b∈Poly⁡ℚb⁡a=0∧coeff⁡b⁡deg⁡b=1
51 1 5 50 3bitr4ri ⊢a∈𝔸↔a∈IntgOver⁡ℚ
52 51 eqriv ⊢𝔸=IntgOver⁡ℚ