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 ‘ 𝐷 ) ) )