pell14qrexpcl

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

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

Proof

Step	Hyp	Ref	Expression
1		elznn0	$⊢ B \in ℤ \leftrightarrow (B \in ℝ \land (B \in ℕ_{0} \lor - B \in ℕ_{0}))$
2		simplll	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land B \in ℕ_{0}) \to D \in (ℕ ∖ ◻_{ℕ})$
3		simpllr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land B \in ℕ_{0}) \to A \in Pell14QR (D)$
4		simpr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land B \in ℕ_{0}) \to B \in ℕ_{0}$
5		pell14qrexpclnn0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land B \in ℕ_{0}) \to A^{B} \in Pell14QR (D)$
6	2 3 4 5	syl3anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land B \in ℕ_{0}) \to A^{B} \in Pell14QR (D)$
7		pell14qrre	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℝ$
8	7	recnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to A \in ℂ$
9	8	ad2antrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to A \in ℂ$
10		simplr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to B \in ℝ$
11	10	recnd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to B \in ℂ$
12		simpr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to - B \in ℕ_{0}$
13		expneg2	$⊢ (A \in ℂ \land B \in ℂ \land - B \in ℕ_{0}) \to A^{B} = \frac{1}{A^{- B}}$
14	9 11 12 13	syl3anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to A^{B} = \frac{1}{A^{- B}}$
15		simplll	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to D \in (ℕ ∖ ◻_{ℕ})$
16		simpllr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to A \in Pell14QR (D)$
17		pell14qrexpclnn0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land - B \in ℕ_{0}) \to A^{- B} \in Pell14QR (D)$
18	15 16 12 17	syl3anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to A^{- B} \in Pell14QR (D)$
19		pell14qrreccl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A^{- B} \in Pell14QR (D)) \to \frac{1}{A^{- B}} \in Pell14QR (D)$
20	15 18 19	syl2anc	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to \frac{1}{A^{- B}} \in Pell14QR (D)$
21	14 20	eqeltrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land - B \in ℕ_{0}) \to A^{B} \in Pell14QR (D)$
22	6 21	jaodan	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \land B \in ℝ) \land (B \in ℕ_{0} \lor - B \in ℕ_{0})) \to A^{B} \in Pell14QR (D)$
23	22	expl	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to ((B \in ℝ \land (B \in ℕ_{0} \lor - B \in ℕ_{0})) \to A^{B} \in Pell14QR (D))$
24	1 23	syl5bi	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to (B \in ℤ \to A^{B} \in Pell14QR (D))$
25	24	3impia	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D) \land B \in ℤ) \to A^{B} \in Pell14QR (D)$

Metamath Proof Explorer

Theorem pell14qrexpcl

Proof