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 35604
Description: Lemma for pellex 35605. 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 10627 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3 pellex.enn . . . . . . . . 9  |-  ( ph  ->  E  e.  NN )
43nncnd 10627 . . . . . . . 8  |-  ( ph  ->  E  e.  CC )
52, 4mulcld 9665 . . . . . . 7  |-  ( ph  ->  ( A  x.  E
)  e.  CC )
6 pellex.dnn . . . . . . . . 9  |-  ( ph  ->  D  e.  NN )
76nncnd 10627 . . . . . . . 8  |-  ( ph  ->  D  e.  CC )
8 pellex.bnn . . . . . . . . . 10  |-  ( ph  ->  B  e.  NN )
98nncnd 10627 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
10 pellex.fnn . . . . . . . . . 10  |-  ( ph  ->  F  e.  NN )
1110nncnd 10627 . . . . . . . . 9  |-  ( ph  ->  F  e.  CC )
129, 11mulcld 9665 . . . . . . . 8  |-  ( ph  ->  ( B  x.  F
)  e.  CC )
137, 12mulcld 9665 . . . . . . 7  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  CC )
145, 13subcld 9988 . . . . . 6  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  CC )
15 pellex.cz . . . . . . 7  |-  ( ph  ->  C  e.  ZZ )
1615zcnd 11043 . . . . . 6  |-  ( ph  ->  C  e.  CC )
17 pellex.cn0 . . . . . 6  |-  ( ph  ->  C  =/=  0 )
1814, 16, 17absdivd 13510 . . . . 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 9994 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F )
) )  =  ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )
2019eqcomd 2431 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =  ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) ) )
2120oveq1d 6318 . . . . . . . . 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 10626 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
233nnred 10626 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
2422, 23remulcld 9673 . . . . . . . . . 10  |-  ( ph  ->  ( A  x.  E
)  e.  RR )
256nnred 10626 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  RR )
268nnred 10626 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
2710nnred 10626 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  RR )
2826, 27remulcld 9673 . . . . . . . . . . 11  |-  ( ph  ->  ( B  x.  F
)  e.  RR )
2925, 28remulcld 9673 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  RR )
3029renegcld 10048 . . . . . . . . . 10  |-  ( ph  -> 
-u ( D  x.  ( B  x.  F
) )  e.  RR )
3116, 17absrpcld 13503 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  C
)  e.  RR+ )
323nnzd 11041 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  ZZ )
33 pellex.xcg . . . . . . . . . . . 12  |-  ( ph  ->  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C ) ) )
34 modmul1 12144 . . . . . . . . . . . 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 1276 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  E )  mod  ( abs `  C
) ) )
364sqcld 12415 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
3711sqcld 12415 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F ^ 2 )  e.  CC )
387, 37mulcld 9665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
3936, 38npcand 9992 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  =  ( E ^
2 ) )
404sqvald 12414 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
4139, 40eqtr2d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  E
)  =  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) ) )
4241oveq1d 6318 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
4323resqcld 12443 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  e.  RR )
4427resqcld 12443 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  e.  RR )
4525, 44remulcld 9673 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  RR )
4643, 45resubcld 10049 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR )
47 0red 9646 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  RR )
4816abscld 13491 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  C
)  e.  RR )
4948recnd 9671 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  e.  CC )
5016, 17absne0d 13502 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  =/=  0 )
5149, 50dividd 10383 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  =  1 )
52 1zzd 10970 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
5351, 52eqeltrd 2511 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  e.  ZZ )
54 mod0 12104 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs `  C
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  C
)  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  /  ( abs `  C ) )  e.  ZZ ) )
5548, 31, 54syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( abs `  C )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  / 
( abs `  C
) )  e.  ZZ ) )
5653, 55mpbird 236 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  C
)  mod  ( abs `  C ) )  =  0 )
5715zred 11042 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
58 absmod0 13360 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( C  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  mod  ( abs `  C
) )  =  0 ) )
5957, 31, 58syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  mod  ( abs `  C ) )  =  0  <->  (
( abs `  C
)  mod  ( abs `  C ) )  =  0 ) )
6056, 59mpbird 236 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C  mod  ( abs `  C ) )  =  0 )
61 pellex.no2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
6261oveq1d 6318 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( C  mod  ( abs `  C ) ) )
63 0mod 12129 . . . . . . . . . . . . . . 15  |-  ( ( abs `  C )  e.  RR+  ->  ( 0  mod  ( abs `  C
) )  =  0 )
6431, 63syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  mod  ( abs `  C ) )  =  0 )
6560, 62, 643eqtr4d 2474 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )
66 modadd1 12135 . . . . . . . . . . . . 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 ) ) )
6746, 47, 45, 31, 65, 66syl221anc 1276 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
6838addid2d 9836 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( F ^
2 ) ) )
6911sqvald 12414 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  =  ( F  x.  F ) )
7069oveq2d 6319 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  =  ( D  x.  ( F  x.  F
) ) )
717, 11, 11mul12d 9844 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F  x.  F )
)  =  ( F  x.  ( D  x.  F ) ) )
7268, 70, 713eqtrd 2468 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( F  x.  ( D  x.  F ) ) )
7372oveq1d 6318 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) ) )
7442, 67, 733eqtrd 2468 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
756nnzd 11041 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  ZZ )
7610nnzd 11041 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ZZ )
7775, 76zmulcld 11048 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  F
)  e.  ZZ )
78 pellex.ycg . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C ) ) )
7978eqcomd 2431 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C ) ) )
80 modmul1 12144 . . . . . . . . . . . . 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
) ) )
8127, 26, 77, 31, 79, 80syl221anc 1276 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
829, 7, 11mul12d 9844 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  x.  ( D  x.  F )
)  =  ( D  x.  ( B  x.  F ) ) )
8382oveq1d 6318 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8481, 83eqtrd 2464 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8535, 74, 843eqtrd 2468 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
86 modadd1 12135 . . . . . . . . . 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 ) ) )
8724, 29, 30, 31, 85, 86syl221anc 1276 . . . . . . . . 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 ) ) )
8813negidd 9978 . . . . . . . . . 10  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  =  0 )
8988oveq1d 6318 . . . . . . . . 9  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
9021, 87, 893eqtrd 2468 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
9190, 64eqtrd 2464 . . . . . . 7  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  0 )
9224, 29resubcld 10049 . . . . . . . 8  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR )
93 absmod0 13360 . . . . . . . 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 ) )
9492, 31, 93syl2anc 666 . . . . . . 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 ) )
9591, 94mpbid 214 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 )
9614abscld 13491 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR )
97 mod0 12104 . . . . . . 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 ) )
9896, 31, 97syl2anc 666 . . . . . 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 ) )
9995, 98mpbid 214 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ )
10018, 99eqeltrd 2511 . . . 4  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ )
10192, 57, 17redivcld 10437 . . . . 5  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  RR )
102 absz 13368 . . . . 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 ) )
103101, 102syl 17 . . . 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 ) )
104100, 103mpbird 236 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ )
105 0lt1 10138 . . . . . . . 8  |-  0  <  1
106 0re 9645 . . . . . . . . 9  |-  0  e.  RR
107 1re 9644 . . . . . . . . 9  |-  1  e.  RR
108106, 107ltnlei 9757 . . . . . . . 8  |-  ( 0  <  1  <->  -.  1  <_  0 )
109105, 108mpbi 212 . . . . . . 7  |-  -.  1  <_  0
1109, 4mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  x.  E
)  e.  CC )
1112, 11mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  F
)  e.  CC )
112110, 111subcld 9988 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  CC )
113112, 16, 17divcld 10385 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  CC )
114113abscld 13491 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  RR )
115114resqcld 12443 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  e.  RR )
1166nnnn0d 10927 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  NN0 )
117116nn0ge0d 10930 . . . . . . . . . 10  |-  ( ph  ->  0  <_  D )
118114sqge0d 12444 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) )
11925, 115, 117, 118mulge0d 10192 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )
12025, 115remulcld 9673 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  e.  RR )
12147, 120suble0d 10206 . . . . . . . . 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 ) ) ) )
122119, 121mpbird 236 . . . . . . . 8  |-  ( ph  ->  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) ) )  <_  0 )
123 breq1 4424 . . . . . . . 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
) )
124122, 123syl5ibrcom 226 . . . . . . 7  |-  ( ph  ->  ( 1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  -> 
1  <_  0 ) )
125109, 124mtoi 182 . . . . . 6  |-  ( ph  ->  -.  1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) ) )
126 absresq 13359 . . . . . . . . . . . 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 ) )
127101, 126syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 ) )
12814, 16, 17sqdivd 12430 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) ^ 2 )  / 
( C ^ 2 ) ) )
12914sqvald 12414 . . . . . . . . . . . 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 )
) ) ) )
130129oveq1d 6318 . . . . . . . . . . 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 ) ) )
131127, 128, 1303eqtrd 2468 . . . . . . . . . 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 ) ) )
13226, 23remulcld 9673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  x.  E
)  e.  RR )
13322, 27remulcld 9673 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  x.  F
)  e.  RR )
134132, 133resubcld 10049 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR )
135134, 57, 17redivcld 10437 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  RR )
136 absresq 13359 . . . . . . . . . . . . . 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 ) )
137135, 136syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) ^
2 ) )
138112, 16, 17sqdivd 12430 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ^ 2 )  =  ( ( ( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 )  /  ( C ^
2 ) ) )
139137, 138eqtrd 2464 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) )
140139oveq2d 6319 . . . . . . . . . . 11  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  =  ( D  x.  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) ) )
141112sqcld 12415 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  e.  CC )
14216sqcld 12415 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  e.  CC )
143 sqne0 12342 . . . . . . . . . . . . . 14  |-  ( C  e.  CC  ->  (
( C ^ 2 )  =/=  0  <->  C  =/=  0 ) )
14416, 143syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( C ^
2 )  =/=  0  <->  C  =/=  0 ) )
14517, 144mpbird 236 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  =/=  0 )
1467, 141, 142, 145divassd 10420 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 ) )  /  ( C ^ 2 ) )  =  ( D  x.  ( ( ( ( B  x.  E )  -  ( A  x.  F ) ) ^
2 )  /  ( C ^ 2 ) ) ) )
147112sqvald 12414 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  =  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )
148147oveq2d 6319 . . . . . . . . . . . 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 )
) ) ) )
149148oveq1d 6318 . . . . . . . . . . 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 ) ) )
150140, 146, 1493eqtr2d 2470 . . . . . . . . . 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 ) ) )
151131, 150oveq12d 6321 . . . . . . . . 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 ) ) ) )
15214, 14mulcld 9665 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
153112, 112mulcld 9665 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  CC )
1547, 153mulcld 9665 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  e.  CC )
155152, 154, 142, 145divsubdird 10424 . . . . . . . . 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 ) ) ) )
1565, 13, 5, 13mulsubd 10079 . . . . . . . . . . . 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 ) ) ) ) ) )
157110, 111, 110, 111mulsubd 10079 . . . . . . . . . . . . . 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 )
) ) ) )
158157oveq2d 6319 . . . . . . . . . . . . 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 ) ) ) ) ) )
159110, 110mulcld 9665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( B  x.  E )
)  e.  CC )
160111, 111mulcld 9665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  F )  x.  ( A  x.  F )
)  e.  CC )
161159, 160addcld 9664 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
162110, 111mulcld 9665 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( A  x.  F )
)  e.  CC )
163162, 162addcld 9664 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
1647, 161, 163subdid 10076 . . . . . . . . . . . . 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 ) ) ) ) ) )
1657, 159, 160adddid 9669 . . . . . . . . . . . . . 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 )
) ) ) )
1667, 162, 162adddid 9669 . . . . . . . . . . . . . 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 )
) ) ) )
167165, 166oveq12d 6321 . . . . . . . . . . . . 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 ) ) ) ) ) )
168158, 164, 1673eqtrd 2468 . . . . . . . . . . . 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 ) ) ) ) ) )
169156, 168oveq12d 6321 . . . . . . . . . . 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 )
) ) ) ) ) )
170169oveq1d 6318 . . . . . . . . . 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 ) ) )
1715, 13mulcomd 9666 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( A  x.  E
) ) )
1727, 12, 5mulassd 9668 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( A  x.  E )
)  =  ( D  x.  ( ( B  x.  F )  x.  ( A  x.  E
) ) ) )
1732, 4mulcomd 9666 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  x.  E
)  =  ( E  x.  A ) )
174173oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  F )  x.  ( E  x.  A ) ) )
1759, 11, 4, 2mul4d 9847 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( E  x.  A )
)  =  ( ( B  x.  E )  x.  ( F  x.  A ) ) )
17611, 2mulcomd 9666 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F  x.  A
)  =  ( A  x.  F ) )
177176oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E )  x.  ( F  x.  A )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
178174, 175, 1773eqtrd 2468 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
179178oveq2d 6319 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  F
)  x.  ( A  x.  E ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) )
180171, 172, 1793eqtrd 2468 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) )
181180, 180oveq12d 6321 . . . . . . . . . . . . . 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 )
) ) ) )
182181oveq2d 6319 . . . . . . . . . . . . 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 ) ) ) ) ) )
183182oveq1d 6318 . . . . . . . . . . . 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 ) ) ) ) ) ) )
1845, 5mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  x.  E )  x.  ( A  x.  E )
)  e.  CC )
18513, 13mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) )  e.  CC )
186184, 185addcld 9664 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
1877, 159mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  e.  CC )
1887, 160mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
189187, 188addcld 9664 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  e.  CC )
1907, 162mulcld 9665 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
191190, 190addcld 9664 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) )  e.  CC )
192186, 189, 191nnncan2d 10023 . . . . . . . . . . . 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 ) ) ) ) ) )
193184, 185, 187, 188addsub4d 10035 . . . . . . . . . . . . 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
) ) ) ) ) )
1945sqvald 12414 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A  x.  E )  x.  ( A  x.  E ) ) )
195110sqvald 12414 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B  x.  E )  x.  ( B  x.  E ) ) )
196195oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )
197194, 196oveq12d 6321 . . . . . . . . . . . . . 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 )
) ) ) )
19813sqvald 12414 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )
199111sqvald 12414 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A  x.  F )  x.  ( A  x.  F ) ) )
200199oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )
201198, 200oveq12d 6321 . . . . . . . . . . . . . 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 )
) ) ) )
202197, 201oveq12d 6321 . . . . . . . . . . . . 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 ) ) ) ) ) )
2032, 4sqmuld 12429 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( E ^
2 ) ) )
2049, 4sqmuld 12429 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( E ^
2 ) ) )
205204oveq2d 6319 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B ^ 2 )  x.  ( E ^ 2 ) ) ) )
2069sqcld 12415 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B ^ 2 )  e.  CC )
2077, 206, 36mulassd 9668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) )  =  ( D  x.  ( ( B ^
2 )  x.  ( E ^ 2 ) ) ) )
208205, 207eqtr4d 2467 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )
209203, 208oveq12d 6321 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A  x.  E ) ^
2 )  -  ( D  x.  ( ( B  x.  E ) ^ 2 ) ) )  =  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  ( ( D  x.  ( B ^
2 ) )  x.  ( E ^ 2 ) ) ) )
2107sqvald 12414 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D ^ 2 )  =  ( D  x.  D ) )
2119, 11sqmuld 12429 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( F ^
2 ) ) )
212210, 211oveq12d 6321 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D ^
2 )  x.  (
( B  x.  F
) ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^ 2 )  x.  ( F ^ 2 ) ) ) )
2137, 12sqmuld 12429 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D ^ 2 )  x.  ( ( B  x.  F ) ^
2 ) ) )
2147, 7mulcld 9665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  D
)  e.  CC )
215214, 206, 37mulassd 9668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^
2 )  x.  ( F ^ 2 ) ) ) )
216212, 213, 2153eqtr4d 2474 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) ) )
2172, 11sqmuld 12429 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( F ^
2 ) ) )
218217oveq2d 6319 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A ^ 2 )  x.  ( F ^ 2 ) ) ) )
2192sqcld 12415 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A ^ 2 )  e.  CC )
2207, 219, 37mulassd 9668 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( D  x.  ( ( A ^
2 )  x.  ( F ^ 2 ) ) ) )
221218, 220eqtr4d 2467 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )
222216, 221oveq12d 6321 . . . . . . . . . . . . . . 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 ) ) ) )
223209, 222oveq12d 6321 . . . . . . . . . . . . . 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 ) ) ) ) )
2247, 206mulcld 9665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( B ^ 2 ) )  e.  CC )
225219, 224, 36subdird 10077 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( ( ( A ^ 2 )  x.  ( E ^
2 ) )  -  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) ) ) )
226 pellex.no1 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  C )
227226oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( C  x.  ( E ^ 2 ) ) )
228225, 227eqtr3d 2466 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  (
( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )  =  ( C  x.  ( E ^ 2 ) ) )
2297, 7, 206mulassd 9668 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  =  ( D  x.  ( D  x.  ( B ^ 2 ) ) ) )
230229oveq1d 6318 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
231230oveq1d 6318 . . . . . . . . . . . . . . . 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 ) ) )
232214, 206mulcld 9665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  e.  CC )
2337, 219mulcld 9665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( A ^ 2 ) )  e.  CC )
234232, 233, 37subdird 10077 . . . . . . . . . . . . . . . 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 ) ) ) )
235 subdi 10054 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
236235eqcomd 2431 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
2377, 224, 219, 236syl3anc 1265 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
238 negsubdi2 9935 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A ^ 2 )  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC )  ->  -u ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )
239238eqcomd 2431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A ^ 2 )  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC )  -> 
( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
240219, 224, 239syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
241226negeqd 9871 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  -u C
)
242240, 241eqtrd 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u C )
243242oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  (
( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( D  x.  -u C ) )
2447, 16mulneg2d 10074 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  -u C
)  =  -u ( D  x.  C )
)
245237, 243, 2443eqtrd 2468 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  -u ( D  x.  C ) )
246245oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) )
247231, 234, 2463eqtr3d 2472 . . . . . . . . . . . . . . 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 ) ) )
248228, 247oveq12d 6321 . . . . . . . . . . . . . 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 ) ) ) )
2497, 16mulcld 9665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  C
)  e.  CC )
250249, 37mulneg1d 10073 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( ( D  x.  C )  x.  ( F ^ 2 ) ) )
2517, 16mulcomd 9666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( D  x.  C
)  =  ( C  x.  D ) )
252251oveq1d 6318 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( ( C  x.  D )  x.  ( F ^ 2 ) ) )
25316, 7, 37mulassd 9668 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( C  x.  D )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
254252, 253eqtrd 2464 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
255254negeqd 9871 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
256250, 255eqtrd 2464 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
257256oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
25816, 36mulcld 9665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( E ^ 2 ) )  e.  CC )
25916, 38mulcld 9665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( D  x.  ( F ^ 2 ) ) )  e.  CC )
260258, 259negsubd 9994 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^
2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
26161oveq2d 6319 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( C  x.  C ) )
262 subdi 10054 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
263262eqcomd 2431 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
26416, 36, 38, 263syl3anc 1265 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26516sqvald 12414 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C ^ 2 )  =  ( C  x.  C ) )
266261, 264, 2653eqtr4d 2474 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C ^ 2 ) )
267257, 260, 2663eqtrd 2468 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( C ^ 2 ) )
268223, 248, 2673eqtrd 2468 . . . . . . . . . . . . 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 ) )
269193, 202, 2683eqtr2d 2470 . . . . . . . . . . . 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 ) )
270183, 192, 2693eqtrd 2468 . . . . . . . . . . 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 ) )
271270oveq1d 6318 . . . . . . . . . 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 ) ) )
272142, 145dividd 10383 . . . . . . . . . 10  |-  ( ph  ->  ( ( C ^
2 )  /  ( C ^ 2 ) )  =  1 )
273170, 271, 2723eqtrd 2468 . . . . . . . . 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 )
274151, 155, 2733eqtr2d 2470 . . . . . . . 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 )
275274adantr 467 . . . . . . 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 )
276 simpr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  =  0 )
277276oveq1d 6318 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  =  ( 0  /  C
) )
278277fveq2d 5883 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  ( abs `  (
0  /  C ) ) )
27916, 17div0d 10384 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  /  C
)  =  0 )
280279abs00bd 13348 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
0  /  C ) )  =  0 )
281280adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( 0  /  C ) )  =  0 )
282278, 281eqtrd 2464 . . . . . . . . 9  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  0 )
283282sq0id 12369 . . . . . . . 8  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  0 )
284283oveq1d 6318 . . . . . . 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 ) ) ) )
285275, 284eqtr3d 2466 . . . . . 6  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  1  =  ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) ) )
286125, 285mtand 664 . . . . 5  |-  ( ph  ->  -.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  =  0 )
287286neqned 2628 . . . 4  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =/=  0 )
28814, 16, 287, 17divne0d 10401 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )
289 nnabscl 13382 . . 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 )
290104, 288, 289syl2anc 666 . 2  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
291112, 16, 17absdivd 13510 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  =  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F ) ) )  /  ( abs `  C
) ) )
292 negsub 9924 . . . . . . . . . . . 12  |-  ( ( ( B  x.  E
)  e.  CC  /\  ( A  x.  F
)  e.  CC )  ->  ( ( B  x.  E )  + 
-u ( A  x.  F ) )  =  ( ( B  x.  E )  -  ( A  x.  F )
) )
293292eqcomd 2431 . . . . . . . . . . 11  |-  ( ( ( B  x.  E
)  e.  CC  /\  ( A  x.  F
)  e.  CC )  ->  ( ( B  x.  E )  -  ( A  x.  F
) )  =  ( ( B  x.  E
)  +  -u ( A  x.  F )
) )
294110, 111, 293syl2anc 666 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  =  ( ( B  x.  E )  +  -u ( A  x.  F ) ) )
295294oveq1d 6318 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) ) )
296133renegcld 10048 . . . . . . . . . 10  |-  ( ph  -> 
-u ( A  x.  F )  e.  RR )
29711, 4mulcomd 9666 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  E
)  =  ( E  x.  F ) )
298297oveq1d 6318 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
299 modmul1 12144 . . . . . . . . . . . 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
) ) )
30026, 27, 32, 31, 78, 299syl221anc 1276 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
301 modmul1 12144 . . . . . . . . . . . 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
) ) )
30222, 23, 76, 31, 33, 301syl221anc 1276 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
303298, 300, 3023eqtr4d 2474 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( A  x.  F )  mod  ( abs `  C
) ) )
304 modadd1 12135 . . . . . . . . . 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 ) ) )
305132, 133, 296, 31, 303, 304syl221anc 1276 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
306111negidd 9978 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  F )  +  -u ( A  x.  F
) )  =  0 )
307306oveq1d 6318 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  F )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
308295, 305, 3073eqtrd 2468 . . . . . . . 8  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
309308, 64eqtrd 2464 . . . . . . 7  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0 )
310 absmod0 13360 . . . . . . . 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 ) )
311134, 31, 310syl2anc 666 . . . . . . 7  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 ) )
312309, 311mpbid 214 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 )
313112abscld 13491 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR )
314 mod0 12104 . . . . . . 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 ) )
315313, 31, 314syl2anc 666 . . . . . 6  |-  ( ph  ->  ( ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F )
) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F
) ) )  / 
( abs `  C
) )  e.  ZZ ) )
316312, 315mpbid 214 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  /  ( abs `  C ) )  e.  ZZ )
317291, 316eqeltrd 2511 . . . 4  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  ZZ )
318 absz 13368 . . . . 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 ) )
319135, 318syl 17 . . . 4  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C )  e.  ZZ  <->  ( abs `  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) )  e.  ZZ ) )
320317, 319mpbird 236 . . 3  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ )
321 pellex.neq . . . . . . 7  |-  ( ph  ->  -.  ( A  =  E  /\  B  =  F ) )
32210nnne0d 10656 . . . . . . . . 9  |-  ( ph  ->  F  =/=  0 )
3233nnne0d 10656 . . . . . . . . 9  |-  ( ph  ->  E  =/=  0 )
3249, 11, 2, 4, 322, 323divmuleqd 10431 . . . . . . . 8  |-  ( ph  ->  ( ( B  /  F )  =  ( A  /  E )  <-> 
( B  x.  E
)  =  ( A  x.  F ) ) )
32561adantr 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
326325eqcomd 2431 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  C  =  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) ) )
327326oveq2d 6319 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  C )  =  ( ( ( B  /  F ) ^
2 )  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
3289, 11, 322divcld 10385 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  F
)  e.  CC )
329328sqcld 12415 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  /  F ) ^ 2 )  e.  CC )
330329adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  e.  CC )
33136adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  e.  CC )
33238adantr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
333330, 331, 332subdid 10076 . . . . . . . . . . . . 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 ) ) ) ) )
334 oveq1 6310 . . . . . . . . . . . . . . . . 17  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( B  /  F
) ^ 2 )  =  ( ( A  /  E ) ^
2 ) )
335334oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( ( B  /  F ) ^ 2 )  x.  ( E ^ 2 ) )  =  ( ( ( A  /  E ) ^ 2 )  x.  ( E ^ 2 ) ) )
336335adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A  /  E ) ^
2 )  x.  ( E ^ 2 ) ) )
3372adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  A  e.  CC )
3384adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  e.  CC )
339323adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  =/=  0 )
340337, 338, 339sqdivd 12430 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( A  /  E ) ^
2 )  =  ( ( A ^ 2 )  /  ( E ^ 2 ) ) )
341340oveq1d 6318 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A  /  E
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A ^ 2 )  / 
( E ^ 2 ) )  x.  ( E ^ 2 ) ) )
342219adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( A ^ 2 )  e.  CC )
343 sqne0 12342 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  CC  ->  (
( E ^ 2 )  =/=  0  <->  E  =/=  0 ) )
3444, 343syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( E ^
2 )  =/=  0  <->  E  =/=  0 ) )
345323, 344mpbird 236 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E ^ 2 )  =/=  0 )
346345adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  =/=  0 )
347342, 331, 346divcan1d 10386 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A ^ 2 )  /  ( E ^ 2 ) )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
348336, 341, 3473eqtrd 2468 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
3497adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  D  e.  CC )
35037adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  e.  CC )
351330, 349, 350mul12d 9844 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B  /  F
) ^ 2 )  x.  ( F ^
2 ) ) ) )
3529adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  B  e.  CC )
35311adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  e.  CC )
354322adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  =/=  0 )
355352, 353, 354sqdivd 12430 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  =  ( ( B ^ 2 )  /  ( F ^ 2 ) ) )
356355oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( F ^
2 ) )  =  ( ( ( B ^ 2 )  / 
( F ^ 2 ) )  x.  ( F ^ 2 ) ) )
357356oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( ( ( B  /  F ) ^
2 )  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B ^ 2 )  /  ( F ^
2 ) )  x.  ( F ^ 2 ) ) ) )
358206adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( B ^ 2 )  e.  CC )
359 sqne0 12342 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  e.  CC  ->  (
( F ^ 2 )  =/=  0  <->  F  =/=  0 ) )
36011, 359syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( F ^
2 )  =/=  0  <->  F  =/=  0 ) )
361322, 360mpbird 236 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F ^ 2 )  =/=  0 )
362361adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  =/=  0 )
363358, 350, 362divcan1d 10386 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B ^ 2 )  /  ( F ^ 2 ) )  x.  ( F ^
2 ) )  =