Metamath Proof Explorer

Theorem jm2.27b

Description: Lemma for jm2.27 . Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Hypotheses jm2.27a1 
|- ( ph -> A e. ( ZZ>= ` 2 ) )
jm2.27a2 
|- ( ph -> B e. NN )
jm2.27a3 
|- ( ph -> C e. NN )
jm2.27a4 
|- ( ph -> D e. NN0 )
jm2.27a5 
|- ( ph -> E e. NN0 )
jm2.27a6 
|- ( ph -> F e. NN0 )
jm2.27a7 
|- ( ph -> G e. NN0 )
jm2.27a8 
|- ( ph -> H e. NN0 )
jm2.27a9 
|- ( ph -> I e. NN0 )
jm2.27a10 
|- ( ph -> J e. NN0 )
jm2.27a11 
|- ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
jm2.27a12 
|- ( ph -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )
jm2.27a13 
|- ( ph -> G e. ( ZZ>= ` 2 ) )
jm2.27a14 
|- ( ph -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )
jm2.27a15 
|- ( ph -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
jm2.27a16 
|- ( ph -> F || ( G - A ) )
jm2.27a17 
|- ( ph -> ( 2 x. C ) || ( G - 1 ) )
jm2.27a18 
|- ( ph -> F || ( H - C ) )
jm2.27a19 
|- ( ph -> ( 2 x. C ) || ( H - B ) )
jm2.27a20 
|- ( ph -> B <_ C )
Assertion jm2.27b 
|- ( ph -> C = ( A rmY B ) )

Proof

Step Hyp Ref Expression
1 jm2.27a1 
 |-  ( ph -> A e. ( ZZ>= ` 2 ) )
2 jm2.27a2 
 |-  ( ph -> B e. NN )
3 jm2.27a3 
 |-  ( ph -> C e. NN )
4 jm2.27a4 
 |-  ( ph -> D e. NN0 )
5 jm2.27a5 
 |-  ( ph -> E e. NN0 )
6 jm2.27a6 
 |-  ( ph -> F e. NN0 )
7 jm2.27a7 
 |-  ( ph -> G e. NN0 )
8 jm2.27a8 
 |-  ( ph -> H e. NN0 )
9 jm2.27a9 
 |-  ( ph -> I e. NN0 )
10 jm2.27a10 
 |-  ( ph -> J e. NN0 )
11 jm2.27a11 
 |-  ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
12 jm2.27a12 
 |-  ( ph -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )
13 jm2.27a13 
 |-  ( ph -> G e. ( ZZ>= ` 2 ) )
14 jm2.27a14 
 |-  ( ph -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )
15 jm2.27a15 
 |-  ( ph -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
16 jm2.27a16 
 |-  ( ph -> F || ( G - A ) )
17 jm2.27a17 
 |-  ( ph -> ( 2 x. C ) || ( G - 1 ) )
18 jm2.27a18 
 |-  ( ph -> F || ( H - C ) )
19 jm2.27a19 
 |-  ( ph -> ( 2 x. C ) || ( H - B ) )
20 jm2.27a20 
 |-  ( ph -> B <_ C )
21 3 nnzd 
 |-  ( ph -> C e. ZZ )
22 rmxycomplete 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ D e. NN0 /\ C e. ZZ ) -> ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 <-> E. p e. ZZ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) )
23 1 4 21 22 syl3anc 
 |-  ( ph -> ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 <-> E. p e. ZZ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) )
24 11 23 mpbid 
 |-  ( ph -> E. p e. ZZ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) )
25 12 adantr 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )
26 1 adantr 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> A e. ( ZZ>= ` 2 ) )
27 6 adantr 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> F e. NN0 )
28 5 nn0zd 
 |-  ( ph -> E e. ZZ )
29 28 adantr 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> E e. ZZ )
30 rmxycomplete 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ F e. NN0 /\ E e. ZZ ) -> ( ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 <-> E. q e. ZZ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) )
31 26 27 29 30 syl3anc 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> ( ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 <-> E. q e. ZZ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) )
32 25 31 mpbid 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> E. q e. ZZ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) )
33 14 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )
34 13 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> G e. ( ZZ>= ` 2 ) )
35 9 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> I e. NN0 )
36 8 nn0zd 
 |-  ( ph -> H e. ZZ )
37 36 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> H e. ZZ )
38 rmxycomplete 
 |-  ( ( G e. ( ZZ>= ` 2 ) /\ I e. NN0 /\ H e. ZZ ) -> ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 <-> E. r e. ZZ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) )
39 34 35 37 38 syl3anc 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 <-> E. r e. ZZ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) )
40 33 39 mpbid 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> E. r e. ZZ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) )
41 1 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> A e. ( ZZ>= ` 2 ) )
42 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> B e. NN )
43 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> C e. NN )
44 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> D e. NN0 )
45 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> E e. NN0 )
46 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> F e. NN0 )
47 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> G e. NN0 )
48 8 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> H e. NN0 )
49 9 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> I e. NN0 )
50 10 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> J e. NN0 )
51 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )
52 12 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )
53 13 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> G e. ( ZZ>= ` 2 ) )
54 14 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )
55 15 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )
56 16 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> F || ( G - A ) )
57 17 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> ( 2 x. C ) || ( G - 1 ) )
58 18 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> F || ( H - C ) )
59 19 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> ( 2 x. C ) || ( H - B ) )
60 20 ad3antrrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> B <_ C )
61 simprl 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> p e. ZZ )
62 61 ad2antrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> p e. ZZ )
63 simprrl 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> D = ( A rmX p ) )
64 63 ad2antrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> D = ( A rmX p ) )
65 simprrr 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> C = ( A rmY p ) )
66 65 ad2antrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> C = ( A rmY p ) )
67 simplrl 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> q e. ZZ )
68 simprl 
 |-  ( ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) -> F = ( A rmX q ) )
69 68 ad2antlr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> F = ( A rmX q ) )
70 simprr 
 |-  ( ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) -> E = ( A rmY q ) )
71 70 ad2antlr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> E = ( A rmY q ) )
72 simprl 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> r e. ZZ )
73 simprrl 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> I = ( G rmX r ) )
74 simprrr 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> H = ( G rmY r ) )
75 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 62 64 66 67 69 71 72 73 74 jm2.27a 
 |-  ( ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) /\ ( r e. ZZ /\ ( I = ( G rmX r ) /\ H = ( G rmY r ) ) ) ) -> C = ( A rmY B ) )
76 40 75 rexlimddv 
 |-  ( ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) /\ ( q e. ZZ /\ ( F = ( A rmX q ) /\ E = ( A rmY q ) ) ) ) -> C = ( A rmY B ) )
77 32 76 rexlimddv 
 |-  ( ( ph /\ ( p e. ZZ /\ ( D = ( A rmX p ) /\ C = ( A rmY p ) ) ) ) -> C = ( A rmY B ) )
78 24 77 rexlimddv 
 |-  ( ph -> C = ( A rmY B ) )