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 ltne 
 |-  ( ( 1 e. RR /\ 1 < 2 ) -> 2 =/= 1 )
36 33 34 35 mp2an 
 |-  2 =/= 1
37 nelsn 
 |-  ( 2 =/= 1 -> -. 2 e. { 1 } )
38 36 37 ax-mp 
 |-  -. 2 e. { 1 }
39 32 38 pm3.2i 
 |-  ( 2 e. NN /\ -. 2 e. { 1 } )
40 ssnelpss 
 |-  ( { 1 } C_ NN -> ( ( 2 e. NN /\ -. 2 e. { 1 } ) -> { 1 } C. NN ) )
41 31 39 40 mp2 
 |-  { 1 } C. NN
42 psseq1 
 |-  ( x = { 1 } -> ( x C. y <-> { 1 } C. y ) )
43 psseq2 
 |-  ( y = NN -> ( { 1 } C. y <-> { 1 } C. NN ) )
44 42 43 1 brabg 
 |-  ( ( { 1 } e. _V /\ NN e. _V ) -> ( { 1 } .< NN <-> { 1 } C. NN ) )
45 23 21 44 mp2an 
 |-  ( { 1 } .< NN <-> { 1 } C. NN )
46 41 45 mpbir 
 |-  { 1 } .< NN
47 27 46 eqbrtri 
 |-  ( lastS ` <" { 1 } "> ) .< NN
48 47 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } "> ) .< NN )
49 48 olcd 
 |-  ( T. -> ( <" { 1 } "> = (/) \/ ( lastS ` <" { 1 } "> ) .< NN ) )
50 22 25 49 chnccats1 
 |-  ( T. -> ( <" { 1 } "> ++ <" NN "> ) e. ( .< Chain _V ) )
51 20 50 eqeltrid 
 |-  ( T. -> <" { 1 } NN "> e. ( .< Chain _V ) )
52 lsws2 
 |-  ( NN e. _V -> ( lastS ` <" { 1 } NN "> ) = NN )
53 21 52 ax-mp 
 |-  ( lastS ` <" { 1 } NN "> ) = NN
54 nthruz 
 |-  ( NN C. NN0 /\ NN0 C. ZZ )
55 54 simpli 
 |-  NN C. NN0
56 psseq1 
 |-  ( x = NN -> ( x C. y <-> NN C. y ) )
57 psseq2 
 |-  ( y = NN0 -> ( NN C. y <-> NN C. NN0 ) )
58 56 57 1 brabg 
 |-  ( ( NN e. _V /\ NN0 e. _V ) -> ( NN .< NN0 <-> NN C. NN0 ) )
59 21 18 58 mp2an 
 |-  ( NN .< NN0 <-> NN C. NN0 )
60 55 59 mpbir 
 |-  NN .< NN0
61 53 60 eqbrtri 
 |-  ( lastS ` <" { 1 } NN "> ) .< NN0
62 61 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN "> ) .< NN0 )
63 62 olcd 
 |-  ( T. -> ( <" { 1 } NN "> = (/) \/ ( lastS ` <" { 1 } NN "> ) .< NN0 ) )
64 19 51 63 chnccats1 
 |-  ( T. -> ( <" { 1 } NN "> ++ <" NN0 "> ) e. ( .< Chain _V ) )
