# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({D}\in ℕ\wedge ¬\sqrt{{D}}\in ℚ\right)\to \exists {x}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{{x}}^{2}-{D}{{y}}^{2}=1$

### Proof

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