Database
BASIC REAL AND COMPLEX FUNCTIONS
Polynomials
Algebraic numbers
1aa
Next ⟩
iaa
Metamath Proof Explorer
Ascii
Structured
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 ∈ 𝔸