Metamath Proof Explorer

Theorem rmxyval

Description: Main definition of the X and Y sequences. Compare definition 2.3 of JonesMatijasevic p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014)

Ref Expression
Assertion rmxyval ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด Xrm ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( ๐ด Yrm ๐‘ ) ) ) = ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) )

Proof

Step Hyp Ref Expression
1 rmxfval โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Xrm ๐‘ ) = ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) )
2 rmyfval โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐ด Yrm ๐‘ ) = ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) )
3 2 oveq2d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( ๐ด Yrm ๐‘ ) ) = ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) )
4 1 3 oveq12d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด Xrm ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( ๐ด Yrm ๐‘ ) ) ) = ( ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) ) )
5 rmxyelxp โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) โˆˆ ( โ„•0 ร— โ„ค ) )
6 fveq2 โŠข ( ๐‘Ž = ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) โ†’ ( 1st โ€˜ ๐‘Ž ) = ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) )
7 fveq2 โŠข ( ๐‘Ž = ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) โ†’ ( 2nd โ€˜ ๐‘Ž ) = ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) )
8 7 oveq2d โŠข ( ๐‘Ž = ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) โ†’ ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘Ž ) ) = ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) )
9 6 8 oveq12d โŠข ( ๐‘Ž = ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) โ†’ ( ( 1st โ€˜ ๐‘Ž ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘Ž ) ) ) = ( ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) ) )
10 fveq2 โŠข ( ๐‘ = ๐‘Ž โ†’ ( 1st โ€˜ ๐‘ ) = ( 1st โ€˜ ๐‘Ž ) )
11 fveq2 โŠข ( ๐‘ = ๐‘Ž โ†’ ( 2nd โ€˜ ๐‘ ) = ( 2nd โ€˜ ๐‘Ž ) )
12 11 oveq2d โŠข ( ๐‘ = ๐‘Ž โ†’ ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) = ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘Ž ) ) )
13 10 12 oveq12d โŠข ( ๐‘ = ๐‘Ž โ†’ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) = ( ( 1st โ€˜ ๐‘Ž ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘Ž ) ) ) )
14 13 cbvmptv โŠข ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) = ( ๐‘Ž โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘Ž ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘Ž ) ) ) )
15 ovex โŠข ( ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) ) โˆˆ V
16 9 14 15 fvmpt โŠข ( ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) โˆˆ ( โ„•0 ร— โ„ค ) โ†’ ( ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) = ( ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) ) )
17 5 16 syl โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) = ( ( 1st โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) ) ) )
18 rmxypairf1o โŠข ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) : ( โ„•0 ร— โ„ค ) โ€“1-1-ontoโ†’ { ๐‘Ž โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„ค ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ๐‘‘ ) ) } )
19 18 adantr โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) : ( โ„•0 ร— โ„ค ) โ€“1-1-ontoโ†’ { ๐‘Ž โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„ค ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ๐‘‘ ) ) } )
20 rmxyelqirr โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) โˆˆ { ๐‘Ž โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„ค ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ๐‘‘ ) ) } )
21 f1ocnvfv2 โŠข ( ( ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) : ( โ„•0 ร— โ„ค ) โ€“1-1-ontoโ†’ { ๐‘Ž โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„ค ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ๐‘‘ ) ) } โˆง ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) โˆˆ { ๐‘Ž โˆฃ โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘‘ โˆˆ โ„ค ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ๐‘‘ ) ) } ) โ†’ ( ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) = ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) )
22 19 20 21 syl2anc โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( โ—ก ( ๐‘ โˆˆ ( โ„•0 ร— โ„ค ) โ†ฆ ( ( 1st โ€˜ ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( 2nd โ€˜ ๐‘ ) ) ) ) โ€˜ ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) ) ) = ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) )
23 4 17 22 3eqtr2d โŠข ( ( ๐ด โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐ด Xrm ๐‘ ) + ( ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ยท ( ๐ด Yrm ๐‘ ) ) ) = ( ( ๐ด + ( โˆš โ€˜ ( ( ๐ด โ†‘ 2 ) โˆ’ 1 ) ) ) โ†‘ ๐‘ ) )