pellexlem5 - Mathbox for Stefan O'Rear

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

Theorem pellexlem5 37397

Description: Lemma for pellex 37399. Invoking fiphp3d 37383, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.)

**Assertion**
Ref	Expression
pellexlem5	⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))

Distinct variable group: 𝑥,𝐷,𝑦,𝑧

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

Step	Hyp	Ref	Expression
1		pellexlem4 37396	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ)
2		fzfi 12771	. . . 4 ⊢ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin
3		diffi 8192	. . . 4 ⊢ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∈ Fin → ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∈ Fin)
4	2, 3	mp1i 13	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∈ Fin)
5		elopab 4983	. . . . 5 ⊢ (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
6		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑎) = (1^st ‘⟨𝑦, 𝑧⟩))
7	6	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑎)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
8		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑎) = (2^nd ‘⟨𝑦, 𝑧⟩))
9	8	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑎)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
10	9	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
11	7, 10	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
12		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
13		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑧 ∈ V
14	12, 13	op1st 7176	. . . . . . . . . . . 12 ⊢ (1^st ‘⟨𝑦, 𝑧⟩) = 𝑦
15	14	oveq1i 6660	. . . . . . . . . . 11 ⊢ ((1^st ‘⟨𝑦, 𝑧⟩)↑2) = (𝑦↑2)
16	12, 13	op2nd 7177	. . . . . . . . . . . . 13 ⊢ (2^nd ‘⟨𝑦, 𝑧⟩) = 𝑧
17	16	oveq1i 6660	. . . . . . . . . . . 12 ⊢ ((2^nd ‘⟨𝑦, 𝑧⟩)↑2) = (𝑧↑2)
18	17	oveq2i 6661	. . . . . . . . . . 11 ⊢ (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)) = (𝐷 · (𝑧↑2))
19	15, 18	oveq12i 6662	. . . . . . . . . 10 ⊢ (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2)))
20	11, 19	syl6eq 2672	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
21	20	ad2antrl 764	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = ((𝑦↑2) − (𝐷 · (𝑧↑2))))
22		simprrl 804	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
23		simpl 473	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝐷 ∈ ℕ)
24		simprr 796	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
25	24	ad2antll 765	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
26		nnz 11399	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
27	26	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑦 ∈ ℤ)
28		zsqcl 12934	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦↑2) ∈ ℤ)
29	27, 28	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑦↑2) ∈ ℤ)
30		nnz 11399	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℤ)
31	30	ad2antrl 764	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℤ)
32		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℕ)
33	32	nnzd 11481	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝑧 ∈ ℤ)
34		zsqcl 12934	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℤ → (𝑧↑2) ∈ ℤ)
35	33, 34	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝑧↑2) ∈ ℤ)
36	31, 35	zmulcld 11488	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (𝐷 · (𝑧↑2)) ∈ ℤ)
37	29, 36	zsubcld 11487	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ)
38		1re 10039	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
39		2re 11090	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
40		nnre 11027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℝ)
41	40	ad2antrl 764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℝ)
42		nnnn0 11299	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ ℕ → 𝐷 ∈ ℕ₀)
43	42	ad2antrl 764	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 𝐷 ∈ ℕ₀)
44	43	nn0ge0d 11354	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → 0 ≤ 𝐷)
45	41, 44	resqrtcld 14156	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (√‘𝐷) ∈ ℝ)
46		remulcl 10021	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℝ ∧ (√‘𝐷) ∈ ℝ) → (2 · (√‘𝐷)) ∈ ℝ)
47	39, 45, 46	sylancr 695	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (2 · (√‘𝐷)) ∈ ℝ)
48		readdcl 10019	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ (2 · (√‘𝐷)) ∈ ℝ) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
49	38, 47, 48	sylancr 695	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
50	49	flcld 12599	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
51	50	znegcld 11484	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ)
52	37	zred 11482	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ)
53	50	zred 11482	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ)
54		nn0abscl 14052	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
55	37, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℕ₀)
56	55	nn0zd 11480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ)
57	56	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℝ)
58		peano2re 10209	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
59	53, 58	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((⌊‘(1 + (2 · (√‘𝐷)))) + 1) ∈ ℝ)
60		simprr 796	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))
61		flltp1 12601	. . . . . . . . . . . . . . . 16 ⊢ ((1 + (2 · (√‘𝐷))) ∈ ℝ → (1 + (2 · (√‘𝐷))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
62	49, 61	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (1 + (2 · (√‘𝐷))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
63	57, 49, 59, 60, 62	lttrd 10198	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1))
64		zleltp1 11428	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
65	56, 50, 64	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < ((⌊‘(1 + (2 · (√‘𝐷)))) + 1)))
66	63, 65	mpbird 247	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))
67		absle 14055	. . . . . . . . . . . . . 14 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) → ((abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
68	67	biimpa 501	. . . . . . . . . . . . 13 ⊢ (((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℝ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℝ) ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
69	52, 53, 66, 68	syl21anc 1325	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷))))))
70		elfz 12332	. . . . . . . . . . . . 13 ⊢ ((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ ∧ -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) → (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ↔ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))))
71	70	biimpar 502	. . . . . . . . . . . 12 ⊢ (((((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ℤ ∧ -(⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ ∧ (⌊‘(1 + (2 · (√‘𝐷)))) ∈ ℤ) ∧ (-(⌊‘(1 + (2 · (√‘𝐷)))) ≤ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≤ (⌊‘(1 + (2 · (√‘𝐷)))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
72	37, 51, 50, 69, 71	syl31anc 1329	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝐷 ∈ ℕ ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
73	22, 23, 25, 72	syl12anc 1324	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℕ ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
74	73	adantlr 751	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))))
75		simprl 794	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
76	75	ad2antll 765	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0)
77		eldifsn 4317	. . . . . . . . 9 ⊢ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0))
78	74, 76, 77	sylanbrc 698	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
79	21, 78	eqeltrd 2701	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
80	79	ex 450	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
81	80	exlimdvv 1862	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (∃𝑦∃𝑧(𝑎 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
82	5, 81	syl5bi 232	. . . 4 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0})))
83	82	imp 445	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}))
84	1, 4, 83	fiphp3d 37383	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ)
85		eldif 3584	. . . . . 6 ⊢ (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ↔ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}))
86		elfzelz 12342	. . . . . . . 8 ⊢ (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → 𝑥 ∈ ℤ)
87		simp2 1062	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ∈ ℤ)
88		velsn 4193	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {0} ↔ 𝑥 = 0)
89	88	biimpri 218	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → 𝑥 ∈ {0})
90	89	necon3bi 2820	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ {0} → 𝑥 ≠ 0)
91	90	3ad2ant3 1084	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → 𝑥 ≠ 0)
92	87, 91	jca 554	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ 𝑥 ∈ ℤ ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))
93	92	3exp 1264	. . . . . . . 8 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ℤ → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
94	86, 93	syl5 34	. . . . . . 7 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) → (¬ 𝑥 ∈ {0} → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0))))
95	94	impd 447	. . . . . 6 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ (-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∧ ¬ 𝑥 ∈ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
96	85, 95	syl5bi 232	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) → (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)))
97		simp2l 1087	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ∈ ℤ)
98		simp2r 1088	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → 𝑥 ≠ 0)
99		nnex 11026	. . . . . . . . . . 11 ⊢ ℕ ∈ V
100	99, 99	xpex 6962	. . . . . . . . . 10 ⊢ (ℕ × ℕ) ∈ V
101		opabssxp 5193	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ)
102		ssdomg 8001	. . . . . . . . . 10 ⊢ ((ℕ × ℕ) ∈ V → ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ⊆ (ℕ × ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)))
103	100, 101, 102	mp2 9	. . . . . . . . 9 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ)
104		xpnnen 14939	. . . . . . . . 9 ⊢ (ℕ × ℕ) ≈ ℕ
105		domentr 8015	. . . . . . . . 9 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ (ℕ × ℕ) ∧ (ℕ × ℕ) ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ)
106	103, 104, 105	mp2an 708	. . . . . . . 8 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ
107		ensym 8005	. . . . . . . . . 10 ⊢ ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → ℕ ≈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥})
108	107	3ad2ant3 1084	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥})
109	100, 101	ssexi 4803	. . . . . . . . . 10 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V
110		fveq2 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → (1^st ‘𝑎) = (1^st ‘𝑏))
111	110	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → ((1^st ‘𝑎)↑2) = ((1^st ‘𝑏)↑2))
112		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑏 → (2^nd ‘𝑎) = (2^nd ‘𝑏))
113	112	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑏 → ((2^nd ‘𝑎)↑2) = ((2^nd ‘𝑏)↑2))
114	113	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑏 → (𝐷 · ((2^nd ‘𝑎)↑2)) = (𝐷 · ((2^nd ‘𝑏)↑2)))
115	111, 114	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
116	115	eqeq1d 2624	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → ((((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥 ↔ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
117	116	elrab 3363	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ↔ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥))
118		simprl 794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → 𝑏 = ⟨𝑦, 𝑧⟩)
119		simprrl 804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ))
120		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (1^st ‘𝑏) = (1^st ‘⟨𝑦, 𝑧⟩))
121	120	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((1^st ‘𝑏)↑2) = ((1^st ‘⟨𝑦, 𝑧⟩)↑2))
122		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (2^nd ‘𝑏) = (2^nd ‘⟨𝑦, 𝑧⟩))
123	122	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((2^nd ‘𝑏)↑2) = ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))
124	123	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (𝐷 · ((2^nd ‘𝑏)↑2)) = (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2)))
125	121, 124	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = (((1^st ‘⟨𝑦, 𝑧⟩)↑2) − (𝐷 · ((2^nd ‘⟨𝑦, 𝑧⟩)↑2))))
126	125, 19	syl6req 2673	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = ⟨𝑦, 𝑧⟩ → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
127	126	ad2antrl 764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))))
128		simplr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥)
129	127, 128	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)
130	118, 119, 129	jca32 558	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) ∧ (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷))))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
131	130	ex 450	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → ((𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → (𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
132	131	2eximdv 1848	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))) → ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥))))
133		elopab 4983	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))))
134		elopab 4983	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ↔ ∃𝑦∃𝑧(𝑏 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)))
135	132, 133, 134	3imtr4g 285	. . . . . . . . . . . . . . 15 ⊢ ((((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → (𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
136	135	expimpd 629	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (((((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥 ∧ 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
137	136	ancomsd 470	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → ((𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∧ (((1^st ‘𝑏)↑2) − (𝐷 · ((2^nd ‘𝑏)↑2))) = 𝑥) → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
138	117, 137	syl5bi 232	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → (𝑏 ∈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} → 𝑏 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
139	138	ssrdv 3609	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0)) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
140	139	3adant3 1081	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
141		ssdomg 8001	. . . . . . . . . 10 ⊢ ({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ∈ V → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ⊆ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}))
142	109, 140, 141	mpsyl 68	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
143		endomtr 8014	. . . . . . . . 9 ⊢ ((ℕ ≈ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
144	108, 142, 143	syl2anc 693	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)})
145		sbth 8080	. . . . . . . 8 ⊢ (({⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≼ ℕ ∧ ℕ ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)}) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
146	106, 144, 145	sylancr 695	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)
147	97, 98, 146	jca32 558	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) ∧ (𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))
148	147	3exp 1264	. . . . 5 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ ℤ ∧ 𝑥 ≠ 0) → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))))
149	96, 148	syld 47	. . . 4 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) → ({𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))))
150	149	impd 447	. . 3 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}) ∧ {𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ) → (𝑥 ∈ ℤ ∧ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))))
151	150	reximdv2 3014	. 2 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → (∃𝑥 ∈ ((-(⌊‘(1 + (2 · (√‘𝐷))))...(⌊‘(1 + (2 · (√‘𝐷))))) ∖ {0}){𝑎 ∈ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ∣ (((1^st ‘𝑎)↑2) − (𝐷 · ((2^nd ‘𝑎)↑2))) = 𝑥} ≈ ℕ → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)))
152	84, 151	mpd 15	1 ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ≠ wne 2794 ∃wrex 2913 {crab 2916 Vcvv 3200 ∖ cdif 3571 ⊆ wss 3574 {csn 4177 ⟨cop 4183 class class class wbr 4653 {copab 4712 × cxp 5112 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 ≈ cen 7952 ≼ cdom 7953 Fincfn 7955 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℚcq 11788 ...cfz 12326 ⌊cfl 12591 ↑cexp 12860 √csqrt 13973 abscabs 13974

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-ico 12181 df-fz 12327 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-dvds 14984 df-gcd 15217 df-numer 15443 df-denom 15444

This theorem is referenced by: pellex 37399

W3C validator