Metamath Proof Explorer

Theorem jm2.27c

Description: Lemma for jm2.27 . Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses jm2.27a1 
|- ( ph -> A e. ( ZZ>= ` 2 ) )
jm2.27a2 
|- ( ph -> B e. NN )
jm2.27a3 
|- ( ph -> C e. NN )
jm2.27c4 
|- ( ph -> C = ( A rmY B ) )
jm2.27c5 
|- D = ( A rmX B )
jm2.27c6 
|- Q = ( B x. ( A rmY B ) )
jm2.27c7 
|- E = ( A rmY ( 2 x. Q ) )
jm2.27c8 
|- F = ( A rmX ( 2 x. Q ) )
jm2.27c9 
|- G = ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) )
jm2.27c10 
|- H = ( G rmY B )
jm2.27c11 
|- I = ( G rmX B )
jm2.27c12 
|- J = ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 )
Assertion jm2.27c 
|- ( ph -> ( ( ( D e. NN0 /\ E e. NN0 /\ F e. NN0 ) /\ ( G e. NN0 /\ H e. NN0 /\ I e. NN0 ) ) /\ ( J e. NN0 /\ ( ( ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 /\ G e. ( ZZ>= ` 2 ) ) /\ ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 /\ E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ F || ( G - A ) ) ) /\ ( ( ( 2 x. C ) || ( G - 1 ) /\ F || ( H - C ) ) /\ ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 jm2.27a1 
 |-  ( ph -> A e. ( ZZ>= ` 2 ) )
2 jm2.27a2 
 |-  ( ph -> B e. NN )
3 jm2.27a3 
 |-  ( ph -> C e. NN )
4 jm2.27c4 
 |-  ( ph -> C = ( A rmY B ) )
5 jm2.27c5 
 |-  D = ( A rmX B )
6 jm2.27c6 
 |-  Q = ( B x. ( A rmY B ) )
7 jm2.27c7 
 |-  E = ( A rmY ( 2 x. Q ) )
8 jm2.27c8 
 |-  F = ( A rmX ( 2 x. Q ) )
9 jm2.27c9 
 |-  G = ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) )
10 jm2.27c10 
 |-  H = ( G rmY B )
11 jm2.27c11 
 |-  I = ( G rmX B )
12 jm2.27c12 
 |-  J = ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 )
13 2 nnzd 
 |-  ( ph -> B e. ZZ )
14 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
15 14 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( A rmX B ) e. NN0 )
16 1 13 15 syl2anc 
 |-  ( ph -> ( A rmX B ) e. NN0 )
17 5 16 eqeltrid 
 |-  ( ph -> D e. NN0 )
18 2z 
 |-  2 e. ZZ
19 3 nnzd 
 |-  ( ph -> C e. ZZ )
20 4 19 eqeltrrd 
 |-  ( ph -> ( A rmY B ) e. ZZ )
21 13 20 zmulcld 
 |-  ( ph -> ( B x. ( A rmY B ) ) e. ZZ )
22 6 21 eqeltrid 
 |-  ( ph -> Q e. ZZ )
23 zmulcl 
 |-  ( ( 2 e. ZZ /\ Q e. ZZ ) -> ( 2 x. Q ) e. ZZ )
24 18 22 23 sylancr 
 |-  ( ph -> ( 2 x. Q ) e. ZZ )
25 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
26 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. Q ) e. ZZ ) -> ( A rmY ( 2 x. Q ) ) e. ZZ )
27 1 24 26 syl2anc 
 |-  ( ph -> ( A rmY ( 2 x. Q ) ) e. ZZ )
28 rmy0 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) = 0 )
29 1 28 syl 
 |-  ( ph -> ( A rmY 0 ) = 0 )
30 2nn 
 |-  2 e. NN
31 4 3 eqeltrrd 
 |-  ( ph -> ( A rmY B ) e. NN )
32 2 31 nnmulcld 
 |-  ( ph -> ( B x. ( A rmY B ) ) e. NN )
33 6 32 eqeltrid 
 |-  ( ph -> Q e. NN )
34 nnmulcl 
 |-  ( ( 2 e. NN /\ Q e. NN ) -> ( 2 x. Q ) e. NN )
35 30 33 34 sylancr 
 |-  ( ph -> ( 2 x. Q ) e. NN )
36 35 nnnn0d 
 |-  ( ph -> ( 2 x. Q ) e. NN0 )
37 36 nn0ge0d 
 |-  ( ph -> 0 <_ ( 2 x. Q ) )
38 0zd 
 |-  ( ph -> 0 e. ZZ )
39 lermy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ ( 2 x. Q ) e. ZZ ) -> ( 0 <_ ( 2 x. Q ) <-> ( A rmY 0 ) <_ ( A rmY ( 2 x. Q ) ) ) )
40 1 38 24 39 syl3anc 
 |-  ( ph -> ( 0 <_ ( 2 x. Q ) <-> ( A rmY 0 ) <_ ( A rmY ( 2 x. Q ) ) ) )
41 37 40 mpbid 
 |-  ( ph -> ( A rmY 0 ) <_ ( A rmY ( 2 x. Q ) ) )
42 29 41 eqbrtrrd 
 |-  ( ph -> 0 <_ ( A rmY ( 2 x. Q ) ) )
43 elnn0z 
 |-  ( ( A rmY ( 2 x. Q ) ) e. NN0 <-> ( ( A rmY ( 2 x. Q ) ) e. ZZ /\ 0 <_ ( A rmY ( 2 x. Q ) ) ) )
44 27 42 43 sylanbrc 
 |-  ( ph -> ( A rmY ( 2 x. Q ) ) e. NN0 )
45 7 44 eqeltrid 
 |-  ( ph -> E e. NN0 )
46 14 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. Q ) e. ZZ ) -> ( A rmX ( 2 x. Q ) ) e. NN0 )
47 1 24 46 syl2anc 
 |-  ( ph -> ( A rmX ( 2 x. Q ) ) e. NN0 )
48 8 47 eqeltrid 
 |-  ( ph -> F e. NN0 )
49 17 45 48 3jca 
 |-  ( ph -> ( D e. NN0 /\ E e. NN0 /\ F e. NN0 ) )
50 2nn0 
 |-  2 e. NN0
51 48 nn0cnd 
 |-  ( ph -> F e. CC )
52 51 sqvald 
 |-  ( ph -> ( F ^ 2 ) = ( F x. F ) )
53 48 48 nn0mulcld 
 |-  ( ph -> ( F x. F ) e. NN0 )
54 52 53 eqeltrd 
 |-  ( ph -> ( F ^ 2 ) e. NN0 )
55 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
56 1 55 syl 
 |-  ( ph -> A e. NN )
57 56 nnnn0d 
 |-  ( ph -> A e. NN0 )
58 57 nn0red 
 |-  ( ph -> A e. RR )
59 48 nn0red 
 |-  ( ph -> F e. RR )
60 59 59 remulcld 
 |-  ( ph -> ( F x. F ) e. RR )
61 rmx1 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) = A )
62 1 61 syl 
 |-  ( ph -> ( A rmX 1 ) = A )
63 35 nnge1d 
 |-  ( ph -> 1 <_ ( 2 x. Q ) )
64 1nn0 
 |-  1 e. NN0
65 64 a1i 
 |-  ( ph -> 1 e. NN0 )
66 lermxnn0 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. NN0 /\ ( 2 x. Q ) e. NN0 ) -> ( 1 <_ ( 2 x. Q ) <-> ( A rmX 1 ) <_ ( A rmX ( 2 x. Q ) ) ) )
67 1 65 36 66 syl3anc 
 |-  ( ph -> ( 1 <_ ( 2 x. Q ) <-> ( A rmX 1 ) <_ ( A rmX ( 2 x. Q ) ) ) )
68 63 67 mpbid 
 |-  ( ph -> ( A rmX 1 ) <_ ( A rmX ( 2 x. Q ) ) )
69 62 68 eqbrtrrd 
 |-  ( ph -> A <_ ( A rmX ( 2 x. Q ) ) )
70 69 8 breqtrrdi 
 |-  ( ph -> A <_ F )
71 48 nn0ge0d 
 |-  ( ph -> 0 <_ F )
72 rmxnn 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. Q ) e. ZZ ) -> ( A rmX ( 2 x. Q ) ) e. NN )
73 1 24 72 syl2anc 
 |-  ( ph -> ( A rmX ( 2 x. Q ) ) e. NN )
74 8 73 eqeltrid 
 |-  ( ph -> F e. NN )
75 74 nnge1d 
 |-  ( ph -> 1 <_ F )
76 59 59 71 75 lemulge12d 
 |-  ( ph -> F <_ ( F x. F ) )
77 58 59 60 70 76 letrd 
 |-  ( ph -> A <_ ( F x. F ) )
78 77 52 breqtrrd 
 |-  ( ph -> A <_ ( F ^ 2 ) )
79 nn0sub 
 |-  ( ( A e. NN0 /\ ( F ^ 2 ) e. NN0 ) -> ( A <_ ( F ^ 2 ) <-> ( ( F ^ 2 ) - A ) e. NN0 ) )
80 57 54 79 syl2anc 
 |-  ( ph -> ( A <_ ( F ^ 2 ) <-> ( ( F ^ 2 ) - A ) e. NN0 ) )
81 78 80 mpbid 
 |-  ( ph -> ( ( F ^ 2 ) - A ) e. NN0 )
82 54 81 nn0mulcld 
 |-  ( ph -> ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) e. NN0 )
83 uzaddcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) e. NN0 ) -> ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) )
84 1 82 83 syl2anc 
 |-  ( ph -> ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) )
85 9 84 eqeltrid 
 |-  ( ph -> G e. ( ZZ>= ` 2 ) )
86 eluznn0 
 |-  ( ( 2 e. NN0 /\ G e. ( ZZ>= ` 2 ) ) -> G e. NN0 )
87 50 85 86 sylancr 
 |-  ( ph -> G e. NN0 )
88 25 fovcl 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( G rmY B ) e. ZZ )
89 85 13 88 syl2anc 
 |-  ( ph -> ( G rmY B ) e. ZZ )
90 rmy0 
 |-  ( G e. ( ZZ>= ` 2 ) -> ( G rmY 0 ) = 0 )
91 85 90 syl 
 |-  ( ph -> ( G rmY 0 ) = 0 )
92 2 nnnn0d 
 |-  ( ph -> B e. NN0 )
93 92 nn0ge0d 
 |-  ( ph -> 0 <_ B )
94 lermy 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ B e. ZZ ) -> ( 0 <_ B <-> ( G rmY 0 ) <_ ( G rmY B ) ) )
95 85 38 13 94 syl3anc 
 |-  ( ph -> ( 0 <_ B <-> ( G rmY 0 ) <_ ( G rmY B ) ) )