65 17 64 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 "> e. ( .< Chain _V ) )
66 lsws3 
 |-  ( NN0 e. _V -> ( lastS ` <" { 1 } NN NN0 "> ) = NN0 )
67 18 66 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 "> ) = NN0
68 54 simpri 
 |-  NN0 C. ZZ
69 psseq1 
 |-  ( x = NN0 -> ( x C. y <-> NN0 C. y ) )
70 psseq2 
 |-  ( y = ZZ -> ( NN0 C. y <-> NN0 C. ZZ ) )
71 69 70 1 brabg 
 |-  ( ( NN0 e. _V /\ ZZ e. _V ) -> ( NN0 .< ZZ <-> NN0 C. ZZ ) )
72 18 15 71 mp2an 
 |-  ( NN0 .< ZZ <-> NN0 C. ZZ )
73 68 72 mpbir 
 |-  NN0 .< ZZ
74 67 73 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 "> ) .< ZZ
75 74 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 "> ) .< ZZ )
76 75 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 "> = (/) \/ ( lastS ` <" { 1 } NN NN0 "> ) .< ZZ ) )
77 16 65 76 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 "> ++ <" ZZ "> ) e. ( .< Chain _V ) )
78 14 77 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ "> e. ( .< Chain _V ) )
79 lsws4 
 |-  ( ZZ e. _V -> ( lastS ` <" { 1 } NN NN0 ZZ "> ) = ZZ )
80 15 79 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ "> ) = ZZ
81 nthruc 
 |-  ( ( NN C. ZZ /\ ZZ C. QQ ) /\ ( QQ C. RR /\ RR C. CC ) )
82 81 simpli 
 |-  ( NN C. ZZ /\ ZZ C. QQ )
83 82 simpri 
 |-  ZZ C. QQ
84 psseq1 
 |-  ( x = ZZ -> ( x C. y <-> ZZ C. y ) )
85 psseq2 
 |-  ( y = QQ -> ( ZZ C. y <-> ZZ C. QQ ) )
86 84 85 1 brabg 
 |-  ( ( ZZ e. _V /\ QQ e. _V ) -> ( ZZ .< QQ <-> ZZ C. QQ ) )
87 15 12 86 mp2an 
 |-  ( ZZ .< QQ <-> ZZ C. QQ )
88 83 87 mpbir 
 |-  ZZ .< QQ
89 80 88 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ "> ) .< QQ
90 89 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ "> ) .< QQ )
91 90 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ "> ) .< QQ ) )
92 13 78 91 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ "> ++ <" QQ "> ) e. ( .< Chain _V ) )
93 11 92 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ "> e. ( .< Chain _V ) )
94 s5cli 
 |-  <" { 1 } NN NN0 ZZ QQ "> e. Word _V
95 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 ) ) )
96 94 95 ax-mp 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) = ( <" { 1 } NN NN0 ZZ QQ "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) )
97 s5len 
 |-  ( # ` <" { 1 } NN NN0 ZZ QQ "> ) = 5
98 97 oveq1i 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) = ( 5 - 1 )
99 5m1e4 
 |-  ( 5 - 1 ) = 4
100 98 99 eqtri 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) = 4
101 100 fveq2i 
 |-  ( <" { 1 } NN NN0 ZZ QQ "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ "> ) - 1 ) ) = ( <" { 1 } NN NN0 ZZ QQ "> ` 4 )
102 96 101 eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) = ( <" { 1 } NN NN0 ZZ QQ "> ` 4 )
103 s4cli 
 |-  <" { 1 } NN NN0 ZZ "> e. Word _V
104 s4len 
 |-  ( # ` <" { 1 } NN NN0 ZZ "> ) = 4
105 11 103 104 cats1fvn 
 |-  ( QQ e. _V -> ( <" { 1 } NN NN0 ZZ QQ "> ` 4 ) = QQ )
106 12 105 ax-mp 
 |-  ( <" { 1 } NN NN0 ZZ QQ "> ` 4 ) = QQ
107 102 106 eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) = QQ
108 qssaa 
 |-  QQ C_ AA
109 qssre 
 |-  QQ C_ RR
110 108 109 ssini 
 |-  QQ C_ ( AA i^i RR )
111 2cn 
 |-  2 e. CC
112 sqrtcl 
 |-  ( 2 e. CC -> ( sqrt ` 2 ) e. CC )
113 111 112 ax-mp 
 |-  ( sqrt ` 2 ) e. CC
114 zsscn 
 |-  ZZ C_ CC
115 1z 
 |-  1 e. ZZ
116 2nn0 
 |-  2 e. NN0
117 plypow 
 |-  ( ( ZZ C_ CC /\ 1 e. ZZ /\ 2 e. NN0 ) -> ( x e. CC |-> ( x ^ 2 ) ) e. ( Poly ` ZZ ) )
118 114 115 116 117 mp3an 
 |-  ( x e. CC |-> ( x ^ 2 ) ) e. ( Poly ` ZZ )
119 118 a1i 
 |-  ( T. -> ( x e. CC |-> ( x ^ 2 ) ) e. ( Poly ` ZZ ) )
120 2z 
 |-  2 e. ZZ
121 114 120 pm3.2i 
 |-  ( ZZ C_ CC /\ 2 e. ZZ )
122 plyconst 
 |-  ( ( ZZ C_ CC /\ 2 e. ZZ ) -> ( CC X. { 2 } ) e. ( Poly ` ZZ ) )
123 121 122 mp1i 
 |-  ( T. -> ( CC X. { 2 } ) e. ( Poly ` ZZ ) )
124 zaddcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a + b ) e. ZZ )
125 124 adantl 
 |-  ( ( T. /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + b ) e. ZZ )
126 zmulcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ )
127 126 adantl 
 |-  ( ( T. /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a x. b ) e. ZZ )
128 neg1z 
 |-  -u 1 e. ZZ
129 128 a1i 
 |-  ( T. -> -u 1 e. ZZ )
130 119 123 125 127 129 plysub 
 |-  ( T. -> ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( Poly ` ZZ ) )
131 130 mptru 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( Poly ` ZZ )
132 0cn 
 |-  0 e. CC
133 ovex 
 |-  ( x ^ 2 ) e. _V
134 133 rgenw 
 |-  A. x e. CC ( x ^ 2 ) e. _V
135 nfcv 
 |-  F/_ x CC
136 135 mptfnf 
 |-  ( A. x e. CC ( x ^ 2 ) e. _V <-> ( x e. CC |-> ( x ^ 2 ) ) Fn CC )
137 134 136 mpbi 
 |-  ( x e. CC |-> ( x ^ 2 ) ) Fn CC
138 2ex 
 |-  2 e. _V
139 fconstmpt 
 |-  ( CC X. { 2 } ) = ( a e. CC |-> 2 )
140 138 139 fnmpti 
 |-  ( CC X. { 2 } ) Fn CC
141 fnfvof 
 |-  ( ( ( ( x e. CC |-> ( x ^ 2 ) ) Fn CC /\ ( CC X. { 2 } ) Fn CC ) /\ ( CC e. _V /\ 0 e. CC ) ) -> ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) - ( ( CC X. { 2 } ) ` 0 ) ) )
142 137 140 141 mpanl12 
 |-  ( ( CC e. _V /\ 0 e. CC ) -> ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) - ( ( CC X. { 2 } ) ` 0 ) ) )
143 3 132 142 mp2an 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) - ( ( CC X. { 2 } ) ` 0 ) )
144 oveq1 
 |-  ( x = 0 -> ( x ^ 2 ) = ( 0 ^ 2 ) )
145 eqid 
 |-  ( x e. CC |-> ( x ^ 2 ) ) = ( x e. CC |-> ( x ^ 2 ) )
146 ovex 
 |-  ( 0 ^ 2 ) e. _V
147 144 145 146 fvmpt 
 |-  ( 0 e. CC -> ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) = ( 0 ^ 2 ) )
148 132 147 ax-mp 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) = ( 0 ^ 2 )
149 sq0 
 |-  ( 0 ^ 2 ) = 0
150 148 149 eqtri 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) = 0
151 138 fvconst2 
 |-  ( 0 e. CC -> ( ( CC X. { 2 } ) ` 0 ) = 2 )
152 132 151 ax-mp 
 |-  ( ( CC X. { 2 } ) ` 0 ) = 2
153 150 152 oveq12i 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) ` 0 ) - ( ( CC X. { 2 } ) ` 0 ) ) = ( 0 - 2 )
154 143 153 eqtri 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) = ( 0 - 2 )
155 df-neg 
 |-  -u 2 = ( 0 - 2 )
