Metamath Proof Explorer


Theorem pell14qrss1234

Description: A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrss1234 ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( Pell14QR โ€˜ ๐ท ) โІ ( Pell1234QR โ€˜ ๐ท ) )

Proof

Step Hyp Ref Expression
1 nn0z โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ค )
2 1 a1i โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ๐‘ โˆˆ โ„•0 โ†’ ๐‘ โˆˆ โ„ค ) )
3 2 anim1d โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ( ๐‘ โˆˆ โ„•0 โˆง โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) โ†’ ( ๐‘ โˆˆ โ„ค โˆง โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) ) )
4 3 reximdv2 โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) โ†’ โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) )
5 4 anim2d โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ( ๐‘Ž โˆˆ โ„ โˆง โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) โ†’ ( ๐‘Ž โˆˆ โ„ โˆง โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) ) )
6 elpell14qr โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ๐‘Ž โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†” ( ๐‘Ž โˆˆ โ„ โˆง โˆƒ ๐‘ โˆˆ โ„•0 โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) ) )
7 elpell1234qr โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ๐‘Ž โˆˆ ( Pell1234QR โ€˜ ๐ท ) โ†” ( ๐‘Ž โˆˆ โ„ โˆง โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค ( ๐‘Ž = ( ๐‘ + ( ( โˆš โ€˜ ๐ท ) ยท ๐‘ ) ) โˆง ( ( ๐‘ โ†‘ 2 ) โˆ’ ( ๐ท ยท ( ๐‘ โ†‘ 2 ) ) ) = 1 ) ) ) )
8 5 6 7 3imtr4d โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ๐‘Ž โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†’ ๐‘Ž โˆˆ ( Pell1234QR โ€˜ ๐ท ) ) )
9 8 ssrdv โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( Pell14QR โ€˜ ๐ท ) โІ ( Pell1234QR โ€˜ ๐ท ) )