96 93 95 mpbid 
 |-  ( ph -> ( G rmY 0 ) <_ ( G rmY B ) )
97 91 96 eqbrtrrd 
 |-  ( ph -> 0 <_ ( G rmY B ) )
98 elnn0z 
 |-  ( ( G rmY B ) e. NN0 <-> ( ( G rmY B ) e. ZZ /\ 0 <_ ( G rmY B ) ) )
99 89 97 98 sylanbrc 
 |-  ( ph -> ( G rmY B ) e. NN0 )
100 10 99 eqeltrid 
 |-  ( ph -> H e. NN0 )
101 14 fovcl 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( G rmX B ) e. NN0 )
102 85 13 101 syl2anc 
 |-  ( ph -> ( G rmX B ) e. NN0 )
103 11 102 eqeltrid 
 |-  ( ph -> I e. NN0 )
104 87 100 103 3jca 
 |-  ( ph -> ( G e. NN0 /\ H e. NN0 /\ I e. NN0 ) )
105 zsqcl 
 |-  ( ( A rmY B ) e. ZZ -> ( ( A rmY B ) ^ 2 ) e. ZZ )
106 20 105 syl 
 |-  ( ph -> ( ( A rmY B ) ^ 2 ) e. ZZ )
107 zmulcl 
 |-  ( ( 2 e. ZZ /\ ( ( A rmY B ) ^ 2 ) e. ZZ ) -> ( 2 x. ( ( A rmY B ) ^ 2 ) ) e. ZZ )
