| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elpell14qr 42865 | . . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))) | 
| 2 |  | 0cnd 11255 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ∈
ℂ) | 
| 3 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℕ) | 
| 4 | 3 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℕ) | 
| 5 | 4 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℝ) | 
| 6 | 4 | nnnn0d 12589 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈
ℕ0) | 
| 7 | 6 | nn0ge0d 12592 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ≤ 𝐷) | 
| 8 | 5, 7 | resqrtcld 15457 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (√‘𝐷) ∈
ℝ) | 
| 9 |  | zre 12619 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℝ) | 
| 10 | 9 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈ ℤ)
→ 𝑏 ∈
ℝ) | 
| 11 | 10 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈ ℝ) | 
| 12 | 8, 11 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((√‘𝐷) · 𝑏) ∈ ℝ) | 
| 13 | 12 | recnd 11290 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((√‘𝐷) · 𝑏) ∈ ℂ) | 
| 14 | 2, 13 | abssubd 15493 | . . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(0 −
((√‘𝐷) ·
𝑏))) =
(abs‘(((√‘𝐷) · 𝑏) − 0))) | 
| 15 | 13 | subid1d 11610 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (((√‘𝐷) · 𝑏) − 0) = ((√‘𝐷) · 𝑏)) | 
| 16 | 15 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
(abs‘(((√‘𝐷) · 𝑏) − 0)) =
(abs‘((√‘𝐷) · 𝑏))) | 
| 17 | 14, 16 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(0 −
((√‘𝐷) ·
𝑏))) =
(abs‘((√‘𝐷) · 𝑏))) | 
| 18 |  | absresq 15342 | . . . . . . . . . . . . . . . 16
⊢
(((√‘𝐷)
· 𝑏) ∈ ℝ
→ ((abs‘((√‘𝐷) · 𝑏))↑2) = (((√‘𝐷) · 𝑏)↑2)) | 
| 19 | 12, 18 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
((abs‘((√‘𝐷) · 𝑏))↑2) = (((√‘𝐷) · 𝑏)↑2)) | 
| 20 | 5 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℂ) | 
| 21 | 20 | sqrtcld 15477 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (√‘𝐷) ∈
ℂ) | 
| 22 | 10 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈ ℤ)
→ 𝑏 ∈
ℂ) | 
| 23 | 22 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈ ℂ) | 
| 24 | 21, 23 | sqmuld 14199 | . . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (((√‘𝐷) · 𝑏)↑2) = (((√‘𝐷)↑2) · (𝑏↑2))) | 
| 25 | 20 | sqsqrtd 15479 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((√‘𝐷)↑2) = 𝐷) | 
| 26 | 25 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (((√‘𝐷)↑2) · (𝑏↑2)) = (𝐷 · (𝑏↑2))) | 
| 27 | 19, 24, 26 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
((abs‘((√‘𝐷) · 𝑏))↑2) = (𝐷 · (𝑏↑2))) | 
| 28 |  | 0lt1 11786 | . . . . . . . . . . . . . . . 16
⊢ 0 <
1 | 
| 29 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) | 
| 30 | 28, 29 | breqtrrid 5180 | . . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < ((𝑎↑2) − (𝐷 · (𝑏↑2)))) | 
| 31 | 11 | resqcld 14166 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝑏↑2) ∈ ℝ) | 
| 32 | 5, 31 | remulcld 11292 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) ∈ ℝ) | 
| 33 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℝ) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈ ℤ)
→ 𝑎 ∈
ℝ) | 
| 35 | 34 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈ ℝ) | 
| 36 | 35 | resqcld 14166 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝑎↑2) ∈ ℝ) | 
| 37 | 32, 36 | posdifd 11851 | . . . . . . . . . . . . . . 15
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((𝐷 · (𝑏↑2)) < (𝑎↑2) ↔ 0 < ((𝑎↑2) − (𝐷 · (𝑏↑2))))) | 
| 38 | 30, 37 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) < (𝑎↑2)) | 
| 39 | 27, 38 | eqbrtrd 5164 | . . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
((abs‘((√‘𝐷) · 𝑏))↑2) < (𝑎↑2)) | 
| 40 | 13 | abscld 15476 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
(abs‘((√‘𝐷) · 𝑏)) ∈ ℝ) | 
| 41 | 13 | absge0d 15484 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ≤
(abs‘((√‘𝐷) · 𝑏))) | 
| 42 |  | nn0ge0 12553 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ ℕ0
→ 0 ≤ 𝑎) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈ ℤ)
→ 0 ≤ 𝑎) | 
| 44 | 43 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ≤ 𝑎) | 
| 45 | 40, 35, 41, 44 | lt2sqd 14296 | . . . . . . . . . . . . 13
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
((abs‘((√‘𝐷) · 𝑏)) < 𝑎 ↔ ((abs‘((√‘𝐷) · 𝑏))↑2) < (𝑎↑2))) | 
| 46 | 39, 45 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
(abs‘((√‘𝐷) · 𝑏)) < 𝑎) | 
| 47 | 17, 46 | eqbrtrd 5164 | . . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(0 −
((√‘𝐷) ·
𝑏))) < 𝑎) | 
| 48 |  | 0red 11265 | . . . . . . . . . . . 12
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ∈
ℝ) | 
| 49 | 48, 12, 35 | absdifltd 15473 | . . . . . . . . . . 11
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((abs‘(0 −
((√‘𝐷) ·
𝑏))) < 𝑎 ↔ ((((√‘𝐷) · 𝑏) − 𝑎) < 0 ∧ 0 < (((√‘𝐷) · 𝑏) + 𝑎)))) | 
| 50 | 47, 49 | mpbid 232 | . . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) →
((((√‘𝐷)
· 𝑏) − 𝑎) < 0 ∧ 0 <
(((√‘𝐷)
· 𝑏) + 𝑎))) | 
| 51 | 50 | simprd 495 | . . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 <
(((√‘𝐷)
· 𝑏) + 𝑎)) | 
| 52 |  | nn0cn 12538 | . . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℂ) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ ℕ0
∧ 𝑏 ∈ ℤ)
→ 𝑎 ∈
ℂ) | 
| 54 | 53 | ad2antlr 727 | . . . . . . . . . 10
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈ ℂ) | 
| 55 | 54, 13 | addcomd 11464 | . . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝑎 + ((√‘𝐷) · 𝑏)) = (((√‘𝐷) · 𝑏) + 𝑎)) | 
| 56 | 51, 55 | breqtrrd 5170 | . . . . . . . 8
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < (𝑎 + ((√‘𝐷) · 𝑏))) | 
| 57 | 56 | adantrl 716 | . . . . . . 7
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 0 < (𝑎 + ((√‘𝐷) · 𝑏))) | 
| 58 |  | simprl 770 | . . . . . . 7
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏))) | 
| 59 | 57, 58 | breqtrrd 5170 | . . . . . 6
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 0 < 𝐴) | 
| 60 | 59 | ex 412 | . . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ0 ∧ 𝑏 ∈ ℤ)) → ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < 𝐴)) | 
| 61 | 60 | rexlimdvva 3212 | . . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < 𝐴)) | 
| 62 | 61 | expimpd 453 | . . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 0 < 𝐴)) | 
| 63 | 1, 62 | sylbid 240 | . 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) → 0 < 𝐴)) | 
| 64 | 63 | imp 406 | 1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴) |