Metamath Proof Explorer

Theorem nthrucw

Description: Some number sets form a chain of proper subsets. This is rephrasing nthruc as a statement about chains; the hypothesis sets the ordering relation to be "is a proper subset". The theorem talks about singleton 1, natural numbers, natural-or-zero numbers, integers, rational numbers, algebraic reals (the definition includes complex numbers as algebraic so intersection is taken), real numbers and complex numbers, which are proper subsets in order. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypothesis nthrucw.1 
|- .< = { <. x , y >. | x C. y }
Assertion nthrucw 
|- <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> e. ( .< Chain _V )

Proof

Step Hyp Ref Expression
1 nthrucw.1 
 |-  .< = { <. x , y >. | x C. y }
2 df-s8 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ++ <" CC "> )
3 cnex 
 |-  CC e. _V
4 3 a1i 
 |-  ( T. -> CC e. _V )
5 df-s7 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ++ <" RR "> )
6 reex 
 |-  RR e. _V
7 6 a1i 
 |-  ( T. -> RR e. _V )
8 df-s6 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> = ( <" { 1 } NN NN0 ZZ QQ "> ++ <" ( AA i^i RR ) "> )
9 6 inex2 
 |-  ( AA i^i RR ) e. _V
10 9 a1i 
 |-  ( T. -> ( AA i^i RR ) e. _V )
11 df-s5 
 |-  <" { 1 } NN NN0 ZZ QQ "> = ( <" { 1 } NN NN0 ZZ "> ++ <" QQ "> )
12 qex 
 |-  QQ e. _V
13 12 a1i 
 |-  ( T. -> QQ e. _V )
14 df-s4 
 |-  <" { 1 } NN NN0 ZZ "> = ( <" { 1 } NN NN0 "> ++ <" ZZ "> )
15 zex 
 |-  ZZ e. _V
16 15 a1i 
 |-  ( T. -> ZZ e. _V )
17 df-s3 
 |-  <" { 1 } NN NN0 "> = ( <" { 1 } NN "> ++ <" NN0 "> )
18 nn0ex 
 |-  NN0 e. _V
19 18 a1i 
 |-  ( T. -> NN0 e. _V )
20 df-s2 
 |-  <" { 1 } NN "> = ( <" { 1 } "> ++ <" NN "> )
21 nnex 
 |-  NN e. _V
22 21 a1i 
 |-  ( T. -> NN e. _V )
23 snex 
 |-  { 1 } e. _V
24 23 a1i 
 |-  ( T. -> { 1 } e. _V )
25 24 s1chn 
 |-  ( T. -> <" { 1 } "> e. ( .< Chain _V ) )
26 lsws1 
 |-  ( { 1 } e. _V -> ( lastS ` <" { 1 } "> ) = { 1 } )
27 23 26 ax-mp 
 |-  ( lastS ` <" { 1 } "> ) = { 1 }
28 1nn 
 |-  1 e. NN
29 1ex 
 |-  1 e. _V
30 29 snss 
 |-  ( 1 e. NN <-> { 1 } C_ NN )
31 28 30 mpbi 
 |-  { 1 } C_ NN
32 2nn 
 |-  2 e. NN
33 1re 
 |-  1 e. RR
34 1lt2 
 |-  1 < 2
35 33 34 gtneii 
 |-  2 =/= 1
36 nelsn 
 |-  ( 2 =/= 1 -> -. 2 e. { 1 } )
37 35 36 ax-mp 
 |-  -. 2 e. { 1 }
38 32 37 pm3.2i 
 |-  ( 2 e. NN /\ -. 2 e. { 1 } )
39 ssnelpss 
 |-  ( { 1 } C_ NN -> ( ( 2 e. NN /\ -. 2 e. { 1 } ) -> { 1 } C. NN ) )
40 31 38 39 mp2 
 |-  { 1 } C. NN
41 psseq1 
 |-  ( x = { 1 } -> ( x C. y <-> { 1 } C. y ) )
42 psseq2 
 |-  ( y = NN -> ( { 1 } C. y <-> { 1 } C. NN ) )
43 23 21 41 42 1 brab 
 |-  ( { 1 } .< NN <-> { 1 } C. NN )
44 40 43 mpbir 
 |-  { 1 } .< NN
45 27 44 eqbrtri 
 |-  ( lastS ` <" { 1 } "> ) .< NN
46 45 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } "> ) .< NN )
47 46 olcd 
 |-  ( T. -> ( <" { 1 } "> = (/) \/ ( lastS ` <" { 1 } "> ) .< NN ) )
48 22 25 47 chnccats1 
 |-  ( T. -> ( <" { 1 } "> ++ <" NN "> ) e. ( .< Chain _V ) )
49 20 48 eqeltrid 
 |-  ( T. -> <" { 1 } NN "> e. ( .< Chain _V ) )
