Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  jm2.27 Unicode version

Theorem jm2.27 27203
Description: Lemma 2.27 of [JonesMatijasevic] p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a 27200 and jm2.27c 27202. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine" (Contributed by Stefan O'Rear, 4-Oct-2014.)
Assertion
Ref Expression
jm2.27  |-  ( ( A  e.  ( ZZ>= ` 
2 )  /\  B  e.  NN  /\  C  e.  NN )  ->  ( C  =  ( A Yrm  B
)  <->  E. d  e.  NN0  E. e  e.  NN0  E. f  e.  NN0  E. g  e. 
NN0  E. h  e.  NN0  E. i  e.  NN0  E. 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 ) ) ) ) )
Distinct variable groups:    A, d,
e, f, g, h, i, j    B, d, e, f, g, h, i, j    C, d, e, f, g, h, i, j

Proof of Theorem jm2.27
StepHypRef Expression
1 simpl1 958 . . . . . . 7  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  A  e.  ( ZZ>= `  2 )
)
2 simpl2 959 . . . . . . 7  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  B  e.  NN )
3 simpl3 960 . . . . . . 7  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  C  e.  NN )
4 simpr 447 . . . . . . 7  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  C  =  ( A Yrm  B ) )
5 eqid 2296 . . . . . . 7  |-  ( A Xrm  B )  =  ( A Xrm  B )
6 eqid 2296 . . . . . . 7  |-  ( B  x.  ( A Yrm  B ) )  =  ( B  x.  ( A Yrm  B ) )
7 eqid 2296 . . . . . . 7  |-  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )
8 eqid 2296 . . . . . . 7  |-  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )
9 eqid 2296 . . . . . . 7  |-  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )
10 eqid 2296 . . . . . . 7  |-  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )
11 eqid 2296 . . . . . . 7  |-  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B )  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B )
12 eqid 2296 . . . . . . 7  |-  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  /  ( 2  x.  ( C ^
2 ) ) )  -  1 )  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  / 
( 2  x.  ( C ^ 2 ) ) )  -  1 )
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12jm2.27c 27202 . . . . . 6  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  ( (
( ( A Xrm  B )  e.  NN0  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  e.  NN0  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  e.  NN0 )  /\  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  e.  NN0  /\  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  e. 
NN0  /\  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B )  e.  NN0 )
)  /\  ( (
( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  /  (
2  x.  ( C ^ 2 ) ) )  -  1 )  e.  NN0  /\  (
( ( ( ( ( A Xrm  B ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) ) ) )
1413simpld 445 . . . . 5  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  ( (
( A Xrm  B )  e. 
NN0  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  e. 
NN0  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  e. 
NN0 )  /\  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  NN0  /\  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  e. 
NN0  /\  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B )  e.  NN0 )
) )
1514simpld 445 . . . 4  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  ( ( A Xrm 
B )  e.  NN0  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  e.  NN0  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  e.  NN0 )
)
1614simprd 449 . . . . 5  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  e.  NN0  /\  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  e.  NN0  /\  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B )  e. 
NN0 ) )
1713simprd 449 . . . . . 6  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  ( (
( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  /  (
2  x.  ( C ^ 2 ) ) )  -  1 )  e.  NN0  /\  (
( ( ( ( ( A Xrm  B ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) ) )
18 oveq1 5881 . . . . . . . . . . . 12  |-  ( j  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  ->  (
j  +  1 )  =  ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  /  ( 2  x.  ( C ^
2 ) ) )  -  1 )  +  1 ) )
1918oveq1d 5889 . . . . . . . . . . 11  |-  ( j  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  ->  (
( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  /  (
2  x.  ( C ^ 2 ) ) )  -  1 )  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) ) )
2019eqeq2d 2307 . . . . . . . . . 10  |-  ( j  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  ->  (
( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  <->  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  /  ( 2  x.  ( C ^
2 ) ) )  -  1 )  +  1 )  x.  (
2  x.  ( C ^ 2 ) ) ) ) )
21203anbi2d 1257 . . . . . . . . 9  |-  ( j  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  ->  (
( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) )  <->  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^
2 )  -  (
( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) ^
2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  /  ( 2  x.  ( C ^
2 ) ) )  -  1 )  +  1 )  x.  (
2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) ) )
2221anbi2d 684 . . . . . . . 8  |-  ( j  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  ->  (
( ( ( ( ( A Xrm  B ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  <->  ( (
( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  /  (
2  x.  ( C ^ 2 ) ) )  -  1 )  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) ) ) )
2322anbi1d 685 . . . . . . 7  |-  ( j  =  ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  ->  (
( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  - 
1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) )  <-> 
( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  - 
1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) ) )
2423rspcev 2897 . . . . . 6  |-  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  / 
( 2  x.  ( C ^ 2 ) ) )  -  1 )  e.  NN0  /\  (
( ( ( ( ( A Xrm  B ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( ( ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  /  ( 2  x.  ( C ^ 2 ) ) )  - 
1 )  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) )  ->  E. j  e.  NN0  ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) )  /\  ( ( ( 2  x.  C )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) )
2517, 24syl 15 . . . . 5  |-  ( ( ( A  e.  (
ZZ>= `  2 )  /\  B  e.  NN  /\  C  e.  NN )  /\  C  =  ( A Yrm  B ) )  ->  E. j  e.  NN0  ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Xrm  B ) ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) )  /\  ( ( ( 2  x.  C )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) )
26 eleq1 2356 . . . . . . . . . 10  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
g  e.  ( ZZ>= ` 
2 )  <->  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
) )
27263anbi3d 1258 . . . . . . . . 9  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^
2 ) ) )  =  1  /\  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 ) ) )  =  1  /\  g  e.  ( ZZ>= `  2 )
)  <->  ( ( ( ( A Xrm  B ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) ) ) )
28 oveq1 5881 . . . . . . . . . . . . . 14  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
g ^ 2 )  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) ^
2 ) )
2928oveq1d 5889 . . . . . . . . . . . . 13  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( g ^ 2 )  -  1 )  =  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 ) )
3029oveq1d 5889 . . . . . . . . . . . 12  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( g ^
2 )  -  1 )  x.  ( h ^ 2 ) )  =  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^ 2 ) ) )
3130oveq2d 5890 . . . . . . . . . . 11  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( i ^ 2 )  -  ( ( ( g ^ 2 )  -  1 )  x.  ( h ^
2 ) ) )  =  ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) ) )
3231eqeq1d 2304 . . . . . . . . . 10  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( i ^
2 )  -  (
( ( g ^
2 )  -  1 )  x.  ( h ^ 2 ) ) )  =  1  <->  (
( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^
2 ) ) )  =  1 ) )
33 oveq1 5881 . . . . . . . . . . 11  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
g  -  A )  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  -  A ) )
3433breq2d 4051 . . . . . . . . . 10  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  ||  ( g  -  A )  <->  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) )
3532, 343anbi13d 1254 . . . . . . . . 9  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( ( i ^ 2 )  -  ( ( ( g ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
g  -  A ) )  <->  ( ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  (
2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) ) )
3627, 35anbi12d 691 . . . . . . . 8  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( ( ( ( A Xrm  B ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  g  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( i ^ 2 )  -  ( ( ( g ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
g  -  A ) ) )  <->  ( (
( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) ) ) )
37 oveq1 5881 . . . . . . . . . . 11  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
g  -  1 )  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  - 
1 ) )
3837breq2d 4051 . . . . . . . . . 10  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( 2  x.  C
)  ||  ( g  -  1 )  <->  ( 2  x.  C )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 ) ) )
3938anbi1d 685 . . . . . . . . 9  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( 2  x.  C )  ||  (
g  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
h  -  C ) )  <->  ( ( 2  x.  C )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( h  -  C
) ) ) )
4039anbi1d 685 . . . . . . . 8  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( ( 2  x.  C )  ||  ( g  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( h  -  C
) )  /\  (
( 2  x.  C
)  ||  ( h  -  B )  /\  B  <_  C ) )  <->  ( (
( 2  x.  C
)  ||  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  ||  ( h  -  C ) )  /\  ( ( 2  x.  C )  ||  ( h  -  B
)  /\  B  <_  C ) ) ) )
4136, 40anbi12d 691 . . . . . . 7  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  (
( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  - 
1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  g  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( i ^ 2 )  -  ( ( ( g ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
g  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
g  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
h  -  C ) )  /\  ( ( 2  x.  C ) 
||  ( h  -  B )  /\  B  <_  C ) ) )  <-> 
( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  - 
1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
h  -  C ) )  /\  ( ( 2  x.  C ) 
||  ( h  -  B )  /\  B  <_  C ) ) ) ) )
4241rexbidv 2577 . . . . . 6  |-  ( g  =  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  ->  ( E. j  e.  NN0  ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  - 
1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  g  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( i ^ 2 )  -  ( ( ( g ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
g  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
g  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
h  -  C ) )  /\  ( ( 2  x.  C ) 
||  ( h  -  B )  /\  B  <_  C ) ) )  <->  E. j  e.  NN0  ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  - 
1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  (
( ( A ^
2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= ` 
2 ) )  /\  ( ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  (
( ( 2  x.  C )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
h  -  C ) )  /\  ( ( 2  x.  C ) 
||  ( h  -  B )  /\  B  <_  C ) ) ) ) )
43 oveq1 5881 . . . . . . . . . . . . 13  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( h ^
2 )  =  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^
2 ) )
4443oveq2d 5890 . . . . . . . . . . . 12  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^ 2 ) )  =  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) ^
2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )
4544oveq2d 5890 . . . . . . . . . . 11  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
h ^ 2 ) ) )  =  ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) ) )
4645eqeq1d 2304 . . . . . . . . . 10  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^ 2 ) ) )  =  1  <->  ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  - 
1 )  x.  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^
2 ) ) )  =  1 ) )
47463anbi1d 1256 . . . . . . . . 9  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( ( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) )  <->  ( (
( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) ) )
4847anbi2d 684 . . . . . . . 8  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) )  <->  ( (
( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^
2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) ) ) )
49 oveq1 5881 . . . . . . . . . . 11  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( h  -  C )  =  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) )
5049breq2d 4051 . . . . . . . . . 10  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( h  -  C
)  <->  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) ) )
5150anbi2d 684 . . . . . . . . 9  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( 2  x.  C ) 
||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  - 
1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) 
||  ( h  -  C ) )  <->  ( (
2  x.  C ) 
||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  - 
1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) 
||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C ) ) ) )
52 oveq1 5881 . . . . . . . . . . 11  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( h  -  B )  =  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B ) )
5352breq2d 4051 . . . . . . . . . 10  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( 2  x.  C )  ||  ( h  -  B
)  <->  ( 2  x.  C )  ||  (
( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B ) ) )
5453anbi1d 685 . . . . . . . . 9  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( 2  x.  C ) 
||  ( h  -  B )  /\  B  <_  C )  <->  ( (
2  x.  C ) 
||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B )  /\  B  <_  C
) ) )
5551, 54anbi12d 691 . . . . . . . 8  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( ( 2  x.  C
)  ||  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  ||  ( h  -  C ) )  /\  ( ( 2  x.  C )  ||  ( h  -  B
)  /\  B  <_  C ) )  <->  ( (
( 2  x.  C
)  ||  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  C
) )  /\  (
( 2  x.  C
)  ||  ( (
( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B )  -  B
)  /\  B  <_  C ) ) ) )
5648, 55anbi12d 691 . . . . . . 7  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^
2 ) ) )  =  1  /\  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 ) ) )  =  1  /\  ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= `  2
) )  /\  (
( ( i ^
2 )  -  (
( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) ^
2 )  -  1 )  x.  ( h ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  -  A ) ) )  /\  ( ( ( 2  x.  C
)  ||  ( ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) )  ||  ( h  -  C ) )  /\  ( ( 2  x.  C )  ||  ( h  -  B
)  /\  B  <_  C ) ) )  <->  ( (
( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^
2 ) ) )  =  1  /\  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 ) ) )  =  1  /\  ( A  +  ( (
( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  -  A ) ) )  e.  ( ZZ>= `  2
) )  /\  (
( ( i ^
2 )  -  (
( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) ^
2 )  -  1 )  x.  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  A ) ) ) Yrm  B ) ^ 2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  =  ( ( j  +  1 )  x.  (
2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) )  /\  ( ( ( 2  x.  C )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  -  C ) )  /\  ( ( 2  x.  C )  ||  ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  -  B )  /\  B  <_  C ) ) ) ) )
5756rexbidv 2577 . . . . . 6  |-  ( h  =  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) ) Yrm  B )  ->  ( E. j  e.  NN0  ( ( ( ( ( ( A Xrm  B ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( C ^ 2 ) ) )  =  1  /\  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm 
B ) ) ) ) ^ 2 )  -  ( ( ( A ^ 2 )  -  1 )  x.  ( ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 ) ) )  =  1  /\  ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) ) ^ 2 )  x.  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  -  A
) ) )  e.  ( ZZ>= `  2 )
)  /\  ( (
( i ^ 2 )  -  ( ( ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) ) ^ 2 )  -  1 )  x.  ( h ^
2 ) ) )  =  1  /\  ( A Yrm  ( 2  x.  ( B  x.  ( A Yrm  B
) ) ) )  =  ( ( j  +  1 )  x.  ( 2  x.  ( C ^ 2 ) ) )  /\  ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  A
) ) )  /\  ( ( ( 2  x.  C )  ||  ( ( A  +  ( ( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^
2 )  x.  (
( ( A Xrm  ( 2  x.  ( B  x.  ( A Yrm  B ) ) ) ) ^ 2 )  -  A ) ) )  -  1 )  /\  ( A Xrm  ( 2  x.  (