108 18 106 107 sylancr 
 |-  ( ph -> ( 2 x. ( ( A rmY B ) ^ 2 ) ) e. ZZ )
109 25 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ Q e. ZZ ) -> ( A rmY Q ) e. ZZ )
110 1 22 109 syl2anc 
 |-  ( ph -> ( A rmY Q ) e. ZZ )
111 zmulcl 
 |-  ( ( 2 e. ZZ /\ ( A rmY Q ) e. ZZ ) -> ( 2 x. ( A rmY Q ) ) e. ZZ )
112 18 110 111 sylancr 
 |-  ( ph -> ( 2 x. ( A rmY Q ) ) e. ZZ )
113 iddvds 
 |-  ( ( B x. ( A rmY B ) ) e. ZZ -> ( B x. ( A rmY B ) ) || ( B x. ( A rmY B ) ) )
114 21 113 syl 
 |-  ( ph -> ( B x. ( A rmY B ) ) || ( B x. ( A rmY B ) ) )
115 114 6 breqtrrdi 
 |-  ( ph -> ( B x. ( A rmY B ) ) || Q )
116 jm2.20nn 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ Q e. NN /\ B e. NN ) -> ( ( ( A rmY B ) ^ 2 ) || ( A rmY Q ) <-> ( B x. ( A rmY B ) ) || Q ) )
117 1 33 2 116 syl3anc 
 |-  ( ph -> ( ( ( A rmY B ) ^ 2 ) || ( A rmY Q ) <-> ( B x. ( A rmY B ) ) || Q ) )
118 115 117 mpbird 
 |-  ( ph -> ( ( A rmY B ) ^ 2 ) || ( A rmY Q ) )
119 18 a1i 
 |-  ( ph -> 2 e. ZZ )
120 dvdscmul 
 |-  ( ( ( ( A rmY B ) ^ 2 ) e. ZZ /\ ( A rmY Q ) e. ZZ /\ 2 e. ZZ ) -> ( ( ( A rmY B ) ^ 2 ) || ( A rmY Q ) -> ( 2 x. ( ( A rmY B ) ^ 2 ) ) || ( 2 x. ( A rmY Q ) ) ) )
121 106 110 119 120 syl3anc 
 |-  ( ph -> ( ( ( A rmY B ) ^ 2 ) || ( A rmY Q ) -> ( 2 x. ( ( A rmY B ) ^ 2 ) ) || ( 2 x. ( A rmY Q ) ) ) )