156 154 155 eqtr4i 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) = -u 2
157 2re 
 |-  2 e. RR
158 157 renegcli 
 |-  -u 2 e. RR
159 2pos 
 |-  0 < 2
160 lt0neg2 
 |-  ( 2 e. RR -> ( 0 < 2 <-> -u 2 < 0 ) )
161 157 160 ax-mp 
 |-  ( 0 < 2 <-> -u 2 < 0 )
162 159 161 mpbi 
 |-  -u 2 < 0
163 ltne 
 |-  ( ( -u 2 e. RR /\ -u 2 < 0 ) -> 0 =/= -u 2 )
164 158 162 163 mp2an 
 |-  0 =/= -u 2
165 164 necomi 
 |-  -u 2 =/= 0
166 156 165 eqnetri 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) =/= 0
167 132 166 pm3.2i 
 |-  ( 0 e. CC /\ ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) =/= 0 )
168 ne0p 
 |-  ( ( 0 e. CC /\ ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` 0 ) =/= 0 ) -> ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) =/= 0p )
169 nelsn 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) =/= 0p -> -. ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. { 0p } )
170 167 168 169 mp2b 
 |-  -. ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. { 0p }
171 131 170 pm3.2i 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( Poly ` ZZ ) /\ -. ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. { 0p } )
172 eldif 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) <-> ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( Poly ` ZZ ) /\ -. ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. { 0p } ) )
173 171 172 mpbir 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( ( Poly ` ZZ ) \ { 0p } )
174 fconstmpt 
 |-  ( CC X. { 2 } ) = ( b e. CC |-> 2 )
175 138 174 fnmpti 
 |-  ( CC X. { 2 } ) Fn CC
176 fnfvof 
 |-  ( ( ( ( x e. CC |-> ( x ^ 2 ) ) Fn CC /\ ( CC X. { 2 } ) Fn CC ) /\ ( CC e. _V /\ ( sqrt ` 2 ) e. CC ) ) -> ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) - ( ( CC X. { 2 } ) ` ( sqrt ` 2 ) ) ) )
177 137 175 176 mpanl12 
 |-  ( ( CC e. _V /\ ( sqrt ` 2 ) e. CC ) -> ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) - ( ( CC X. { 2 } ) ` ( sqrt ` 2 ) ) ) )
178 3 113 177 mp2an 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) - ( ( CC X. { 2 } ) ` ( sqrt ` 2 ) ) )
179 oveq1 
 |-  ( x = ( sqrt ` 2 ) -> ( x ^ 2 ) = ( ( sqrt ` 2 ) ^ 2 ) )
180 ovex 
 |-  ( ( sqrt ` 2 ) ^ 2 ) e. _V
181 179 145 180 fvmpt 
 |-  ( ( sqrt ` 2 ) e. CC -> ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) = ( ( sqrt ` 2 ) ^ 2 ) )
182 113 181 ax-mp 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) = ( ( sqrt ` 2 ) ^ 2 )
183 sqrtth 
 |-  ( 2 e. CC -> ( ( sqrt ` 2 ) ^ 2 ) = 2 )
184 111 183 ax-mp 
 |-  ( ( sqrt ` 2 ) ^ 2 ) = 2
185 182 184 eqtri 
 |-  ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) = 2
