Metamath Proof Explorer

Theorem pellexlem2

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem2 ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2<1+2⁢D

Proof

Step Hyp Ref Expression
1 simpl3 ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B∈ℕ
2 1 nnred ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B∈ℝ
3 2 resqcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2∈ℝ
4 2 sqge0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0≤B2
5 3 4 absidd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2=B2
6 5 eqcomd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2=B2
7 6 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2B2=A2−D⁢B2B2
8 simpl2 ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A∈ℕ
9 8 nncnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A∈ℂ
10 9 sqcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2∈ℂ
11 simpl1 ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D∈ℕ
12 11 nncnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D∈ℂ
13 1 nncnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B∈ℂ
14 13 sqcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2∈ℂ
15 12 14 mulcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D⁢B2∈ℂ
16 10 15 subcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2∈ℂ
17 1 nnne0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B≠0
18 sqne0 ⊢B∈ℂ→B2≠0↔B≠0
19 18 biimpar ⊢B∈ℂ∧B≠0→B2≠0
20 13 17 19 syl2anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2≠0
21 16 14 20 absdivd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2B2=A2−D⁢B2B2
22 7 21 eqtr4d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2B2=A2−D⁢B2B2
23 22 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢A2−D⁢B2B2=B2⁢A2−D⁢B2B2
24 16 abscld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2∈ℝ
25 24 recnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2∈ℂ
26 25 14 20 divcan2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢A2−D⁢B2B2=A2−D⁢B2
27 10 15 14 20 divsubdird ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2B2=A2B2−D⁢B2B2
28 9 13 17 sqdivd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB2=A2B2
29 28 eqcomd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2B2=AB2
30 11 nnred ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D∈ℝ
31 11 nnnn0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D∈ℕ0
32 31 nn0ge0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0≤D
33 remsqsqrt ⊢D∈ℝ∧0≤D→D⁢D=D
34 30 32 33 syl2anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D⁢D=D
35 30 32 resqrtcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D∈ℝ
36 35 recnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D∈ℂ
37 36 sqvald ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D2=D⁢D
38 12 14 20 divcan4d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D⁢B2B2=D
39 34 37 38 3eqtr4rd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D⁢B2B2=D2
40 29 39 oveq12d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2B2−D⁢B2B2=AB2−D2
41 9 13 17 divcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB∈ℂ
42 subsq ⊢AB∈ℂ∧D∈ℂ→AB2−D2=AB+D⁢AB−D
43 41 36 42 syl2anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB2−D2=AB+D⁢AB−D
44 41 36 addcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D∈ℂ
45 8 nnred ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A∈ℝ
46 45 1 nndivred ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB∈ℝ
47 46 35 resubcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D∈ℝ
48 47 recnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D∈ℂ
49 44 48 mulcomd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D⁢AB−D=AB−D⁢AB+D
50 43 49 eqtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB2−D2=AB−D⁢AB+D
51 27 40 50 3eqtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2B2=AB−D⁢AB+D
52 51 fveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2B2=AB−D⁢AB+D
53 52 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢A2−D⁢B2B2=B2⁢AB−D⁢AB+D
54 23 26 53 3eqtr3d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2=B2⁢AB−D⁢AB+D
55 48 44 absmuld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D⁢AB+D=AB−D⁢AB+D
56 55 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢AB−D⁢AB+D=B2⁢AB−D⁢AB+D
57 48 abscld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D∈ℝ
58 44 abscld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D∈ℝ
59 57 58 remulcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D⁢AB+D∈ℝ
60 3 59 remulcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢AB−D⁢AB+D∈ℝ
61 2nn0 ⊢2∈ℕ0
62 61 nn0negzi ⊢−2∈ℤ
63 62 a1i ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→−2∈ℤ
64 2 17 63 reexpclzd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B−2∈ℝ
65 64 58 remulcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B−2⁢AB+D∈ℝ
66 3 65 remulcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2⁢AB+D∈ℝ
67 1red ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1∈ℝ
68 2re ⊢2∈ℝ
69 68 a1i ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→2∈ℝ
70 69 35 remulcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→2⁢D∈ℝ
71 67 70 readdcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1+2⁢D∈ℝ
72 simpr ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D<B−2
73 8 nngt0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<A
74 1 nngt0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<B
75 45 2 73 74 divgt0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<AB
76 11 nngt0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<D
77 sqrtgt0 ⊢D∈ℝ∧0<D→0<D
78 30 76 77 syl2anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<D
79 46 35 75 78 addgt0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<AB+D
80 79 gt0ne0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D≠0
81 absgt0 ⊢AB+D∈ℂ→AB+D≠0↔0<AB+D
82 81 biimpa ⊢AB+D∈ℂ∧AB+D≠0→0<AB+D
83 44 80 82 syl2anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<AB+D
84 ltmul1 ⊢AB−D∈ℝ∧B−2∈ℝ∧AB+D∈ℝ∧0<AB+D→AB−D<B−2↔AB−D⁢AB+D<B−2⁢AB+D
85 57 64 58 83 84 syl112anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D<B−2↔AB−D⁢AB+D<B−2⁢AB+D
86 72 85 mpbid ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D⁢AB+D<B−2⁢AB+D
87 2 17 sqgt0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<B2
88 ltmul2 ⊢AB−D⁢AB+D∈ℝ∧B−2⁢AB+D∈ℝ∧B2∈ℝ∧0<B2→AB−D⁢AB+D<B−2⁢AB+D↔B2⁢AB−D⁢AB+D<B2⁢B−2⁢AB+D
89 59 65 3 87 88 syl112anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D⁢AB+D<B−2⁢AB+D↔B2⁢AB−D⁢AB+D<B2⁢B−2⁢AB+D
90 86 89 mpbid ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢AB−D⁢AB+D<B2⁢B−2⁢AB+D
91 13 17 63 expclzd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B−2∈ℂ
92 58 recnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D∈ℂ
93 mulass ⊢B2∈ℂ∧B−2∈ℂ∧AB+D∈ℂ→B2⁢B−2⁢AB+D=B2⁢B−2⁢AB+D
94 93 eqcomd ⊢B2∈ℂ∧B−2∈ℂ∧AB+D∈ℂ→B2⁢B−2⁢AB+D=B2⁢B−2⁢AB+D
95 14 91 92 94 syl3anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2⁢AB+D=B2⁢B−2⁢AB+D
96 expneg ⊢B∈ℂ∧2∈ℕ0→B−2=1B2
97 13 61 96 sylancl ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B−2=1B2
98 97 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2=B2⁢1B2
99 14 20 recidd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢1B2=1
100 98 99 eqtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2=1
101 100 oveq1d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2⁢AB+D=1⁢AB+D
102 92 mullidd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1⁢AB+D=AB+D
103 95 101 102 3eqtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2⁢AB+D=AB+D
104 41 36 addcomd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D=D+AB
105 ppncan ⊢D∈ℂ∧D∈ℂ∧AB∈ℂ→D+D+AB−D=D+AB
106 105 eqcomd ⊢D∈ℂ∧D∈ℂ∧AB∈ℂ→D+AB=D+D+AB−D
107 36 36 41 106 syl3anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D+AB=D+D+AB−D
108 36 36 addcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D+D∈ℂ
109 108 48 addcomd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D+D+AB−D=AB−D+D+D
110 2times ⊢D∈ℂ→2⁢D=D+D
111 110 eqcomd ⊢D∈ℂ→D+D=2⁢D
112 36 111 syl ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D+D=2⁢D
113 112 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D+D+D=AB-D+2⁢D
114 109 113 eqtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→D+D+AB−D=AB-D+2⁢D
115 104 107 114 3eqtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D=AB-D+2⁢D
116 115 fveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D=AB-D+2⁢D
117 47 70 readdcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB-D+2⁢D∈ℝ
118 117 recnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB-D+2⁢D∈ℂ
119 118 abscld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB-D+2⁢D∈ℝ
120 70 recnd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→2⁢D∈ℂ
121 120 abscld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→2⁢D∈ℝ
122 57 121 readdcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D+2⁢D∈ℝ
123 48 120 abstrid ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB-D+2⁢D≤AB−D+2⁢D
124 0le2 ⊢0≤2
125 124 a1i ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0≤2
126 30 32 sqrtge0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0≤D
127 69 35 125 126 mulge0d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0≤2⁢D
128 70 127 absidd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→2⁢D=2⁢D
129 128 oveq2d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D+2⁢D=AB−D+2⁢D
130 1 nnsqcld ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2∈ℕ
131 130 nnge1d ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1≤B2
132 0lt1 ⊢0<1
133 132 a1i ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→0<1
134 lerec ⊢1∈ℝ∧0<1∧B2∈ℝ∧0<B2→1≤B2↔1B2≤11
135 67 133 3 87 134 syl22anc ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1≤B2↔1B2≤11
136 131 135 mpbid ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1B2≤11
137 1div1e1 ⊢11=1
138 136 137 breqtrdi ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→1B2≤1
139 97 138 eqbrtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B−2≤1
140 57 64 67 72 139 ltletrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D<1
141 57 67 140 ltled ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D≤1
142 57 67 70 141 leadd1dd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D+2⁢D≤1+2⁢D
143 129 142 eqbrtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB−D+2⁢D≤1+2⁢D
144 119 122 71 123 143 letrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB-D+2⁢D≤1+2⁢D
145 116 144 eqbrtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→AB+D≤1+2⁢D
146 103 145 eqbrtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢B−2⁢AB+D≤1+2⁢D
147 60 66 71 90 146 ltletrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢AB−D⁢AB+D<1+2⁢D
148 56 147 eqbrtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→B2⁢AB−D⁢AB+D<1+2⁢D
149 54 148 eqbrtrd ⊢D∈ℕ∧A∈ℕ∧B∈ℕ∧AB−D<B−2→A2−D⁢B2<1+2⁢D