Metamath Proof Explorer

Theorem pell14qrexpclnn0

Description: Lemma for pell14qrexpcl . (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrexpclnn0 ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) โˆง ๐ต โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐ต ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )

Proof

Step Hyp Ref Expression
1 oveq2 โŠข ( ๐‘Ž = 0 โ†’ ( ๐ด โ†‘ ๐‘Ž ) = ( ๐ด โ†‘ 0 ) )
2 1 eleq1d โŠข ( ๐‘Ž = 0 โ†’ ( ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†” ( ๐ด โ†‘ 0 ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) )
3 2 imbi2d โŠข ( ๐‘Ž = 0 โ†’ ( ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†” ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ 0 ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
4 oveq2 โŠข ( ๐‘Ž = ๐‘ โ†’ ( ๐ด โ†‘ ๐‘Ž ) = ( ๐ด โ†‘ ๐‘ ) )
5 4 eleq1d โŠข ( ๐‘Ž = ๐‘ โ†’ ( ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†” ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) )
6 5 imbi2d โŠข ( ๐‘Ž = ๐‘ โ†’ ( ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†” ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
7 oveq2 โŠข ( ๐‘Ž = ( ๐‘ + 1 ) โ†’ ( ๐ด โ†‘ ๐‘Ž ) = ( ๐ด โ†‘ ( ๐‘ + 1 ) ) )
8 7 eleq1d โŠข ( ๐‘Ž = ( ๐‘ + 1 ) โ†’ ( ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†” ( ๐ด โ†‘ ( ๐‘ + 1 ) ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) )
9 8 imbi2d โŠข ( ๐‘Ž = ( ๐‘ + 1 ) โ†’ ( ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†” ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ( ๐‘ + 1 ) ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
10 oveq2 โŠข ( ๐‘Ž = ๐ต โ†’ ( ๐ด โ†‘ ๐‘Ž ) = ( ๐ด โ†‘ ๐ต ) )
11 10 eleq1d โŠข ( ๐‘Ž = ๐ต โ†’ ( ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†” ( ๐ด โ†‘ ๐ต ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) )
12 11 imbi2d โŠข ( ๐‘Ž = ๐ต โ†’ ( ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘Ž ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†” ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐ต ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
13 pell14qrre โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐ด โˆˆ โ„ )
14 13 recnd โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐ด โˆˆ โ„‚ )
15 14 exp0d โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ 0 ) = 1 )
16 pell14qrne0 โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐ด โ‰  0 )
17 14 16 dividd โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด / ๐ด ) = 1 )
18 15 17 eqtr4d โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ 0 ) = ( ๐ด / ๐ด ) )
19 pell14qrdivcl โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด / ๐ด ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
20 19 3anidm23 โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด / ๐ด ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
21 18 20 eqeltrd โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ 0 ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
22 14 3ad2ant2 โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐ด โˆˆ โ„‚ )
23 simp1 โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐‘ โˆˆ โ„•0 )
24 22 23 expp1d โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ( ๐‘ + 1 ) ) = ( ( ๐ด โ†‘ ๐‘ ) ยท ๐ด ) )
25 simp2l โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) )
26 simp3 โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
27 simp2r โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) )
28 pell14qrmulcl โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ( ๐ด โ†‘ ๐‘ ) ยท ๐ด ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
29 25 26 27 28 syl3anc โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ( ๐ด โ†‘ ๐‘ ) ยท ๐ด ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
30 24 29 eqeltrd โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โˆง ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ( ๐‘ + 1 ) ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )
31 30 3exp โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†’ ( ๐ด โ†‘ ( ๐‘ + 1 ) ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
32 31 a2d โŠข ( ๐‘ โˆˆ โ„•0 โ†’ ( ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ( ๐‘ + 1 ) ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
33 3 6 9 12 21 32 nn0ind โŠข ( ๐ต โˆˆ โ„•0 โ†’ ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) ) โ†’ ( ๐ด โ†‘ ๐ต ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) )
34 33 expdcom โŠข ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โ†’ ( ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) โ†’ ( ๐ต โˆˆ โ„•0 โ†’ ( ๐ด โ†‘ ๐ต ) โˆˆ ( Pell14QR โ€˜ ๐ท ) ) ) )
35 34 3imp โŠข ( ( ๐ท โˆˆ ( โ„• โˆ– โ—ปNN ) โˆง ๐ด โˆˆ ( Pell14QR โ€˜ ๐ท ) โˆง ๐ต โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐ต ) โˆˆ ( Pell14QR โ€˜ ๐ท ) )