Metamath Proof Explorer

Theorem pell14qrexpcl

Description: Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrexpcl 
|- ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ZZ ) -> ( A ^ B ) e. ( Pell14QR ` D ) )

Proof

Step Hyp Ref Expression
1 elznn0 
 |-  ( B e. ZZ <-> ( B e. RR /\ ( B e. NN0 \/ -u B e. NN0 ) ) )
2 simplll 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ B e. NN0 ) -> D e. ( NN \ []NN ) )
3 simpllr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ B e. NN0 ) -> A e. ( Pell14QR ` D ) )
4 simpr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ B e. NN0 ) -> B e. NN0 )
5 pell14qrexpclnn0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. NN0 ) -> ( A ^ B ) e. ( Pell14QR ` D ) )
6 2 3 4 5 syl3anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ B e. NN0 ) -> ( A ^ B ) e. ( Pell14QR ` D ) )
7 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
8 7 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. CC )
9 8 ad2antrr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> A e. CC )
10 simplr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> B e. RR )
11 10 recnd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> B e. CC )
12 simpr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> -u B e. NN0 )
13 expneg2 
 |-  ( ( A e. CC /\ B e. CC /\ -u B e. NN0 ) -> ( A ^ B ) = ( 1 / ( A ^ -u B ) ) )
14 9 11 12 13 syl3anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> ( A ^ B ) = ( 1 / ( A ^ -u B ) ) )
15 simplll 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> D e. ( NN \ []NN ) )
16 simpllr 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> A e. ( Pell14QR ` D ) )
17 pell14qrexpclnn0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ -u B e. NN0 ) -> ( A ^ -u B ) e. ( Pell14QR ` D ) )
18 15 16 12 17 syl3anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> ( A ^ -u B ) e. ( Pell14QR ` D ) )
19 pell14qrreccl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A ^ -u B ) e. ( Pell14QR ` D ) ) -> ( 1 / ( A ^ -u B ) ) e. ( Pell14QR ` D ) )
20 15 18 19 syl2anc 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> ( 1 / ( A ^ -u B ) ) e. ( Pell14QR ` D ) )
21 14 20 eqeltrd 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ -u B e. NN0 ) -> ( A ^ B ) e. ( Pell14QR ` D ) )
22 6 21 jaodan 
 |-  ( ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ B e. RR ) /\ ( B e. NN0 \/ -u B e. NN0 ) ) -> ( A ^ B ) e. ( Pell14QR ` D ) )
23 22 expl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( B e. RR /\ ( B e. NN0 \/ -u B e. NN0 ) ) -> ( A ^ B ) e. ( Pell14QR ` D ) ) )
24 1 23 syl5bi 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( B e. ZZ -> ( A ^ B ) e. ( Pell14QR ` D ) ) )
25 24 3impia 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. ZZ ) -> ( A ^ B ) e. ( Pell14QR ` D ) )