Metamath Proof Explorer

Theorem pell14qrexpclnn0

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

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( a = 0 -> ( A ^ a ) = ( A ^ 0 ) )
2 1 eleq1d 
 |-  ( a = 0 -> ( ( A ^ a ) e. ( Pell14QR ` D ) <-> ( A ^ 0 ) e. ( Pell14QR ` D ) ) )
3 2 imbi2d 
 |-  ( a = 0 -> ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ a ) e. ( Pell14QR ` D ) ) <-> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ 0 ) e. ( Pell14QR ` D ) ) ) )
4 oveq2 
 |-  ( a = b -> ( A ^ a ) = ( A ^ b ) )
5 4 eleq1d 
 |-  ( a = b -> ( ( A ^ a ) e. ( Pell14QR ` D ) <-> ( A ^ b ) e. ( Pell14QR ` D ) ) )
6 5 imbi2d 
 |-  ( a = b -> ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ a ) e. ( Pell14QR ` D ) ) <-> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ b ) e. ( Pell14QR ` D ) ) ) )
7 oveq2 
 |-  ( a = ( b + 1 ) -> ( A ^ a ) = ( A ^ ( b + 1 ) ) )
8 7 eleq1d 
 |-  ( a = ( b + 1 ) -> ( ( A ^ a ) e. ( Pell14QR ` D ) <-> ( A ^ ( b + 1 ) ) e. ( Pell14QR ` D ) ) )
9 8 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ a ) e. ( Pell14QR ` D ) ) <-> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ ( b + 1 ) ) e. ( Pell14QR ` D ) ) ) )
10 oveq2 
 |-  ( a = B -> ( A ^ a ) = ( A ^ B ) )
11 10 eleq1d 
 |-  ( a = B -> ( ( A ^ a ) e. ( Pell14QR ` D ) <-> ( A ^ B ) e. ( Pell14QR ` D ) ) )
12 11 imbi2d 
 |-  ( a = B -> ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ a ) e. ( Pell14QR ` D ) ) <-> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ B ) e. ( Pell14QR ` D ) ) ) )
13 pell14qrre 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. RR )
14 13 recnd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A e. CC )
15 14 exp0d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ 0 ) = 1 )
16 pell14qrne0 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> A =/= 0 )
17 14 16 dividd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A / A ) = 1 )
18 15 17 eqtr4d 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ 0 ) = ( A / A ) )
19 pell14qrdivcl 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ A e. ( Pell14QR ` D ) ) -> ( A / A ) e. ( Pell14QR ` D ) )
20 19 3anidm23 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A / A ) e. ( Pell14QR ` D ) )
21 18 20 eqeltrd 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ 0 ) e. ( Pell14QR ` D ) )
22 14 3ad2ant2 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> A e. CC )
23 simp1 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> b e. NN0 )
24 22 23 expp1d 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> ( A ^ ( b + 1 ) ) = ( ( A ^ b ) x. A ) )
25 simp2l 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> D e. ( NN \ []NN ) )
26 simp3 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> ( A ^ b ) e. ( Pell14QR ` D ) )
27 simp2r 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> A e. ( Pell14QR ` D ) )
28 pell14qrmulcl 
 |-  ( ( D e. ( NN \ []NN ) /\ ( A ^ b ) e. ( Pell14QR ` D ) /\ A e. ( Pell14QR ` D ) ) -> ( ( A ^ b ) x. A ) e. ( Pell14QR ` D ) )
29 25 26 27 28 syl3anc 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> ( ( A ^ b ) x. A ) e. ( Pell14QR ` D ) )
30 24 29 eqeltrd 
 |-  ( ( b e. NN0 /\ ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) /\ ( A ^ b ) e. ( Pell14QR ` D ) ) -> ( A ^ ( b + 1 ) ) e. ( Pell14QR ` D ) )
31 30 3exp 
 |-  ( b e. NN0 -> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( ( A ^ b ) e. ( Pell14QR ` D ) -> ( A ^ ( b + 1 ) ) e. ( Pell14QR ` D ) ) ) )
32 31 a2d 
 |-  ( b e. NN0 -> ( ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ b ) e. ( Pell14QR ` D ) ) -> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ ( b + 1 ) ) e. ( Pell14QR ` D ) ) ) )
33 3 6 9 12 21 32 nn0ind 
 |-  ( B e. NN0 -> ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) ) -> ( A ^ B ) e. ( Pell14QR ` D ) ) )
34 33 expdcom 
 |-  ( D e. ( NN \ []NN ) -> ( A e. ( Pell14QR ` D ) -> ( B e. NN0 -> ( A ^ B ) e. ( Pell14QR ` D ) ) ) )
35 34 3imp 
 |-  ( ( D e. ( NN \ []NN ) /\ A e. ( Pell14QR ` D ) /\ B e. NN0 ) -> ( A ^ B ) e. ( Pell14QR ` D ) )