Metamath Proof Explorer


Theorem constr0

Description: The first step of the construction of constructible numbers is the pair { 0 , 1 } . In this theorem and the following, we use ( CN ) for the N -th intermediate iteration of the constructible number. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypothesis constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
Assertion constr0 C = 0 1

Proof

Step Hyp Ref Expression
1 constr0.1 C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
2 1 fveq1i C = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
3 prex 0 1 V
4 3 rdg0 rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1 = 0 1
5 2 4 eqtri C = 0 1