50 lsws2 
 |-  ( NN e. _V -> ( lastS ` <" { 1 } NN "> ) = NN )
51 21 50 ax-mp 
 |-  ( lastS ` <" { 1 } NN "> ) = NN
52 nthruz 
 |-  ( NN C. NN0 /\ NN0 C. ZZ )
53 52 simpli 
 |-  NN C. NN0
54 psseq1 
 |-  ( x = NN -> ( x C. y <-> NN C. y ) )
55 psseq2 
 |-  ( y = NN0 -> ( NN C. y <-> NN C. NN0 ) )
56 21 18 54 55 1 brab 
 |-  ( NN .< NN0 <-> NN C. NN0 )
57 53 56 mpbir 
 |-  NN .< NN0
58 51 57 eqbrtri 
 |-  ( lastS ` <" { 1 } NN "> ) .< NN0
59 58 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN "> ) .< NN0 )
60 59 olcd 
 |-  ( T. -> ( <" { 1 } NN "> = (/) \/ ( lastS ` <" { 1 } NN "> ) .< NN0 ) )
61 19 49 60 chnccats1 
 |-  ( T. -> ( <" { 1 } NN "> ++ <" NN0 "> ) e. ( .< Chain _V ) )
62 17 61 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 "> e. ( .< Chain _V ) )
63 lsws3 
 |-  ( NN0 e. _V -> ( lastS ` <" { 1 } NN NN0 "> ) = NN0 )
64 18 63 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 "> ) = NN0
65 52 simpri 
 |-  NN0 C. ZZ
66 psseq1 
 |-  ( x = NN0 -> ( x C. y <-> NN0 C. y ) )
67 psseq2 
 |-  ( y = ZZ -> ( NN0 C. y <-> NN0 C. ZZ ) )
68 18 15 66 67 1 brab 
 |-  ( NN0 .< ZZ <-> NN0 C. ZZ )
69 65 68 mpbir 
 |-  NN0 .< ZZ
70 64 69 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 "> ) .< ZZ
71 70 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 "> ) .< ZZ )
72 71 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 "> = (/) \/ ( lastS ` <" { 1 } NN NN0 "> ) .< ZZ ) )
73 16 62 72 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 "> ++ <" ZZ "> ) e. ( .< Chain _V ) )
74 14 73 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ "> e. ( .< Chain _V ) )
75 lsws4 
 |-  ( ZZ e. _V -> ( lastS ` <" { 1 } NN NN0 ZZ "> ) = ZZ )
76 15 75 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ "> ) = ZZ
77 nthruc 
 |-  ( ( NN C. ZZ /\ ZZ C. QQ ) /\ ( QQ C. RR /\ RR C. CC ) )
78 77 simpli 
 |-  ( NN C. ZZ /\ ZZ C. QQ )
79 78 simpri 
 |-  ZZ C. QQ
80 psseq1 
 |-  ( x = ZZ -> ( x C. y <-> ZZ C. y ) )
81 psseq2 
 |-  ( y = QQ -> ( ZZ C. y <-> ZZ C. QQ ) )
82 15 12 80 81 1 brab 
 |-  ( ZZ .< QQ <-> ZZ C. QQ )
83 79 82 mpbir 
 |-  ZZ .< QQ
84 76 83 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ "> ) .< QQ
85 84 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ "> ) .< QQ )
86 85 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ "> ) .< QQ ) )
87 13 74 86 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ "> ++ <" QQ "> ) e. ( .< Chain _V ) )
88 11 87 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ "> e. ( .< Chain _V ) )
89 s5cli 
 |-  <" { 1 } NN NN0 ZZ QQ "> e. Word _V
90 lsw 
 |-  ( <" { 1 } NN NN0 ZZ QQ "> e. Word _V -> ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) = ( <" { 1 } NN NN0 ZZ QQ "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) ) )
91 89 90 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) = ( <" { 1 } NN NN0 ZZ QQ "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) )
92 s5len 
 |-  ( # ` <" { 1 } NN NN0 ZZ QQ "> ) = 5
93 92 oveq1i 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) = ( 5 - 1 )
94 5m1e4 
 |-  ( 5 - 1 ) = 4
95 93 94 eqtri 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) = 4
96 95 fveq2i 
 |-  ( <" { 1 } NN NN0 ZZ QQ "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) ) = ( <" { 1 } NN NN0 ZZ QQ "> ` 4 )
97 s4cli 
 |-  <" { 1 } NN NN0 ZZ "> e. Word _V
98 s4len 
 |-  ( # ` <" { 1 } NN NN0 ZZ "> ) = 4
99 11 97 98 cats1fvn 
 |-  ( QQ e. _V -> ( <" { 1 } NN NN0 ZZ QQ "> ` 4 ) = QQ )
100 12 99 ax-mp 
 |-  ( <" { 1 } NN NN0 ZZ QQ "> ` 4 ) = QQ
101 91 96 100 3eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) = QQ
102 qssaa 
 |-  QQ C_ AA
103 qssre 
 |-  QQ C_ RR
104 102 103 ssini 
 |-  QQ C_ ( AA i^i RR )
