Database
BASIC REAL AND COMPLEX FUNCTIONS
Polynomials
Algebraic numbers
1aa
Next ⟩
iaa
Metamath Proof Explorer
Ascii
Unicode
Theorem
1aa
Description:
One is algebraic.
(Contributed by
Ender Ting
, 21-Jul-2026)
Ref
Expression
Assertion
1aa
⊢
1
∈
𝔸
Proof
Step
Hyp
Ref
Expression
1
qssaa
⊢
ℚ
⊆
𝔸
2
zssq
⊢
ℤ
⊆
ℚ
3
1z
⊢
1
∈
ℤ
4
2
3
sselii
⊢
1
∈
ℚ
5
1
4
sselii
⊢
1
∈
𝔸