Metamath Proof Explorer

Theorem pell14qrexpclnn0

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

Ref Expression
Assertion pell14qrexpclnn0 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑎 = 0 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 0 ) )
2 1 eleq1d ⊢ ( 𝑎 = 0 → ( ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ↑ 0 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
3 2 imbi2d ⊢ ( 𝑎 = 0 → ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 0 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
4 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 𝑏 ) )
5 4 eleq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
6 5 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
7 oveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ ( 𝑏 + 1 ) ) )
8 7 eleq1d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ↑ ( 𝑏 + 1 ) ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
9 8 imbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
10 oveq2 ⊢ ( 𝑎 = 𝐵 → ( 𝐴 ↑ 𝑎 ) = ( 𝐴 ↑ 𝐵 ) )
11 10 eleq1d ⊢ ( 𝑎 = 𝐵 → ( ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
12 11 imbi2d ⊢ ( 𝑎 = 𝐵 → ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑎 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ↔ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
13 pell14qrre ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℝ )
14 13 recnd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℂ )
15 14 exp0d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 0 ) = 1 )
16 pell14qrne0 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ≠ 0 )
17 14 16 dividd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 / 𝐴 ) = 1 )
18 15 17 eqtr4d ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 0 ) = ( 𝐴 / 𝐴 ) )
19 pell14qrdivcl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 / 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) )
20 19 3anidm23 ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 / 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) )
21 18 20 eqeltrd ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 0 ) ∈ ( Pell14QR ‘ 𝐷 ) )
22 14 3ad2ant2 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ℂ )
23 simp1 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝑏 ∈ ℕ0 )
24 22 23 expp1d ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) = ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) )
25 simp2l ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐷 ∈ ( ℕ ∖ ◻NN ) )
26 simp3 ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) )
27 simp2r ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
28 pell14qrmulcl ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) )
29 25 26 27 28 syl3anc ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( ( 𝐴 ↑ 𝑏 ) · 𝐴 ) ∈ ( Pell14QR ‘ 𝐷 ) )
30 24 29 eqeltrd ⊢ ( ( 𝑏 ∈ ℕ0 ∧ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ∧ ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) ∈ ( Pell14QR ‘ 𝐷 ) )
31 30 3exp ⊢ ( 𝑏 ∈ ℕ0 → ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
32 31 a2d ⊢ ( 𝑏 ∈ ℕ0 → ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝑏 ) ∈ ( Pell14QR ‘ 𝐷 ) ) → ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ ( 𝑏 + 1 ) ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
33 3 6 9 12 21 32 nn0ind ⊢ ( 𝐵 ∈ ℕ0 → ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) )
34 33 expdcom ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) → ( 𝐵 ∈ ℕ0 → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
35 34 3imp ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ ( Pell14QR ‘ 𝐷 ) )