pell14qrgt0 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pell14qrgt0		Structured version Visualization version GIF version

Theorem pell14qrgt0 42191

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

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

Proof of Theorem pell14qrgt0 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpell14qr 42181	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))))
2		0cnd 11223	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ∈ ℂ)
3		eldifi 4122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → 𝐷 ∈ ℕ)
4	3	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℕ)
5	4	nnred 12243	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℝ)
6	4	nnnn0d 12548	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℕ₀)
7	6	nn0ge0d 12551	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ≤ 𝐷)
8	5, 7	resqrtcld 15382	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (√‘𝐷) ∈ ℝ)
9		zre 12578	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℝ)
10	9	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℝ)
11	10	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈ ℝ)
12	8, 11	remulcld 11260	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((√‘𝐷) · 𝑏) ∈ ℝ)
13	12	recnd 11258	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((√‘𝐷) · 𝑏) ∈ ℂ)
14	2, 13	abssubd 15418	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(0 − ((√‘𝐷) · 𝑏))) = (abs‘(((√‘𝐷) · 𝑏) − 0)))
15	13	subid1d 11576	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (((√‘𝐷) · 𝑏) − 0) = ((√‘𝐷) · 𝑏))
16	15	fveq2d 6895	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(((√‘𝐷) · 𝑏) − 0)) = (abs‘((√‘𝐷) · 𝑏)))
17	14, 16	eqtrd 2767	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(0 − ((√‘𝐷) · 𝑏))) = (abs‘((√‘𝐷) · 𝑏)))
18		absresq 15267	. . . . . . . . . . . . . . . 16 ⊢ (((√‘𝐷) · 𝑏) ∈ ℝ → ((abs‘((√‘𝐷) · 𝑏))↑2) = (((√‘𝐷) · 𝑏)↑2))
19	12, 18	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((abs‘((√‘𝐷) · 𝑏))↑2) = (((√‘𝐷) · 𝑏)↑2))
20	5	recnd 11258	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝐷 ∈ ℂ)
21	20	sqrtcld 15402	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (√‘𝐷) ∈ ℂ)
22	10	recnd 11258	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ) → 𝑏 ∈ ℂ)
23	22	ad2antlr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑏 ∈ ℂ)
24	21, 23	sqmuld 14140	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (((√‘𝐷) · 𝑏)↑2) = (((√‘𝐷)↑2) · (𝑏↑2)))
25	20	sqsqrtd 15404	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((√‘𝐷)↑2) = 𝐷)
26	25	oveq1d 7429	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (((√‘𝐷)↑2) · (𝑏↑2)) = (𝐷 · (𝑏↑2)))
27	19, 24, 26	3eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((abs‘((√‘𝐷) · 𝑏))↑2) = (𝐷 · (𝑏↑2)))
28		0lt1 11752	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
29		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
30	28, 29	breqtrrid 5180	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < ((𝑎↑2) − (𝐷 · (𝑏↑2))))
31	11	resqcld 14107	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝑏↑2) ∈ ℝ)
32	5, 31	remulcld 11260	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) ∈ ℝ)
33		nn0re 12497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℕ₀ → 𝑎 ∈ ℝ)
34	33	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ) → 𝑎 ∈ ℝ)
35	34	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈ ℝ)
36	35	resqcld 14107	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝑎↑2) ∈ ℝ)
37	32, 36	posdifd 11817	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((𝐷 · (𝑏↑2)) < (𝑎↑2) ↔ 0 < ((𝑎↑2) − (𝐷 · (𝑏↑2)))))
38	30, 37	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐷 · (𝑏↑2)) < (𝑎↑2))
39	27, 38	eqbrtrd 5164	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((abs‘((√‘𝐷) · 𝑏))↑2) < (𝑎↑2))
40	13	abscld 15401	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘((√‘𝐷) · 𝑏)) ∈ ℝ)
41	13	absge0d 15409	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ≤ (abs‘((√‘𝐷) · 𝑏)))
42		nn0ge0 12513	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ ℕ₀ → 0 ≤ 𝑎)
43	42	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ) → 0 ≤ 𝑎)
44	43	ad2antlr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ≤ 𝑎)
45	40, 35, 41, 44	lt2sqd 14236	. . . . . . . . . . . . 13 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((abs‘((√‘𝐷) · 𝑏)) < 𝑎 ↔ ((abs‘((√‘𝐷) · 𝑏))↑2) < (𝑎↑2)))
46	39, 45	mpbird 257	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘((√‘𝐷) · 𝑏)) < 𝑎)
47	17, 46	eqbrtrd 5164	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (abs‘(0 − ((√‘𝐷) · 𝑏))) < 𝑎)
48		0red 11233	. . . . . . . . . . . 12 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 ∈ ℝ)
49	48, 12, 35	absdifltd 15398	. . . . . . . . . . 11 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((abs‘(0 − ((√‘𝐷) · 𝑏))) < 𝑎 ↔ ((((√‘𝐷) · 𝑏) − 𝑎) < 0 ∧ 0 < (((√‘𝐷) · 𝑏) + 𝑎))))
50	47, 49	mpbid 231	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → ((((√‘𝐷) · 𝑏) − 𝑎) < 0 ∧ 0 < (((√‘𝐷) · 𝑏) + 𝑎)))
51	50	simprd 495	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < (((√‘𝐷) · 𝑏) + 𝑎))
52		nn0cn 12498	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ ℕ₀ → 𝑎 ∈ ℂ)
53	52	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ) → 𝑎 ∈ ℂ)
54	53	ad2antlr 726	. . . . . . . . . 10 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 𝑎 ∈ ℂ)
55	54, 13	addcomd 11432	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝑎 + ((√‘𝐷) · 𝑏)) = (((√‘𝐷) · 𝑏) + 𝑎))
56	51, 55	breqtrrd 5170	. . . . . . . 8 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < (𝑎 + ((√‘𝐷) · 𝑏)))
57	56	adantrl 715	. . . . . . 7 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 0 < (𝑎 + ((√‘𝐷) · 𝑏)))
58		simprl 770	. . . . . . 7 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)))
59	57, 58	breqtrrd 5170	. . . . . 6 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 0 < 𝐴)
60	59	ex 412	. . . . 5 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ (𝑎 ∈ ℕ₀ ∧ 𝑏 ∈ ℤ)) → ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < 𝐴))
61	60	rexlimdvva 3206	. . . 4 ⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → 0 < 𝐴))
62	61	expimpd 453	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 0 < 𝐴))
63	1, 62	sylbid 239	. 2 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell14QR‘𝐷) → 0 < 𝐴))
64	63	imp 406	1 ⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1534 ∈ wcel 2099 ∃wrex 3065 ∖ cdif 3941 class class class wbr 5142 ‘cfv 6542 (class class class)co 7414 ℂcc 11122 ℝcr 11123 0cc0 11124 1c1 11125 + caddc 11127 · cmul 11129 < clt 11264 ≤ cle 11265 − cmin 11460 ℕcn 12228 2c2 12283 ℕ₀cn0 12488 ℤcz 12574 ↑cexp 14044 √csqrt 15198 abscabs 15199 ◻_NNcsquarenn 42168 Pell14QRcpell14qr 42171

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7732 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201 ax-pre-sup 11202

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7863 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-er 8716 df-en 8954 df-dom 8955 df-sdom 8956 df-sup 9451 df-pnf 11266 df-mnf 11267 df-xr 11268 df-ltxr 11269 df-le 11270 df-sub 11462 df-neg 11463 df-div 11888 df-nn 12229 df-2 12291 df-3 12292 df-n0 12489 df-z 12575 df-uz 12839 df-rp 12993 df-seq 13985 df-exp 14045 df-cj 15064 df-re 15065 df-im 15066 df-sqrt 15200 df-abs 15201 df-pell14qr 42175

This theorem is referenced by: pell14qrrp 42192 elpell14qr2 42194 elpell1qr2 42204 pellfundex 42218

W3C validator