Metamath Proof Explorer

Theorem numtowerdt

Description: Certain number sets and fields form a tower. In particular, singleton 1, natural numbers, natural numbers with zero, integers, rationals, algebraic reals (notice that current definition allows algebraic numbers to be complex thus the restriction), reals and complex number sets are a tower of proper subsets. (Contributed by Ender Ting, 31-Jul-2026)

Ref Expression
Assertion numtowerdt 
|- <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> e. ( [C.] Chain _V )

Proof

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