105 sqrtnnaa 
 |-  ( 2 e. NN -> ( sqrt ` 2 ) e. AA )
106 32 105 ax-mp 
 |-  ( sqrt ` 2 ) e. AA
107 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
108 106 107 elini 
 |-  ( sqrt ` 2 ) e. ( AA i^i RR )
109 sqrt2irr 
 |-  ( sqrt ` 2 ) e/ QQ
110 109 neli 
 |-  -. ( sqrt ` 2 ) e. QQ
111 108 110 pm3.2i 
 |-  ( ( sqrt ` 2 ) e. ( AA i^i RR ) /\ -. ( sqrt ` 2 ) e. QQ )
112 ssnelpss 
 |-  ( QQ C_ ( AA i^i RR ) -> ( ( ( sqrt ` 2 ) e. ( AA i^i RR ) /\ -. ( sqrt ` 2 ) e. QQ ) -> QQ C. ( AA i^i RR ) ) )
113 104 111 112 mp2 
 |-  QQ C. ( AA i^i RR )
114 psseq1 
 |-  ( x = QQ -> ( x C. y <-> QQ C. y ) )
115 psseq2 
 |-  ( y = ( AA i^i RR ) -> ( QQ C. y <-> QQ C. ( AA i^i RR ) ) )
116 12 9 114 115 1 brab 
 |-  ( QQ .< ( AA i^i RR ) <-> QQ C. ( AA i^i RR ) )
117 113 116 mpbir 
 |-  QQ .< ( AA i^i RR )
118 101 117 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) .< ( AA i^i RR )
119 118 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) .< ( AA i^i RR ) )
120 119 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) .< ( AA i^i RR ) ) )
121 10 88 120 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ "> ++ <" ( AA i^i RR ) "> ) e. ( .< Chain _V ) )
122 8 121 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> e. ( .< Chain _V ) )
123 s6cli 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> e. Word _V
124 lsw 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> e. Word _V -> ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) ) )
125 123 124 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) )
126 s6len 
 |-  ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = 6
127 126 oveq1i 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) = ( 6 - 1 )
128 6m1e5 
 |-  ( 6 - 1 ) = 5
129 127 128 eqtri 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) = 5
130 129 fveq2i 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` 5 )
131 8 89 92 cats1fvn 
 |-  ( ( AA i^i RR ) e. _V -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` 5 ) = ( AA i^i RR ) )
132 9 131 ax-mp 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` 5 ) = ( AA i^i RR )
133 125 130 132 3eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = ( AA i^i RR )
134 inss2 
 |-  ( AA i^i RR ) C_ RR
135 aaliou3r 
 |-  sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR
136 aaliou3 
 |-  sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e/ AA
137 136 neli 
 |-  -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. AA
138 elinel1 
 |-  ( sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR ) -> sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. AA )
139 137 138 mto 
 |-  -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR )
140 135 139 pm3.2i 
 |-  ( sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR /\ -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR ) )
141 ssnelpss 
 |-  ( ( AA i^i RR ) C_ RR -> ( ( sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR /\ -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR ) ) -> ( AA i^i RR ) C. RR ) )
142 134 140 141 mp2 
 |-  ( AA i^i RR ) C. RR
143 psseq1 
 |-  ( x = ( AA i^i RR ) -> ( x C. y <-> ( AA i^i RR ) C. y ) )
144 psseq2 
 |-  ( y = RR -> ( ( AA i^i RR ) C. y <-> ( AA i^i RR ) C. RR ) )
145 9 6 143 144 1 brab 
 |-  ( ( AA i^i RR ) .< RR <-> ( AA i^i RR ) C. RR )
146 142 145 mpbir 
 |-  ( AA i^i RR ) .< RR
147 133 146 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) .< RR
148 147 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) .< RR )
149 148 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) .< RR ) )
150 7 122 149 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ++ <" RR "> ) e. ( .< Chain _V ) )
151 5 150 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> e. ( .< Chain _V ) )
152 s7cli 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> e. Word _V
153 lsw 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> e. Word _V -> ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) ) )
154 152 153 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) )
155 s7len 
 |-  ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) = 7
156 155 oveq1i 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) = ( 7 - 1 )
157 7m1e6 
 |-  ( 7 - 1 ) = 6
158 156 157 eqtri 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) = 6
159 158 fveq2i 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` 6 )
160 5 123 126 cats1fvn 
 |-  ( RR e. _V -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` 6 ) = RR )
161 6 160 ax-mp 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` 6 ) = RR
162 154 159 161 3eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) = RR
163 77 simpri 
 |-  ( QQ C. RR /\ RR C. CC )
164 163 simpri 
 |-  RR C. CC
165 psseq1 
 |-  ( x = RR -> ( x C. y <-> RR C. y ) )
166 psseq2 
 |-  ( y = CC -> ( RR C. y <-> RR C. CC ) )
167 6 3 165 166 1 brab 
 |-  ( RR .< CC <-> RR C. CC )
168 164 167 mpbir 
 |-  RR .< CC
169 162 168 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) .< CC
170 169 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) .< CC )
171 170 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) .< CC ) )
172 4 151 171 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ++ <" CC "> ) e. ( .< Chain _V ) )
173 2 172 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> e. ( .< Chain _V ) )
174 173 mptru 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> e. ( .< Chain _V )