Metamath Proof Explorer


Theorem pellexlem3

Description: Lemma for pellex . To each good rational approximation of ( sqrtD ) , there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem3 D ¬ D x | 0 < x x D < denom x 2 y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D

Proof

Step Hyp Ref Expression
1 nnex V
2 1 1 xpex × V
3 opabssxp y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D ×
4 2 3 ssexi y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D V
5 simprl D ¬ D a 0 < a a D < denom a 2 a
6 simprrl D ¬ D a 0 < a a D < denom a 2 0 < a
7 qgt0numnn a 0 < a numer a
8 5 6 7 syl2anc D ¬ D a 0 < a a D < denom a 2 numer a
9 qdencl a denom a
10 5 9 syl D ¬ D a 0 < a a D < denom a 2 denom a
11 8 10 jca D ¬ D a 0 < a a D < denom a 2 numer a denom a
12 simpll D ¬ D a 0 < a a D < denom a 2 D
13 simplr D ¬ D a 0 < a a D < denom a 2 ¬ D
14 pellexlem1 D numer a denom a ¬ D numer a 2 D denom a 2 0
15 12 8 10 13 14 syl31anc D ¬ D a 0 < a a D < denom a 2 numer a 2 D denom a 2 0
16 simprrr D ¬ D a 0 < a a D < denom a 2 a D < denom a 2
17 qeqnumdivden a a = numer a denom a
18 17 oveq1d a a D = numer a denom a D
19 18 fveq2d a a D = numer a denom a D
20 19 breq1d a a D < denom a 2 numer a denom a D < denom a 2
21 5 20 syl D ¬ D a 0 < a a D < denom a 2 a D < denom a 2 numer a denom a D < denom a 2
22 16 21 mpbid D ¬ D a 0 < a a D < denom a 2 numer a denom a D < denom a 2
23 pellexlem2 D numer a denom a numer a denom a D < denom a 2 numer a 2 D denom a 2 < 1 + 2 D
24 12 8 10 22 23 syl31anc D ¬ D a 0 < a a D < denom a 2 numer a 2 D denom a 2 < 1 + 2 D
25 11 15 24 jca32 D ¬ D a 0 < a a D < denom a 2 numer a denom a numer a 2 D denom a 2 0 numer a 2 D denom a 2 < 1 + 2 D
26 25 ex D ¬ D a 0 < a a D < denom a 2 numer a denom a numer a 2 D denom a 2 0 numer a 2 D denom a 2 < 1 + 2 D
27 breq2 x = a 0 < x 0 < a
28 fvoveq1 x = a x D = a D
29 fveq2 x = a denom x = denom a
30 29 oveq1d x = a denom x 2 = denom a 2
31 28 30 breq12d x = a x D < denom x 2 a D < denom a 2
32 27 31 anbi12d x = a 0 < x x D < denom x 2 0 < a a D < denom a 2
33 32 elrab a x | 0 < x x D < denom x 2 a 0 < a a D < denom a 2
34 fvex numer a V
35 fvex denom a V
36 eleq1 y = numer a y numer a
37 36 anbi1d y = numer a y z numer a z
38 oveq1 y = numer a y 2 = numer a 2
39 38 oveq1d y = numer a y 2 D z 2 = numer a 2 D z 2
40 39 neeq1d y = numer a y 2 D z 2 0 numer a 2 D z 2 0
41 39 fveq2d y = numer a y 2 D z 2 = numer a 2 D z 2
42 41 breq1d y = numer a y 2 D z 2 < 1 + 2 D numer a 2 D z 2 < 1 + 2 D
43 40 42 anbi12d y = numer a y 2 D z 2 0 y 2 D z 2 < 1 + 2 D numer a 2 D z 2 0 numer a 2 D z 2 < 1 + 2 D
44 37 43 anbi12d y = numer a y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D numer a z numer a 2 D z 2 0 numer a 2 D z 2 < 1 + 2 D
45 eleq1 z = denom a z denom a
46 45 anbi2d z = denom a numer a z numer a denom a
47 oveq1 z = denom a z 2 = denom a 2
48 47 oveq2d z = denom a D z 2 = D denom a 2
49 48 oveq2d z = denom a numer a 2 D z 2 = numer a 2 D denom a 2
50 49 neeq1d z = denom a numer a 2 D z 2 0 numer a 2 D denom a 2 0
51 49 fveq2d z = denom a numer a 2 D z 2 = numer a 2 D denom a 2
52 51 breq1d z = denom a numer a 2 D z 2 < 1 + 2 D numer a 2 D denom a 2 < 1 + 2 D
53 50 52 anbi12d z = denom a numer a 2 D z 2 0 numer a 2 D z 2 < 1 + 2 D numer a 2 D denom a 2 0 numer a 2 D denom a 2 < 1 + 2 D
54 46 53 anbi12d z = denom a numer a z numer a 2 D z 2 0 numer a 2 D z 2 < 1 + 2 D numer a denom a numer a 2 D denom a 2 0 numer a 2 D denom a 2 < 1 + 2 D
55 34 35 44 54 opelopab numer a denom a y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D numer a denom a numer a 2 D denom a 2 0 numer a 2 D denom a 2 < 1 + 2 D
56 26 33 55 3imtr4g D ¬ D a x | 0 < x x D < denom x 2 numer a denom a y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D
57 ssrab2 x | 0 < x x D < denom x 2
58 simprl D ¬ D a x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2 a x | 0 < x x D < denom x 2
59 57 58 sseldi D ¬ D a x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2 a
60 simprr D ¬ D a x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2
61 57 60 sseldi D ¬ D a x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2 b
62 34 35 opth numer a denom a = numer b denom b numer a = numer b denom a = denom b
63 simprl a b numer a = numer b denom a = denom b numer a = numer b
64 simprr a b numer a = numer b denom a = denom b denom a = denom b
65 63 64 oveq12d a b numer a = numer b denom a = denom b numer a denom a = numer b denom b
66 simpll a b numer a = numer b denom a = denom b a
67 66 17 syl a b numer a = numer b denom a = denom b a = numer a denom a
68 simplr a b numer a = numer b denom a = denom b b
69 qeqnumdivden b b = numer b denom b
70 68 69 syl a b numer a = numer b denom a = denom b b = numer b denom b
71 65 67 70 3eqtr4d a b numer a = numer b denom a = denom b a = b
72 71 ex a b numer a = numer b denom a = denom b a = b
73 62 72 syl5bi a b numer a denom a = numer b denom b a = b
74 fveq2 a = b numer a = numer b
75 fveq2 a = b denom a = denom b
76 74 75 opeq12d a = b numer a denom a = numer b denom b
77 73 76 impbid1 a b numer a denom a = numer b denom b a = b
78 59 61 77 syl2anc D ¬ D a x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2 numer a denom a = numer b denom b a = b
79 78 ex D ¬ D a x | 0 < x x D < denom x 2 b x | 0 < x x D < denom x 2 numer a denom a = numer b denom b a = b
80 56 79 dom2d D ¬ D y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D V x | 0 < x x D < denom x 2 y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D
81 4 80 mpi D ¬ D x | 0 < x x D < denom x 2 y z | y z y 2 D z 2 0 y 2 D z 2 < 1 + 2 D