Metamath Proof Explorer

Theorem pell14qrgt0

Description: A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pell14qrgt0 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 0 < 𝐴 )

Proof

Step Hyp Ref Expression
1 elpell14qr ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ↔ ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) ) )
2 0cnd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 ∈ ℂ )
3 eldifi ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → 𝐷 ∈ ℕ )
4 3 ad3antrrr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝐷 ∈ ℕ )
5 4 nnred ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝐷 ∈ ℝ )
6 4 nnnn0d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝐷 ∈ ℕ0 )
7 6 nn0ge0d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 ≤ 𝐷 )
8 5 7 resqrtcld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( √ ‘ 𝐷 ) ∈ ℝ )
9 zre ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℝ )
10 9 adantl ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℝ )
11 10 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝑏 ∈ ℝ )
12 8 11 remulcld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℝ )
13 12 recnd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℂ )
14 2 13 abssubd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( abs ‘ ( 0 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = ( abs ‘ ( ( ( √ ‘ 𝐷 ) · 𝑏 ) − 0 ) ) )
15 13 subid1d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( ( √ ‘ 𝐷 ) · 𝑏 ) − 0 ) = ( ( √ ‘ 𝐷 ) · 𝑏 ) )
16 15 fveq2d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( abs ‘ ( ( ( √ ‘ 𝐷 ) · 𝑏 ) − 0 ) ) = ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
17 14 16 eqtrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( abs ‘ ( 0 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) = ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
18 absresq ⊢ ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ∈ ℝ → ( ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) )
19 12 18 syl ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) )
20 5 recnd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝐷 ∈ ℂ )
21 20 sqrtcld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( √ ‘ 𝐷 ) ∈ ℂ )
22 10 recnd ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℂ )
23 22 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝑏 ∈ ℂ )
24 21 23 sqmuld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( ( √ ‘ 𝐷 ) · 𝑏 ) ↑ 2 ) = ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) )
25 20 sqsqrtd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( √ ‘ 𝐷 ) ↑ 2 ) = 𝐷 )
26 25 oveq1d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( ( √ ‘ 𝐷 ) ↑ 2 ) · ( 𝑏 ↑ 2 ) ) = ( 𝐷 · ( 𝑏 ↑ 2 ) ) )
27 19 24 26 3eqtrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↑ 2 ) = ( 𝐷 · ( 𝑏 ↑ 2 ) ) )
28 0lt1 ⊢ 0 < 1
29 simpr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 )
30 28 29 breqtrrid ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 < ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) )
31 11 resqcld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝑏 ↑ 2 ) ∈ ℝ )
32 5 31 remulcld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐷 · ( 𝑏 ↑ 2 ) ) ∈ ℝ )
33 nn0re ⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℝ )
34 33 adantr ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℝ )
35 34 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝑎 ∈ ℝ )
36 35 resqcld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝑎 ↑ 2 ) ∈ ℝ )
37 32 36 posdifd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( 𝐷 · ( 𝑏 ↑ 2 ) ) < ( 𝑎 ↑ 2 ) ↔ 0 < ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) ) )
38 30 37 mpbird ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝐷 · ( 𝑏 ↑ 2 ) ) < ( 𝑎 ↑ 2 ) )
39 27 38 eqbrtrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↑ 2 ) < ( 𝑎 ↑ 2 ) )
40 13 abscld ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∈ ℝ )
41 13 absge0d ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 ≤ ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
42 nn0ge0 ⊢ ( 𝑎 ∈ ℕ0 → 0 ≤ 𝑎 )
43 42 adantr ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) → 0 ≤ 𝑎 )
44 43 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 ≤ 𝑎 )
45 40 35 41 44 lt2sqd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) < 𝑎 ↔ ( ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ↑ 2 ) < ( 𝑎 ↑ 2 ) ) )
46 39 45 mpbird ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( abs ‘ ( ( √ ‘ 𝐷 ) · 𝑏 ) ) < 𝑎 )
47 17 46 eqbrtrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( abs ‘ ( 0 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) < 𝑎 )
48 0red ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 ∈ ℝ )
49 48 12 35 absdifltd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( abs ‘ ( 0 − ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ) < 𝑎 ↔ ( ( ( ( √ ‘ 𝐷 ) · 𝑏 ) − 𝑎 ) < 0 ∧ 0 < ( ( ( √ ‘ 𝐷 ) · 𝑏 ) + 𝑎 ) ) ) )
50 47 49 mpbid ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( ( ( ( √ ‘ 𝐷 ) · 𝑏 ) − 𝑎 ) < 0 ∧ 0 < ( ( ( √ ‘ 𝐷 ) · 𝑏 ) + 𝑎 ) ) )
51 50 simprd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 < ( ( ( √ ‘ 𝐷 ) · 𝑏 ) + 𝑎 ) )
52 nn0cn ⊢ ( 𝑎 ∈ ℕ0 → 𝑎 ∈ ℂ )
53 52 adantr ⊢ ( ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℂ )
54 53 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 𝑎 ∈ ℂ )
55 54 13 addcomd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) = ( ( ( √ ‘ 𝐷 ) · 𝑏 ) + 𝑎 ) )
56 51 55 breqtrrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 < ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
57 56 adantrl ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 0 < ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
58 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) )
59 57 58 breqtrrd ⊢ ( ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) ∧ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 0 < 𝐴 )
60 59 ex ⊢ ( ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) ∧ ( 𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 < 𝐴 ) )
61 60 rexlimdvva ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ℝ ) → ( ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) → 0 < 𝐴 ) )
62 61 expimpd ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( ( 𝐴 ∈ ℝ ∧ ∃ 𝑎 ∈ ℕ0 ∃ 𝑏 ∈ ℤ ( 𝐴 = ( 𝑎 + ( ( √ ‘ 𝐷 ) · 𝑏 ) ) ∧ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 ) ) → 0 < 𝐴 ) )
63 1 62 sylbid ⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) → 0 < 𝐴 ) )
64 63 imp ⊢ ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ) → 0 < 𝐴 )