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 ⁡ ℚ