122 118 121 mpd 
 |-  ( ph -> ( 2 x. ( ( A rmY B ) ^ 2 ) ) || ( 2 x. ( A rmY Q ) ) )
123 14 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ Q e. ZZ ) -> ( A rmX Q ) e. NN0 )
124 1 22 123 syl2anc 
 |-  ( ph -> ( A rmX Q ) e. NN0 )
125 124 nn0zd 
 |-  ( ph -> ( A rmX Q ) e. ZZ )
126 dvdsmul1 
 |-  ( ( ( 2 x. ( A rmY Q ) ) e. ZZ /\ ( A rmX Q ) e. ZZ ) -> ( 2 x. ( A rmY Q ) ) || ( ( 2 x. ( A rmY Q ) ) x. ( A rmX Q ) ) )
127 112 125 126 syl2anc 
 |-  ( ph -> ( 2 x. ( A rmY Q ) ) || ( ( 2 x. ( A rmY Q ) ) x. ( A rmX Q ) ) )
128 rmydbl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ Q e. ZZ ) -> ( A rmY ( 2 x. Q ) ) = ( ( 2 x. ( A rmX Q ) ) x. ( A rmY Q ) ) )
129 1 22 128 syl2anc 
 |-  ( ph -> ( A rmY ( 2 x. Q ) ) = ( ( 2 x. ( A rmX Q ) ) x. ( A rmY Q ) ) )
130 2cnd 
 |-  ( ph -> 2 e. CC )
131 124 nn0cnd 
 |-  ( ph -> ( A rmX Q ) e. CC )
132 110 zcnd 
 |-  ( ph -> ( A rmY Q ) e. CC )
133 130 131 132 mul32d 
 |-  ( ph -> ( ( 2 x. ( A rmX Q ) ) x. ( A rmY Q ) ) = ( ( 2 x. ( A rmY Q ) ) x. ( A rmX Q ) ) )
134 129 133 eqtrd 
 |-  ( ph -> ( A rmY ( 2 x. Q ) ) = ( ( 2 x. ( A rmY Q ) ) x. ( A rmX Q ) ) )
135 127 134 breqtrrd 
 |-  ( ph -> ( 2 x. ( A rmY Q ) ) || ( A rmY ( 2 x. Q ) ) )
136 108 112 27 122 135 dvdstrd 
 |-  ( ph -> ( 2 x. ( ( A rmY B ) ^ 2 ) ) || ( A rmY ( 2 x. Q ) ) )
137 4 oveq1d 
 |-  ( ph -> ( C ^ 2 ) = ( ( A rmY B ) ^ 2 ) )
138 137 oveq2d 
 |-  ( ph -> ( 2 x. ( C ^ 2 ) ) = ( 2 x. ( ( A rmY B ) ^ 2 ) ) )
139 7 a1i 
 |-  ( ph -> E = ( A rmY ( 2 x. Q ) ) )
140 136 138 139 3brtr4d 
 |-  ( ph -> ( 2 x. ( C ^ 2 ) ) || E )
141 7 27 eqeltrid 
 |-  ( ph -> E e. ZZ )
142 35 nngt0d 
 |-  ( ph -> 0 < ( 2 x. Q ) )
143 ltrmy 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ /\ ( 2 x. Q ) e. ZZ ) -> ( 0 < ( 2 x. Q ) <-> ( A rmY 0 ) < ( A rmY ( 2 x. Q ) ) ) )
144 1 38 24 143 syl3anc 
 |-  ( ph -> ( 0 < ( 2 x. Q ) <-> ( A rmY 0 ) < ( A rmY ( 2 x. Q ) ) ) )
145 142 144 mpbid 
 |-  ( ph -> ( A rmY 0 ) < ( A rmY ( 2 x. Q ) ) )
146 29 eqcomd 
 |-  ( ph -> 0 = ( A rmY 0 ) )
147 145 146 139 3brtr4d 
 |-  ( ph -> 0 < E )
148 elnnz 
 |-  ( E e. NN <-> ( E e. ZZ /\ 0 < E ) )
149 141 147 148 sylanbrc 
 |-  ( ph -> E e. NN )
150 3 nnsqcld 
 |-  ( ph -> ( C ^ 2 ) e. NN )
151 nnmulcl 
 |-  ( ( 2 e. NN /\ ( C ^ 2 ) e. NN ) -> ( 2 x. ( C ^ 2 ) ) e. NN )
152 30 150 151 sylancr 
 |-  ( ph -> ( 2 x. ( C ^ 2 ) ) e. NN )
153 nndivdvds 
 |-  ( ( E e. NN /\ ( 2 x. ( C ^ 2 ) ) e. NN ) -> ( ( 2 x. ( C ^ 2 ) ) || E <-> ( E / ( 2 x. ( C ^ 2 ) ) ) e. NN ) )
154 149 152 153 syl2anc 
 |-  ( ph -> ( ( 2 x. ( C ^ 2 ) ) || E <-> ( E / ( 2 x. ( C ^ 2 ) ) ) e. NN ) )
