Metamath Proof Explorer

Theorem jm2.27

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 and jm2.27c . Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine". (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion jm2.27 
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) -> ( C = ( A rmY 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> A e. ( ZZ>= ` 2 ) )
2 simpl2 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> B e. NN )
3 simpl3 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> C e. NN )
4 simpr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> C = ( A rmY B ) )
5 eqid 
 |-  ( A rmX B ) = ( A rmX B )
6 eqid 
 |-  ( B x. ( A rmY B ) ) = ( B x. ( A rmY B ) )
7 eqid 
 |-  ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) )
8 eqid 
 |-  ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) )
9 eqid 
 |-  ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) )
10 eqid 
 |-  ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B )
11 eqid 
 |-  ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B )
12 eqid 
 |-  ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 )
13 1 2 3 4 5 6 7 8 9 10 11 12 jm2.27c 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> ( ( ( ( A rmX B ) e. NN0 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 ) /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) e. NN0 ) ) /\ ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) e. NN0 /\ ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) ) )
14 13 simpld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> ( ( ( A rmX B ) e. NN0 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 ) /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) e. NN0 ) ) )
15 14 simpld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> ( ( A rmX B ) e. NN0 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 ) )
16 14 simprd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) e. NN0 ) )
17 13 simprd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) e. NN0 /\ ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) )
18 oveq1 
 |-  ( j = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) -> ( j + 1 ) = ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) )
19 18 oveq1d 
 |-  ( j = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) -> ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
20 19 eqeq2d 
 |-  ( j = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) -> ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) <-> ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) ) )
21 20 3anbi2d 
 |-  ( j = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) -> ( ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) <-> ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) )
22 21 anbi2d 
 |-  ( j = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) -> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) ) )
23 22 anbi1d 
 |-  ( j = ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) -> ( ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) )
24 23 rspcev 
 |-  ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) e. NN0 /\ ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( ( ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) / ( 2 x. ( C ^ 2 ) ) ) - 1 ) + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) -> E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) )
25 17 24 syl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) )
26 eleq1 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( g e. ( ZZ>= ` 2 ) <-> ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) )
27 26 3anbi3d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) <-> ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) ) )
28 oveq1 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( g ^ 2 ) = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) )
29 28 oveq1d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( g ^ 2 ) - 1 ) = ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) )
30 29 oveq1d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) = ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) )
31 30 oveq2d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) )
32 31 eqeq1d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 <-> ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 ) )
33 oveq1 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( g - A ) = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) )
34 33 breq2d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) <-> ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) )
35 32 34 3anbi13d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) <-> ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) )
36 27 35 anbi12d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) ) )
37 oveq1 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( g - 1 ) = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) )
38 37 breq2d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( 2 x. C ) || ( g - 1 ) <-> ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) ) )
39 38 anbi1d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) <-> ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) ) )
40 39 anbi1d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) <-> ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) )
41 36 40 anbi12d 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) )
42 41 rexbidv 
 |-  ( g = ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) -> ( E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) <-> E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) )
43 oveq1 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( h ^ 2 ) = ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) )
44 43 oveq2d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) = ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) )
45 44 oveq2d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) )
46 45 eqeq1d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 <-> ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 ) )
47 46 3anbi1d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) <-> ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) )
48 47 anbi2d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) ) )
49 oveq1 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( h - C ) = ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) )
50 49 breq2d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) <-> ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) )
51 50 anbi2d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) <-> ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) ) )
52 oveq1 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( h - B ) = ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) )
53 52 breq2d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( 2 x. C ) || ( h - B ) <-> ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) ) )
54 53 anbi1d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) <-> ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) )
55 51 54 anbi12d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) <-> ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) )
56 48 55 anbi12d 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) )
57 56 rexbidv 
 |-  ( h = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) -> ( E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) <-> E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) )
58 oveq1 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( i ^ 2 ) = ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) )
59 58 oveq1d 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) )
60 59 eqeq1d 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 <-> ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 ) )
61 60 3anbi1d 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) <-> ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) )
62 61 anbi2d 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) ) )
63 62 anbi1d 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) )
64 63 rexbidv 
 |-  ( i = ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) -> ( E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) <-> E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) )
