# Metamath Proof Explorer

## Theorem pell14qrexpclnn0

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

Ref Expression
Assertion pell14qrexpclnn0 ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\wedge {B}\in {ℕ}_{0}\right)\to {{A}}^{{B}}\in \mathrm{Pell14QR}\left({D}\right)$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{a}=0\to {{A}}^{{a}}={{A}}^{0}$
2 1 eleq1d ${⊢}{a}=0\to \left({{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)↔{{A}}^{0}\in \mathrm{Pell14QR}\left({D}\right)\right)$
3 2 imbi2d ${⊢}{a}=0\to \left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)\right)↔\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{0}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
4 oveq2 ${⊢}{a}={b}\to {{A}}^{{a}}={{A}}^{{b}}$
5 4 eleq1d ${⊢}{a}={b}\to \left({{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)↔{{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)$
6 5 imbi2d ${⊢}{a}={b}\to \left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)\right)↔\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
7 oveq2 ${⊢}{a}={b}+1\to {{A}}^{{a}}={{A}}^{{b}+1}$
8 7 eleq1d ${⊢}{a}={b}+1\to \left({{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)↔{{A}}^{{b}+1}\in \mathrm{Pell14QR}\left({D}\right)\right)$
9 8 imbi2d ${⊢}{a}={b}+1\to \left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)\right)↔\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}+1}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
10 oveq2 ${⊢}{a}={B}\to {{A}}^{{a}}={{A}}^{{B}}$
11 10 eleq1d ${⊢}{a}={B}\to \left({{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)↔{{A}}^{{B}}\in \mathrm{Pell14QR}\left({D}\right)\right)$
12 11 imbi2d ${⊢}{a}={B}\to \left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{a}}\in \mathrm{Pell14QR}\left({D}\right)\right)↔\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{B}}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
13 pell14qrre ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {A}\in ℝ$
14 13 recnd ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {A}\in ℂ$
15 14 exp0d ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{0}=1$
16 pell14qrne0 ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {A}\ne 0$
17 14 16 dividd ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to \frac{{A}}{{A}}=1$
18 15 17 eqtr4d ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{0}=\frac{{A}}{{A}}$
19 pell14qrdivcl ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to \frac{{A}}{{A}}\in \mathrm{Pell14QR}\left({D}\right)$
20 19 3anidm23 ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to \frac{{A}}{{A}}\in \mathrm{Pell14QR}\left({D}\right)$
21 18 20 eqeltrd ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{0}\in \mathrm{Pell14QR}\left({D}\right)$
22 14 3ad2ant2 ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {A}\in ℂ$
23 simp1 ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {b}\in {ℕ}_{0}$
24 22 23 expp1d ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}+1}={{A}}^{{b}}{A}$
25 simp2l ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {D}\in \left(ℕ\setminus {◻}_{ℕ}\right)$
26 simp3 ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)$
27 simp2r ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {A}\in \mathrm{Pell14QR}\left({D}\right)$
28 pell14qrmulcl ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}}{A}\in \mathrm{Pell14QR}\left({D}\right)$
29 25 26 27 28 syl3anc ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}}{A}\in \mathrm{Pell14QR}\left({D}\right)$
30 24 29 eqeltrd ${⊢}\left({b}\in {ℕ}_{0}\wedge \left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\wedge {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}+1}\in \mathrm{Pell14QR}\left({D}\right)$
31 30 3exp ${⊢}{b}\in {ℕ}_{0}\to \left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to \left({{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\to {{A}}^{{b}+1}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
32 31 a2d ${⊢}{b}\in {ℕ}_{0}\to \left(\left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}}\in \mathrm{Pell14QR}\left({D}\right)\right)\to \left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{b}+1}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
33 3 6 9 12 21 32 nn0ind ${⊢}{B}\in {ℕ}_{0}\to \left(\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\right)\to {{A}}^{{B}}\in \mathrm{Pell14QR}\left({D}\right)\right)$
34 33 expdcom ${⊢}{D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\to \left({A}\in \mathrm{Pell14QR}\left({D}\right)\to \left({B}\in {ℕ}_{0}\to {{A}}^{{B}}\in \mathrm{Pell14QR}\left({D}\right)\right)\right)$
35 34 3imp ${⊢}\left({D}\in \left(ℕ\setminus {◻}_{ℕ}\right)\wedge {A}\in \mathrm{Pell14QR}\left({D}\right)\wedge {B}\in {ℕ}_{0}\right)\to {{A}}^{{B}}\in \mathrm{Pell14QR}\left({D}\right)$