Metamath Proof Explorer

Theorem pell1234qrdich

Description: A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell1234qrdich ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 elpell1234qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
2 simp-4r ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ∈ ℝ )
3 oveq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
4 3 eqeq2d ⊢ ( 𝑐 = 𝑎 → ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↔ 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) )
5 oveq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
6 5 oveq1d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) )
7 6 eqeq1d ⊢ ( 𝑐 = 𝑎 → ( ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ↔ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
8 4 7 anbi12d ⊢ ( 𝑐 = 𝑎 → ( ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ↔ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) )
9 8 rexbidv ⊢ ( 𝑐 = 𝑎 → ( ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ↔ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) )
10 9 rspcev ⊢ ( ( 𝑎 ∈ ℕ0 ∧ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
11 10 adantll ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) )
12 elpell14qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
13 12 ad4antr ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
14 2 11 13 mpbir2and ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
15 14 orcd ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑎 ∈ ℕ0 ) ∧ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) )
16 15 exp31 ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑎 ∈ ℕ0 → ( ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) ) )
17 simp-5r ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 ∈ ℝ )
18 17 renegcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - 𝐴 ∈ ℝ )
19 simpllr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - 𝑎 ∈ ℕ0 )
20 znegcl ⊢ ( 𝑏 ∈ ℤ → - 𝑏 ∈ ℤ )
21 20 ad2antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - 𝑏 ∈ ℤ )
22 simprl ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
23 22 negeqd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - 𝐴 = - ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
24 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
25 24 ad4antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝑎 ∈ ℂ )
26 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
27 26 nncnd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℂ )
28 27 ad5antr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐷 ∈ ℂ )
29 28 sqrtcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( √ ‘ 𝐷 ) ∈ ℂ )
30 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
31 30 ad2antlr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝑏 ∈ ℂ )
32 29 31 mulcld ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℂ )
33 25 32 negdid ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( - 𝑎 + - ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
34 mulneg2 ⊢ ( ( ( √ ‘ 𝐷 ) ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( √ ‘ 𝐷 ) · - 𝑏 ) = - ( ( √ ‘ 𝐷 ) · 𝑏 ) )
35 34 eqcomd ⊢ ( ( ( √ ‘ 𝐷 ) ∈ ℂ ∧ 𝑏 ∈ ℂ ) → - ( ( √ ‘ 𝐷 ) · 𝑏 ) = ( ( √ ‘ 𝐷 ) · - 𝑏 ) )
36 29 31 35 syl2anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - ( ( √ ‘ 𝐷 ) · 𝑏 ) = ( ( √ ‘ 𝐷 ) · - 𝑏 ) )
37 36 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( - 𝑎 + - ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · - 𝑏 ) ) )
38 23 33 37 3eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · - 𝑏 ) ) )
39 sqneg ⊢ ( 𝑎 ∈ ℂ → ( - 𝑎 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
40 25 39 syl ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( - 𝑎 ↑ 2 ) = ( 𝑎 ↑ 2 ) )
41 sqneg ⊢ ( 𝑏 ∈ ℂ → ( - 𝑏 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
42 31 41 syl ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( - 𝑏 ↑ 2 ) = ( 𝑏 ↑ 2 ) )
43 42 oveq2d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝐷 · ( - 𝑏 ↑ 2 ) ) = ( 𝐷 · ( 𝑏 ↑ 2 ) ) )
44 40 43 oveq12d ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( - 𝑏 ↑ 2 ) ) ) = ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) )
45 simprr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 )
46 44 45 eqtrd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( - 𝑏 ↑ 2 ) ) ) = 1 )
47 oveq1 ⊢ ( 𝑐 = - 𝑎 → ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) )
48 47 eqeq2d ⊢ ( 𝑐 = - 𝑎 → ( - 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ↔ - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ) )
49 oveq1 ⊢ ( 𝑐 = - 𝑎 → ( 𝑐 ↑ 2 ) = ( - 𝑎 ↑ 2 ) )
50 49 oveq1d ⊢ ( 𝑐 = - 𝑎 → ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) )
51 50 eqeq1d ⊢ ( 𝑐 = - 𝑎 → ( ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ↔ ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) )
52 48 51 anbi12d ⊢ ( 𝑐 = - 𝑎 → ( ( - 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ↔ ( - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) )
53 oveq2 ⊢ ( 𝑑 = - 𝑏 → ( ( √ ‘ 𝐷 ) · 𝑑 ) = ( ( √ ‘ 𝐷 ) · - 𝑏 ) )
54 53 oveq2d ⊢ ( 𝑑 = - 𝑏 → ( - 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · - 𝑏 ) ) )
55 54 eqeq2d ⊢ ( 𝑑 = - 𝑏 → ( - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ↔ - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · - 𝑏 ) ) ) )
56 oveq1 ⊢ ( 𝑑 = - 𝑏 → ( 𝑑 ↑ 2 ) = ( - 𝑏 ↑ 2 ) )
57 56 oveq2d ⊢ ( 𝑑 = - 𝑏 → ( 𝐷 · ( 𝑑 ↑ 2 ) ) = ( 𝐷 · ( - 𝑏 ↑ 2 ) ) )
58 57 oveq2d ⊢ ( 𝑑 = - 𝑏 → ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( - 𝑏 ↑ 2 ) ) ) )
59 58 eqeq1d ⊢ ( 𝑑 = - 𝑏 → ( ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ↔ ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( - 𝑏 ↑ 2 ) ) ) = 1 ) )
60 55 59 anbi12d ⊢ ( 𝑑 = - 𝑏 → ( ( - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ↔ ( - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · - 𝑏 ) ) ∧ ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( - 𝑏 ↑ 2 ) ) ) = 1 ) ) )
61 52 60 rspc2ev ⊢ ( ( - 𝑎 ∈ ℕ0 ∧ - 𝑏 ∈ ℤ ∧ ( - 𝐴 = ( - 𝑎 + ( ( √ ‘ 𝐷 ) · - 𝑏 ) ) ∧ ( ( - 𝑎 ↑ 2 ) − ( 𝐷 · ( - 𝑏 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( - 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) )
62 19 21 38 46 61 syl112anc ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( - 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) )
63 elpell14qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( - 𝐴 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( - 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) )
64 63 ad5antr ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( - 𝐴 ∈ ℝ ∧ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( - 𝐴 = ( 𝑐 + ( ( √ ‘ 𝐷 ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( 𝐷 · ( 𝑑 ↑ 2 ) ) ) = 1 ) ) ) )
65 18 62 64 mpbir2and ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) )
66 65 olcd ⊢ ( ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) )
67 66 ex ⊢ ( ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) ∧ 𝑏 ∈ ℤ ) → ( ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
68 67 rexlimdva ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) ∧ - 𝑎 ∈ ℕ0 ) → ( ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
69 68 ex ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) → ( - 𝑎 ∈ ℕ0 → ( ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) ) )
70 elznn0 ⊢ ( 𝑎 ∈ ℤ ↔ ( 𝑎 ∈ ℝ ∧ ( 𝑎 ∈ ℕ0 ∨ - 𝑎 ∈ ℕ0 ) ) )
71 70 simprbi ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 ∈ ℕ0 ∨ - 𝑎 ∈ ℕ0 ) )
72 71 adantl ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑎 ∈ ℕ0 ∨ - 𝑎 ∈ ℕ0 ) )
73 16 69 72 mpjaod ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ 𝑎 ∈ ℤ ) → ( ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
74 73 rexlimdva ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
75 74 expimpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
76 1 75 sylbid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) ) )
77 76 imp ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell1234QR ‘ 𝐷 ) ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∨ - 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) )