186 138 fvconst2 
 |-  ( ( sqrt ` 2 ) e. CC -> ( ( CC X. { 2 } ) ` ( sqrt ` 2 ) ) = 2 )
187 113 186 ax-mp 
 |-  ( ( CC X. { 2 } ) ` ( sqrt ` 2 ) ) = 2
188 185 187 oveq12i 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) ` ( sqrt ` 2 ) ) - ( ( CC X. { 2 } ) ` ( sqrt ` 2 ) ) ) = ( 2 - 2 )
189 178 188 eqtri 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = ( 2 - 2 )
190 subid 
 |-  ( 2 e. CC -> ( 2 - 2 ) = 0 )
191 111 190 ax-mp 
 |-  ( 2 - 2 ) = 0
192 189 191 eqtri 
 |-  ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = 0
193 fveq1 
 |-  ( a = ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) -> ( a ` ( sqrt ` 2 ) ) = ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) )
194 193 eqeq1d 
 |-  ( a = ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) -> ( ( a ` ( sqrt ` 2 ) ) = 0 <-> ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = 0 ) )
195 194 rspcev 
 |-  ( ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = 0 ) -> E. a e. ( ( Poly ` ZZ ) \ { 0p } ) ( a ` ( sqrt ` 2 ) ) = 0 )
196 fveq1 
 |-  ( a = x -> ( a ` ( sqrt ` 2 ) ) = ( x ` ( sqrt ` 2 ) ) )
197 196 eqeq1d 
 |-  ( a = x -> ( ( a ` ( sqrt ` 2 ) ) = 0 <-> ( x ` ( sqrt ` 2 ) ) = 0 ) )
198 197 cbvrexvw 
 |-  ( E. a e. ( ( Poly ` ZZ ) \ { 0p } ) ( a ` ( sqrt ` 2 ) ) = 0 <-> E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` 2 ) ) = 0 )
199 195 198 sylib 
 |-  ( ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) e. ( ( Poly ` ZZ ) \ { 0p } ) /\ ( ( ( x e. CC |-> ( x ^ 2 ) ) oF - ( CC X. { 2 } ) ) ` ( sqrt ` 2 ) ) = 0 ) -> E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` 2 ) ) = 0 )
200 173 192 199 mp2an 
 |-  E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` 2 ) ) = 0
201 113 200 pm3.2i 
 |-  ( ( sqrt ` 2 ) e. CC /\ E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` 2 ) ) = 0 )
202 elaa 
 |-  ( ( sqrt ` 2 ) e. AA <-> ( ( sqrt ` 2 ) e. CC /\ E. x e. ( ( Poly ` ZZ ) \ { 0p } ) ( x ` ( sqrt ` 2 ) ) = 0 ) )
203 201 202 mpbir 
 |-  ( sqrt ` 2 ) e. AA
204 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
205 203 204 elini 
 |-  ( sqrt ` 2 ) e. ( AA i^i RR )
206 sqrt2irr 
 |-  ( sqrt ` 2 ) e/ QQ
207 df-nel 
 |-  ( ( sqrt ` 2 ) e/ QQ <-> -. ( sqrt ` 2 ) e. QQ )
208 206 207 mpbi 
 |-  -. ( sqrt ` 2 ) e. QQ
209 205 208 pm3.2i 
 |-  ( ( sqrt ` 2 ) e. ( AA i^i RR ) /\ -. ( sqrt ` 2 ) e. QQ )
210 ssnelpss 
 |-  ( QQ C_ ( AA i^i RR ) -> ( ( ( sqrt ` 2 ) e. ( AA i^i RR ) /\ -. ( sqrt ` 2 ) e. QQ ) -> QQ C. ( AA i^i RR ) ) )
211 110 209 210 mp2 
 |-  QQ C. ( AA i^i RR )
212 psseq1 
 |-  ( x = QQ -> ( x C. y <-> QQ C. y ) )
213 psseq2 
 |-  ( y = ( AA i^i RR ) -> ( QQ C. y <-> QQ C. ( AA i^i RR ) ) )
214 212 213 1 brabg 
 |-  ( ( QQ e. _V /\ ( AA i^i RR ) e. _V ) -> ( QQ .< ( AA i^i RR ) <-> QQ C. ( AA i^i RR ) ) )
215 12 9 214 mp2an 
 |-  ( QQ .< ( AA i^i RR ) <-> QQ C. ( AA i^i RR ) )
216 211 215 mpbir 
 |-  QQ .< ( AA i^i RR )
