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 30745
Description: Lemma for pellex 30746. 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 10559 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3 pellex.enn . . . . . . . . 9  |-  ( ph  ->  E  e.  NN )
43nncnd 10559 . . . . . . . 8  |-  ( ph  ->  E  e.  CC )
52, 4mulcld 9619 . . . . . . 7  |-  ( ph  ->  ( A  x.  E
)  e.  CC )
6 pellex.dnn . . . . . . . . 9  |-  ( ph  ->  D  e.  NN )
76nncnd 10559 . . . . . . . 8  |-  ( ph  ->  D  e.  CC )
8 pellex.bnn . . . . . . . . . 10  |-  ( ph  ->  B  e.  NN )
98nncnd 10559 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
10 pellex.fnn . . . . . . . . . 10  |-  ( ph  ->  F  e.  NN )
1110nncnd 10559 . . . . . . . . 9  |-  ( ph  ->  F  e.  CC )
129, 11mulcld 9619 . . . . . . . 8  |-  ( ph  ->  ( B  x.  F
)  e.  CC )
137, 12mulcld 9619 . . . . . . 7  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  CC )
145, 13subcld 9936 . . . . . 6  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  CC )
15 pellex.cz . . . . . . 7  |-  ( ph  ->  C  e.  ZZ )
1615zcnd 10976 . . . . . 6  |-  ( ph  ->  C  e.  CC )
17 pellex.cn0 . . . . . 6  |-  ( ph  ->  C  =/=  0 )
1814, 16, 17absdivd 13267 . . . . 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 9942 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F )
) )  =  ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )
2019eqcomd 2451 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =  ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) ) )
2120oveq1d 6296 . . . . . . . . 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 10558 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
233nnred 10558 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
2422, 23remulcld 9627 . . . . . . . . . 10  |-  ( ph  ->  ( A  x.  E
)  e.  RR )
256nnred 10558 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  RR )
268nnred 10558 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
2710nnred 10558 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  RR )
2826, 27remulcld 9627 . . . . . . . . . . 11  |-  ( ph  ->  ( B  x.  F
)  e.  RR )
2925, 28remulcld 9627 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  RR )
3029renegcld 9993 . . . . . . . . . 10  |-  ( ph  -> 
-u ( D  x.  ( B  x.  F
) )  e.  RR )
3116, 17absrpcld 13260 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  C
)  e.  RR+ )
323nnzd 10974 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  ZZ )
33 pellex.xcg . . . . . . . . . . . 12  |-  ( ph  ->  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C ) ) )
34 modmul1 12021 . . . . . . . . . . . 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 1240 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  E )  mod  ( abs `  C
) ) )
364sqcld 12289 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
3711sqcld 12289 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F ^ 2 )  e.  CC )
387, 37mulcld 9619 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
3936, 38npcand 9940 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  =  ( E ^
2 ) )
404sqvald 12288 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
4139, 40eqtr2d 2485 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  E
)  =  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) ) )
4241oveq1d 6296 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
4323resqcld 12317 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  e.  RR )
4427resqcld 12317 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  e.  RR )
4525, 44remulcld 9627 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  RR )
4643, 45resubcld 9994 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR )
47 0red 9600 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  RR )
4816abscld 13248 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  C
)  e.  RR )
4948recnd 9625 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  e.  CC )
5016, 17absne0d 13259 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  =/=  0 )
5149, 50dividd 10325 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  =  1 )
52 1zzd 10902 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
5351, 52eqeltrd 2531 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  e.  ZZ )
54 mod0 11984 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs `  C
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  C
)  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  /  ( abs `  C ) )  e.  ZZ ) )
5548, 31, 54syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( abs `  C )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  / 
( abs `  C
) )  e.  ZZ ) )
5653, 55mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  C
)  mod  ( abs `  C ) )  =  0 )
5715zred 10975 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
58 absmod0 13117 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( C  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  mod  ( abs `  C
) )  =  0 ) )
5957, 31, 58syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  mod  ( abs `  C ) )  =  0  <->  (
( abs `  C
)  mod  ( abs `  C ) )  =  0 ) )
6056, 59mpbird 232 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C  mod  ( abs `  C ) )  =  0 )
61 pellex.no2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
6261oveq1d 6296 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( C  mod  ( abs `  C ) ) )
63 0mod 12008 . . . . . . . . . . . . . . 15  |-  ( ( abs `  C )  e.  RR+  ->  ( 0  mod  ( abs `  C
) )  =  0 )
6431, 63syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  mod  ( abs `  C ) )  =  0 )
6560, 62, 643eqtr4d 2494 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )
66 modadd1 12014 . . . . . . . . . . . . 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 1240 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
6838addid2d 9784 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( F ^
2 ) ) )
6911sqvald 12288 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  =  ( F  x.  F ) )
7069oveq2d 6297 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  =  ( D  x.  ( F  x.  F
) ) )
717, 11, 11mul12d 9792 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F  x.  F )
)  =  ( F  x.  ( D  x.  F ) ) )
7268, 70, 713eqtrd 2488 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( F  x.  ( D  x.  F ) ) )
7372oveq1d 6296 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) ) )
7442, 67, 733eqtrd 2488 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
756nnzd 10974 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  ZZ )
7610nnzd 10974 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ZZ )
7775, 76zmulcld 10981 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  F
)  e.  ZZ )
78 pellex.ycg . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C ) ) )
7978eqcomd 2451 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C ) ) )
80 modmul1 12021 . . . . . . . . . . . . 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 1240 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
829, 7, 11mul12d 9792 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  x.  ( D  x.  F )
)  =  ( D  x.  ( B  x.  F ) ) )
8382oveq1d 6296 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8481, 83eqtrd 2484 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8535, 74, 843eqtrd 2488 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
86 modadd1 12014 . . . . . . . . . 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 1240 . . . . . . . . 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 9926 . . . . . . . . . 10  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  =  0 )
8988oveq1d 6296 . . . . . . . . 9  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
9021, 87, 893eqtrd 2488 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
9190, 64eqtrd 2484 . . . . . . 7  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  0 )
9224, 29resubcld 9994 . . . . . . . 8  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR )
93 absmod0 13117 . . . . . . . 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 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 ) )
9591, 94mpbid 210 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 )
9614abscld 13248 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR )
97 mod0 11984 . . . . . . 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 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 ) )
9995, 98mpbid 210 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ )
10018, 99eqeltrd 2531 . . . 4  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ )
10192, 57, 17redivcld 10379 . . . . 5  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  RR )
102 absz 13125 . . . . 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 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 ) )
104100, 103mpbird 232 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ )
105 0lt1 10082 . . . . . . . 8  |-  0  <  1
106 0re 9599 . . . . . . . . 9  |-  0  e.  RR
107 1re 9598 . . . . . . . . 9  |-  1  e.  RR
108106, 107ltnlei 9708 . . . . . . . 8  |-  ( 0  <  1  <->  -.  1  <_  0 )
109105, 108mpbi 208 . . . . . . 7  |-  -.  1  <_  0
1109, 4mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  x.  E
)  e.  CC )
1112, 11mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  F
)  e.  CC )
112110, 111subcld 9936 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  CC )
113112, 16, 17divcld 10327 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  CC )
114113abscld 13248 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  RR )
115114resqcld 12317 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  e.  RR )
1166nnnn0d 10859 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  NN0 )
117116nn0ge0d 10862 . . . . . . . . . 10  |-  ( ph  ->  0  <_  D )
118114sqge0d 12318 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) )
11925, 115, 117, 118mulge0d 10136 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )
12025, 115remulcld 9627 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  e.  RR )
12147, 120suble0d 10150 . . . . . . . . 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 232 . . . . . . . 8  |-  ( ph  ->  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) ) )  <_  0 )
123 breq1 4440 . . . . . . . 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 222 . . . . . . 7  |-  ( ph  ->  ( 1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  -> 
1  <_  0 ) )
125109, 124mtoi 178 . . . . . 6  |-  ( ph  ->  -.  1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) ) )
126 absresq 13116 . . . . . . . . . . . 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 16 . . . . . . . . . . 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 12304 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) ^ 2 )  / 
( C ^ 2 ) ) )
12914sqvald 12288 . . . . . . . . . . . 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 6296 . . . . . . . . . . 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 2488 . . . . . . . . . 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 9627 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  x.  E
)  e.  RR )
13322, 27remulcld 9627 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  x.  F
)  e.  RR )
134132, 133resubcld 9994 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR )
135134, 57, 17redivcld 10379 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  RR )
136 absresq 13116 . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) ^
2 ) )
138112, 16, 17sqdivd 12304 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ^ 2 )  =  ( ( ( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 )  /  ( C ^
2 ) ) )
139137, 138eqtrd 2484 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) )
140139oveq2d 6297 . . . . . . . . . . 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 12289 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  e.  CC )
14216sqcld 12289 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  e.  CC )
143 sqne0 12215 . . . . . . . . . . . . . 14  |-  ( C  e.  CC  ->  (
( C ^ 2 )  =/=  0  <->  C  =/=  0 ) )
14416, 143syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( C ^
2 )  =/=  0  <->  C  =/=  0 ) )
14517, 144mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  =/=  0 )
1467, 141, 142, 145divassd 10362 . . . . . . . . . . 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 12288 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  =  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )
148147oveq2d 6297 . . . . . . . . . . . 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 6296 . . . . . . . . . . 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 2490 . . . . . . . . . 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 6299 . . . . . . . . 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 9619 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
153112, 112mulcld 9619 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  CC )
1547, 153mulcld 9619 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  e.  CC )
155152, 154, 142, 145divsubdird 10366 . . . . . . . . 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 10022 . . . . . . . . . . . 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 10022 . . . . . . . . . . . . . 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 6297 . . . . . . . . . . . . 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 9619 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( B  x.  E )
)  e.  CC )
160111, 111mulcld 9619 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  F )  x.  ( A  x.  F )
)  e.  CC )
161159, 160addcld 9618 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
162110, 111mulcld 9619 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( A  x.  F )
)  e.  CC )
163162, 162addcld 9618 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
1647, 161, 163subdid 10019 . . . . . . . . . . . . 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 9623 . . . . . . . . . . . . . 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 9623 . . . . . . . . . . . . . 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 6299 . . . . . . . . . . . . 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 2488 . . . . . . . . . . . 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 6299 . . . . . . . . . . 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 6296 . . . . . . . . . 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 9620 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( A  x.  E
) ) )
1727, 12, 5mulassd 9622 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( A  x.  E )
)  =  ( D  x.  ( ( B  x.  F )  x.  ( A  x.  E
) ) ) )
1732, 4mulcomd 9620 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  x.  E
)  =  ( E  x.  A ) )
174173oveq2d 6297 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  F )  x.  ( E  x.  A ) ) )
1759, 11, 4, 2mul4d 9795 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( E  x.  A )
)  =  ( ( B  x.  E )  x.  ( F  x.  A ) ) )
17611, 2mulcomd 9620 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F  x.  A
)  =  ( A  x.  F ) )
177176oveq2d 6297 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E )  x.  ( F  x.  A )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
178174, 175, 1773eqtrd 2488 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
179178oveq2d 6297 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  F
)  x.  ( A  x.  E ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) )
180171, 172, 1793eqtrd 2488 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) )
181180, 180oveq12d 6299 . . . . . . . . . . . . . 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 6297 . . . . . . . . . . . . 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 6296 . . . . . . . . . . . 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 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  x.  E )  x.  ( A  x.  E )
)  e.  CC )
18513, 13mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) )  e.  CC )
186184, 185addcld 9618 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
1877, 159mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  e.  CC )
1887, 160mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
189187, 188addcld 9618 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  e.  CC )
1907, 162mulcld 9619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
191190, 190addcld 9618 . . . . . . . . . . . . 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 9971 . . . . . . . . . . . 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 9983 . . . . . . . . . . . . 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 12288 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A  x.  E )  x.  ( A  x.  E ) ) )
195110sqvald 12288 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B  x.  E )  x.  ( B  x.  E ) ) )
196195oveq2d 6297 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )
197194, 196oveq12d 6299 . . . . . . . . . . . . . 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 12288 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )
199111sqvald 12288 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A  x.  F )  x.  ( A  x.  F ) ) )
200199oveq2d 6297 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )
201198, 200oveq12d 6299 . . . . . . . . . . . . . 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 6299 . . . . . . . . . . . . 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 12303 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( E ^
2 ) ) )
2049, 4sqmuld 12303 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( E ^
2 ) ) )
205204oveq2d 6297 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B ^ 2 )  x.  ( E ^ 2 ) ) ) )
2069sqcld 12289 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B ^ 2 )  e.  CC )
2077, 206, 36mulassd 9622 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) )  =  ( D  x.  ( ( B ^
2 )  x.  ( E ^ 2 ) ) ) )
208205, 207eqtr4d 2487 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )
209203, 208oveq12d 6299 . . . . . . . . . . . . . . 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 12288 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D ^ 2 )  =  ( D  x.  D ) )
2119, 11sqmuld 12303 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( F ^
2 ) ) )
212210, 211oveq12d 6299 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D ^
2 )  x.  (
( B  x.  F
) ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^ 2 )  x.  ( F ^ 2 ) ) ) )
2137, 12sqmuld 12303 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D ^ 2 )  x.  ( ( B  x.  F ) ^
2 ) ) )
2147, 7mulcld 9619 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  D
)  e.  CC )
215214, 206, 37mulassd 9622 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^
2 )  x.  ( F ^ 2 ) ) ) )
216212, 213, 2153eqtr4d 2494 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) ) )
2172, 11sqmuld 12303 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( F ^
2 ) ) )
218217oveq2d 6297 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A ^ 2 )  x.  ( F ^ 2 ) ) ) )
2192sqcld 12289 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A ^ 2 )  e.  CC )
2207, 219, 37mulassd 9622 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( D  x.  ( ( A ^
2 )  x.  ( F ^ 2 ) ) ) )
221218, 220eqtr4d 2487 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )
222216, 221oveq12d 6299 . . . . . . . . . . . . . . 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 6299 . . . . . . . . . . . . . 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 9619 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( B ^ 2 ) )  e.  CC )
225219, 224, 36subdird 10020 . . . . . . . . . . . . . . . 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 6296 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( C  x.  ( E ^ 2 ) ) )
228225, 227eqtr3d 2486 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  (
( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )  =  ( C  x.  ( E ^ 2 ) ) )
2297, 7, 206mulassd 9622 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  =  ( D  x.  ( D  x.  ( B ^ 2 ) ) ) )
230229oveq1d 6296 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
231230oveq1d 6296 . . . . . . . . . . . . . . . 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 9619 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  e.  CC )
2337, 219mulcld 9619 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( A ^ 2 ) )  e.  CC )
234232, 233, 37subdird 10020 . . . . . . . . . . . . . . . 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 9997 . . . . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
238 negsubdi2 9883 . . . . . . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
241226negeqd 9819 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  -u C
)
242240, 241eqtrd 2484 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u C )
243242oveq2d 6297 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  (
( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( D  x.  -u C ) )
2447, 16mulneg2d 10017 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  -u C
)  =  -u ( D  x.  C )
)
245237, 243, 2443eqtrd 2488 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  -u ( D  x.  C ) )
246245oveq1d 6296 . . . . . . . . . . . . . . . 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 2492 . . . . . . . . . . . . . . 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 6299 . . . . . . . . . . . . . 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 9619 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  C
)  e.  CC )
250249, 37mulneg1d 10016 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( ( D  x.  C )  x.  ( F ^ 2 ) ) )
2517, 16mulcomd 9620 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( D  x.  C
)  =  ( C  x.  D ) )
252251oveq1d 6296 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( ( C  x.  D )  x.  ( F ^ 2 ) ) )
25316, 7, 37mulassd 9622 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( C  x.  D )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
254252, 253eqtrd 2484 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
255254negeqd 9819 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
256250, 255eqtrd 2484 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
257256oveq2d 6297 . . . . . . . . . . . . . . 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 9619 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( E ^ 2 ) )  e.  CC )
25916, 38mulcld 9619 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( D  x.  ( F ^ 2 ) ) )  e.  CC )
260258, 259negsubd 9942 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^
2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
26161oveq2d 6297 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( C  x.  C ) )
262 subdi 9997 . . . . . . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26516sqvald 12288 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C ^ 2 )  =  ( C  x.  C ) )
266261, 264, 2653eqtr4d 2494 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C ^ 2 ) )
267257, 260, 2663eqtrd 2488 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( C ^ 2 ) )
268223, 248, 2673eqtrd 2488 . . . . . . . . . . . . 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 2490 . . . . . . . . . . . 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 2488 . . . . . . . . . . 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 6296 . . . . . . . . . 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 10325 . . . . . . . . . 10  |-  ( ph  ->  ( ( C ^
2 )  /  ( C ^ 2 ) )  =  1 )
273170, 271, 2723eqtrd 2488 . . . . . . . . 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 2490 . . . . . . . 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 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 )
276 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  =  0 )
277276oveq1d 6296 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  =  ( 0  /  C
) )
278277fveq2d 5860 . . . . . . . . . 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 10326 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  /  C
)  =  0 )
280279abs00bd 13105 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
0  /  C ) )  =  0 )
281280adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( 0  /  C ) )  =  0 )
282278, 281eqtrd 2484 . . . . . . . . 9  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  0 )
283282sq0id 12242 . . . . . . . 8  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  0 )
284283oveq1d 6296 . . . . . . 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 2486 . . . . . 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 659 . . . . 5  |-  ( ph  ->  -.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  =  0 )
287286neqned 2646 . . . 4  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =/=  0 )
28814, 16, 287, 17divne0d 10343 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )
289 nnabscl 13139 . . 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 661 . 2  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
291112, 16, 17absdivd 13267 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  =  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F ) ) )  /  ( abs `  C
) ) )
292 negsub 9872 . . . . . . . . . . . 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 2451 . . . . . . . . . . 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 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  =  ( ( B  x.  E )  +  -u ( A  x.  F ) ) )
295294oveq1d 6296 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) ) )
296133renegcld 9993 . . . . . . . . . 10  |-  ( ph  -> 
-u ( A  x.  F )  e.  RR )
29711, 4mulcomd 9620 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  E
)  =  ( E  x.  F ) )
298297oveq1d 6296 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
299 modmul1 12021 . . . . . . . . . . . 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 1240 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
301 modmul1 12021 . . . . . . . . . . . 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 1240 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
303298, 300, 3023eqtr4d 2494 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( A  x.  F )  mod  ( abs `  C
) ) )
304 modadd1 12014 . . . . . . . . . 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 1240 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
306111negidd 9926 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  F )  +  -u ( A  x.  F
) )  =  0 )
307306oveq1d 6296 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  F )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
308295, 305, 3073eqtrd 2488 . . . . . . . 8  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
309308, 64eqtrd 2484 . . . . . . 7  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0 )
310 absmod0 13117 . . . . . . . 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 661 . . . . . . 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 210 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 )
313112abscld 13248 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR )
314 mod0 11984 . . . . . . 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 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 ) )
316312, 315mpbid 210 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  /  ( abs `  C ) )  e.  ZZ )
317291, 316eqeltrd 2531 . . . 4  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  ZZ )
318 absz 13125 . . . . 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 16 . . . 4  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C )  e.  ZZ  <->  ( abs `  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) )  e.  ZZ ) )
320317, 319mpbird 232 . . 3  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ )
321 pellex.neq . . . . . . 7  |-  ( ph  ->  -.  ( A  =  E  /\  B  =  F ) )
32210nnne0d 10587 . . . . . . . . 9  |-  ( ph  ->  F  =/=  0 )
3233nnne0d 10587 . . . . . . . . 9  |-  ( ph  ->  E  =/=  0 )
3249, 11, 2, 4, 322, 323divmuleqd 10373 . . . . . . . 8  |-  ( ph  ->  ( ( B  /  F )  =  ( A  /  E )  <-> 
( B  x.  E
)  =  ( A  x.  F ) ) )
32561adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
326325eqcomd 2451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  C  =  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) ) )
327326oveq2d 6297 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  C )  =  ( ( ( B  /  F ) ^
2 )  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
3289, 11, 322divcld 10327 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  F
)  e.  CC )
329328sqcld 12289 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  /  F ) ^ 2 )  e.  CC )
330329adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  e.  CC )
33136adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  e.  CC )
33238adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
333330, 331, 332subdid 10019 . . . . . . . . . . . . 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 6288 . . . . . . . . . . . . . . . . 17  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( B  /  F
) ^ 2 )  =  ( ( A  /  E ) ^
2 ) )
335334oveq1d 6296 . . . . . . . . . . . . . . . 16  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( ( B  /  F ) ^ 2 )  x.  ( E ^ 2 ) )  =  ( ( ( A  /  E ) ^ 2 )  x.  ( E ^ 2 ) ) )
336335adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A  /  E ) ^
2 )  x.  ( E ^ 2 ) ) )
3372adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  A  e.  CC )
3384adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  e.  CC )
339323adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  =/=  0 )
340337, 338, 339sqdivd 12304 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( A  /  E ) ^
2 )  =  ( ( A ^ 2 )  /  ( E ^ 2 ) ) )
341340oveq1d 6296 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A  /  E
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A ^ 2 )  / 
( E ^ 2 ) )  x.  ( E ^ 2 ) ) )
342219adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( A ^ 2 )  e.  CC )
343 sqne0 12215 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  CC  ->  (
( E ^ 2 )  =/=  0  <->  E  =/=  0 ) )
3444, 343syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( E ^
2 )  =/=  0  <->  E  =/=  0 ) )
345323, 344mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E ^ 2 )  =/=  0 )
346345adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  =/=  0 )
347342, 331, 346divcan1d 10328 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A ^ 2 )  /  ( E ^ 2 ) )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
348336, 341, 3473eqtrd 2488 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
3497adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  D  e.  CC )
35037adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  e.  CC )
351330, 349, 350mul12d 9792 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B  /  F
) ^ 2 )  x.  ( F ^
2 ) ) ) )
3529adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  B  e.  CC )
35311adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  e.  CC )
354322adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  =/=  0 )
355352, 353, 354sqdivd 12304 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  =  ( ( B ^ 2 )  /  ( F ^ 2 ) ) )
356355oveq1d 6296 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( F ^
2 ) )  =  ( ( ( B ^ 2 )  / 
( F ^ 2 ) )  x.  ( F ^ 2 ) ) )
357356oveq2d 6297 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( ( ( B  /  F ) ^
2 )  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B ^ 2 )  /  ( F ^
2 ) )  x.  ( F ^ 2 ) ) ) )
358206adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( B ^ 2 )  e.  CC )
359 sqne0 12215 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  e.  CC  ->  (
( F ^ 2 )  =/=  0  <->  F  =/=  0 ) )
36011, 359syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( F ^
2 )  =/=  0  <->  F  =/=  0 ) )
361322, 360mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F ^ 2 )  =/=  0 )
362361adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  =/=  0 )
363358, 350, 362divcan1d 10328 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B ^ 2 )  /  ( F ^ 2 ) )  x.  ( F ^
2 ) )  =  (