Metamath Proof Explorer

Theorem constrsslem

Description: Lemma for constrss . This lemma requires the additional condition that 0 is the constructible number; that condition is removed in constrss . (Proposed by Saveliy Skresanov, 23-JUn-2025.) (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses constr0.1 
|- C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
constrsscn.1 
|- ( ph -> N e. On )
constrsslem.1 
|- ( ph -> 0 e. ( C ` N ) )
Assertion constrsslem 
|- ( ph -> ( C ` N ) C_ ( C ` suc N ) )

Proof

Step Hyp Ref Expression
1 constr0.1 
 |-  C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
2 constrsscn.1 
 |-  ( ph -> N e. On )
3 constrsslem.1 
 |-  ( ph -> 0 e. ( C ` N ) )
4 1 2 constrsscn 
 |-  ( ph -> ( C ` N ) C_ CC )
5 4 sselda 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> x e. CC )
6 simpr 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> x e. ( C ` N ) )
7 id 
 |-  ( a = x -> a = x )
8 oveq2 
 |-  ( a = x -> ( b - a ) = ( b - x ) )
9 8 oveq2d 
 |-  ( a = x -> ( t x. ( b - a ) ) = ( t x. ( b - x ) ) )
10 7 9 oveq12d 
 |-  ( a = x -> ( a + ( t x. ( b - a ) ) ) = ( x + ( t x. ( b - x ) ) ) )
11 10 eqeq2d 
 |-  ( a = x -> ( x = ( a + ( t x. ( b - a ) ) ) <-> x = ( x + ( t x. ( b - x ) ) ) ) )
12 11 anbi1d 
 |-  ( a = x -> ( ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
13 12 rexbidv 
 |-  ( a = x -> ( E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
14 13 2rexbidv 
 |-  ( a = x -> ( E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
15 14 2rexbidv 
 |-  ( a = x -> ( E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
16 15 adantl 
 |-  ( ( ( ph /\ x e. ( C ` N ) ) /\ a = x ) -> ( E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
17 3 adantr 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> 0 e. ( C ` N ) )
18 oveq1 
 |-  ( b = 0 -> ( b - x ) = ( 0 - x ) )
19 18 oveq2d 
 |-  ( b = 0 -> ( t x. ( b - x ) ) = ( t x. ( 0 - x ) ) )
20 19 oveq2d 
 |-  ( b = 0 -> ( x + ( t x. ( b - x ) ) ) = ( x + ( t x. ( 0 - x ) ) ) )
21 20 eqeq2d 
 |-  ( b = 0 -> ( x = ( x + ( t x. ( b - x ) ) ) <-> x = ( x + ( t x. ( 0 - x ) ) ) ) )
22 21 anbi1d 
 |-  ( b = 0 -> ( ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
23 22 2rexbidv 
 |-  ( b = 0 -> ( E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
24 23 2rexbidv 
 |-  ( b = 0 -> ( E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
25 24 adantl 
 |-  ( ( ( ph /\ x e. ( C ` N ) ) /\ b = 0 ) -> ( E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
26 oveq2 
 |-  ( c = 0 -> ( x - c ) = ( x - 0 ) )
27 26 fveq2d 
 |-  ( c = 0 -> ( abs ` ( x - c ) ) = ( abs ` ( x - 0 ) ) )
28 27 eqeq1d 
 |-  ( c = 0 -> ( ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) )
29 28 anbi2d 
 |-  ( c = 0 -> ( ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) ) )
30 29 rexbidv 
 |-  ( c = 0 -> ( E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) ) )
31 30 2rexbidv 
 |-  ( c = 0 -> ( E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) ) )
32 31 adantl 
 |-  ( ( ( ph /\ x e. ( C ` N ) ) /\ c = 0 ) -> ( E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) ) )
33 oveq1 
 |-  ( e = x -> ( e - f ) = ( x - f ) )
34 33 fveq2d 
 |-  ( e = x -> ( abs ` ( e - f ) ) = ( abs ` ( x - f ) ) )
35 34 eqeq2d 
 |-  ( e = x -> ( ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) )
36 35 anbi2d 
 |-  ( e = x -> ( ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) <-> ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) ) )
37 36 2rexbidv 
 |-  ( e = x -> ( E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) ) )
38 37 adantl 
 |-  ( ( ( ph /\ x e. ( C ` N ) ) /\ e = x ) -> ( E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) ) )
39 oveq2 
 |-  ( f = 0 -> ( x - f ) = ( x - 0 ) )
40 39 fveq2d 
 |-  ( f = 0 -> ( abs ` ( x - f ) ) = ( abs ` ( x - 0 ) ) )
41 40 eqeq2d 
 |-  ( f = 0 -> ( ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) <-> ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) )
42 41 anbi2d 
 |-  ( f = 0 -> ( ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) <-> ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) ) )
43 42 rexbidv 
 |-  ( f = 0 -> ( E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) <-> E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) ) )
44 43 adantl 
 |-  ( ( ( ph /\ x e. ( C ` N ) ) /\ f = 0 ) -> ( E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) <-> E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) ) )
45 0red 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> 0 e. RR )
46 oveq1 
 |-  ( t = 0 -> ( t x. ( 0 - x ) ) = ( 0 x. ( 0 - x ) ) )
47 46 oveq2d 
 |-  ( t = 0 -> ( x + ( t x. ( 0 - x ) ) ) = ( x + ( 0 x. ( 0 - x ) ) ) )
48 47 eqeq2d 
 |-  ( t = 0 -> ( x = ( x + ( t x. ( 0 - x ) ) ) <-> x = ( x + ( 0 x. ( 0 - x ) ) ) ) )
49 48 anbi1d 
 |-  ( t = 0 -> ( ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) <-> ( x = ( x + ( 0 x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) ) )
50 49 adantl 
 |-  ( ( ( ph /\ x e. ( C ` N ) ) /\ t = 0 ) -> ( ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) <-> ( x = ( x + ( 0 x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) ) )
51 0cnd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> 0 e. CC )
52 51 5 subcld 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( 0 - x ) e. CC )
53 52 mul02d 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( 0 x. ( 0 - x ) ) = 0 )
54 53 oveq2d 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( x + ( 0 x. ( 0 - x ) ) ) = ( x + 0 ) )
55 5 addridd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( x + 0 ) = x )
56 54 55 eqtr2d 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> x = ( x + ( 0 x. ( 0 - x ) ) ) )
57 eqidd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) )
58 56 57 jca 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( x = ( x + ( 0 x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) )
59 45 50 58 rspcedvd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - 0 ) ) ) )
60 17 44 59 rspcedvd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( x - f ) ) ) )
61 6 38 60 rspcedvd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - 0 ) ) = ( abs ` ( e - f ) ) ) )
62 17 32 61 rspcedvd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( 0 - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) )
63 17 25 62 rspcedvd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( x + ( t x. ( b - x ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) )
64 6 16 63 rspcedvd 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) )
65 64 3mix2d 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. d e. ( C ` N ) E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. d e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
66 eqid 
 |-  ( C ` N ) = ( C ` N )
67 1 2 66 constrsuc 
 |-  ( ph -> ( x e. ( C ` suc N ) <-> ( x e. CC /\ ( E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. d e. ( C ` N ) E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. d e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) ) )
68 67 adantr 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> ( x e. ( C ` suc N ) <-> ( x e. CC /\ ( E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. d e. ( C ` N ) E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. ( C ` N ) E. b e. ( C ` N ) E. c e. ( C ` N ) E. d e. ( C ` N ) E. e e. ( C ` N ) E. f e. ( C ` N ) ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) ) )
69 5 65 68 mpbir2and 
 |-  ( ( ph /\ x e. ( C ` N ) ) -> x e. ( C ` suc N ) )
70 69 ex 
 |-  ( ph -> ( x e. ( C ` N ) -> x e. ( C ` suc N ) ) )
71 70 ssrdv 
 |-  ( ph -> ( C ` N ) C_ ( C ` suc N ) )