Metamath Proof Explorer


Theorem constrsuc

Description: Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses 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
constrsuc.1 φ N On
constrsuc.2 S = C N
Assertion constrsuc φ X C suc N 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

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 constrsuc.1 φ N On
3 constrsuc.2 S = C N
4 1 fveq1i C suc N = 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 suc N
5 rdgsuc N On 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 suc N = 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 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 N
6 2 5 syl φ 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 suc N = 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 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 N
7 4 6 eqtrid φ C suc N = 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 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 N
8 1 fveq1i C N = 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 N
9 3 8 eqtri S = 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 N
10 9 fveq2i 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 S = 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 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 N
11 7 10 eqtr4di φ C suc N = 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 S
12 11 eleq2d φ X C suc N X 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 S
13 eqid 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 = 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
14 id s = S s = S
15 rexeq s = S d s t r x = a + t b a x = c + r d c b a d c 0 d S t r x = a + t b a x = c + r d c b a d c 0
16 14 15 rexeqbidv s = S c s d s t r x = a + t b a x = c + r d c b a d c 0 c S d S t r x = a + t b a x = c + r d c b a d c 0
17 14 16 rexeqbidv s = S b s c s d s t r x = a + t b a x = c + r d c b a d c 0 b S c S d S t r x = a + t b a x = c + r d c b a d c 0
18 14 17 rexeqbidv s = S 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 d S t r x = a + t b a x = c + r d c b a d c 0
19 rexeq s = S f s t x = a + t b a x c = e f f S t x = a + t b a x c = e f
20 14 19 rexeqbidv s = S e s f s t x = a + t b a x c = e f e S f S t x = a + t b a x c = e f
21 14 20 rexeqbidv s = S c s e s f s t x = a + t b a x c = e f c S e S f S t x = a + t b a x c = e f
22 14 21 rexeqbidv s = S b s c s e s f s t x = a + t b a x c = e f b S c S e S f S t x = a + t b a x c = e f
23 14 22 rexeqbidvv s = S 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 e S f S t x = a + t b a x c = e f
24 rexeq s = S f s a d x a = b c x d = e f f S a d x a = b c x d = e f
25 14 24 rexeqbidv s = S e s f s a d x a = b c x d = e f e S f S a d x a = b c x d = e f
26 14 25 rexeqbidv s = S d s e s f s a d x a = b c x d = e f d S e S f S a d x a = b c x d = e f
27 14 26 rexeqbidv s = S c s d s e s f s a d x a = b c x d = e f c S d S e S f S a d x a = b c x d = e f
28 14 27 rexeqbidv s = S b s c s d s e s f s a d x a = b c x d = e f b S c S d S e S f S a d x a = b c x d = e f
29 14 28 rexeqbidvv s = S a s b s c s d s e s f s a d x a = b c x d = e f a S b S c S d S e S f S a d x a = b c x d = e f
30 18 23 29 3orbi123d s = S 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 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
31 30 rabbidv s = S 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 = 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
32 31 adantl φ s = S 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 = 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
33 3 fvexi S V
34 33 a1i φ S V
35 cnex V
36 ssrab2 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
37 35 36 ssexi 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 V
38 37 a1i φ 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 V
39 13 32 34 38 fvmptd2 φ 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 S = 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
40 39 eleq2d φ X 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 S X 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
41 eqeq1 x = y x = a + t b a y = a + t b a
42 eqeq1 x = y x = c + r d c y = c + r d c
43 41 42 3anbi12d x = y x = a + t b a x = c + r d c b a d c 0 y = a + t b a y = c + r d c b a d c 0
44 43 2rexbidv x = y t r x = a + t b a x = c + r d c b a d c 0 t r y = a + t b a y = c + r d c b a d c 0
45 44 2rexbidv x = y c S d S t r x = a + t b a x = c + r d c b a d c 0 c S d S t r y = a + t b a y = c + r d c b a d c 0
46 45 2rexbidv x = y 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 d S t r y = a + t b a y = c + r d c b a d c 0
47 fvoveq1 x = y x c = y c
48 47 eqeq1d x = y x c = e f y c = e f
49 41 48 anbi12d x = y x = a + t b a x c = e f y = a + t b a y c = e f
50 49 2rexbidv x = y f S t x = a + t b a x c = e f f S t y = a + t b a y c = e f
51 50 2rexbidv x = y c S e S f S t x = a + t b a x c = e f c S e S f S t y = a + t b a y c = e f
52 51 2rexbidv x = y 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 e S f S t y = a + t b a y c = e f
53 fvoveq1 x = y x a = y a
54 53 eqeq1d x = y x a = b c y a = b c
55 fvoveq1 x = y x d = y d
56 55 eqeq1d x = y x d = e f y d = e f
57 54 56 3anbi23d x = y a d x a = b c x d = e f a d y a = b c y d = e f
58 57 2rexbidv x = y e S f S a d x a = b c x d = e f e S f S a d y a = b c y d = e f
59 58 2rexbidv x = y c S d S e S f S a d x a = b c x d = e f c S d S e S f S a d y a = b c y d = e f
60 59 2rexbidv x = y a S b S c S d S e S f S a d x a = b c x d = e f a S b S c S d S e S f S a d y a = b c y d = e f
61 46 52 60 3orbi123d x = y 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 a S b S c S d S t r y = a + t b a y = c + r d c b a d c 0 a S b S c S e S f S t y = a + t b a y c = e f a S b S c S d S e S f S a d y a = b c y d = e f
62 61 cbvrabv 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 = y | a S b S c S d S t r y = a + t b a y = c + r d c b a d c 0 a S b S c S e S f S t y = a + t b a y c = e f a S b S c S d S e S f S a d y a = b c y d = e f
63 62 eleq2i X 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 X y | a S b S c S d S t r y = a + t b a y = c + r d c b a d c 0 a S b S c S e S f S t y = a + t b a y c = e f a S b S c S d S e S f S a d y a = b c y d = e f
64 eqeq1 y = X y = a + t b a X = a + t b a
65 eqeq1 y = X y = c + r d c X = c + r d c
66 64 65 3anbi12d y = X y = a + t b a y = c + r d c b a d c 0 X = a + t b a X = c + r d c b a d c 0
67 66 2rexbidv y = X t r y = a + t b a y = c + r d c b a d c 0 t r X = a + t b a X = c + r d c b a d c 0
68 67 2rexbidv y = X c S d S t r y = a + t b a y = c + r d c b a d c 0 c S d S t r X = a + t b a X = c + r d c b a d c 0
69 68 2rexbidv y = X a S b S c S d S t r y = a + t b a y = c + r d c b a d c 0 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
70 fvoveq1 y = X y c = X c
71 70 eqeq1d y = X y c = e f X c = e f
72 64 71 anbi12d y = X y = a + t b a y c = e f X = a + t b a X c = e f
73 72 2rexbidv y = X f S t y = a + t b a y c = e f f S t X = a + t b a X c = e f
74 73 2rexbidv y = X c S e S f S t y = a + t b a y c = e f c S e S f S t X = a + t b a X c = e f
75 74 2rexbidv y = X a S b S c S e S f S t y = a + t b a y c = e f a S b S c S e S f S t X = a + t b a X c = e f
76 fvoveq1 y = X y a = X a
77 76 eqeq1d y = X y a = b c X a = b c
78 fvoveq1 y = X y d = X d
79 78 eqeq1d y = X y d = e f X d = e f
80 77 79 3anbi23d y = X a d y a = b c y d = e f a d X a = b c X d = e f
81 80 2rexbidv y = X e S f S a d y a = b c y d = e f e S f S a d X a = b c X d = e f
82 81 2rexbidv y = X c S d S e S f S a d y a = b c y d = e f c S d S e S f S a d X a = b c X d = e f
83 82 2rexbidv y = X a S b S c S d S e S f S a d y a = b c y d = e f a S b S c S d S e S f S a d X a = b c X d = e f
84 69 75 83 3orbi123d y = X a S b S c S d S t r y = a + t b a y = c + r d c b a d c 0 a S b S c S e S f S t y = a + t b a y c = e f a S b S c S d S e S f S a d y a = b c y d = e f 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
85 84 elrab X y | a S b S c S d S t r y = a + t b a y = c + r d c b a d c 0 a S b S c S e S f S t y = a + t b a y c = e f a S b S c S d S e S f S a d y a = b c y d = e f 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
86 63 85 bitri X 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 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
87 86 a1i φ X 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 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
88 12 40 87 3bitrd φ X C suc N 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