155 140 154 mpbid 
 |-  ( ph -> ( E / ( 2 x. ( C ^ 2 ) ) ) e. NN )
156 nnm1nn0 
 |-  ( ( E / ( 2 x. ( C ^ 2 ) ) ) e. NN -> ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 ) e. NN0 )
157 155 156 syl 
 |-  ( ph -> ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 ) e. NN0 )
158 12 157 eqeltrid 
 |-  ( ph -> J e. NN0 )
159 5 oveq1i 
 |-  ( D ^ 2 ) = ( ( A rmX B ) ^ 2 )
160 159 a1i 
 |-  ( ph -> ( D ^ 2 ) = ( ( A rmX B ) ^ 2 ) )
161 137 oveq2d 
 |-  ( ph -> ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY B ) ^ 2 ) ) )
162 160 161 oveq12d 
 |-  ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY B ) ^ 2 ) ) ) )
163 rmxynorm 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY B ) ^ 2 ) ) ) = 1 )
164 1 13 163 syl2anc 
 |-  ( ph -> ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY B ) ^ 2 ) ) ) = 1 )
165 162 164 eqtrd 
 |-  ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
166 8 oveq1i 
 |-  ( F ^ 2 ) = ( ( A rmX ( 2 x. Q ) ) ^ 2 )
167 7 oveq1i 
 |-  ( E ^ 2 ) = ( ( A rmY ( 2 x. Q ) ) ^ 2 )
168 167 oveq2i 
 |-  ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. Q ) ) ^ 2 ) )
169 166 168 oveq12i 
 |-  ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = ( ( ( A rmX ( 2 x. Q ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. Q ) ) ^ 2 ) ) )
170 rmxynorm 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( 2 x. Q ) e. ZZ ) -> ( ( ( A rmX ( 2 x. Q ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. Q ) ) ^ 2 ) ) ) = 1 )
171 1 24 170 syl2anc 
 |-  ( ph -> ( ( ( A rmX ( 2 x. Q ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. Q ) ) ^ 2 ) ) ) = 1 )
172 169 171 syl5eq 
 |-  ( ph -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )
