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

Theorem pellexlem6 29324
Description: Lemma for pellex 29325. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)
Hypotheses
Ref Expression
pellex.ann  |-  ( ph  ->  A  e.  NN )
pellex.bnn  |-  ( ph  ->  B  e.  NN )
pellex.cz  |-  ( ph  ->  C  e.  ZZ )
pellex.dnn  |-  ( ph  ->  D  e.  NN )
pellex.irr  |-  ( ph  ->  -.  ( sqr `  D
)  e.  QQ )
pellex.enn  |-  ( ph  ->  E  e.  NN )
pellex.fnn  |-  ( ph  ->  F  e.  NN )
pellex.neq  |-  ( ph  ->  -.  ( A  =  E  /\  B  =  F ) )
pellex.cn0  |-  ( ph  ->  C  =/=  0 )
pellex.no1  |-  ( ph  ->  ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  C )
pellex.no2  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
pellex.xcg  |-  ( ph  ->  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C ) ) )
pellex.ycg  |-  ( ph  ->  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C ) ) )
Assertion
Ref Expression
pellexlem6  |-  ( ph  ->  E. a  e.  NN  E. b  e.  NN  (
( a ^ 2 )  -  ( D  x.  ( b ^
2 ) ) )  =  1 )
Distinct variable groups:    a, b, A    B, a, b    C, a, b    D, a, b    E, a, b    F, a, b    ph, a, b

Proof of Theorem pellexlem6
StepHypRef Expression
1 pellex.ann . . . . . . . . 9  |-  ( ph  ->  A  e.  NN )
21nncnd 10450 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3 pellex.enn . . . . . . . . 9  |-  ( ph  ->  E  e.  NN )
43nncnd 10450 . . . . . . . 8  |-  ( ph  ->  E  e.  CC )
52, 4mulcld 9518 . . . . . . 7  |-  ( ph  ->  ( A  x.  E
)  e.  CC )
6 pellex.dnn . . . . . . . . 9  |-  ( ph  ->  D  e.  NN )
76nncnd 10450 . . . . . . . 8  |-  ( ph  ->  D  e.  CC )
8 pellex.bnn . . . . . . . . . 10  |-  ( ph  ->  B  e.  NN )
98nncnd 10450 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
10 pellex.fnn . . . . . . . . . 10  |-  ( ph  ->  F  e.  NN )
1110nncnd 10450 . . . . . . . . 9  |-  ( ph  ->  F  e.  CC )
129, 11mulcld 9518 . . . . . . . 8  |-  ( ph  ->  ( B  x.  F
)  e.  CC )
137, 12mulcld 9518 . . . . . . 7  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  CC )
145, 13subcld 9831 . . . . . 6  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  CC )
15 pellex.cz . . . . . . 7  |-  ( ph  ->  C  e.  ZZ )
1615zcnd 10860 . . . . . 6  |-  ( ph  ->  C  e.  CC )
17 pellex.cn0 . . . . . 6  |-  ( ph  ->  C  =/=  0 )
1814, 16, 17absdivd 13060 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  =  ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) ) )
195, 13negsubd 9837 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F )
) )  =  ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )
2019eqcomd 2462 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =  ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) ) )
2120oveq1d 6216 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  ( ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) ) )
221nnred 10449 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
233nnred 10449 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
2422, 23remulcld 9526 . . . . . . . . . 10  |-  ( ph  ->  ( A  x.  E
)  e.  RR )
256nnred 10449 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  RR )
268nnred 10449 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
2710nnred 10449 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  RR )
2826, 27remulcld 9526 . . . . . . . . . . 11  |-  ( ph  ->  ( B  x.  F
)  e.  RR )
2925, 28remulcld 9526 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  RR )
3029renegcld 9887 . . . . . . . . . 10  |-  ( ph  -> 
-u ( D  x.  ( B  x.  F
) )  e.  RR )
3116, 17absrpcld 13053 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  C
)  e.  RR+ )
323nnzd 10858 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  ZZ )
33 pellex.xcg . . . . . . . . . . . 12  |-  ( ph  ->  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C ) ) )
34 modmul1 11870 . . . . . . . . . . . 12  |-  ( ( ( A  e.  RR  /\  E  e.  RR )  /\  ( E  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C
) ) )  -> 
( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  E )  mod  ( abs `  C
) ) )
3522, 23, 32, 31, 33, 34syl221anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  E )  mod  ( abs `  C
) ) )
364sqcld 12124 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
3711sqcld 12124 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F ^ 2 )  e.  CC )
387, 37mulcld 9518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
3936, 38npcand 9835 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  =  ( E ^
2 ) )
404sqvald 12123 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
4139, 40eqtr2d 2496 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  E
)  =  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) ) )
4241oveq1d 6216 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
4323resqcld 12152 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  e.  RR )
4427resqcld 12152 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  e.  RR )
4525, 44remulcld 9526 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  RR )
4643, 45resubcld 9888 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR )
47 0re 9498 . . . . . . . . . . . . . 14  |-  0  e.  RR
4847a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  RR )
4916abscld 13041 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  C
)  e.  RR )
5049recnd 9524 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  e.  CC )
5116, 17absne0d 13052 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  =/=  0 )
5250, 51dividd 10217 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  =  1 )
53 1z 10788 . . . . . . . . . . . . . . . . . 18  |-  1  e.  ZZ
5453a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
5552, 54eqeltrd 2542 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  e.  ZZ )
56 mod0 11833 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs `  C
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  C
)  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  /  ( abs `  C ) )  e.  ZZ ) )
5749, 31, 56syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( abs `  C )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  / 
( abs `  C
) )  e.  ZZ ) )
5855, 57mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  C
)  mod  ( abs `  C ) )  =  0 )
5915zred 10859 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
60 absmod0 12911 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( C  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  mod  ( abs `  C
) )  =  0 ) )
6159, 31, 60syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  mod  ( abs `  C ) )  =  0  <->  (
( abs `  C
)  mod  ( abs `  C ) )  =  0 ) )
6258, 61mpbird 232 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C  mod  ( abs `  C ) )  =  0 )
63 pellex.no2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
6463oveq1d 6216 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( C  mod  ( abs `  C ) ) )
65 0mod 11857 . . . . . . . . . . . . . . 15  |-  ( ( abs `  C )  e.  RR+  ->  ( 0  mod  ( abs `  C
) )  =  0 )
6631, 65syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  mod  ( abs `  C ) )  =  0 )
6762, 64, 663eqtr4d 2505 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )
68 modadd1 11863 . . . . . . . . . . . . 13  |-  ( ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR  /\  0  e.  RR )  /\  ( ( D  x.  ( F ^ 2 ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  /\  (
( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )  ->  ( (
( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  mod  ( abs `  C
) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
6946, 48, 45, 31, 67, 68syl221anc 1230 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
7038addid2d 9682 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( F ^
2 ) ) )
7111sqvald 12123 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  =  ( F  x.  F ) )
7271oveq2d 6217 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  =  ( D  x.  ( F  x.  F
) ) )
737, 11, 11mul12d 9690 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F  x.  F )
)  =  ( F  x.  ( D  x.  F ) ) )
7470, 72, 733eqtrd 2499 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( F  x.  ( D  x.  F ) ) )
7574oveq1d 6216 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) ) )
7642, 69, 753eqtrd 2499 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
776nnzd 10858 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  ZZ )
7810nnzd 10858 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ZZ )
7977, 78zmulcld 10865 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  F
)  e.  ZZ )
80 pellex.ycg . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C ) ) )
8180eqcomd 2462 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C ) ) )
82 modmul1 11870 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  RR  /\  B  e.  RR )  /\  ( ( D  x.  F )  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C
) ) )  -> 
( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
8327, 26, 79, 31, 81, 82syl221anc 1230 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
849, 7, 11mul12d 9690 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  x.  ( D  x.  F )
)  =  ( D  x.  ( B  x.  F ) ) )
8584oveq1d 6216 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8683, 85eqtrd 2495 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8735, 76, 863eqtrd 2499 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
88 modadd1 11863 . . . . . . . . . 10  |-  ( ( ( ( A  x.  E )  e.  RR  /\  ( D  x.  ( B  x.  F )
)  e.  RR )  /\  ( -u ( D  x.  ( B  x.  F ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  /\  ( ( A  x.  E )  mod  ( abs `  C
) )  =  ( ( D  x.  ( B  x.  F )
)  mod  ( abs `  C ) ) )  ->  ( ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) ) )
8924, 29, 30, 31, 87, 88syl221anc 1230 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) ) )
9013negidd 9821 . . . . . . . . . 10  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  =  0 )
9190oveq1d 6216 . . . . . . . . 9  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
9221, 89, 913eqtrd 2499 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
9392, 66eqtrd 2495 . . . . . . 7  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  0 )
9424, 29resubcld 9888 . . . . . . . 8  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR )
95 absmod0 12911 . . . . . . . 8  |-  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 ) )
9694, 31, 95syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 ) )
9793, 96mpbid 210 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 )
9814abscld 13041 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR )
99 mod0 11833 . . . . . . 7  |-  ( ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ ) )
10098, 31, 99syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ ) )
10197, 100mpbid 210 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ )
10218, 101eqeltrd 2542 . . . 4  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ )
10394, 59, 17redivcld 10271 . . . . 5  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  RR )
104 absz 12919 . . . . 5  |-  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  e.  RR  ->  ( (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  e.  ZZ  <->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ ) )
105103, 104syl 16 . . . 4  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C )  e.  ZZ  <->  ( abs `  ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ ) )
106102, 105mpbird 232 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ )
107 0lt1 9974 . . . . . . . 8  |-  0  <  1
108 1re 9497 . . . . . . . . 9  |-  1  e.  RR
10947, 108ltnlei 9607 . . . . . . . 8  |-  ( 0  <  1  <->  -.  1  <_  0 )
110107, 109mpbi 208 . . . . . . 7  |-  -.  1  <_  0
1119, 4mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  x.  E
)  e.  CC )
1122, 11mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  F
)  e.  CC )
113111, 112subcld 9831 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  CC )
114113, 16, 17divcld 10219 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  CC )
115114abscld 13041 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  RR )
116115resqcld 12152 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  e.  RR )
1176nnnn0d 10748 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  NN0 )
118117nn0ge0d 10751 . . . . . . . . . 10  |-  ( ph  ->  0  <_  D )
119115sqge0d 12153 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) )
12025, 116, 118, 119mulge0d 10028 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )
12125, 116remulcld 9526 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  e.  RR )
12248, 121suble0d 10042 . . . . . . . . 9  |-  ( ph  ->  ( ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  <_  0  <->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) ) )
123120, 122mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) ) )  <_  0 )
124 breq1 4404 . . . . . . . 8  |-  ( 1  =  ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  ->  (
1  <_  0  <->  ( 0  -  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  <_  0
) )
125123, 124syl5ibrcom 222 . . . . . . 7  |-  ( ph  ->  ( 1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  -> 
1  <_  0 ) )
126110, 125mtoi 178 . . . . . 6  |-  ( ph  ->  -.  1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) ) )
127 absresq 12910 . . . . . . . . . . . 12  |-  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  e.  RR  ->  ( ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ) ^
2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
) ^ 2 ) )
128103, 127syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 ) )
12914, 16, 17sqdivd 12139 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) ^ 2 )  / 
( C ^ 2 ) ) )
13014sqvald 12123 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) ^ 2 )  =  ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) ) )
131130oveq1d 6216 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) ) ^
2 )  /  ( C ^ 2 ) )  =  ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  / 
( C ^ 2 ) ) )
132128, 129, 1313eqtrd 2499 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( C ^ 2 ) ) )
13326, 23remulcld 9526 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  x.  E
)  e.  RR )
13422, 27remulcld 9526 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  x.  F
)  e.  RR )
135133, 134resubcld 9888 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR )
136135, 59, 17redivcld 10271 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  RR )
137 absresq 12910 . . . . . . . . . . . . . 14  |-  ( ( ( ( B  x.  E )  -  ( A  x.  F )
)  /  C )  e.  RR  ->  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) ^
2 ) )
138136, 137syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) ^
2 ) )
139113, 16, 17sqdivd 12139 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ^ 2 )  =  ( ( ( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 )  /  ( C ^
2 ) ) )
140138, 139eqtrd 2495 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) )
141140oveq2d 6217 . . . . . . . . . . 11  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  =  ( D  x.  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) ) )
142113sqcld 12124 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  e.  CC )
14316sqcld 12124 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  e.  CC )
144 sqne0 12050 . . . . . . . . . . . . . 14  |-  ( C  e.  CC  ->  (
( C ^ 2 )  =/=  0  <->  C  =/=  0 ) )
14516, 144syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( C ^
2 )  =/=  0  <->  C  =/=  0 ) )
14617, 145mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  =/=  0 )
1477, 142, 143, 146divassd 10254 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 ) )  /  ( C ^ 2 ) )  =  ( D  x.  ( ( ( ( B  x.  E )  -  ( A  x.  F ) ) ^
2 )  /  ( C ^ 2 ) ) ) )
148113sqvald 12123 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  =  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )
149148oveq2d 6217 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 ) )  =  ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F )
) ) ) )
150149oveq1d 6216 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 ) )  /  ( C ^ 2 ) )  =  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F )
) ) )  / 
( C ^ 2 ) ) )
151141, 147, 1503eqtr2d 2501 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  =  ( ( D  x.  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )  /  ( C ^
2 ) ) )
152132, 151oveq12d 6219 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
) ) ^ 2 )  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  =  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  / 
( C ^ 2 ) )  -  (
( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  /  ( C ^ 2 ) ) ) )
15314, 14mulcld 9518 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
154113, 113mulcld 9518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  CC )
1557, 154mulcld 9518 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  e.  CC )
156153, 155, 143, 146divsubdird 10258 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  -  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) ) )  /  ( C ^ 2 ) )  =  ( ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  / 
( C ^ 2 ) )  -  (
( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  /  ( C ^ 2 ) ) ) )
1575, 13, 5, 13mulsubd 9915 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  =  ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F
) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) ) ) ) )
158111, 112, 111, 112mulsubd 9915 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  =  ( ( ( ( B  x.  E )  x.  ( B  x.  E )
)  +  ( ( A  x.  F )  x.  ( A  x.  F ) ) )  -  ( ( ( B  x.  E )  x.  ( A  x.  F ) )  +  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )
159158oveq2d 6217 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  =  ( D  x.  ( ( ( ( B  x.  E
)  x.  ( B  x.  E ) )  +  ( ( A  x.  F )  x.  ( A  x.  F
) ) )  -  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
160111, 111mulcld 9518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( B  x.  E )
)  e.  CC )
161112, 112mulcld 9518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  F )  x.  ( A  x.  F )
)  e.  CC )
162160, 161addcld 9517 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
163111, 112mulcld 9518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( A  x.  F )
)  e.  CC )
164163, 163addcld 9517 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
1657, 162, 164subdid 9912 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  (
( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  -  ( ( ( B  x.  E
)  x.  ( A  x.  F ) )  +  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) ) )  =  ( ( D  x.  ( ( ( B  x.  E
)  x.  ( B  x.  E ) )  +  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )  -  ( D  x.  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
1667, 160, 161adddid 9522 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  x.  ( B  x.  E )
)  +  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  =  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )
1677, 163, 163adddid 9522 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  x.  ( A  x.  F )
)  +  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) )  =  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )
168166, 167oveq12d 6219 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) ) )  -  ( D  x.  ( (
( B  x.  E
)  x.  ( A  x.  F ) )  +  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) ) )  =  ( ( ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) )  +  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
169159, 165, 1683eqtrd 2499 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  =  ( ( ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) )  +  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
170157, 169oveq12d 6219 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  -  ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F )
) ) ) )  =  ( ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F
) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) ) )
171170oveq1d 6216 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  -  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) ) )  /  ( C ^ 2 ) )  =  ( ( ( ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) ) ) )  -  ( ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) ) )  / 
( C ^ 2 ) ) )
1725, 13mulcomd 9519 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( A  x.  E
) ) )
1737, 12, 5mulassd 9521 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( A  x.  E )
)  =  ( D  x.  ( ( B  x.  F )  x.  ( A  x.  E
) ) ) )
1742, 4mulcomd 9519 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  x.  E
)  =  ( E  x.  A ) )
175174oveq2d 6217 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  F )  x.  ( E  x.  A ) ) )
1769, 11, 4, 2mul4d 9693 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( E  x.  A )
)  =  ( ( B  x.  E )  x.  ( F  x.  A ) ) )
17711, 2mulcomd 9519 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F  x.  A
)  =  ( A  x.  F ) )
178177oveq2d 6217 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E )  x.  ( F  x.  A )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
179175, 176, 1783eqtrd 2499 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
180179oveq2d 6217 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  F
)  x.  ( A  x.  E ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) )
181172, 173, 1803eqtrd 2499 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) )
182181, 181oveq12d 6219 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) )  +  ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) ) )  =  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )
183182oveq2d 6217 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E )  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) ) ) )  =  ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) ) )
184183oveq1d 6216 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) )  +  ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  =  ( ( ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )  -  ( ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) ) ) )
1855, 5mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  x.  E )  x.  ( A  x.  E )
)  e.  CC )
18613, 13mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) )  e.  CC )
187185, 186addcld 9517 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
1887, 160mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  e.  CC )
1897, 161mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
190188, 189addcld 9517 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  e.  CC )
1917, 163mulcld 9518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
192191, 191addcld 9517 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) )  e.  CC )
193187, 190, 192nnncan2d 9866 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  =  ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) )  +  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) ) ) ) )
194185, 186, 188, 189addsub4d 9878 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E )  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )  =  ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  -  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) ) )  +  ( ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) )  -  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) ) ) )
1955sqvald 12123 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A  x.  E )  x.  ( A  x.  E ) ) )
196111sqvald 12123 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B  x.  E )  x.  ( B  x.  E ) ) )
197196oveq2d 6217 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )
198195, 197oveq12d 6219 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A  x.  E ) ^
2 )  -  ( D  x.  ( ( B  x.  E ) ^ 2 ) ) )  =  ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  -  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) ) ) )
19913sqvald 12123 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )
200112sqvald 12123 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A  x.  F )  x.  ( A  x.  F ) ) )
201200oveq2d 6217 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )
202199, 201oveq12d 6219 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) ) ^
2 )  -  ( D  x.  ( ( A  x.  F ) ^ 2 ) ) )  =  ( ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) )  -  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )
203198, 202oveq12d 6219 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E ) ^ 2 )  -  ( D  x.  (
( B  x.  E
) ^ 2 ) ) )  +  ( ( ( D  x.  ( B  x.  F
) ) ^ 2 )  -  ( D  x.  ( ( A  x.  F ) ^
2 ) ) ) )  =  ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  -  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )  +  ( ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) )  -  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) ) ) ) )
2042, 4sqmuld 12138 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( E ^
2 ) ) )
2059, 4sqmuld 12138 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( E ^
2 ) ) )
206205oveq2d 6217 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B ^ 2 )  x.  ( E ^ 2 ) ) ) )
2079sqcld 12124 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B ^ 2 )  e.  CC )
2087, 207, 36mulassd 9521 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) )  =  ( D  x.  ( ( B ^
2 )  x.  ( E ^ 2 ) ) ) )
209206, 208eqtr4d 2498 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )
210204, 209oveq12d 6219 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A  x.  E ) ^
2 )  -  ( D  x.  ( ( B  x.  E ) ^ 2 ) ) )  =  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  ( ( D  x.  ( B ^
2 ) )  x.  ( E ^ 2 ) ) ) )
2117sqvald 12123 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D ^ 2 )  =  ( D  x.  D ) )
2129, 11sqmuld 12138 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( F ^
2 ) ) )
213211, 212oveq12d 6219 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D ^
2 )  x.  (
( B  x.  F
) ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^ 2 )  x.  ( F ^ 2 ) ) ) )
2147, 12sqmuld 12138 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D ^ 2 )  x.  ( ( B  x.  F ) ^
2 ) ) )
2157, 7mulcld 9518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  D
)  e.  CC )
216215, 207, 37mulassd 9521 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^
2 )  x.  ( F ^ 2 ) ) ) )
217213, 214, 2163eqtr4d 2505 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) ) )
2182, 11sqmuld 12138 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( F ^
2 ) ) )
219218oveq2d 6217 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A ^ 2 )  x.  ( F ^ 2 ) ) ) )
2202sqcld 12124 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A ^ 2 )  e.  CC )
2217, 220, 37mulassd 9521 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( D  x.  ( ( A ^
2 )  x.  ( F ^ 2 ) ) ) )
222219, 221eqtr4d 2498 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )
223217, 222oveq12d 6219 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) ) ^
2 )  -  ( D  x.  ( ( A  x.  F ) ^ 2 ) ) )  =  ( ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) )  -  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) ) ) )
224210, 223oveq12d 6219 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( A  x.  E ) ^ 2 )  -  ( D  x.  (
( B  x.  E
) ^ 2 ) ) )  +  ( ( ( D  x.  ( B  x.  F
) ) ^ 2 )  -  ( D  x.  ( ( A  x.  F ) ^
2 ) ) ) )  =  ( ( ( ( A ^
2 )  x.  ( E ^ 2 ) )  -  ( ( D  x.  ( B ^
2 ) )  x.  ( E ^ 2 ) ) )  +  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  x.  ( F ^ 2 ) )  -  (
( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) ) ) )
2257, 207mulcld 9518 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( B ^ 2 ) )  e.  CC )
226220, 225, 36subdird 9913 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( ( ( A ^ 2 )  x.  ( E ^
2 ) )  -  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) ) ) )
227 pellex.no1 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  C )
228227oveq1d 6216 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( C  x.  ( E ^ 2 ) ) )
229226, 228eqtr3d 2497 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  (
( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )  =  ( C  x.  ( E ^ 2 ) ) )
2307, 7, 207mulassd 9521 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  =  ( D  x.  ( D  x.  ( B ^ 2 ) ) ) )
231230oveq1d 6216 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
232231oveq1d 6216 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) ) )
233215, 207mulcld 9518 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  e.  CC )
2347, 220mulcld 9518 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( A ^ 2 ) )  e.  CC )
235233, 234, 37subdird 9913 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) )  -  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) ) ) )
236 subdi 9890 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC  /\  ( A ^ 2 )  e.  CC )  ->  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
237236eqcomd 2462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC  /\  ( A ^ 2 )  e.  CC )  ->  (
( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
2387, 225, 220, 237syl3anc 1219 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
239 negsubdi2 9780 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A ^ 2 )  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC )  ->  -u ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )
240239eqcomd 2462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A ^ 2 )  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC )  -> 
( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
241220, 225, 240syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
242227negeqd 9716 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  -u C
)
243241, 242eqtrd 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u C )
244243oveq2d 6217 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  (
( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( D  x.  -u C ) )
2457, 16mulneg2d 9910 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  -u C
)  =  -u ( D  x.  C )
)
246238, 244, 2453eqtrd 2499 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  -u ( D  x.  C ) )
247246oveq1d 6216 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) )
248232, 235, 2473eqtr3d 2503 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  x.  ( F ^ 2 ) )  -  (
( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )  =  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) )
249229, 248oveq12d 6219 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( A ^ 2 )  x.  ( E ^
2 ) )  -  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) ) )  +  ( ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) )  -  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) ) )
2507, 16mulcld 9518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  C
)  e.  CC )
251250, 37mulneg1d 9909 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( ( D  x.  C )  x.  ( F ^ 2 ) ) )
2527, 16mulcomd 9519 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( D  x.  C
)  =  ( C  x.  D ) )
253252oveq1d 6216 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( ( C  x.  D )  x.  ( F ^ 2 ) ) )
25416, 7, 37mulassd 9521 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( C  x.  D )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
255253, 254eqtrd 2495 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
256255negeqd 9716 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
257251, 256eqtrd 2495 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
258257oveq2d 6217 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
25916, 36mulcld 9518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( E ^ 2 ) )  e.  CC )
26016, 38mulcld 9518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( D  x.  ( F ^ 2 ) ) )  e.  CC )
261259, 260negsubd 9837 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^
2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
26263oveq2d 6217 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( C  x.  C ) )
263 subdi 9890 . . . . . . . . . . . . . . . . . 18  |-  ( ( C  e.  CC  /\  ( E ^ 2 )  e.  CC  /\  ( D  x.  ( F ^ 2 ) )  e.  CC )  -> 
( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
264263eqcomd 2462 . . . . . . . . . . . . . . . . 17  |-  ( ( C  e.  CC  /\  ( E ^ 2 )  e.  CC  /\  ( D  x.  ( F ^ 2 ) )  e.  CC )  -> 
( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26516, 36, 38, 264syl3anc 1219 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26616sqvald 12123 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C ^ 2 )  =  ( C  x.  C ) )
267262, 265, 2663eqtr4d 2505 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C ^ 2 ) )
268258, 261, 2673eqtrd 2499 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( C ^ 2 ) )
269224, 249, 2683eqtrd 2499 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E ) ^ 2 )  -  ( D  x.  (
( B  x.  E
) ^ 2 ) ) )  +  ( ( ( D  x.  ( B  x.  F
) ) ^ 2 )  -  ( D  x.  ( ( A  x.  F ) ^
2 ) ) ) )  =  ( C ^ 2 ) )
270194, 203, 2693eqtr2d 2501 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( A  x.  E )  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )  =  ( C ^
2 ) )
271184, 193, 2703eqtrd 2499 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) )  +  ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  =  ( C ^ 2 ) )
272271oveq1d 6216 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F
) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  /  ( C ^ 2 ) )  =  ( ( C ^ 2 )  / 
( C ^ 2 ) ) )
273143, 146dividd 10217 . . . . . . . . . 10  |-  ( ph  ->  ( ( C ^
2 )  /  ( C ^ 2 ) )  =  1 )
274171, 272, 2733eqtrd 2499 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  -  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) ) )  /  ( C ^ 2 ) )  =  1 )
275152, 156, 2743eqtr2d 2501 . . . . . . . 8  |-  ( ph  ->  ( ( ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
) ) ^ 2 )  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  =  1 )
276275adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  =  1 )
277 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  =  0 )
278277oveq1d 6216 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  =  ( 0  /  C
) )
279278fveq2d 5804 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  ( abs `  (
0  /  C ) ) )
28016, 17div0d 10218 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  /  C
)  =  0 )
281280abs00bd 12899 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
0  /  C ) )  =  0 )
282281adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( 0  /  C ) )  =  0 )
283279, 282eqtrd 2495 . . . . . . . . 9  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  0 )
284283sq0id 12077 . . . . . . . 8  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  0 )
285284oveq1d 6216 . . . . . . 7  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) ) )
286276, 285eqtr3d 2497 . . . . . 6  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  1  =  ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) ) )
287126, 286mtand 659 . . . . 5  |-  ( ph  ->  -.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  =  0 )
288287neneqad 2656 . . . 4  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =/=  0 )
28914, 16, 288, 17divne0d 10235 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )
290 nnabscl 12932 . . 3  |-  ( ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ  /\  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
291106, 289, 290syl2anc 661 . 2  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
292113, 16, 17absdivd 13060 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  =  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F ) ) )  /  ( abs `  C
) ) )
293 negsub 9769 . . . . . . . . . . . 12  |-  ( ( ( B  x.  E
)  e.  CC  /\  ( A  x.  F
)  e.  CC )  ->  ( ( B  x.  E )  + 
-u ( A  x.  F ) )  =  ( ( B  x.  E )  -  ( A  x.  F )
) )
294293eqcomd 2462 . . . . . . . . . . 11  |-  ( ( ( B  x.  E
)  e.  CC  /\  ( A  x.  F
)  e.  CC )  ->  ( ( B  x.  E )  -  ( A  x.  F
) )  =  ( ( B  x.  E
)  +  -u ( A  x.  F )
) )
295111, 112, 294syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  =  ( ( B  x.  E )  +  -u ( A  x.  F ) ) )
296295oveq1d 6216 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) ) )
297134renegcld 9887 . . . . . . . . . 10  |-  ( ph  -> 
-u ( A  x.  F )  e.  RR )
29811, 4mulcomd 9519 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  E
)  =  ( E  x.  F ) )
299298oveq1d 6216 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
300 modmul1 11870 . . . . . . . . . . . 12  |-  ( ( ( B  e.  RR  /\  F  e.  RR )  /\  ( E  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C
) ) )  -> 
( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
30126, 27, 32, 31, 80, 300syl221anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
302 modmul1 11870 . . . . . . . . . . . 12  |-  ( ( ( A  e.  RR  /\  E  e.  RR )  /\  ( F  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C
) ) )  -> 
( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
30322, 23, 78, 31, 33, 302syl221anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
304299, 301, 3033eqtr4d 2505 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( A  x.  F )  mod  ( abs `  C
) ) )
305 modadd1 11863 . . . . . . . . . 10  |-  ( ( ( ( B  x.  E )  e.  RR  /\  ( A  x.  F
)  e.  RR )  /\  ( -u ( A  x.  F )  e.  RR  /\  ( abs `  C )  e.  RR+ )  /\  ( ( B  x.  E )  mod  ( abs `  C
) )  =  ( ( A  x.  F
)  mod  ( abs `  C ) ) )  ->  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
306133, 134, 297, 31, 304, 305syl221anc 1230 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
307112negidd 9821 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  F )  +  -u ( A  x.  F
) )  =  0 )
308307oveq1d 6216 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  F )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
309296, 306, 3083eqtrd 2499 . . . . . . . 8  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
310309, 66eqtrd 2495 . . . . . . 7  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0 )
311 absmod0 12911 . . . . . . . 8  |-  ( ( ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F
) ) )  mod  ( abs `  C
) )  =  0 ) )
312135, 31, 311syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 ) )
313310, 312mpbid 210 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 )
314113abscld 13041 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR )
315 mod0 11833 . . . . . . 7  |-  ( ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F )
) )  /  ( abs `  C ) )  e.  ZZ ) )
316314, 31, 315syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F )
) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F
) ) )  / 
( abs `  C
) )  e.  ZZ ) )
317313, 316mpbid 210 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  /  ( abs `  C ) )  e.  ZZ )
318292, 317eqeltrd 2542 . . . 4  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  ZZ )
319 absz 12919 . . . . 5  |-  ( ( ( ( B  x.  E )  -  ( A  x.  F )
)  /  C )  e.  RR  ->  (
( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ  <->  ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) )  e.  ZZ ) )
320136, 319syl 16 . . . 4  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C )  e.  ZZ  <->  ( abs `  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) )  e.  ZZ ) )
321318, 320mpbird 232 . . 3  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ )
322 pellex.neq . . . . . . 7  |-  ( ph  ->  -.  ( A  =  E  /\  B  =  F ) )
32310nnne0d 10478 . . . . . . . . 9  |-  ( ph  ->  F  =/=  0 )
3243nnne0d 10478 . . . . . . . . 9  |-  ( ph  ->  E  =/=  0 )
3259, 11, 2, 4, 323, 324divmuleqd 10265 . . . . . . . 8  |-  ( ph  ->  ( ( B  /  F )  =  ( A  /  E )  <-> 
( B  x.  E
)  =  ( A  x.  F ) ) )
32663adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
327326eqcomd 2462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  C  =  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) ) )
328327oveq2d 6217 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  C )  =  ( ( ( B  /  F ) ^
2 )  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
3299, 11, 323divcld 10219 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  F
)  e.  CC )
330329sqcld 12124 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  /  F ) ^ 2 )  e.  CC )
331330adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  e.  CC )
33236adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  e.  CC )
33338adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
334331, 332, 333subdid 9912 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( ( ( B  /  F ) ^
2 )  x.  ( E ^ 2 ) )  -  ( ( ( B  /  F ) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
335 oveq1 6208 . . . . . . . . . . . . . . . . 17  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( B  /  F
) ^ 2 )  =  ( ( A  /  E ) ^
2 ) )
336335oveq1d 6216 . . . . . . . . . . . . . . . 16  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( ( B  /  F ) ^ 2 )  x.  ( E ^ 2 ) )  =  ( ( ( A  /  E ) ^ 2 )  x.  ( E ^ 2 ) ) )
337336adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A  /  E ) ^
2 )  x.  ( E ^ 2 ) ) )
3382adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  A  e.  CC )
3394adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  e.  CC )
340324adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  =/=  0 )
341338, 339, 340sqdivd 12139 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( A  /  E ) ^
2 )  =  ( ( A ^ 2 )  /  ( E ^ 2 ) ) )
342341oveq1d 6216 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A  /  E
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A ^ 2 )  / 
( E ^ 2 ) )  x.  ( E ^ 2 ) ) )
343220adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( A ^ 2 )  e.  CC )
344 sqne0 12050 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  CC  ->  (
( E ^ 2 )  =/=  0  <->  E  =/=  0 ) )
3454, 344syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( E ^
2 )  =/=  0  <->  E  =/=  0 ) )
346324, 345mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E ^ 2 )  =/=  0 )
347346adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  =/=  0 )
348343, 332, 347divcan1d 10220 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A ^ 2 )  /  ( E ^ 2 ) )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
349337, 342, 3483eqtrd 2499 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
3507adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  D  e.  CC )
35137adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  e.  CC )
352331, 350, 351mul12d 9690 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B  /  F
) ^ 2 )  x.  ( F ^
2 ) ) ) )
3539adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  B  e.  CC )
35411adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  e.  CC )
355323adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  =/=  0 )
356353, 354, 355sqdivd 12139 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  =  ( ( B ^ 2 )  /  ( F ^ 2 ) ) )
357356oveq1d 6216 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( F ^
2 ) )  =  ( ( ( B ^ 2 )  / 
( F ^ 2 ) )  x.  ( F ^ 2 ) ) )
358357oveq2d 6217 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( ( ( B  /  F ) ^
2 )  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B ^ 2 )  /  ( F ^
2 ) )  x.  ( F ^ 2 ) ) ) )
359207adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( B ^ 2 )  e.  CC )
360 sqne0 12050 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  e.  CC  ->  (
( F ^ 2 )  =/=  0  <->  F  =/=  0 ) )
36111, 360syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( F ^
2 )  =/=  0  <->  F  =/=  0 ) )
362323, 361mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F ^ 2 )  =/=  0 )
363362adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  =/=  0 )
364359, 351, 363divcan1d 10220 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B ^ 2 )  /  ( F ^ 2 )