217 107 216 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) .< ( AA i^i RR )
218 217 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) .< ( AA i^i RR ) )
219 218 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ QQ "> ) .< ( AA i^i RR ) ) )
220 10 93 219 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ "> ++ <" ( AA i^i RR ) "> ) e. ( .< Chain _V ) )
221 8 220 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> e. ( .< Chain _V ) )
222 s6cli 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> e. Word _V
223 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 ) ) )
224 222 223 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 ) )
225 s6len 
 |-  ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = 6
226 225 oveq1i 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) = ( 6 - 1 )
227 6m1e5 
 |-  ( 6 - 1 ) = 5
228 226 227 eqtri 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) - 1 ) = 5
229 228 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 )
230 224 229 eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` 5 )
231 8 94 97 cats1fvn 
 |-  ( ( AA i^i RR ) e. _V -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` 5 ) = ( AA i^i RR ) )
232 9 231 ax-mp 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ` 5 ) = ( AA i^i RR )
233 230 232 eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) = ( AA i^i RR )
234 inss2 
 |-  ( AA i^i RR ) C_ RR
235 nnuz 
 |-  NN = ( ZZ>= ` 1 )
236 1zzd 
 |-  ( T. -> 1 e. ZZ )
237 id 
 |-  ( k e. NN -> k e. NN )
238 ovexd 
 |-  ( k e. NN -> ( 2 ^ -u ( ! ` k ) ) e. _V )
239 id 
 |-  ( a = k -> a = k )
240 239 fveq2d 
 |-  ( a = k -> ( ! ` a ) = ( ! ` k ) )
241 240 negeqd 
 |-  ( a = k -> -u ( ! ` a ) = -u ( ! ` k ) )
242 241 oveq2d 
 |-  ( a = k -> ( 2 ^ -u ( ! ` a ) ) = ( 2 ^ -u ( ! ` k ) ) )
243 eqid 
 |-  ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
244 242 243 fvmptg 
 |-  ( ( k e. NN /\ ( 2 ^ -u ( ! ` k ) ) e. _V ) -> ( ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ` k ) = ( 2 ^ -u ( ! ` k ) ) )
245 237 238 244 syl2anc 
 |-  ( k e. NN -> ( ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ` k ) = ( 2 ^ -u ( ! ` k ) ) )
246 245 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ` k ) = ( 2 ^ -u ( ! ` k ) ) )
247 157 a1i 
 |-  ( k e. NN -> 2 e. RR )
248 2ne0 
 |-  2 =/= 0
249 248 a1i 
 |-  ( k e. NN -> 2 =/= 0 )
250 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
251 250 faccld 
 |-  ( k e. NN -> ( ! ` k ) e. NN )
252 nnz 
 |-  ( ( ! ` k ) e. NN -> ( ! ` k ) e. ZZ )
253 znegcl 
 |-  ( ( ! ` k ) e. ZZ -> -u ( ! ` k ) e. ZZ )
254 251 252 253 3syl 
 |-  ( k e. NN -> -u ( ! ` k ) e. ZZ )
255 247 249 254 reexpclzd 
 |-  ( k e. NN -> ( 2 ^ -u ( ! ` k ) ) e. RR )
256 255 adantl 
 |-  ( ( T. /\ k e. NN ) -> ( 2 ^ -u ( ! ` k ) ) e. RR )
257 eqid 
 |-  ( n e. ( ZZ>= ` 1 ) |-> ( ( 2 ^ -u ( ! ` 1 ) ) x. ( ( 1 / 2 ) ^ ( n - 1 ) ) ) ) = ( n e. ( ZZ>= ` 1 ) |-> ( ( 2 ^ -u ( ! ` 1 ) ) x. ( ( 1 / 2 ) ^ ( n - 1 ) ) ) )