173 165 172 85 3jca 
 |-  ( ph -> ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 /\ G e. ( ZZ>= ` 2 ) ) )
174 11 oveq1i 
 |-  ( I ^ 2 ) = ( ( G rmX B ) ^ 2 )
175 10 oveq1i 
 |-  ( H ^ 2 ) = ( ( G rmY B ) ^ 2 )
176 175 oveq2i 
 |-  ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) = ( ( ( G ^ 2 ) - 1 ) x. ( ( G rmY B ) ^ 2 ) )
177 174 176 oveq12i 
 |-  ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = ( ( ( G rmX B ) ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( ( G rmY B ) ^ 2 ) ) )
178 rmxynorm 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( ( ( G rmX B ) ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( ( G rmY B ) ^ 2 ) ) ) = 1 )
179 85 13 178 syl2anc 
 |-  ( ph -> ( ( ( G rmX B ) ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( ( G rmY B ) ^ 2 ) ) ) = 1 )
180 177 179 syl5eq 
 |-  ( ph -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )
181 12 a1i 
 |-  ( ph -> J = ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 ) )
182 181 oveq1d 
 |-  ( ph -> ( J + 1 ) = ( ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) )
183 141 zcnd 
 |-  ( ph -> E e. CC )
184 152 nncnd 
 |-  ( ph -> ( 2 x. ( C ^ 2 ) ) e. CC )
185 152 nnne0d 
 |-  ( ph -> ( 2 x. ( C ^ 2 ) ) =/= 0 )
186 183 184 185 divcld 
 |-  ( ph -> ( E / ( 2 x. ( C ^ 2 ) ) ) e. CC )
187 ax-1cn 
 |-  1 e. CC
188 npcan 
 |-  ( ( ( E / ( 2 x. ( C ^ 2 ) ) ) e. CC /\ 1 e. CC ) -> ( ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) = ( E / ( 2 x. ( C ^ 2 ) ) ) )
189 186 187 188 sylancl 
 |-  ( ph -> ( ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) = ( E / ( 2 x. ( C ^ 2 ) ) ) )
190 182 189 eqtrd 
 |-  ( ph -> ( J + 1 ) = ( E / ( 2 x. ( C ^ 2 ) ) ) )
191 190 oveq1d 
 |-  ( ph -> ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) = ( ( E / ( 2 x. ( C ^ 2 ) ) ) x. ( 2 x. ( C ^ 2 ) ) ) )
192 183 184 185 divcan1d 
 |-  ( ph -> ( ( E / ( 2 x. ( C ^ 2 ) ) ) x. ( 2 x. ( C ^ 2 ) ) ) = E )
193 191 192 eqtr2d 
 |-  ( ph -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
194 48 nn0zd 
 |-  ( ph -> F e. ZZ )
195 81 nn0zd 
 |-  ( ph -> ( ( F ^ 2 ) - A ) e. ZZ )
196 194 195 zmulcld 
 |-  ( ph -> ( F x. ( ( F ^ 2 ) - A ) ) e. ZZ )
197 dvdsmul1 
 |-  ( ( F e. ZZ /\ ( F x. ( ( F ^ 2 ) - A ) ) e. ZZ ) -> F || ( F x. ( F x. ( ( F ^ 2 ) - A ) ) ) )
198 194 196 197 syl2anc 
 |-  ( ph -> F || ( F x. ( F x. ( ( F ^ 2 ) - A ) ) ) )
199 9 oveq1i 
 |-  ( G - A ) = ( ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) - A )
200 57 nn0cnd 
 |-  ( ph -> A e. CC )
201 82 nn0cnd 
 |-  ( ph -> ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) e. CC )
202 200 201 pncan2d 
 |-  ( ph -> ( ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) - A ) = ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) )
203 52 oveq1d 
 |-  ( ph -> ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) = ( ( F x. F ) x. ( ( F ^ 2 ) - A ) ) )
204 81 nn0cnd 
 |-  ( ph -> ( ( F ^ 2 ) - A ) e. CC )
205 51 51 204 mulassd 
 |-  ( ph -> ( ( F x. F ) x. ( ( F ^ 2 ) - A ) ) = ( F x. ( F x. ( ( F ^ 2 ) - A ) ) ) )
206 202 203 205 3eqtrd 
 |-  ( ph -> ( ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) - A ) = ( F x. ( F x. ( ( F ^ 2 ) - A ) ) ) )
207 199 206 syl5eq 
 |-  ( ph -> ( G - A ) = ( F x. ( F x. ( ( F ^ 2 ) - A ) ) ) )
208 198 207 breqtrrd 
 |-  ( ph -> F || ( G - A ) )
209 180 193 208 3jca 
 |-  ( ph -> ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 /\ E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ F || ( G - A ) ) )
210 zmulcl 
 |-  ( ( 2 e. ZZ /\ C e. ZZ ) -> ( 2 x. C ) e. ZZ )
211 18 19 210 sylancr 
 |-  ( ph -> ( 2 x. C ) e. ZZ )
212 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
213 1 212 syl 
 |-  ( ph -> A e. ZZ )
214 82 nn0zd 
 |-  ( ph -> ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) e. ZZ )
215 1z 
 |-  1 e. ZZ
216 zsubcl 
 |-  ( ( 1 e. ZZ /\ A e. ZZ ) -> ( 1 - A ) e. ZZ )
217 215 213 216 sylancr 
 |-  ( ph -> ( 1 - A ) e. ZZ )
218 zmulcl 
 |-  ( ( 1 e. ZZ /\ ( 1 - A ) e. ZZ ) -> ( 1 x. ( 1 - A ) ) e. ZZ )
219 215 217 218 sylancr 
 |-  ( ph -> ( 1 x. ( 1 - A ) ) e. ZZ )
220 congid 
 |-  ( ( ( 2 x. C ) e. ZZ /\ A e. ZZ ) -> ( 2 x. C ) || ( A - A ) )
221 211 213 220 syl2anc 
 |-  ( ph -> ( 2 x. C ) || ( A - A ) )
222 54 nn0zd 
 |-  ( ph -> ( F ^ 2 ) e. ZZ )
223 215 a1i 
 |-  ( ph -> 1 e. ZZ )
224 3 nncnd 
 |-  ( ph -> C e. CC )
225 130 224 224 mulassd 
 |-  ( ph -> ( ( 2 x. C ) x. C ) = ( 2 x. ( C x. C ) ) )
226 224 sqvald 
 |-  ( ph -> ( C ^ 2 ) = ( C x. C ) )
227 226 oveq2d 
 |-  ( ph -> ( 2 x. ( C ^ 2 ) ) = ( 2 x. ( C x. C ) ) )
228 225 227 eqtr4d 
 |-  ( ph -> ( ( 2 x. C ) x. C ) = ( 2 x. ( C ^ 2 ) ) )
229 228 140 eqbrtrd 
 |-  ( ph -> ( ( 2 x. C ) x. C ) || E )
230 muldvds1 
 |-  ( ( ( 2 x. C ) e. ZZ /\ C e. ZZ /\ E e. ZZ ) -> ( ( ( 2 x. C ) x. C ) || E -> ( 2 x. C ) || E ) )
231 211 19 141 230 syl3anc 
 |-  ( ph -> ( ( ( 2 x. C ) x. C ) || E -> ( 2 x. C ) || E ) )
232 229 231 mpd 
 |-  ( ph -> ( 2 x. C ) || E )
233 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
234 213 233 syl 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
235 peano2zm 
 |-  ( ( A ^ 2 ) e. ZZ -> ( ( A ^ 2 ) - 1 ) e. ZZ )
236 234 235 syl 
 |-  ( ph -> ( ( A ^ 2 ) - 1 ) e. ZZ )
237 236 141 zmulcld 
 |-  ( ph -> ( ( ( A ^ 2 ) - 1 ) x. E ) e. ZZ )
238 dvdsmultr2 
 |-  ( ( ( 2 x. C ) e. ZZ /\ ( ( ( A ^ 2 ) - 1 ) x. E ) e. ZZ /\ E e. ZZ ) -> ( ( 2 x. C ) || E -> ( 2 x. C ) || ( ( ( ( A ^ 2 ) - 1 ) x. E ) x. E ) ) )
239 211 237 141 238 syl3anc 
 |-  ( ph -> ( ( 2 x. C ) || E -> ( 2 x. C ) || ( ( ( ( A ^ 2 ) - 1 ) x. E ) x. E ) ) )
240 232 239 mpd 
 |-  ( ph -> ( 2 x. C ) || ( ( ( ( A ^ 2 ) - 1 ) x. E ) x. E ) )
241 183 sqvald 
 |-  ( ph -> ( E ^ 2 ) = ( E x. E ) )
242 241 oveq2d 
 |-  ( ph -> ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( E x. E ) ) )
243 200 sqcld 
 |-  ( ph -> ( A ^ 2 ) e. CC )
244 subcl 
 |-  ( ( ( A ^ 2 ) e. CC /\ 1 e. CC ) -> ( ( A ^ 2 ) - 1 ) e. CC )
245 243 187 244 sylancl 
 |-  ( ph -> ( ( A ^ 2 ) - 1 ) e. CC )
246 245 183 183 mulassd 
 |-  ( ph -> ( ( ( ( A ^ 2 ) - 1 ) x. E ) x. E ) = ( ( ( A ^ 2 ) - 1 ) x. ( E x. E ) ) )
247 242 246 eqtr4d 
 |-  ( ph -> ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) = ( ( ( ( A ^ 2 ) - 1 ) x. E ) x. E ) )
248 240 247 breqtrrd 
 |-  ( ph -> ( 2 x. C ) || ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) )
249 51 sqcld 
 |-  ( ph -> ( F ^ 2 ) e. CC )
250 183 sqcld 
 |-  ( ph -> ( E ^ 2 ) e. CC )
251 245 250 mulcld 
 |-  ( ph -> ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) e. CC )
252 187 a1i 
 |-  ( ph -> 1 e. CC )
253 subsub23 
 |-  ( ( ( F ^ 2 ) e. CC /\ ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) e. CC /\ 1 e. CC ) -> ( ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 <-> ( ( F ^ 2 ) - 1 ) = ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) )
254 249 251 252 253 syl3anc 
 |-  ( ph -> ( ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 <-> ( ( F ^ 2 ) - 1 ) = ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) )
255 172 254 mpbid 
 |-  ( ph -> ( ( F ^ 2 ) - 1 ) = ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) )
256 248 255 breqtrrd 
 |-  ( ph -> ( 2 x. C ) || ( ( F ^ 2 ) - 1 ) )
257 congsub 
 |-  ( ( ( ( 2 x. C ) e. ZZ /\ ( F ^ 2 ) e. ZZ /\ 1 e. ZZ ) /\ ( A e. ZZ /\ A e. ZZ ) /\ ( ( 2 x. C ) || ( ( F ^ 2 ) - 1 ) /\ ( 2 x. C ) || ( A - A ) ) ) -> ( 2 x. C ) || ( ( ( F ^ 2 ) - A ) - ( 1 - A ) ) )
258 211 222 223 213 213 256 221 257 syl322anc 
 |-  ( ph -> ( 2 x. C ) || ( ( ( F ^ 2 ) - A ) - ( 1 - A ) ) )
259 congmul 
 |-  ( ( ( ( 2 x. C ) e. ZZ /\ ( F ^ 2 ) e. ZZ /\ 1 e. ZZ ) /\ ( ( ( F ^ 2 ) - A ) e. ZZ /\ ( 1 - A ) e. ZZ ) /\ ( ( 2 x. C ) || ( ( F ^ 2 ) - 1 ) /\ ( 2 x. C ) || ( ( ( F ^ 2 ) - A ) - ( 1 - A ) ) ) ) -> ( 2 x. C ) || ( ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) - ( 1 x. ( 1 - A ) ) ) )
260 211 222 223 195 217 256 258 259 syl322anc 
 |-  ( ph -> ( 2 x. C ) || ( ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) - ( 1 x. ( 1 - A ) ) ) )
261 congadd 
 |-  ( ( ( ( 2 x. C ) e. ZZ /\ A e. ZZ /\ A e. ZZ ) /\ ( ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) e. ZZ /\ ( 1 x. ( 1 - A ) ) e. ZZ ) /\ ( ( 2 x. C ) || ( A - A ) /\ ( 2 x. C ) || ( ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) - ( 1 x. ( 1 - A ) ) ) ) ) -> ( 2 x. C ) || ( ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) - ( A + ( 1 x. ( 1 - A ) ) ) ) )
262 211 213 213 214 219 221 260 261 syl322anc 
 |-  ( ph -> ( 2 x. C ) || ( ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) - ( A + ( 1 x. ( 1 - A ) ) ) ) )
263 9 a1i 
 |-  ( ph -> G = ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) )
264 217 zcnd 
 |-  ( ph -> ( 1 - A ) e. CC )
265 264 mulid2d 
 |-  ( ph -> ( 1 x. ( 1 - A ) ) = ( 1 - A ) )
266 265 oveq2d 
 |-  ( ph -> ( A + ( 1 x. ( 1 - A ) ) ) = ( A + ( 1 - A ) ) )
267 pncan3 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A + ( 1 - A ) ) = 1 )
268 200 187 267 sylancl 
 |-  ( ph -> ( A + ( 1 - A ) ) = 1 )
269 266 268 eqtr2d 
 |-  ( ph -> 1 = ( A + ( 1 x. ( 1 - A ) ) ) )
270 263 269 oveq12d 
 |-  ( ph -> ( G - 1 ) = ( ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) ) - ( A + ( 1 x. ( 1 - A ) ) ) ) )
271 262 270 breqtrrd 
 |-  ( ph -> ( 2 x. C ) || ( G - 1 ) )
272 eluzelz 
 |-  ( G e. ( ZZ>= ` 2 ) -> G e. ZZ )
