Step | Hyp | Ref
| Expression |
1 | | qcn 12438 |
. 2
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
ℂ) |
2 | | qsscn 12435 |
. . . . . . 7
⊢ ℚ
⊆ ℂ |
3 | | 1z 12086 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
4 | | zq 12429 |
. . . . . . . 8
⊢ (1 ∈
ℤ → 1 ∈ ℚ) |
5 | 3, 4 | ax-mp 5 |
. . . . . . 7
⊢ 1 ∈
ℚ |
6 | | plyid 24950 |
. . . . . . 7
⊢ ((ℚ
⊆ ℂ ∧ 1 ∈ ℚ) → Xp ∈
(Poly‘ℚ)) |
7 | 2, 5, 6 | mp2an 692 |
. . . . . 6
⊢
Xp ∈ (Poly‘ℚ) |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
Xp ∈ (Poly‘ℚ)) |
9 | | plyconst 24947 |
. . . . . 6
⊢ ((ℚ
⊆ ℂ ∧ 𝐴
∈ ℚ) → (ℂ × {𝐴}) ∈
(Poly‘ℚ)) |
10 | 2, 9 | mpan 690 |
. . . . 5
⊢ (𝐴 ∈ ℚ → (ℂ
× {𝐴}) ∈
(Poly‘ℚ)) |
11 | | qaddcl 12440 |
. . . . . 6
⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 + 𝑦) ∈ ℚ) |
12 | 11 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 + 𝑦) ∈ ℚ) |
13 | | qmulcl 12442 |
. . . . . 6
⊢ ((𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ) → (𝑥 · 𝑦) ∈ ℚ) |
14 | 13 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ (𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ)) → (𝑥 · 𝑦) ∈ ℚ) |
15 | | qnegcl 12441 |
. . . . . . 7
⊢ (1 ∈
ℚ → -1 ∈ ℚ) |
16 | 5, 15 | ax-mp 5 |
. . . . . 6
⊢ -1 ∈
ℚ |
17 | 16 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℚ → -1 ∈
ℚ) |
18 | 8, 10, 12, 14, 17 | plysub 24960 |
. . . 4
⊢ (𝐴 ∈ ℚ →
(Xp ∘f − (ℂ × {𝐴})) ∈
(Poly‘ℚ)) |
19 | | peano2cn 10883 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈
ℂ) |
20 | 1, 19 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℚ → (𝐴 + 1) ∈
ℂ) |
21 | | fnresi 6459 |
. . . . . . . . . . 11
⊢ ( I
↾ ℂ) Fn ℂ |
22 | | df-idp 24930 |
. . . . . . . . . . . 12
⊢
Xp = ( I ↾ ℂ) |
23 | 22 | fneq1i 6429 |
. . . . . . . . . . 11
⊢
(Xp Fn ℂ ↔ ( I ↾ ℂ) Fn
ℂ) |
24 | 21, 23 | mpbir 234 |
. . . . . . . . . 10
⊢
Xp Fn ℂ |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ →
Xp Fn ℂ) |
26 | | fnconstg 6560 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ → (ℂ
× {𝐴}) Fn
ℂ) |
27 | | cnex 10689 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℚ → ℂ
∈ V) |
29 | | inidm 4107 |
. . . . . . . . 9
⊢ (ℂ
∩ ℂ) = ℂ |
30 | 22 | fveq1i 6669 |
. . . . . . . . . . 11
⊢
(Xp‘(𝐴 + 1)) = (( I ↾ ℂ)‘(𝐴 + 1)) |
31 | | fvresi 6939 |
. . . . . . . . . . 11
⊢ ((𝐴 + 1) ∈ ℂ → (( I
↾ ℂ)‘(𝐴 +
1)) = (𝐴 +
1)) |
32 | 30, 31 | syl5eq 2785 |
. . . . . . . . . 10
⊢ ((𝐴 + 1) ∈ ℂ →
(Xp‘(𝐴 + 1)) = (𝐴 + 1)) |
33 | 32 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℚ ∧ (𝐴 + 1) ∈ ℂ) →
(Xp‘(𝐴 + 1)) = (𝐴 + 1)) |
34 | | fvconst2g 6968 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℚ ∧ (𝐴 + 1) ∈ ℂ) →
((ℂ × {𝐴})‘(𝐴 + 1)) = 𝐴) |
35 | 25, 26, 28, 28, 29, 33, 34 | ofval 7429 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℚ ∧ (𝐴 + 1) ∈ ℂ) →
((Xp ∘f − (ℂ × {𝐴}))‘(𝐴 + 1)) = ((𝐴 + 1) − 𝐴)) |
36 | 20, 35 | mpdan 687 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ →
((Xp ∘f − (ℂ × {𝐴}))‘(𝐴 + 1)) = ((𝐴 + 1) − 𝐴)) |
37 | | ax-1cn 10666 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
38 | | pncan2 10964 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐴 + 1)
− 𝐴) =
1) |
39 | 1, 37, 38 | sylancl 589 |
. . . . . . 7
⊢ (𝐴 ∈ ℚ → ((𝐴 + 1) − 𝐴) = 1) |
40 | 36, 39 | eqtrd 2773 |
. . . . . 6
⊢ (𝐴 ∈ ℚ →
((Xp ∘f − (ℂ × {𝐴}))‘(𝐴 + 1)) = 1) |
41 | | ax-1ne0 10677 |
. . . . . . 7
⊢ 1 ≠
0 |
42 | 41 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℚ → 1 ≠
0) |
43 | 40, 42 | eqnetrd 3001 |
. . . . 5
⊢ (𝐴 ∈ ℚ →
((Xp ∘f − (ℂ × {𝐴}))‘(𝐴 + 1)) ≠ 0) |
44 | | ne0p 24948 |
. . . . 5
⊢ (((𝐴 + 1) ∈ ℂ ∧
((Xp ∘f − (ℂ × {𝐴}))‘(𝐴 + 1)) ≠ 0) → (Xp
∘f − (ℂ × {𝐴})) ≠
0𝑝) |
45 | 20, 43, 44 | syl2anc 587 |
. . . 4
⊢ (𝐴 ∈ ℚ →
(Xp ∘f − (ℂ × {𝐴})) ≠
0𝑝) |
46 | | eldifsn 4672 |
. . . 4
⊢
((Xp ∘f − (ℂ ×
{𝐴})) ∈
((Poly‘ℚ) ∖ {0𝑝}) ↔
((Xp ∘f − (ℂ × {𝐴})) ∈ (Poly‘ℚ)
∧ (Xp ∘f − (ℂ × {𝐴})) ≠
0𝑝)) |
47 | 18, 45, 46 | sylanbrc 586 |
. . 3
⊢ (𝐴 ∈ ℚ →
(Xp ∘f − (ℂ × {𝐴})) ∈ ((Poly‘ℚ)
∖ {0𝑝})) |
48 | 22 | fveq1i 6669 |
. . . . . . . 8
⊢
(Xp‘𝐴) = (( I ↾ ℂ)‘𝐴) |
49 | | fvresi 6939 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (( I
↾ ℂ)‘𝐴) =
𝐴) |
50 | 48, 49 | syl5eq 2785 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(Xp‘𝐴) = 𝐴) |
51 | 50 | adantl 485 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ) →
(Xp‘𝐴) = 𝐴) |
52 | | fvconst2g 6968 |
. . . . . 6
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ) →
((ℂ × {𝐴})‘𝐴) = 𝐴) |
53 | 25, 26, 28, 28, 29, 51, 52 | ofval 7429 |
. . . . 5
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ∈ ℂ) →
((Xp ∘f − (ℂ × {𝐴}))‘𝐴) = (𝐴 − 𝐴)) |
54 | 1, 53 | mpdan 687 |
. . . 4
⊢ (𝐴 ∈ ℚ →
((Xp ∘f − (ℂ × {𝐴}))‘𝐴) = (𝐴 − 𝐴)) |
55 | 1 | subidd 11056 |
. . . 4
⊢ (𝐴 ∈ ℚ → (𝐴 − 𝐴) = 0) |
56 | 54, 55 | eqtrd 2773 |
. . 3
⊢ (𝐴 ∈ ℚ →
((Xp ∘f − (ℂ × {𝐴}))‘𝐴) = 0) |
57 | | fveq1 6667 |
. . . . 5
⊢ (𝑓 = (Xp
∘f − (ℂ × {𝐴})) → (𝑓‘𝐴) = ((Xp
∘f − (ℂ × {𝐴}))‘𝐴)) |
58 | 57 | eqeq1d 2740 |
. . . 4
⊢ (𝑓 = (Xp
∘f − (ℂ × {𝐴})) → ((𝑓‘𝐴) = 0 ↔ ((Xp
∘f − (ℂ × {𝐴}))‘𝐴) = 0)) |
59 | 58 | rspcev 3524 |
. . 3
⊢
(((Xp ∘f − (ℂ ×
{𝐴})) ∈
((Poly‘ℚ) ∖ {0𝑝}) ∧
((Xp ∘f − (ℂ × {𝐴}))‘𝐴) = 0) → ∃𝑓 ∈ ((Poly‘ℚ) ∖
{0𝑝})(𝑓‘𝐴) = 0) |
60 | 47, 56, 59 | syl2anc 587 |
. 2
⊢ (𝐴 ∈ ℚ →
∃𝑓 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0) |
61 | | elqaa 25062 |
. 2
⊢ (𝐴 ∈ 𝔸 ↔ (𝐴 ∈ ℂ ∧
∃𝑓 ∈
((Poly‘ℚ) ∖ {0𝑝})(𝑓‘𝐴) = 0)) |
62 | 1, 60, 61 | sylanbrc 586 |
1
⊢ (𝐴 ∈ ℚ → 𝐴 ∈
𝔸) |