pell14qrexpclnn0

		Ref	Expression
	Assertion	pell14qrexpclnn0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land B \in ℕ_{0}) \to A^{B} \in Pell14QR (D)$

Proof

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

Metamath Proof Explorer

Theorem pell14qrexpclnn0

Proof