273 85 272 syl 
 |-  ( ph -> G e. ZZ )
274 273 213 zsubcld 
 |-  ( ph -> ( G - A ) e. ZZ )
275 10 89 eqeltrid 
 |-  ( ph -> H e. ZZ )
276 275 19 zsubcld 
 |-  ( ph -> ( H - C ) e. ZZ )
277 jm2.15nn0 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ A e. ( ZZ>= ` 2 ) /\ B e. NN0 ) -> ( G - A ) || ( ( G rmY B ) - ( A rmY B ) ) )
278 85 1 92 277 syl3anc 
 |-  ( ph -> ( G - A ) || ( ( G rmY B ) - ( A rmY B ) ) )
279 10 a1i 
 |-  ( ph -> H = ( G rmY B ) )
280 279 4 oveq12d 
 |-  ( ph -> ( H - C ) = ( ( G rmY B ) - ( A rmY B ) ) )
281 278 280 breqtrrd 
 |-  ( ph -> ( G - A ) || ( H - C ) )
282 194 274 276 208 281 dvdstrd 
 |-  ( ph -> F || ( H - C ) )
283 peano2zm 
 |-  ( G e. ZZ -> ( G - 1 ) e. ZZ )
284 273 283 syl 
 |-  ( ph -> ( G - 1 ) e. ZZ )
285 275 13 zsubcld 
 |-  ( ph -> ( H - B ) e. ZZ )
286 jm2.16nn0 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ B e. NN0 ) -> ( G - 1 ) || ( ( G rmY B ) - B ) )
287 85 92 286 syl2anc 
 |-  ( ph -> ( G - 1 ) || ( ( G rmY B ) - B ) )
288 10 oveq1i 
 |-  ( H - B ) = ( ( G rmY B ) - B )
289 287 288 breqtrrdi 
 |-  ( ph -> ( G - 1 ) || ( H - B ) )
290 211 284 285 271 289 dvdstrd 
 |-  ( ph -> ( 2 x. C ) || ( H - B ) )
291 rmygeid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN0 ) -> B <_ ( A rmY B ) )
292 1 92 291 syl2anc 
 |-  ( ph -> B <_ ( A rmY B ) )
293 292 4 breqtrrd 
 |-  ( ph -> B <_ C )
294 290 293 jca 
 |-  ( ph -> ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) )
295 271 282 294 jca31 
 |-  ( ph -> ( ( ( 2 x. C ) || ( G - 1 ) /\ F || ( H - C ) ) /\ ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) ) )
296 173 209 295 jca31 
 |-  ( ph -> ( ( ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 /\ G e. ( ZZ>= ` 2 ) ) /\ ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 /\ E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ F || ( G - A ) ) ) /\ ( ( ( 2 x. C ) || ( G - 1 ) /\ F || ( H - C ) ) /\ ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) ) ) )
297 158 296 jca 
 |-  ( ph -> ( J e. NN0 /\ ( ( ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 /\ G e. ( ZZ>= ` 2 ) ) /\ ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 /\ E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ F || ( G - A ) ) ) /\ ( ( ( 2 x. C ) || ( G - 1 ) /\ F || ( H - C ) ) /\ ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) ) ) ) )
298 49 104 297 jca31 
 |-  ( ph -> ( ( ( D e. NN0 /\ E e. NN0 /\ F e. NN0 ) /\ ( G e. NN0 /\ H e. NN0 /\ I e. NN0 ) ) /\ ( J e. NN0 /\ ( ( ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 /\ G e. ( ZZ>= ` 2 ) ) /\ ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 /\ E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ F || ( G - A ) ) ) /\ ( ( ( 2 x. C ) || ( G - 1 ) /\ F || ( H - C ) ) /\ ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) ) ) ) ) )