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 35095
Description: Lemma for pellex 35096. 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 10510 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3 pellex.enn . . . . . . . . 9  |-  ( ph  ->  E  e.  NN )
43nncnd 10510 . . . . . . . 8  |-  ( ph  ->  E  e.  CC )
52, 4mulcld 9564 . . . . . . 7  |-  ( ph  ->  ( A  x.  E
)  e.  CC )
6 pellex.dnn . . . . . . . . 9  |-  ( ph  ->  D  e.  NN )
76nncnd 10510 . . . . . . . 8  |-  ( ph  ->  D  e.  CC )
8 pellex.bnn . . . . . . . . . 10  |-  ( ph  ->  B  e.  NN )
98nncnd 10510 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
10 pellex.fnn . . . . . . . . . 10  |-  ( ph  ->  F  e.  NN )
1110nncnd 10510 . . . . . . . . 9  |-  ( ph  ->  F  e.  CC )
129, 11mulcld 9564 . . . . . . . 8  |-  ( ph  ->  ( B  x.  F
)  e.  CC )
137, 12mulcld 9564 . . . . . . 7  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  CC )
145, 13subcld 9885 . . . . . 6  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  CC )
15 pellex.cz . . . . . . 7  |-  ( ph  ->  C  e.  ZZ )
1615zcnd 10927 . . . . . 6  |-  ( ph  ->  C  e.  CC )
17 pellex.cn0 . . . . . 6  |-  ( ph  ->  C  =/=  0 )
1814, 16, 17absdivd 13340 . . . . 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 9891 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F )
) )  =  ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )
2019eqcomd 2408 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =  ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) ) )
2120oveq1d 6247 . . . . . . . . 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 10509 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
233nnred 10509 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
2422, 23remulcld 9572 . . . . . . . . . 10  |-  ( ph  ->  ( A  x.  E
)  e.  RR )
256nnred 10509 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  RR )
268nnred 10509 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
2710nnred 10509 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  RR )
2826, 27remulcld 9572 . . . . . . . . . . 11  |-  ( ph  ->  ( B  x.  F
)  e.  RR )
2925, 28remulcld 9572 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  RR )
3029renegcld 9945 . . . . . . . . . 10  |-  ( ph  -> 
-u ( D  x.  ( B  x.  F
) )  e.  RR )
3116, 17absrpcld 13333 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  C
)  e.  RR+ )
323nnzd 10925 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  ZZ )
33 pellex.xcg . . . . . . . . . . . 12  |-  ( ph  ->  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C ) ) )
34 modmul1 11992 . . . . . . . . . . . 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 1239 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  E )  mod  ( abs `  C
) ) )
364sqcld 12260 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
3711sqcld 12260 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F ^ 2 )  e.  CC )
387, 37mulcld 9564 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
3936, 38npcand 9889 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  =  ( E ^
2 ) )
404sqvald 12259 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
4139, 40eqtr2d 2442 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  E
)  =  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) ) )
4241oveq1d 6247 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
4323resqcld 12288 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  e.  RR )
4427resqcld 12288 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  e.  RR )
4525, 44remulcld 9572 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  RR )
4643, 45resubcld 9946 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR )
47 0red 9545 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  RR )
4816abscld 13321 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  C
)  e.  RR )
4948recnd 9570 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  e.  CC )
5016, 17absne0d 13332 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  =/=  0 )
5149, 50dividd 10277 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  =  1 )
52 1zzd 10854 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
5351, 52eqeltrd 2488 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  e.  ZZ )
54 mod0 11952 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs `  C
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  C
)  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  /  ( abs `  C ) )  e.  ZZ ) )
5548, 31, 54syl2anc 659 . . . . . . . . . . . . . . . 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 10926 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
58 absmod0 13190 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( C  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  mod  ( abs `  C
) )  =  0 ) )
5957, 31, 58syl2anc 659 . . . . . . . . . . . . . . 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 6247 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( C  mod  ( abs `  C ) ) )
63 0mod 11977 . . . . . . . . . . . . . . 15  |-  ( ( abs `  C )  e.  RR+  ->  ( 0  mod  ( abs `  C
) )  =  0 )
6431, 63syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  mod  ( abs `  C ) )  =  0 )
6560, 62, 643eqtr4d 2451 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )
66 modadd1 11983 . . . . . . . . . . . . 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 1239 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
6838addid2d 9733 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( F ^
2 ) ) )
6911sqvald 12259 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  =  ( F  x.  F ) )
7069oveq2d 6248 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  =  ( D  x.  ( F  x.  F
) ) )
717, 11, 11mul12d 9741 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F  x.  F )
)  =  ( F  x.  ( D  x.  F ) ) )
7268, 70, 713eqtrd 2445 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( F  x.  ( D  x.  F ) ) )
7372oveq1d 6247 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) ) )
7442, 67, 733eqtrd 2445 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
756nnzd 10925 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  ZZ )
7610nnzd 10925 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ZZ )
7775, 76zmulcld 10932 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  F
)  e.  ZZ )
78 pellex.ycg . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C ) ) )
7978eqcomd 2408 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C ) ) )
80 modmul1 11992 . . . . . . . . . . . . 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 1239 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
829, 7, 11mul12d 9741 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  x.  ( D  x.  F )
)  =  ( D  x.  ( B  x.  F ) ) )
8382oveq1d 6247 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8481, 83eqtrd 2441 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8535, 74, 843eqtrd 2445 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
86 modadd1 11983 . . . . . . . . . 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 1239 . . . . . . . . 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 9875 . . . . . . . . . 10  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  =  0 )
8988oveq1d 6247 . . . . . . . . 9  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
9021, 87, 893eqtrd 2445 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
9190, 64eqtrd 2441 . . . . . . 7  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  0 )
9224, 29resubcld 9946 . . . . . . . 8  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR )
93 absmod0 13190 . . . . . . . 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 659 . . . . . . 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 13321 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR )
97 mod0 11952 . . . . . . 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 659 . . . . . 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 2488 . . . 4  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ )
10192, 57, 17redivcld 10331 . . . . 5  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  RR )
102 absz 13198 . . . . 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 232 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ )
105 0lt1 10033 . . . . . . . 8  |-  0  <  1
106 0re 9544 . . . . . . . . 9  |-  0  e.  RR
107 1re 9543 . . . . . . . . 9  |-  1  e.  RR
108106, 107ltnlei 9655 . . . . . . . 8  |-  ( 0  <  1  <->  -.  1  <_  0 )
109105, 108mpbi 208 . . . . . . 7  |-  -.  1  <_  0
1109, 4mulcld 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  x.  E
)  e.  CC )
1112, 11mulcld 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  F
)  e.  CC )
112110, 111subcld 9885 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  CC )
113112, 16, 17divcld 10279 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  CC )
114113abscld 13321 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  RR )
115114resqcld 12288 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  e.  RR )
1166nnnn0d 10811 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  NN0 )
117116nn0ge0d 10814 . . . . . . . . . 10  |-  ( ph  ->  0  <_  D )
118114sqge0d 12289 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) )
11925, 115, 117, 118mulge0d 10087 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )
12025, 115remulcld 9572 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  e.  RR )
12147, 120suble0d 10101 . . . . . . . . 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 4395 . . . . . . . 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 13189 . . . . . . . . . . . 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 12275 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) ^ 2 )  / 
( C ^ 2 ) ) )
12914sqvald 12259 . . . . . . . . . . . 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 6247 . . . . . . . . . . 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 2445 . . . . . . . . . 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 9572 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  x.  E
)  e.  RR )
13322, 27remulcld 9572 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  x.  F
)  e.  RR )
134132, 133resubcld 9946 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR )
135134, 57, 17redivcld 10331 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  RR )
136 absresq 13189 . . . . . . . . . . . . . 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 12275 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ^ 2 )  =  ( ( ( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 )  /  ( C ^
2 ) ) )
139137, 138eqtrd 2441 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) )
140139oveq2d 6248 . . . . . . . . . . 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 12260 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  e.  CC )
14216sqcld 12260 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  e.  CC )
143 sqne0 12187 . . . . . . . . . . . . . 14  |-  ( C  e.  CC  ->  (
( C ^ 2 )  =/=  0  <->  C  =/=  0 ) )
14416, 143syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( C ^
2 )  =/=  0  <->  C  =/=  0 ) )
14517, 144mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  =/=  0 )
1467, 141, 142, 145divassd 10314 . . . . . . . . . . 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 12259 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  =  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )
148147oveq2d 6248 . . . . . . . . . . . 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 6247 . . . . . . . . . . 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 2447 . . . . . . . . . 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 6250 . . . . . . . . 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 9564 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
153112, 112mulcld 9564 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  CC )
1547, 153mulcld 9564 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  e.  CC )
155152, 154, 142, 145divsubdird 10318 . . . . . . . . 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 9974 . . . . . . . . . . . 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 9974 . . . . . . . . . . . . . 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 6248 . . . . . . . . . . . . 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 9564 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( B  x.  E )
)  e.  CC )
160111, 111mulcld 9564 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  F )  x.  ( A  x.  F )
)  e.  CC )
161159, 160addcld 9563 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
162110, 111mulcld 9564 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( A  x.  F )
)  e.  CC )
163162, 162addcld 9563 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
1647, 161, 163subdid 9971 . . . . . . . . . . . . 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 9568 . . . . . . . . . . . . . 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 9568 . . . . . . . . . . . . . 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 6250 . . . . . . . . . . . . 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 2445 . . . . . . . . . . . 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 6250 . . . . . . . . . . 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 6247 . . . . . . . . . 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 9565 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( A  x.  E
) ) )
1727, 12, 5mulassd 9567 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( A  x.  E )
)  =  ( D  x.  ( ( B  x.  F )  x.  ( A  x.  E
) ) ) )
1732, 4mulcomd 9565 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  x.  E
)  =  ( E  x.  A ) )
174173oveq2d 6248 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  F )  x.  ( E  x.  A ) ) )
1759, 11, 4, 2mul4d 9744 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( E  x.  A )
)  =  ( ( B  x.  E )  x.  ( F  x.  A ) ) )
17611, 2mulcomd 9565 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F  x.  A
)  =  ( A  x.  F ) )
177176oveq2d 6248 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E )  x.  ( F  x.  A )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
178174, 175, 1773eqtrd 2445 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
179178oveq2d 6248 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  F
)  x.  ( A  x.  E ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) )
180171, 172, 1793eqtrd 2445 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) )
181180, 180oveq12d 6250 . . . . . . . . . . . . . 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 6248 . . . . . . . . . . . . 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 6247 . . . . . . . . . . . 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 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  x.  E )  x.  ( A  x.  E )
)  e.  CC )
18513, 13mulcld 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) )  e.  CC )
186184, 185addcld 9563 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
1877, 159mulcld 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  e.  CC )
1887, 160mulcld 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
189187, 188addcld 9563 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  e.  CC )
1907, 162mulcld 9564 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
191190, 190addcld 9563 . . . . . . . . . . . . 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 9920 . . . . . . . . . . . 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 9932 . . . . . . . . . . . . 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 12259 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A  x.  E )  x.  ( A  x.  E ) ) )
195110sqvald 12259 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B  x.  E )  x.  ( B  x.  E ) ) )
196195oveq2d 6248 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )
197194, 196oveq12d 6250 . . . . . . . . . . . . . 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 12259 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )
199111sqvald 12259 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A  x.  F )  x.  ( A  x.  F ) ) )
200199oveq2d 6248 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )
201198, 200oveq12d 6250 . . . . . . . . . . . . . 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 6250 . . . . . . . . . . . . 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 12274 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( E ^
2 ) ) )
2049, 4sqmuld 12274 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( E ^
2 ) ) )
205204oveq2d 6248 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B ^ 2 )  x.  ( E ^ 2 ) ) ) )
2069sqcld 12260 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B ^ 2 )  e.  CC )
2077, 206, 36mulassd 9567 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) )  =  ( D  x.  ( ( B ^
2 )  x.  ( E ^ 2 ) ) ) )
208205, 207eqtr4d 2444 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )
209203, 208oveq12d 6250 . . . . . . . . . . . . . . 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 12259 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D ^ 2 )  =  ( D  x.  D ) )
2119, 11sqmuld 12274 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( F ^
2 ) ) )
212210, 211oveq12d 6250 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D ^
2 )  x.  (
( B  x.  F
) ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^ 2 )  x.  ( F ^ 2 ) ) ) )
2137, 12sqmuld 12274 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D ^ 2 )  x.  ( ( B  x.  F ) ^
2 ) ) )
2147, 7mulcld 9564 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  D
)  e.  CC )
215214, 206, 37mulassd 9567 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^
2 )  x.  ( F ^ 2 ) ) ) )
216212, 213, 2153eqtr4d 2451 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) ) )
2172, 11sqmuld 12274 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( F ^
2 ) ) )
218217oveq2d 6248 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A ^ 2 )  x.  ( F ^ 2 ) ) ) )
2192sqcld 12260 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A ^ 2 )  e.  CC )
2207, 219, 37mulassd 9567 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( D  x.  ( ( A ^
2 )  x.  ( F ^ 2 ) ) ) )
221218, 220eqtr4d 2444 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )
222216, 221oveq12d 6250 . . . . . . . . . . . . . . 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 6250 . . . . . . . . . . . . . 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 9564 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( B ^ 2 ) )  e.  CC )
225219, 224, 36subdird 9972 . . . . . . . . . . . . . . . 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 6247 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( C  x.  ( E ^ 2 ) ) )
228225, 227eqtr3d 2443 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  (
( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )  =  ( C  x.  ( E ^ 2 ) ) )
2297, 7, 206mulassd 9567 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  =  ( D  x.  ( D  x.  ( B ^ 2 ) ) ) )
230229oveq1d 6247 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
231230oveq1d 6247 . . . . . . . . . . . . . . . 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 9564 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  e.  CC )
2337, 219mulcld 9564 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( A ^ 2 ) )  e.  CC )
234232, 233, 37subdird 9972 . . . . . . . . . . . . . . . 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 9949 . . . . . . . . . . . . . . . . . . . 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 2408 . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
238 negsubdi2 9832 . . . . . . . . . . . . . . . . . . . . . 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 2408 . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
241226negeqd 9768 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  -u C
)
242240, 241eqtrd 2441 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u C )
243242oveq2d 6248 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  (
( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( D  x.  -u C ) )
2447, 16mulneg2d 9969 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  -u C
)  =  -u ( D  x.  C )
)
245237, 243, 2443eqtrd 2445 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  -u ( D  x.  C ) )
246245oveq1d 6247 . . . . . . . . . . . . . . . 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 2449 . . . . . . . . . . . . . . 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 6250 . . . . . . . . . . . . . 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 9564 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  C
)  e.  CC )
250249, 37mulneg1d 9968 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( ( D  x.  C )  x.  ( F ^ 2 ) ) )
2517, 16mulcomd 9565 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( D  x.  C
)  =  ( C  x.  D ) )
252251oveq1d 6247 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( ( C  x.  D )  x.  ( F ^ 2 ) ) )
25316, 7, 37mulassd 9567 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( C  x.  D )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
254252, 253eqtrd 2441 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
255254negeqd 9768 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
256250, 255eqtrd 2441 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
257256oveq2d 6248 . . . . . . . . . . . . . . 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 9564 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( E ^ 2 ) )  e.  CC )
25916, 38mulcld 9564 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( D  x.  ( F ^ 2 ) ) )  e.  CC )
260258, 259negsubd 9891 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^
2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
26161oveq2d 6248 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( C  x.  C ) )
262 subdi 9949 . . . . . . . . . . . . . . . . . 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 2408 . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26516sqvald 12259 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C ^ 2 )  =  ( C  x.  C ) )
266261, 264, 2653eqtr4d 2451 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C ^ 2 ) )
267257, 260, 2663eqtrd 2445 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( C ^ 2 ) )
268223, 248, 2673eqtrd 2445 . . . . . . . . . . . . 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 2447 . . . . . . . . . . . 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 2445 . . . . . . . . . . 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 6247 . . . . . . . . . 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 10277 . . . . . . . . . 10  |-  ( ph  ->  ( ( C ^
2 )  /  ( C ^ 2 ) )  =  1 )
273170, 271, 2723eqtrd 2445 . . . . . . . . 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 2447 . . . . . . . 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 463 . . . . . . 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 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  =  0 )
277276oveq1d 6247 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  =  ( 0  /  C
) )
278277fveq2d 5807 . . . . . . . . . 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 10278 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  /  C
)  =  0 )
280279abs00bd 13178 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
0  /  C ) )  =  0 )
281280adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( 0  /  C ) )  =  0 )
282278, 281eqtrd 2441 . . . . . . . . 9  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  0 )
283282sq0id 12214 . . . . . . . 8  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  0 )
284283oveq1d 6247 . . . . . . 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 2443 . . . . . 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 657 . . . . 5  |-  ( ph  ->  -.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  =  0 )
287286neqned 2604 . . . 4  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =/=  0 )
28814, 16, 287, 17divne0d 10295 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )
289 nnabscl 13212 . . 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 659 . 2  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
291112, 16, 17absdivd 13340 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  =  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F ) ) )  /  ( abs `  C
) ) )
292 negsub 9821 . . . . . . . . . . . 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 2408 . . . . . . . . . . 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 659 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  =  ( ( B  x.  E )  +  -u ( A  x.  F ) ) )
295294oveq1d 6247 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) ) )
296133renegcld 9945 . . . . . . . . . 10  |-  ( ph  -> 
-u ( A  x.  F )  e.  RR )
29711, 4mulcomd 9565 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  E
)  =  ( E  x.  F ) )
298297oveq1d 6247 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
299 modmul1 11992 . . . . . . . . . . . 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 1239 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
301 modmul1 11992 . . . . . . . . . . . 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 1239 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
303298, 300, 3023eqtr4d 2451 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( A  x.  F )  mod  ( abs `  C
) ) )
304 modadd1 11983 . . . . . . . . . 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 1239 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
306111negidd 9875 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  F )  +  -u ( A  x.  F
) )  =  0 )
307306oveq1d 6247 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  F )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
308295, 305, 3073eqtrd 2445 . . . . . . . 8  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
309308, 64eqtrd 2441 . . . . . . 7  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0 )
310 absmod0 13190 . . . . . . . 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 659 . . . . . . 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 13321 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR )
314 mod0 11952 . . . . . . 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 659 . . . . . 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 2488 . . . 4  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  ZZ )
318 absz 13198 . . . . 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 232 . . 3  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ )
321 pellex.neq . . . . . . 7  |-  ( ph  ->  -.  ( A  =  E  /\  B  =  F ) )
32210nnne0d 10539 . . . . . . . . 9  |-  ( ph  ->  F  =/=  0 )
3233nnne0d 10539 . . . . . . . . 9  |-  ( ph  ->  E  =/=  0 )
3249, 11, 2, 4, 322, 323divmuleqd 10325 . . . . . . . 8  |-  ( ph  ->  ( ( B  /  F )  =  ( A  /  E )  <-> 
( B  x.  E
)  =  ( A  x.  F ) ) )
32561adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
326325eqcomd 2408 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  C  =  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) ) )
327326oveq2d 6248 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  C )  =  ( ( ( B  /  F ) ^
2 )  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
3289, 11, 322divcld 10279 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  F
)  e.  CC )
329328sqcld 12260 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  /  F ) ^ 2 )  e.  CC )
330329adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  e.  CC )
33136adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  e.  CC )
33238adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
333330, 331, 332subdid 9971 . . . . . . . . . . . . 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 6239 . . . . . . . . . . . . . . . . 17  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( B  /  F
) ^ 2 )  =  ( ( A  /  E ) ^
2 ) )
335334oveq1d 6247 . . . . . . . . . . . . . . . 16  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( ( B  /  F ) ^ 2 )  x.  ( E ^ 2 ) )  =  ( ( ( A  /  E ) ^ 2 )  x.  ( E ^ 2 ) ) )
336335adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A  /  E ) ^
2 )  x.  ( E ^ 2 ) ) )
3372adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  A  e.  CC )
3384adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  e.  CC )
339323adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  =/=  0 )
340337, 338, 339sqdivd 12275 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( A  /  E ) ^
2 )  =  ( ( A ^ 2 )  /  ( E ^ 2 ) ) )
341340oveq1d 6247 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A  /  E
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A ^ 2 )  / 
( E ^ 2 ) )  x.  ( E ^ 2 ) ) )
342219adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( A ^ 2 )  e.  CC )
343 sqne0 12187 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  CC  ->  (
( E ^ 2 )  =/=  0  <->  E  =/=  0 ) )
3444, 343syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( E ^
2 )  =/=  0  <->  E  =/=  0 ) )
345323, 344mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E ^ 2 )  =/=  0 )
346345adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  =/=  0 )
347342, 331, 346divcan1d 10280 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A ^ 2 )  /  ( E ^ 2 ) )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
348336, 341, 3473eqtrd 2445 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
3497adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  D  e.  CC )
35037adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  e.  CC )
351330, 349, 350mul12d 9741 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B  /  F
) ^ 2 )  x.  ( F ^
2 ) ) ) )
3529adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  B  e.  CC )
35311adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  e.  CC )
354322adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  =/=  0 )
355352, 353, 354sqdivd 12275 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  =  ( ( B ^ 2 )  /  ( F ^ 2 ) ) )
356355oveq1d 6247 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( F ^
2 ) )  =  ( ( ( B ^ 2 )  / 
( F ^ 2 ) )  x.  ( F ^ 2 ) ) )
357356oveq2d 6248 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( ( ( B  /  F ) ^
2 )  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B ^ 2 )  /  ( F ^
2 ) )  x.  ( F ^ 2 ) ) ) )
358206adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( B ^ 2 )  e.  CC )
359 sqne0 12187 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  e.  CC  ->  (
( F ^ 2 )  =/=  0  <->  F  =/=  0 ) )
36011, 359syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( F ^
2 )  =/=  0  <->  F  =/=  0 ) )
361322, 360mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F ^ 2 )  =/=  0 )
362361adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  =/=  0 )
363358, 350, 362divcan1d 10280 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B ^ 2 )  /  ( F ^ 2 ) )  x.  ( F ^
2 ) )  =  (