258 257 243 aaliou3lem3 
 |-  ( 1 e. NN -> ( seq 1 ( + , ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ) e. dom ~~> /\ sum_ b e. ( ZZ>= ` 1 ) ( ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ` b ) e. RR+ /\ sum_ b e. ( ZZ>= ` 1 ) ( ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ` b ) <_ ( 2 x. ( 2 ^ -u ( ! ` 1 ) ) ) ) )
259 258 simp1d 
 |-  ( 1 e. NN -> seq 1 ( + , ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ) e. dom ~~> )
260 28 259 mp1i 
 |-  ( T. -> seq 1 ( + , ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) ) ) e. dom ~~> )
261 235 236 246 256 260 isumrecl 
 |-  ( T. -> sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR )
262 261 mptru 
 |-  sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR
263 aaliou3 
 |-  sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e/ AA
264 df-nel 
 |-  ( sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e/ AA <-> -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. AA )
265 263 264 mpbi 
 |-  -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. AA
266 elinel1 
 |-  ( sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR ) -> sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. AA )
267 265 266 mto 
 |-  -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR )
268 262 267 pm3.2i 
 |-  ( sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR /\ -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. ( AA i^i RR ) )
269 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 ) )
270 234 268 269 mp2 
 |-  ( AA i^i RR ) C. RR
271 psseq1 
 |-  ( x = ( AA i^i RR ) -> ( x C. y <-> ( AA i^i RR ) C. y ) )
272 psseq2 
 |-  ( y = RR -> ( ( AA i^i RR ) C. y <-> ( AA i^i RR ) C. RR ) )
273 271 272 1 brabg 
 |-  ( ( ( AA i^i RR ) e. _V /\ RR e. _V ) -> ( ( AA i^i RR ) .< RR <-> ( AA i^i RR ) C. RR ) )
274 9 6 273 mp2an 
 |-  ( ( AA i^i RR ) .< RR <-> ( AA i^i RR ) C. RR )
275 270 274 mpbir 
 |-  ( AA i^i RR ) .< RR
276 233 275 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) .< RR
277 276 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) .< RR )
278 277 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ) .< RR ) )
279 7 221 278 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) "> ++ <" RR "> ) e. ( .< Chain _V ) )
280 5 279 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> e. ( .< Chain _V ) )
281 s7cli 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> e. Word _V
282 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 ) ) )
283 281 282 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 ) )
284 s7len 
 |-  ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) = 7
285 284 oveq1i 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) = ( 7 - 1 )
286 7m1e6 
 |-  ( 7 - 1 ) = 6
287 285 286 eqtri 
 |-  ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) = 6
288 287 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 )
289 5 222 225 cats1fvn 
 |-  ( RR e. _V -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` 6 ) = RR )
290 6 289 ax-mp 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` 6 ) = RR
291 288 290 eqtri 
 |-  ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ` ( ( # ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) - 1 ) ) = RR
292 283 291 eqtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) = RR
293 81 simpri 
 |-  ( QQ C. RR /\ RR C. CC )
294 293 simpri 
 |-  RR C. CC
295 psseq1 
 |-  ( x = RR -> ( x C. y <-> RR C. y ) )
296 psseq2 
 |-  ( y = CC -> ( RR C. y <-> RR C. CC ) )
297 295 296 1 brabg 
 |-  ( ( RR e. _V /\ CC e. _V ) -> ( RR .< CC <-> RR C. CC ) )
298 6 3 297 mp2an 
 |-  ( RR .< CC <-> RR C. CC )
299 294 298 mpbir 
 |-  RR .< CC
300 292 299 eqbrtri 
 |-  ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) .< CC
301 300 a1i 
 |-  ( T. -> ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) .< CC )
302 301 olcd 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> = (/) \/ ( lastS ` <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ) .< CC ) )
303 4 280 302 chnccats1 
 |-  ( T. -> ( <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR "> ++ <" CC "> ) e. ( .< Chain _V ) )
304 2 303 eqeltrid 
 |-  ( T. -> <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> e. ( .< Chain _V ) )
305 304 mptru 
 |-  <" { 1 } NN NN0 ZZ QQ ( AA i^i RR ) RR CC "> e. ( .< Chain _V )