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 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 elznn0 ⊢ ( 𝐵 ∈ ℤ ↔ ( 𝐵 ∈ ℝ ∧ ( 𝐵 ∈ ℕ0 ∨ - 𝐵 ∈ ℕ0 ) ) )
2 simplll ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
3 simpllr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
4 simpr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℕ0 )
5 pell14qrexpclnn0 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
6 2 3 4 5 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
7 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℂ )
9 8 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
10 simplr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℝ )
11 10 recnd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
12 simpr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → - 𝐵 ∈ ℕ0 )
13 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
14 9 11 12 13 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
15 simplll ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
16 simpllr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
17 pell14qrexpclnn0 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
18 15 16 12 17 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
19 pell14qrreccl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ↑ - 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ ( Pell14QR ‘ 𝐷 ) )
20 15 18 19 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ ( Pell14QR ‘ 𝐷 ) )
21 14 20 eqeltrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
22 6 21 jaodan ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐵 ∈ ℕ0 ∨ - 𝐵 ∈ ℕ0 ) ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )
23 22 expl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( ( 𝐵 ∈ ℝ ∧ ( 𝐵 ∈ ℕ0 ∨ - 𝐵 ∈ ℕ0 ) ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
24 1 23 syl5bi ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐵 ∈ ℤ → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
25 24 3impia ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )