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 D ¬ D x y x 2 D y 2 = 1

Proof

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