pellex

Description: Every Pell equation has a nontrivial solution. Theorem 62 in vandenDries p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014)

		Ref	Expression
	Assertion	pellex	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1$

Proof

Step	Hyp	Ref	Expression
1		fzfi	$⊢ (0 \dots \|a\| - 1) \in Fin$
2		xpfi	$⊢ ((0 \dots \|a\| - 1) \in Fin \land (0 \dots \|a\| - 1) \in Fin) \to (0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1) \in Fin$
3	1 1 2	mp2an	$⊢ (0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1) \in Fin$
4		isfinite	$⊢ (0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1) \in Fin \leftrightarrow ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ ω$
5	3 4	mpbi	$⊢ ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ ω$
6		nnenom	$⊢ ℕ \approx ω$
7	6	ensymi	$⊢ ω \approx ℕ$
8		sdomentr	$⊢ (((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ ω \land ω \approx ℕ) \to ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ ℕ$
9	5 7 8	mp2an	$⊢ ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ ℕ$
10		ensym	$⊢ \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ \to ℕ \approx \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}$
11	10	ad2antll	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)) \to ℕ \approx \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}$
12		sdomentr	$⊢ (((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ ℕ \land ℕ \approx \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}) \to ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}$
13	9 11 12	sylancr	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)) \to ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) ≺ \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}$
14		opabssxp	$⊢ \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \subseteq ℕ \times ℕ$
15	14	sseli	$⊢ d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \to d \in (ℕ \times ℕ)$
16		simprrl	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to 1^{st} (d) \in ℕ$
17	16	nnzd	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to 1^{st} (d) \in ℤ$
18		simpllr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to a \in ℤ$
19		simplr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to a \neq 0$
20		nnabscl	$⊢ (a \in ℤ \land a \neq 0) \to \|a\| \in ℕ$
21	18 19 20	syl2anc	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to \|a\| \in ℕ$
22		zmodfz	$⊢ (1^{st} (d) \in ℤ \land \|a\| \in ℕ) \to 1^{st} (d) \mod \|a\| \in (0 \dots \|a\| - 1)$
23	17 21 22	syl2anc	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to 1^{st} (d) \mod \|a\| \in (0 \dots \|a\| - 1)$
24		simprrr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to 2^{nd} (d) \in ℕ$
25	24	nnzd	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to 2^{nd} (d) \in ℤ$
26		zmodfz	$⊢ (2^{nd} (d) \in ℤ \land \|a\| \in ℕ) \to 2^{nd} (d) \mod \|a\| \in (0 \dots \|a\| - 1)$
27	25 21 26	syl2anc	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to 2^{nd} (d) \mod \|a\| \in (0 \dots \|a\| - 1)$
28	23 27	jca	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))) \to (1^{st} (d) \mod \|a\| \in (0 \dots \|a\| - 1) \land 2^{nd} (d) \mod \|a\| \in (0 \dots \|a\| - 1))$
29	28	ex	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to ((d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ)) \to (1^{st} (d) \mod \|a\| \in (0 \dots \|a\| - 1) \land 2^{nd} (d) \mod \|a\| \in (0 \dots \|a\| - 1)))$
30		elxp7	$⊢ d \in (ℕ \times ℕ) \leftrightarrow (d \in (V \times V) \land (1^{st} (d) \in ℕ \land 2^{nd} (d) \in ℕ))$
31		opelxp	$⊢ ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ \in ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)) \leftrightarrow (1^{st} (d) \mod \|a\| \in (0 \dots \|a\| - 1) \land 2^{nd} (d) \mod \|a\| \in (0 \dots \|a\| - 1))$
32	29 30 31	3imtr4g	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to (d \in (ℕ \times ℕ) \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ \in ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)))$
33	15 32	syl5	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to (d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ \in ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1)))$
34	33	imp	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}) \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ \in ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1))$
35	34	adantlrr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)) \land d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}) \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ \in ((0 \dots \|a\| - 1) \times (0 \dots \|a\| - 1))$
36		fveq2	$⊢ d = e \to 1^{st} (d) = 1^{st} (e)$
37	36	oveq1d	$⊢ d = e \to 1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\|$
38		fveq2	$⊢ d = e \to 2^{nd} (d) = 2^{nd} (e)$
39	38	oveq1d	$⊢ d = e \to 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|$
40	37 39	opeq12d	$⊢ d = e \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩$
41	13 35 40	fphpd	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)) \to \exists d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \exists e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)$
42		eleq1w	$⊢ b = f \to (b \in ℕ \leftrightarrow f \in ℕ)$
43		eleq1w	$⊢ c = g \to (c \in ℕ \leftrightarrow g \in ℕ)$
44	42 43	bi2anan9	$⊢ (b = f \land c = g) \to ((b \in ℕ \land c \in ℕ) \leftrightarrow (f \in ℕ \land g \in ℕ))$
45		oveq1	$⊢ b = f \to b^{2} = f^{2}$
46		oveq1	$⊢ c = g \to c^{2} = g^{2}$
47	46	oveq2d	$⊢ c = g \to D c^{2} = D g^{2}$
48	45 47	oveqan12d	$⊢ (b = f \land c = g) \to b^{2} - D c^{2} = f^{2} - D g^{2}$
49	48	eqeq1d	$⊢ (b = f \land c = g) \to (b^{2} - D c^{2} = a \leftrightarrow f^{2} - D g^{2} = a)$
50	44 49	anbi12d	$⊢ (b = f \land c = g) \to (((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a) \leftrightarrow ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a))$
51	50	cbvopabv	$⊢ \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} = \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\}$
52	51	eleq2i	$⊢ e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \leftrightarrow e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\}$
53	52	biimpi	$⊢ e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \to e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\}$
54		elopab	$⊢ d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \leftrightarrow \exists b \exists c (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))$
55		elopab	$⊢ e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\} \leftrightarrow \exists f \exists g (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a))$
56		simp3ll	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)) \to b \in ℕ$
57	56	3expb	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to b \in ℕ$
58	57	3ad2ant1	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to b \in ℕ$
59		simp3lr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)) \to c \in ℕ$
60	59	3expb	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to c \in ℕ$
61	60	3ad2ant1	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to c \in ℕ$
62		simp1lr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to a \in ℤ$
63	62	3adant1r	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to a \in ℤ$
64		simp-4l	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to D \in ℕ$
65	64	3ad2ant1	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to D \in ℕ$
66		simp-4r	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to \neg \sqrt{D} \in ℚ$
67	66	3ad2ant1	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to \neg \sqrt{D} \in ℚ$
68		simp2ll	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to f \in ℕ$
69	68	3adant2l	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to f \in ℕ$
70		simp2lr	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to g \in ℕ$
71	70	3adant2l	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to g \in ℕ$
72		simp2l	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to e = ⟨f, g⟩$
73		simp1rl	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to d = ⟨b, c⟩$
74		simp3l	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to d \neq e$
75		simp3	$⊢ (e = ⟨f, g⟩ \land d = ⟨b, c⟩ \land d \neq e) \to d \neq e$
76		simp2	$⊢ (e = ⟨f, g⟩ \land d = ⟨b, c⟩ \land d \neq e) \to d = ⟨b, c⟩$
77		simp1	$⊢ (e = ⟨f, g⟩ \land d = ⟨b, c⟩ \land d \neq e) \to e = ⟨f, g⟩$
78	75 76 77	3netr3d	$⊢ (e = ⟨f, g⟩ \land d = ⟨b, c⟩ \land d \neq e) \to ⟨b, c⟩ \neq ⟨f, g⟩$
79		vex	$⊢ b \in V$
80		vex	$⊢ c \in V$
81	79 80	opth	$⊢ ⟨b, c⟩ = ⟨f, g⟩ \leftrightarrow (b = f \land c = g)$
82	81	necon3abii	$⊢ ⟨b, c⟩ \neq ⟨f, g⟩ \leftrightarrow \neg (b = f \land c = g)$
83	78 82	sylib	$⊢ (e = ⟨f, g⟩ \land d = ⟨b, c⟩ \land d \neq e) \to \neg (b = f \land c = g)$
84	72 73 74 83	syl3anc	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to \neg (b = f \land c = g)$
85		simp1lr	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to a \neq 0$
86		simp1rr	$⊢ ((d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to b^{2} - D c^{2} = a$
87	86	3adant1l	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to b^{2} - D c^{2} = a$
88		simp2rr	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to f^{2} - D g^{2} = a$
89		simp3r	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩$
90		simp3	$⊢ (d = ⟨b, c⟩ \land e = ⟨f, g⟩ \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩$
91		ovex	$⊢ 1^{st} (d) \mod \|a\| \in V$
92		ovex	$⊢ 2^{nd} (d) \mod \|a\| \in V$
93	91 92	opth	$⊢ ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩ \leftrightarrow (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)$
94	90 93	sylib	$⊢ (d = ⟨b, c⟩ \land e = ⟨f, g⟩ \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)$
95		simprl	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\|$
96		simpll	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to d = ⟨b, c⟩$
97	96	fveq2d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (d) = 1^{st} (⟨b, c⟩)$
98	79 80	op1st	$⊢ 1^{st} (⟨b, c⟩) = b$
99	97 98	eqtrdi	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (d) = b$
100	99	oveq1d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (d) \mod \|a\| = b \mod \|a\|$
101		simplr	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to e = ⟨f, g⟩$
102	101	fveq2d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (e) = 1^{st} (⟨f, g⟩)$
103		vex	$⊢ f \in V$
104		vex	$⊢ g \in V$
105	103 104	op1st	$⊢ 1^{st} (⟨f, g⟩) = f$
106	102 105	eqtrdi	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (e) = f$
107	106	oveq1d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 1^{st} (e) \mod \|a\| = f \mod \|a\|$
108	95 100 107	3eqtr3d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to b \mod \|a\| = f \mod \|a\|$
109		simprr	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|$
110	96	fveq2d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (d) = 2^{nd} (⟨b, c⟩)$
111	79 80	op2nd	$⊢ 2^{nd} (⟨b, c⟩) = c$
112	110 111	eqtrdi	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (d) = c$
113	112	oveq1d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (d) \mod \|a\| = c \mod \|a\|$
114	101	fveq2d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (e) = 2^{nd} (⟨f, g⟩)$
115	103 104	op2nd	$⊢ 2^{nd} (⟨f, g⟩) = g$
116	114 115	eqtrdi	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (e) = g$
117	116	oveq1d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to 2^{nd} (e) \mod \|a\| = g \mod \|a\|$
118	109 113 117	3eqtr3d	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to c \mod \|a\| = g \mod \|a\|$
119	108 118	jca	$⊢ ((d = ⟨b, c⟩ \land e = ⟨f, g⟩) \land (1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|)) \to (b \mod \|a\| = f \mod \|a\| \land c \mod \|a\| = g \mod \|a\|)$
120	119	ex	$⊢ (d = ⟨b, c⟩ \land e = ⟨f, g⟩) \to ((1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|) \to (b \mod \|a\| = f \mod \|a\| \land c \mod \|a\| = g \mod \|a\|))$
121	120	3adant3	$⊢ (d = ⟨b, c⟩ \land e = ⟨f, g⟩ \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to ((1^{st} (d) \mod \|a\| = 1^{st} (e) \mod \|a\| \land 2^{nd} (d) \mod \|a\| = 2^{nd} (e) \mod \|a\|) \to (b \mod \|a\| = f \mod \|a\| \land c \mod \|a\| = g \mod \|a\|))$
122	94 121	mpd	$⊢ (d = ⟨b, c⟩ \land e = ⟨f, g⟩ \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to (b \mod \|a\| = f \mod \|a\| \land c \mod \|a\| = g \mod \|a\|)$
123	73 72 89 122	syl3anc	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to (b \mod \|a\| = f \mod \|a\| \land c \mod \|a\| = g \mod \|a\|)$
124	123	simpld	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to b \mod \|a\| = f \mod \|a\|$
125	123	simprd	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to c \mod \|a\| = g \mod \|a\|$
126	58 61 63 65 67 69 71 84 85 87 88 124 125	pellexlem6	$⊢ (((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \land (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \land (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1$
127	126	3exp	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to ((e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1))$
128	127	exlimdvv	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to (\exists f \exists g (e = ⟨f, g⟩ \land ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)) \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1))$
129	55 128	syl5bi	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a))) \to (e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\} \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1))$
130	129	ex	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to ((d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)) \to (e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\} \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1)))$
131	130	exlimdvv	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to (\exists b \exists c (d = ⟨b, c⟩ \land ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)) \to (e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\} \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1)))$
132	54 131	syl5bi	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to (d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \to (e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\} \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1)))$
133	132	impd	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to ((d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \land e \in \{⟨f, g⟩ \| ((f \in ℕ \land g \in ℕ) \land f^{2} - D g^{2} = a)\}) \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1))$
134	53 133	sylan2i	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to ((d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \land e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\}) \to ((d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1))$
135	134	rexlimdvv	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \to (\exists d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \exists e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1)$
136	135	imp	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land a \neq 0) \land \exists d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \exists e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1$
137	136	adantlrr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)) \land \exists d \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \exists e \in \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} (d \neq e \land ⟨1^{st} (d) \mod \|a\|, 2^{nd} (d) \mod \|a\|⟩ = ⟨1^{st} (e) \mod \|a\|, 2^{nd} (e) \mod \|a\|⟩)) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1$
138	41 137	mpdan	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in ℤ) \land (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1$
139		pellexlem5	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists a \in ℤ (a \neq 0 \land \{⟨b, c⟩ \| ((b \in ℕ \land c \in ℕ) \land b^{2} - D c^{2} = a)\} \approx ℕ)$
140	138 139	r19.29a	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists x \in ℕ \exists y \in ℕ x^{2} - D y^{2} = 1$

Metamath Proof Explorer

Theorem pellex

Proof