![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elqaa | Structured version Visualization version GIF version |
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 25760 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 |
---|---|
elqaa | ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elaa 25760 | . . 3 ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) | |
2 | zssq 12924 | . . . . . 6 ⊢ ℤ ⊆ ℚ | |
3 | qsscn 12928 | . . . . . 6 ⊢ ℚ ⊆ ℂ | |
4 | plyss 25644 | . . . . . 6 ⊢ ((ℤ ⊆ ℚ ∧ ℚ ⊆ ℂ) → (Poly‘ℤ) ⊆ (Poly‘ℚ)) | |
5 | 2, 3, 4 | mp2an 690 | . . . . 5 ⊢ (Poly‘ℤ) ⊆ (Poly‘ℚ) |
6 | ssdif 4136 | . . . . 5 ⊢ ((Poly‘ℤ) ⊆ (Poly‘ℚ) → ((Poly‘ℤ) ∖ {0𝑝}) ⊆ ((Poly‘ℚ) ∖ {0𝑝})) | |
7 | ssrexv 4048 | . . . . 5 ⊢ (((Poly‘ℤ) ∖ {0𝑝}) ⊆ ((Poly‘ℚ) ∖ {0𝑝}) → (∃𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0 → ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) | |
8 | 5, 6, 7 | mp2b 10 | . . . 4 ⊢ (∃𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0 → ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0) |
9 | 8 | anim2i 617 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℤ) ∖ {0𝑝})(𝑓‘𝐴) = 0) → (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
10 | 1, 9 | sylbi 216 | . 2 ⊢ (𝐴 ∈ 𝔸 → (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
11 | simpll 765 | . . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})) ∧ (𝑓‘𝐴) = 0) → 𝐴 ∈ ℂ) | |
12 | simplr 767 | . . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})) ∧ (𝑓‘𝐴) = 0) → 𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})) | |
13 | simpr 485 | . . . 4 ⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})) ∧ (𝑓‘𝐴) = 0) → (𝑓‘𝐴) = 0) | |
14 | eqid 2732 | . . . 4 ⊢ (coeff‘𝑓) = (coeff‘𝑓) | |
15 | fveq2 6879 | . . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → ((coeff‘𝑓)‘𝑚) = ((coeff‘𝑓)‘𝑘)) | |
16 | 15 | oveq1d 7409 | . . . . . . . . 9 ⊢ (𝑚 = 𝑘 → (((coeff‘𝑓)‘𝑚) · 𝑗) = (((coeff‘𝑓)‘𝑘) · 𝑗)) |
17 | 16 | eleq1d 2818 | . . . . . . . 8 ⊢ (𝑚 = 𝑘 → ((((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ ↔ (((coeff‘𝑓)‘𝑘) · 𝑗) ∈ ℤ)) |
18 | 17 | rabbidv 3440 | . . . . . . 7 ⊢ (𝑚 = 𝑘 → {𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ} = {𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑘) · 𝑗) ∈ ℤ}) |
19 | oveq2 7402 | . . . . . . . . 9 ⊢ (𝑗 = 𝑛 → (((coeff‘𝑓)‘𝑘) · 𝑗) = (((coeff‘𝑓)‘𝑘) · 𝑛)) | |
20 | 19 | eleq1d 2818 | . . . . . . . 8 ⊢ (𝑗 = 𝑛 → ((((coeff‘𝑓)‘𝑘) · 𝑗) ∈ ℤ ↔ (((coeff‘𝑓)‘𝑘) · 𝑛) ∈ ℤ)) |
21 | 20 | cbvrabv 3442 | . . . . . . 7 ⊢ {𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑘) · 𝑗) ∈ ℤ} = {𝑛 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑘) · 𝑛) ∈ ℤ} |
22 | 18, 21 | eqtrdi 2788 | . . . . . 6 ⊢ (𝑚 = 𝑘 → {𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ} = {𝑛 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑘) · 𝑛) ∈ ℤ}) |
23 | 22 | infeq1d 9456 | . . . . 5 ⊢ (𝑚 = 𝑘 → inf({𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) |
24 | 23 | cbvmptv 5255 | . . . 4 ⊢ (𝑚 ∈ ℕ0 ↦ inf({𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ}, ℝ, < )) = (𝑘 ∈ ℕ0 ↦ inf({𝑛 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑘) · 𝑛) ∈ ℤ}, ℝ, < )) |
25 | eqid 2732 | . . . 4 ⊢ (seq0( · , (𝑚 ∈ ℕ0 ↦ inf({𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ}, ℝ, < )))‘(deg‘𝑓)) = (seq0( · , (𝑚 ∈ ℕ0 ↦ inf({𝑗 ∈ ℕ ∣ (((coeff‘𝑓)‘𝑚) · 𝑗) ∈ ℤ}, ℝ, < )))‘(deg‘𝑓)) | |
26 | 11, 12, 13, 14, 24, 25 | elqaalem3 25765 | . . 3 ⊢ (((𝐴 ∈ ℂ ∧ 𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})) ∧ (𝑓‘𝐴) = 0) → 𝐴 ∈ 𝔸) |
27 | 26 | r19.29an 3158 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0) → 𝐴 ∈ 𝔸) |
28 | 10, 27 | impbii 208 | 1 ⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧ ∃𝑓 ∈ ((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃wrex 3070 {crab 3432 ∖ cdif 3942 ⊆ wss 3945 {csn 4623 ↦ cmpt 5225 ‘cfv 6533 (class class class)co 7394 infcinf 9420 ℂcc 11092 ℝcr 11093 0cc0 11094 · cmul 11099 < clt 11232 ℕcn 12196 ℕ0cn0 12456 ℤcz 12542 ℚcq 12916 seqcseq 13950 0𝑝c0p 25117 Polycply 25629 coeffccoe 25631 degcdgr 25632 𝔸caa 25758 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5357 ax-pr 5421 ax-un 7709 ax-inf2 9620 ax-cnex 11150 ax-resscn 11151 ax-1cn 11152 ax-icn 11153 ax-addcl 11154 ax-addrcl 11155 ax-mulcl 11156 ax-mulrcl 11157 ax-mulcom 11158 ax-addass 11159 ax-mulass 11160 ax-distr 11161 ax-i2m1 11162 ax-1ne0 11163 ax-1rid 11164 ax-rnegex 11165 ax-rrecex 11166 ax-cnre 11167 ax-pre-lttri 11168 ax-pre-lttrn 11169 ax-pre-ltadd 11170 ax-pre-mulgt0 11171 ax-pre-sup 11172 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5568 df-eprel 5574 df-po 5582 df-so 5583 df-fr 5625 df-se 5626 df-we 5627 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7350 df-ov 7397 df-oprab 7398 df-mpo 7399 df-of 7654 df-om 7840 df-1st 7959 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8355 df-rdg 8394 df-1o 8450 df-er 8688 df-map 8807 df-pm 8808 df-en 8925 df-dom 8926 df-sdom 8927 df-fin 8928 df-sup 9421 df-inf 9422 df-oi 9489 df-card 9918 df-pnf 11234 df-mnf 11235 df-xr 11236 df-ltxr 11237 df-le 11238 df-sub 11430 df-neg 11431 df-div 11856 df-nn 12197 df-2 12259 df-3 12260 df-n0 12457 df-z 12543 df-uz 12807 df-q 12917 df-rp 12959 df-fz 13469 df-fzo 13612 df-fl 13741 df-mod 13819 df-seq 13951 df-exp 14012 df-hash 14275 df-cj 15030 df-re 15031 df-im 15032 df-sqrt 15166 df-abs 15167 df-clim 15416 df-rlim 15417 df-sum 15617 df-0p 25118 df-ply 25633 df-coe 25635 df-dgr 25636 df-aa 25759 |
This theorem is referenced by: qaa 25767 dgraalem 41722 dgraaub 41725 aaitgo 41739 aacllem 47560 |
Copyright terms: Public domain | W3C validator |