65 42 57 64 rspc3ev 
 |-  ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) e. NN0 /\ ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) e. NN0 ) /\ E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) e. ( ZZ>= ` 2 ) ) /\ ( ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmX B ) ^ 2 ) - ( ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) ^ 2 ) - 1 ) x. ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - A ) ) ) /\ ( ( ( 2 x. C ) || ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - C ) ) /\ ( ( 2 x. C ) || ( ( ( A + ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) x. ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - A ) ) ) rmY B ) - B ) /\ B <_ C ) ) ) ) -> E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) )
66 16 25 65 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY B ) ) -> E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) )
67 oveq1 
 |-  ( d = ( A rmX B ) -> ( d ^ 2 ) = ( ( A rmX B ) ^ 2 ) )
68 67 oveq1d 
 |-  ( d = ( A rmX B ) -> ( ( d ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) )
69 68 eqeq1d 
 |-  ( d = ( A rmX B ) -> ( ( ( d ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 <-> ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 ) )
70 69 3anbi1d 
 |-  ( d = ( A rmX B ) -> ( ( ( ( d ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) <-> ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) ) )
71 70 anbi1d 
 |-  ( d = ( A rmX B ) -> ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 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 ) ) ) ) )
72 71 anbi1d 
 |-  ( d = ( A rmX B ) -> ( ( ( ( ( ( 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 ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) ) )
73 72 2rexbidv 
 |-  ( d = ( A rmX B ) -> ( 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 ) ) ) <-> E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) ) )
74 73 2rexbidv 
 |-  ( d = ( A rmX B ) -> ( 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 ) ) ) <-> E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) ) )
75 oveq1 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( e ^ 2 ) = ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) )
76 75 oveq2d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) = ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) )
77 76 oveq2d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) )
78 77 eqeq1d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 <-> ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 ) )
79 78 3anbi2d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) <-> ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) ) )
80 eqeq1 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( e = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) <-> ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) ) )
81 80 3anbi2d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ e = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ f || ( g - A ) ) <-> ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ f || ( g - A ) ) ) )
82 79 81 anbi12d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ f || ( g - A ) ) ) ) )
83 82 anbi1d 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( 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 ) ) ) ) )
84 83 2rexbidv 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) <-> E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( 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 ) ) ) ) )
85 84 2rexbidv 
 |-  ( e = ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 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 ) ) ) <-> E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( 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 ) ) ) ) )
86 oveq1 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( f ^ 2 ) = ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) )
87 86 oveq1d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) )
88 87 eqeq1d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 <-> ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 ) )
89 88 3anbi2d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) <-> ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) ) )
90 breq1 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( f || ( g - A ) <-> ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) )
91 90 3anbi3d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ f || ( g - A ) ) <-> ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) )
92 89 91 anbi12d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ f || ( g - A ) ) ) <-> ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) ) )
93 breq1 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( f || ( h - C ) <-> ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) )
94 93 anbi2d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( 2 x. C ) || ( g - 1 ) /\ f || ( h - C ) ) <-> ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) ) )
95 94 anbi1d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( 2 x. C ) || ( g - 1 ) /\ f || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) <-> ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) )
96 92 95 anbi12d 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( 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 ) ) ) <-> ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) )
97 96 2rexbidv 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( 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 ) ) ) <-> E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) )
98 97 2rexbidv 
 |-  ( f = ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) -> ( E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( 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 ) ) ) <-> E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) )
99 74 85 98 rspc3ev 
 |-  ( ( ( ( A rmX B ) e. NN0 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) e. NN0 ) /\ E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( ( A rmX B ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ ( A rmY ( 2 x. ( B x. ( A rmY B ) ) ) ) = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ ( A rmX ( 2 x. ( B x. ( A rmY B ) ) ) ) || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) -> 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 ) ) ) )
100 15 66 99 syl2anc 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ C = ( A rmY 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 ) ) ) )
101 100 ex 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) -> ( C = ( A rmY 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 ) ) ) ) )
102 simpll1 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> A e. ( ZZ>= ` 2 ) )
103 102 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> A e. ( ZZ>= ` 2 ) )
104 simpll2 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> B e. NN )
105 104 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> B e. NN )
106 simpll3 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> C e. NN )
107 106 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> C e. NN )
108 simplrl 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> d e. NN0 )
109 108 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> d e. NN0 )
110 simplrr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> e e. NN0 )
111 110 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> e e. NN0 )
112 simprl 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> f e. NN0 )
113 112 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> f e. NN0 )
114 simprr 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) -> g e. NN0 )
115 114 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> g e. NN0 )
116 simprl 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) /\ ( h e. NN0 /\ i e. NN0 ) ) -> h e. NN0 )
117 116 ad2antrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> h e. NN0 )
118 simprr 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) /\ ( h e. NN0 /\ i e. NN0 ) ) -> i e. NN0 )
119 118 ad2antrr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> i e. NN0 )
120 simplr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> j e. NN0 )
121 simp2l1 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> ( ( d ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
122 121 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> ( ( d ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
123 simp2l2 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 )
124 123 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 )
125 simp2l3 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> g e. ( ZZ>= ` 2 ) )
126 125 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> g e. ( ZZ>= ` 2 ) )
127 simp2r1 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 )
128 127 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 )
129 simp2r2 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> e = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
130 129 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> e = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
131 simp2r3 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> f || ( g - A ) )
132 131 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> f || ( g - A ) )
133 simp3ll 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> ( 2 x. C ) || ( g - 1 ) )
134 133 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> ( 2 x. C ) || ( g - 1 ) )
135 simp3lr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> f || ( h - C ) )
136 135 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> f || ( h - C ) )
137 simp3rl 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> ( 2 x. C ) || ( h - B ) )
138 137 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> ( 2 x. C ) || ( h - B ) )
139 simp3rr 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) -> B <_ C )
140 139 3expb 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> B <_ C )
141 103 105 107 109 111 113 115 117 119 120 122 124 126 128 130 132 134 136 138 140 jm2.27b 
 |-  ( ( ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( 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 ) ) ) ) -> C = ( A rmY B ) )
142 141 rexlimdva2 
 |-  ( ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ g e. NN0 ) ) /\ ( h e. NN0 /\ 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 ) ) ) -> C = ( A rmY B ) ) )
143 142 rexlimdvva 
 |-  ( ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ e e. NN0 ) ) /\ ( f e. NN0 /\ 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 ) ) ) -> C = ( A rmY B ) ) )
144 143 rexlimdvva 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) /\ ( d e. NN0 /\ 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 ) ) ) -> C = ( A rmY B ) ) )
145 144 rexlimdvva 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) -> ( 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 ) ) ) -> C = ( A rmY B ) ) )
146 101 145 impbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) -> ( C = ( A rmY 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 ) ) ) ) )