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≼yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D

Proof

Step Hyp Ref Expression
1 nnex ⊢ℕ∈V
2 1 1 xpex ⊢ℕ×ℕ∈V
3 opabssxp ⊢yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D⊆ℕ×ℕ
4 2 3 ssexi ⊢yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<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⁡a2−D⁢denom⁡a2≠0
15 12 8 10 13 14 syl31anc ⊢D∈ℕ∧¬D∈ℚ∧a∈ℚ∧0<a∧a−D<denom⁡a−2→numer⁡a2−D⁢denom⁡a2≠0
16 simprrr ⊢D∈ℕ∧¬D∈ℚ∧a∈ℚ∧0<a∧a−D<denom⁡a−2→a−D<denom⁡a−2
17 qeqnumdivden ⊢a∈ℚ→a=numer⁡adenom⁡a
18 17 oveq1d ⊢a∈ℚ→a−D=numer⁡adenom⁡a−D
19 18 fveq2d ⊢a∈ℚ→a−D=numer⁡adenom⁡a−D
20 19 breq1d ⊢a∈ℚ→a−D<denom⁡a−2↔numer⁡adenom⁡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⁡adenom⁡a−D<denom⁡a−2
22 16 21 mpbid ⊢D∈ℕ∧¬D∈ℚ∧a∈ℚ∧0<a∧a−D<denom⁡a−2→numer⁡adenom⁡a−D<denom⁡a−2
23 pellexlem2 ⊢D∈ℕ∧numer⁡a∈ℕ∧denom⁡a∈ℕ∧numer⁡adenom⁡a−D<denom⁡a−2→numer⁡a2−D⁢denom⁡a2<1+2⁢D
24 12 8 10 22 23 syl31anc ⊢D∈ℕ∧¬D∈ℚ∧a∈ℚ∧0<a∧a−D<denom⁡a−2→numer⁡a2−D⁢denom⁡a2<1+2⁢D
25 11 15 24 jca32 ⊢D∈ℕ∧¬D∈ℚ∧a∈ℚ∧0<a∧a−D<denom⁡a−2→numer⁡a∈ℕ∧denom⁡a∈ℕ∧numer⁡a2−D⁢denom⁡a2≠0∧numer⁡a2−D⁢denom⁡a2<1+2⁢D
26 25 ex ⊢D∈ℕ∧¬D∈ℚ→a∈ℚ∧0<a∧a−D<denom⁡a−2→numer⁡a∈ℕ∧denom⁡a∈ℕ∧numer⁡a2−D⁢denom⁡a2≠0∧numer⁡a2−D⁢denom⁡a2<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→y2=numer⁡a2
39 38 oveq1d ⊢y=numer⁡a→y2−D⁢z2=numer⁡a2−D⁢z2
40 39 neeq1d ⊢y=numer⁡a→y2−D⁢z2≠0↔numer⁡a2−D⁢z2≠0
41 39 fveq2d ⊢y=numer⁡a→y2−D⁢z2=numer⁡a2−D⁢z2
42 41 breq1d ⊢y=numer⁡a→y2−D⁢z2<1+2⁢D↔numer⁡a2−D⁢z2<1+2⁢D
43 40 42 anbi12d ⊢y=numer⁡a→y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D↔numer⁡a2−D⁢z2≠0∧numer⁡a2−D⁢z2<1+2⁢D
44 37 43 anbi12d ⊢y=numer⁡a→y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D↔numer⁡a∈ℕ∧z∈ℕ∧numer⁡a2−D⁢z2≠0∧numer⁡a2−D⁢z2<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→z2=denom⁡a2
48 47 oveq2d ⊢z=denom⁡a→D⁢z2=D⁢denom⁡a2
49 48 oveq2d ⊢z=denom⁡a→numer⁡a2−D⁢z2=numer⁡a2−D⁢denom⁡a2
50 49 neeq1d ⊢z=denom⁡a→numer⁡a2−D⁢z2≠0↔numer⁡a2−D⁢denom⁡a2≠0
51 49 fveq2d ⊢z=denom⁡a→numer⁡a2−D⁢z2=numer⁡a2−D⁢denom⁡a2
52 51 breq1d ⊢z=denom⁡a→numer⁡a2−D⁢z2<1+2⁢D↔numer⁡a2−D⁢denom⁡a2<1+2⁢D
53 50 52 anbi12d ⊢z=denom⁡a→numer⁡a2−D⁢z2≠0∧numer⁡a2−D⁢z2<1+2⁢D↔numer⁡a2−D⁢denom⁡a2≠0∧numer⁡a2−D⁢denom⁡a2<1+2⁢D
54 46 53 anbi12d ⊢z=denom⁡a→numer⁡a∈ℕ∧z∈ℕ∧numer⁡a2−D⁢z2≠0∧numer⁡a2−D⁢z2<1+2⁢D↔numer⁡a∈ℕ∧denom⁡a∈ℕ∧numer⁡a2−D⁢denom⁡a2≠0∧numer⁡a2−D⁢denom⁡a2<1+2⁢D
55 34 35 44 54 opelopab ⊢numer⁡adenom⁡a∈yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D↔numer⁡a∈ℕ∧denom⁡a∈ℕ∧numer⁡a2−D⁢denom⁡a2≠0∧numer⁡a2−D⁢denom⁡a2<1+2⁢D
56 26 33 55 3imtr4g ⊢D∈ℕ∧¬D∈ℚ→a∈x∈ℚ|0<x∧x−D<denom⁡x−2→numer⁡adenom⁡a∈yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<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 sselid ⊢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 sselid ⊢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⁡adenom⁡a=numer⁡bdenom⁡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⁡adenom⁡a=numer⁡bdenom⁡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⁡adenom⁡a
68 simplr ⊢a∈ℚ∧b∈ℚ∧numer⁡a=numer⁡b∧denom⁡a=denom⁡b→b∈ℚ
69 qeqnumdivden ⊢b∈ℚ→b=numer⁡bdenom⁡b
70 68 69 syl ⊢a∈ℚ∧b∈ℚ∧numer⁡a=numer⁡b∧denom⁡a=denom⁡b→b=numer⁡bdenom⁡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 biimtrid ⊢a∈ℚ∧b∈ℚ→numer⁡adenom⁡a=numer⁡bdenom⁡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⁡adenom⁡a=numer⁡bdenom⁡b
77 73 76 impbid1 ⊢a∈ℚ∧b∈ℚ→numer⁡adenom⁡a=numer⁡bdenom⁡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⁡adenom⁡a=numer⁡bdenom⁡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⁡adenom⁡a=numer⁡bdenom⁡b↔a=b
80 56 79 dom2d ⊢D∈ℕ∧¬D∈ℚ→yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D∈V→x∈ℚ|0<x∧x−D<denom⁡x−2≼yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D
81 4 80 mpi ⊢D∈ℕ∧¬D∈ℚ→x∈ℚ|0<x∧x−D<denom⁡x−2≼yz|y∈ℕ∧z∈ℕ∧y2−D⁢z2≠0∧y2−D⁢z2<1+2⁢D