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 29128
Description: Lemma for pellex 29129. 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 10330 . . . . . . . 8  |-  ( ph  ->  A  e.  CC )
3 pellex.enn . . . . . . . . 9  |-  ( ph  ->  E  e.  NN )
43nncnd 10330 . . . . . . . 8  |-  ( ph  ->  E  e.  CC )
52, 4mulcld 9398 . . . . . . 7  |-  ( ph  ->  ( A  x.  E
)  e.  CC )
6 pellex.dnn . . . . . . . . 9  |-  ( ph  ->  D  e.  NN )
76nncnd 10330 . . . . . . . 8  |-  ( ph  ->  D  e.  CC )
8 pellex.bnn . . . . . . . . . 10  |-  ( ph  ->  B  e.  NN )
98nncnd 10330 . . . . . . . . 9  |-  ( ph  ->  B  e.  CC )
10 pellex.fnn . . . . . . . . . 10  |-  ( ph  ->  F  e.  NN )
1110nncnd 10330 . . . . . . . . 9  |-  ( ph  ->  F  e.  CC )
129, 11mulcld 9398 . . . . . . . 8  |-  ( ph  ->  ( B  x.  F
)  e.  CC )
137, 12mulcld 9398 . . . . . . 7  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  CC )
145, 13subcld 9711 . . . . . 6  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  CC )
15 pellex.cz . . . . . . 7  |-  ( ph  ->  C  e.  ZZ )
1615zcnd 10740 . . . . . 6  |-  ( ph  ->  C  e.  CC )
17 pellex.cn0 . . . . . 6  |-  ( ph  ->  C  =/=  0 )
1814, 16, 17absdivd 12933 . . . . 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 9717 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F )
) )  =  ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )
2019eqcomd 2443 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =  ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) ) )
2120oveq1d 6101 . . . . . . . . 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 10329 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
233nnred 10329 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  RR )
2422, 23remulcld 9406 . . . . . . . . . 10  |-  ( ph  ->  ( A  x.  E
)  e.  RR )
256nnred 10329 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  RR )
268nnred 10329 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
2710nnred 10329 . . . . . . . . . . . 12  |-  ( ph  ->  F  e.  RR )
2826, 27remulcld 9406 . . . . . . . . . . 11  |-  ( ph  ->  ( B  x.  F
)  e.  RR )
2925, 28remulcld 9406 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  ( B  x.  F )
)  e.  RR )
3029renegcld 9767 . . . . . . . . . 10  |-  ( ph  -> 
-u ( D  x.  ( B  x.  F
) )  e.  RR )
3116, 17absrpcld 12926 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  C
)  e.  RR+ )
323nnzd 10738 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  ZZ )
33 pellex.xcg . . . . . . . . . . . 12  |-  ( ph  ->  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C ) ) )
34 modmul1 11744 . . . . . . . . . . . 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 1229 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  E )  mod  ( abs `  C
) ) )
364sqcld 11998 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
3711sqcld 11998 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F ^ 2 )  e.  CC )
387, 37mulcld 9398 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
3936, 38npcand 9715 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  =  ( E ^
2 ) )
404sqvald 11997 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
4139, 40eqtr2d 2471 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  x.  E
)  =  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) ) )
4241oveq1d 6101 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
4323resqcld 12026 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E ^ 2 )  e.  RR )
4427resqcld 12026 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  e.  RR )
4525, 44remulcld 9406 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  e.  RR )
4643, 45resubcld 9768 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR )
47 0re 9378 . . . . . . . . . . . . . 14  |-  0  e.  RR
4847a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  RR )
4916abscld 12914 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( abs `  C
)  e.  RR )
5049recnd 9404 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  e.  CC )
5116, 17absne0d 12925 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( abs `  C
)  =/=  0 )
5250, 51dividd 10097 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  =  1 )
53 1z 10668 . . . . . . . . . . . . . . . . . 18  |-  1  e.  ZZ
5453a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ZZ )
5552, 54eqeltrd 2512 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( abs `  C
)  /  ( abs `  C ) )  e.  ZZ )
56 mod0 11707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( abs `  C
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  C
)  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  /  ( abs `  C ) )  e.  ZZ ) )
5749, 31, 56syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( abs `  C )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  / 
( abs `  C
) )  e.  ZZ ) )
5855, 57mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( abs `  C
)  mod  ( abs `  C ) )  =  0 )
5915zred 10739 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
60 absmod0 12784 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( C  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  C )  mod  ( abs `  C
) )  =  0 ) )
6159, 31, 60syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  mod  ( abs `  C ) )  =  0  <->  (
( abs `  C
)  mod  ( abs `  C ) )  =  0 ) )
6258, 61mpbird 232 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C  mod  ( abs `  C ) )  =  0 )
63 pellex.no2 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
6463oveq1d 6101 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( C  mod  ( abs `  C ) ) )
65 0mod 11731 . . . . . . . . . . . . . . 15  |-  ( ( abs `  C )  e.  RR+  ->  ( 0  mod  ( abs `  C
) )  =  0 )
6631, 65syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  mod  ( abs `  C ) )  =  0 )
6762, 64, 663eqtr4d 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )
68 modadd1 11737 . . . . . . . . . . . . 13  |-  ( ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  e.  RR  /\  0  e.  RR )  /\  ( ( D  x.  ( F ^ 2 ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  /\  (
( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C ) ) )  ->  ( (
( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^
2 ) ) )  mod  ( abs `  C
) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
6946, 48, 45, 31, 67, 68syl221anc 1229 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) ) )
7038addid2d 9562 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( F ^
2 ) ) )
7111sqvald 11997 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( F ^ 2 )  =  ( F  x.  F ) )
7271oveq2d 6102 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F ^ 2 ) )  =  ( D  x.  ( F  x.  F
) ) )
737, 11, 11mul12d 9570 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  ( F  x.  F )
)  =  ( F  x.  ( D  x.  F ) ) )
7470, 72, 733eqtrd 2474 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  +  ( D  x.  ( F ^ 2 ) ) )  =  ( F  x.  ( D  x.  F ) ) )
7574oveq1d 6101 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 0  +  ( D  x.  ( F ^ 2 ) ) )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) ) )
7642, 69, 753eqtrd 2474 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
776nnzd 10738 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  ZZ )
7810nnzd 10738 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ZZ )
7977, 78zmulcld 10745 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  F
)  e.  ZZ )
80 pellex.ycg . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C ) ) )
8180eqcomd 2443 . . . . . . . . . . . . 13  |-  ( ph  ->  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C ) ) )
82 modmul1 11744 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  RR  /\  B  e.  RR )  /\  ( ( D  x.  F )  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( F  mod  ( abs `  C ) )  =  ( B  mod  ( abs `  C
) ) )  -> 
( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
8327, 26, 79, 31, 81, 82syl221anc 1229 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( B  x.  ( D  x.  F ) )  mod  ( abs `  C
) ) )
849, 7, 11mul12d 9570 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  x.  ( D  x.  F )
)  =  ( D  x.  ( B  x.  F ) ) )
8584oveq1d 6101 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8683, 85eqtrd 2470 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  ( D  x.  F
) )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
8735, 76, 863eqtrd 2474 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  E )  mod  ( abs `  C ) )  =  ( ( D  x.  ( B  x.  F ) )  mod  ( abs `  C
) ) )
88 modadd1 11737 . . . . . . . . . 10  |-  ( ( ( ( A  x.  E )  e.  RR  /\  ( D  x.  ( B  x.  F )
)  e.  RR )  /\  ( -u ( D  x.  ( B  x.  F ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  /\  ( ( A  x.  E )  mod  ( abs `  C
) )  =  ( ( D  x.  ( B  x.  F )
)  mod  ( abs `  C ) ) )  ->  ( ( ( A  x.  E )  +  -u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) ) )
8924, 29, 30, 31, 87, 88syl221anc 1229 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  E )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) ) )
9013negidd 9701 . . . . . . . . . 10  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  +  -u ( D  x.  ( B  x.  F )
) )  =  0 )
9190oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) )  + 
-u ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
9221, 89, 913eqtrd 2474 . . . . . . . 8  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
9392, 66eqtrd 2470 . . . . . . 7  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  mod  ( abs `  C ) )  =  0 )
9424, 29resubcld 9768 . . . . . . . 8  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR )
95 absmod0 12784 . . . . . . . 8  |-  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 ) )
9694, 31, 95syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 ) )
9793, 96mpbid 210 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0 )
9814abscld 12914 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR )
99 mod0 11707 . . . . . . 7  |-  ( ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ ) )
10098, 31, 99syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ ) )
10197, 100mpbid 210 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( abs `  C ) )  e.  ZZ )
10218, 101eqeltrd 2512 . . . 4  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ )
10394, 59, 17redivcld 10151 . . . . 5  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  RR )
104 absz 12792 . . . . 5  |-  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  e.  RR  ->  ( (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  e.  ZZ  <->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ ) )
105103, 104syl 16 . . . 4  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C )  e.  ZZ  <->  ( abs `  ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  ZZ ) )
106102, 105mpbird 232 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ )
107 0lt1 9854 . . . . . . . 8  |-  0  <  1
108 1re 9377 . . . . . . . . 9  |-  1  e.  RR
10947, 108ltnlei 9487 . . . . . . . 8  |-  ( 0  <  1  <->  -.  1  <_  0 )
110107, 109mpbi 208 . . . . . . 7  |-  -.  1  <_  0
1119, 4mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  x.  E
)  e.  CC )
1122, 11mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  x.  F
)  e.  CC )
113111, 112subcld 9711 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  CC )
114113, 16, 17divcld 10099 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  CC )
115114abscld 12914 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  RR )
116115resqcld 12026 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  e.  RR )
1176nnnn0d 10628 . . . . . . . . . . 11  |-  ( ph  ->  D  e.  NN0 )
118117nn0ge0d 10631 . . . . . . . . . 10  |-  ( ph  ->  0  <_  D )
119115sqge0d 12027 . . . . . . . . . 10  |-  ( ph  ->  0  <_  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) )
12025, 116, 118, 119mulge0d 9908 . . . . . . . . 9  |-  ( ph  ->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )
12125, 116remulcld 9406 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  e.  RR )
12248, 121suble0d 9922 . . . . . . . . 9  |-  ( ph  ->  ( ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  <_  0  <->  0  <_  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) ) )
123120, 122mpbird 232 . . . . . . . 8  |-  ( ph  ->  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ) ^
2 ) ) )  <_  0 )
124 breq1 4290 . . . . . . . 8  |-  ( 1  =  ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  ->  (
1  <_  0  <->  ( 0  -  ( D  x.  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  <_  0
) )
125123, 124syl5ibrcom 222 . . . . . . 7  |-  ( ph  ->  ( 1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  -> 
1  <_  0 ) )
126110, 125mtoi 178 . . . . . 6  |-  ( ph  ->  -.  1  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) ) )
127 absresq 12783 . . . . . . . . . . . 12  |-  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  e.  RR  ->  ( ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ) ^
2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
) ^ 2 ) )
128103, 127syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 ) )
12914, 16, 17sqdivd 12013 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) ^ 2 )  / 
( C ^ 2 ) ) )
13014sqvald 11997 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) ^ 2 )  =  ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) ) )
131130oveq1d 6101 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) ) ^
2 )  /  ( C ^ 2 ) )  =  ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  / 
( C ^ 2 ) ) )
132128, 129, 1313eqtrd 2474 . . . . . . . . . 10  |-  ( ph  ->  ( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  /  ( C ^ 2 ) ) )
13326, 23remulcld 9406 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  x.  E
)  e.  RR )
13422, 27remulcld 9406 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( A  x.  F
)  e.  RR )
135133, 134resubcld 9768 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR )
136135, 59, 17redivcld 10151 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  RR )
137 absresq 12783 . . . . . . . . . . . . . 14  |-  ( ( ( ( B  x.  E )  -  ( A  x.  F )
)  /  C )  e.  RR  ->  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) ^
2 ) )
138136, 137syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) ^
2 ) )
139113, 16, 17sqdivd 12013 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C ) ^ 2 )  =  ( ( ( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 )  /  ( C ^
2 ) ) )
140138, 139eqtrd 2470 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 )  =  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) )
141140oveq2d 6102 . . . . . . . . . . 11  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  =  ( D  x.  ( ( ( ( B  x.  E
)  -  ( A  x.  F ) ) ^ 2 )  / 
( C ^ 2 ) ) ) )
142113sqcld 11998 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  e.  CC )
14316sqcld 11998 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  e.  CC )
144 sqne0 11924 . . . . . . . . . . . . . 14  |-  ( C  e.  CC  ->  (
( C ^ 2 )  =/=  0  <->  C  =/=  0 ) )
14516, 144syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( C ^
2 )  =/=  0  <->  C  =/=  0 ) )
14617, 145mpbird 232 . . . . . . . . . . . 12  |-  ( ph  ->  ( C ^ 2 )  =/=  0 )
1477, 142, 143, 146divassd 10134 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 ) )  /  ( C ^ 2 ) )  =  ( D  x.  ( ( ( ( B  x.  E )  -  ( A  x.  F ) ) ^
2 )  /  ( C ^ 2 ) ) ) )
148113sqvald 11997 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 )  =  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )
149148oveq2d 6102 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
) ^ 2 ) )  =  ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F )
) ) ) )
150149oveq1d 6101 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F
) ) ^ 2 ) )  /  ( C ^ 2 ) )  =  ( ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F )
) ) )  / 
( C ^ 2 ) ) )
151141, 147, 1503eqtr2d 2476 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) )  =  ( ( D  x.  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F
) ) ) )  /  ( C ^
2 ) ) )
152132, 151oveq12d 6104 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
) ) ^ 2 )  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  =  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  / 
( C ^ 2 ) )  -  (
( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  /  ( C ^ 2 ) ) ) )
15314, 14mulcld 9398 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
154113, 113mulcld 9398 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  CC )
1557, 154mulcld 9398 . . . . . . . . . 10  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  e.  CC )
156153, 155, 143, 146divsubdird 10138 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  -  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) ) )  /  ( C ^ 2 ) )  =  ( ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  / 
( C ^ 2 ) )  -  (
( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  /  ( C ^ 2 ) ) ) )
1575, 13, 5, 13mulsubd 9795 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  x.  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) ) )  =  ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F
) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) ) ) ) )
158111, 112, 111, 112mulsubd 9795 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  x.  (
( B  x.  E
)  -  ( A  x.  F ) ) )  =  ( ( ( ( B  x.  E )  x.  ( B  x.  E )
)  +  ( ( A  x.  F )  x.  ( A  x.  F ) ) )  -  ( ( ( B  x.  E )  x.  ( A  x.  F ) )  +  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )
159158oveq2d 6102 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  =  ( D  x.  ( ( ( ( B  x.  E
)  x.  ( B  x.  E ) )  +  ( ( A  x.  F )  x.  ( A  x.  F
) ) )  -  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
160111, 111mulcld 9398 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( B  x.  E )
)  e.  CC )
161112, 112mulcld 9398 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  F )  x.  ( A  x.  F )
)  e.  CC )
162160, 161addcld 9397 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
163111, 112mulcld 9398 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  x.  E )  x.  ( A  x.  F )
)  e.  CC )
164163, 163addcld 9397 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
1657, 162, 164subdid 9792 . . . . . . . . . . . . 13  |-  ( ph  ->  ( D  x.  (
( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) )  -  ( ( ( B  x.  E
)  x.  ( A  x.  F ) )  +  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) ) )  =  ( ( D  x.  ( ( ( B  x.  E
)  x.  ( B  x.  E ) )  +  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )  -  ( D  x.  ( ( ( B  x.  E )  x.  ( A  x.  F
) )  +  ( ( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
1667, 160, 161adddid 9402 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  x.  ( B  x.  E )
)  +  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  =  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )
1677, 163, 163adddid 9402 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  x.  ( A  x.  F )
)  +  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) )  =  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )
168166, 167oveq12d 6104 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( ( B  x.  E )  x.  ( B  x.  E
) )  +  ( ( A  x.  F
)  x.  ( A  x.  F ) ) ) )  -  ( D  x.  ( (
( B  x.  E
)  x.  ( A  x.  F ) )  +  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) ) )  =  ( ( ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) )  +  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
169159, 165, 1683eqtrd 2474 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) )  =  ( ( ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) )  +  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) ) ) ) )
170157, 169oveq12d 6104 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) ) )  -  ( D  x.  ( ( ( B  x.  E )  -  ( A  x.  F ) )  x.  ( ( B  x.  E )  -  ( A  x.  F )
) ) ) )  =  ( ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F
) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) ) )
171170oveq1d 6101 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  -  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) ) )  /  ( C ^ 2 ) )  =  ( ( ( ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) ) ) )  -  ( ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) ) )  / 
( C ^ 2 ) ) )
1725, 13mulcomd 9399 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( A  x.  E
) ) )
1737, 12, 5mulassd 9401 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( A  x.  E )
)  =  ( D  x.  ( ( B  x.  F )  x.  ( A  x.  E
) ) ) )
1742, 4mulcomd 9399 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( A  x.  E
)  =  ( E  x.  A ) )
175174oveq2d 6102 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  F )  x.  ( E  x.  A ) ) )
1769, 11, 4, 2mul4d 9573 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F )  x.  ( E  x.  A )
)  =  ( ( B  x.  E )  x.  ( F  x.  A ) ) )
17711, 2mulcomd 9399 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F  x.  A
)  =  ( A  x.  F ) )
178177oveq2d 6102 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E )  x.  ( F  x.  A )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
179175, 176, 1783eqtrd 2474 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( B  x.  F )  x.  ( A  x.  E )
)  =  ( ( B  x.  E )  x.  ( A  x.  F ) ) )
180179oveq2d 6102 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  F
)  x.  ( A  x.  E ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F
) ) ) )
181172, 173, 1803eqtrd 2474 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) )
182181, 181oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) )  +  ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) ) )  =  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )
183182oveq2d 6102 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E )  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) ) ) )  =  ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) ) )
184183oveq1d 6101 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) )  +  ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  =  ( ( ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) )  -  ( ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) ) ) )
1855, 5mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( A  x.  E )  x.  ( A  x.  E )
)  e.  CC )
18613, 13mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) )  e.  CC )
187185, 186addcld 9397 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A  x.  E )  x.  ( A  x.  E
) )  +  ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) ) )  e.  CC )
1887, 160mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( B  x.  E ) ) )  e.  CC )
1897, 161mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) )  e.  CC )
190188, 189addcld 9397 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  e.  CC )
1917, 163mulcld 9398 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( D  x.  (
( B  x.  E
)  x.  ( A  x.  F ) ) )  e.  CC )
192191, 191addcld 9397 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) )  e.  CC )
193187, 190, 192nnncan2d 9746 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  =  ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) )  +  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) ) ) ) )
194185, 186, 188, 189addsub4d 9758 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E )  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )  =  ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  -  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) ) )  +  ( ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) )  -  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) ) ) )
1955sqvald 11997 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A  x.  E )  x.  ( A  x.  E ) ) )
196111sqvald 11997 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B  x.  E )  x.  ( B  x.  E ) ) )
197196oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )
198195, 197oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A  x.  E ) ^
2 )  -  ( D  x.  ( ( B  x.  E ) ^ 2 ) ) )  =  ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  -  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) ) ) )
19913sqvald 11997 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )
200112sqvald 11997 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A  x.  F )  x.  ( A  x.  F ) ) )
201200oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F
) ) ) )
202199, 201oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) ) ^
2 )  -  ( D  x.  ( ( A  x.  F ) ^ 2 ) ) )  =  ( ( ( D  x.  ( B  x.  F )
)  x.  ( D  x.  ( B  x.  F ) ) )  -  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )
203198, 202oveq12d 6104 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E ) ^ 2 )  -  ( D  x.  (
( B  x.  E
) ^ 2 ) ) )  +  ( ( ( D  x.  ( B  x.  F
) ) ^ 2 )  -  ( D  x.  ( ( A  x.  F ) ^
2 ) ) ) )  =  ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  -  ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E
) ) ) )  +  ( ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) )  -  ( D  x.  (
( A  x.  F
)  x.  ( A  x.  F ) ) ) ) ) )
2042, 4sqmuld 12012 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( A  x.  E ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( E ^
2 ) ) )
2059, 4sqmuld 12012 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  E ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( E ^
2 ) ) )
206205oveq2d 6102 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( D  x.  ( ( B ^ 2 )  x.  ( E ^ 2 ) ) ) )
2079sqcld 11998 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( B ^ 2 )  e.  CC )
2087, 207, 36mulassd 9401 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) )  =  ( D  x.  ( ( B ^
2 )  x.  ( E ^ 2 ) ) ) )
209206, 208eqtr4d 2473 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( B  x.  E
) ^ 2 ) )  =  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )
210204, 209oveq12d 6104 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A  x.  E ) ^
2 )  -  ( D  x.  ( ( B  x.  E ) ^ 2 ) ) )  =  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  ( ( D  x.  ( B ^
2 ) )  x.  ( E ^ 2 ) ) ) )
2117sqvald 11997 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D ^ 2 )  =  ( D  x.  D ) )
2129, 11sqmuld 12012 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( B  x.  F ) ^ 2 )  =  ( ( B ^ 2 )  x.  ( F ^
2 ) ) )
213211, 212oveq12d 6104 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D ^
2 )  x.  (
( B  x.  F
) ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^ 2 )  x.  ( F ^ 2 ) ) ) )
2147, 12sqmuld 12012 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( D ^ 2 )  x.  ( ( B  x.  F ) ^
2 ) ) )
2157, 7mulcld 9398 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  D
)  e.  CC )
216215, 207, 37mulassd 9401 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( ( D  x.  D )  x.  ( ( B ^
2 )  x.  ( F ^ 2 ) ) ) )
217213, 214, 2163eqtr4d 2480 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( D  x.  ( B  x.  F
) ) ^ 2 )  =  ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) ) )
2182, 11sqmuld 12012 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( A  x.  F ) ^ 2 )  =  ( ( A ^ 2 )  x.  ( F ^
2 ) ) )
219218oveq2d 6102 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( D  x.  ( ( A ^ 2 )  x.  ( F ^ 2 ) ) ) )
2202sqcld 11998 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A ^ 2 )  e.  CC )
2217, 220, 37mulassd 9401 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) )  =  ( D  x.  ( ( A ^
2 )  x.  ( F ^ 2 ) ) ) )
222219, 221eqtr4d 2473 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D  x.  (
( A  x.  F
) ^ 2 ) )  =  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )
223217, 222oveq12d 6104 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( D  x.  ( B  x.  F ) ) ^
2 )  -  ( D  x.  ( ( A  x.  F ) ^ 2 ) ) )  =  ( ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) )  -  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) ) ) )
224210, 223oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( A  x.  E ) ^ 2 )  -  ( D  x.  (
( B  x.  E
) ^ 2 ) ) )  +  ( ( ( D  x.  ( B  x.  F
) ) ^ 2 )  -  ( D  x.  ( ( A  x.  F ) ^
2 ) ) ) )  =  ( ( ( ( A ^
2 )  x.  ( E ^ 2 ) )  -  ( ( D  x.  ( B ^
2 ) )  x.  ( E ^ 2 ) ) )  +  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  x.  ( F ^ 2 ) )  -  (
( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) ) ) )
2257, 207mulcld 9398 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( B ^ 2 ) )  e.  CC )
226220, 225, 36subdird 9793 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( ( ( A ^ 2 )  x.  ( E ^
2 ) )  -  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) ) ) )
227 pellex.no1 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  C )
228227oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  x.  ( E ^ 2 ) )  =  ( C  x.  ( E ^ 2 ) ) )
229226, 228eqtr3d 2472 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( A ^ 2 )  x.  ( E ^ 2 ) )  -  (
( D  x.  ( B ^ 2 ) )  x.  ( E ^
2 ) ) )  =  ( C  x.  ( E ^ 2 ) ) )
2307, 7, 207mulassd 9401 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  =  ( D  x.  ( D  x.  ( B ^ 2 ) ) ) )
231230oveq1d 6101 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
232231oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( ( ( D  x.  ( D  x.  ( B ^
2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) ) )
233215, 207mulcld 9398 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  D )  x.  ( B ^ 2 ) )  e.  CC )
2347, 220mulcld 9398 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D  x.  ( A ^ 2 ) )  e.  CC )
235233, 234, 37subdird 9793 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( ( ( ( D  x.  D
)  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) )  -  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) ) ) )
236 subdi 9770 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( D  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC  /\  ( A ^ 2 )  e.  CC )  ->  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) ) )
237236eqcomd 2443 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC  /\  ( A ^ 2 )  e.  CC )  ->  (
( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
2387, 225, 220, 237syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  ( D  x.  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) ) ) )
239 negsubdi2 9660 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A ^ 2 )  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC )  ->  -u ( ( A ^
2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )
240239eqcomd 2443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A ^ 2 )  e.  CC  /\  ( D  x.  ( B ^ 2 ) )  e.  CC )  -> 
( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
241220, 225, 240syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) ) )
242227negeqd 9596 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  -> 
-u ( ( A ^ 2 )  -  ( D  x.  ( B ^ 2 ) ) )  =  -u C
)
243241, 242eqtrd 2470 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  ( B ^ 2 ) )  -  ( A ^ 2 ) )  =  -u C )
244243oveq2d 6102 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  (
( D  x.  ( B ^ 2 ) )  -  ( A ^
2 ) ) )  =  ( D  x.  -u C ) )
2457, 16mulneg2d 9790 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  -u C
)  =  -u ( D  x.  C )
)
246238, 244, 2453eqtrd 2474 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^
2 ) ) )  =  -u ( D  x.  C ) )
247246oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( D  x.  ( D  x.  ( B ^ 2 ) ) )  -  ( D  x.  ( A ^ 2 ) ) )  x.  ( F ^ 2 ) )  =  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) )
248232, 235, 2473eqtr3d 2478 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( D  x.  D )  x.  ( B ^
2 ) )  x.  ( F ^ 2 ) )  -  (
( D  x.  ( A ^ 2 ) )  x.  ( F ^
2 ) ) )  =  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) )
249229, 248oveq12d 6104 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( A ^ 2 )  x.  ( E ^
2 ) )  -  ( ( D  x.  ( B ^ 2 ) )  x.  ( E ^ 2 ) ) )  +  ( ( ( ( D  x.  D )  x.  ( B ^ 2 ) )  x.  ( F ^
2 ) )  -  ( ( D  x.  ( A ^ 2 ) )  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C )  x.  ( F ^ 2 ) ) ) )
2507, 16mulcld 9398 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( D  x.  C
)  e.  CC )
251250, 37mulneg1d 9789 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( ( D  x.  C )  x.  ( F ^ 2 ) ) )
2527, 16mulcomd 9399 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( D  x.  C
)  =  ( C  x.  D ) )
253252oveq1d 6101 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( ( C  x.  D )  x.  ( F ^ 2 ) ) )
25416, 7, 37mulassd 9401 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( C  x.  D )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
255253, 254eqtrd 2470 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
256255negeqd 9596 . . . . . . . . . . . . . . . . 17  |-  ( ph  -> 
-u ( ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
257251, 256eqtrd 2470 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( -u ( D  x.  C )  x.  ( F ^ 2 ) )  =  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )
258257oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
25916, 36mulcld 9398 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( E ^ 2 ) )  e.  CC )
26016, 38mulcld 9398 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  ( D  x.  ( F ^ 2 ) ) )  e.  CC )
261259, 260negsubd 9717 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  -u ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( C  x.  ( E ^
2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
26263oveq2d 6102 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( C  x.  C ) )
263 subdi 9770 . . . . . . . . . . . . . . . . . 18  |-  ( ( C  e.  CC  /\  ( E ^ 2 )  e.  CC  /\  ( D  x.  ( F ^ 2 ) )  e.  CC )  -> 
( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) )  =  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
264263eqcomd 2443 . . . . . . . . . . . . . . . . 17  |-  ( ( C  e.  CC  /\  ( E ^ 2 )  e.  CC  /\  ( D  x.  ( F ^ 2 ) )  e.  CC )  -> 
( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26516, 36, 38, 264syl3anc 1218 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
26616sqvald 11997 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C ^ 2 )  =  ( C  x.  C ) )
267262, 265, 2663eqtr4d 2480 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  -  ( C  x.  ( D  x.  ( F ^ 2 ) ) ) )  =  ( C ^ 2 ) )
268258, 261, 2673eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( C  x.  ( E ^ 2 ) )  +  ( -u ( D  x.  C
)  x.  ( F ^ 2 ) ) )  =  ( C ^ 2 ) )
269224, 249, 2683eqtrd 2474 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A  x.  E ) ^ 2 )  -  ( D  x.  (
( B  x.  E
) ^ 2 ) ) )  +  ( ( ( D  x.  ( B  x.  F
) ) ^ 2 )  -  ( D  x.  ( ( A  x.  F ) ^
2 ) ) ) )  =  ( C ^ 2 ) )
270194, 203, 2693eqtr2d 2476 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( A  x.  E )  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F
) )  x.  ( D  x.  ( B  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E ) ) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F )
) ) ) )  =  ( C ^
2 ) )
271184, 193, 2703eqtrd 2474 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  x.  ( A  x.  E ) )  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F )
) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F )
) )  +  ( ( A  x.  E
)  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  =  ( C ^ 2 ) )
272271oveq1d 6101 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( ( ( A  x.  E )  x.  ( A  x.  E )
)  +  ( ( D  x.  ( B  x.  F ) )  x.  ( D  x.  ( B  x.  F
) ) ) )  -  ( ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F
) ) )  +  ( ( A  x.  E )  x.  ( D  x.  ( B  x.  F ) ) ) ) )  -  (
( ( D  x.  ( ( B  x.  E )  x.  ( B  x.  E )
) )  +  ( D  x.  ( ( A  x.  F )  x.  ( A  x.  F ) ) ) )  -  ( ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F ) ) )  +  ( D  x.  ( ( B  x.  E )  x.  ( A  x.  F )
) ) ) ) )  /  ( C ^ 2 ) )  =  ( ( C ^ 2 )  / 
( C ^ 2 ) ) )
273143, 146dividd 10097 . . . . . . . . . 10  |-  ( ph  ->  ( ( C ^
2 )  /  ( C ^ 2 ) )  =  1 )
274171, 272, 2733eqtrd 2474 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  x.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) ) )  -  ( D  x.  (
( ( B  x.  E )  -  ( A  x.  F )
)  x.  ( ( B  x.  E )  -  ( A  x.  F ) ) ) ) )  /  ( C ^ 2 ) )  =  1 )
275152, 156, 2743eqtr2d 2476 . . . . . . . 8  |-  ( ph  ->  ( ( ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
) ) ^ 2 )  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) )  =  1 )
276275adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  =  1 )
277 simpr 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( A  x.  E
)  -  ( D  x.  ( B  x.  F ) ) )  =  0 )
278277oveq1d 6101 . . . . . . . . . . 11  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C )  =  ( 0  /  C
) )
279278fveq2d 5690 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  ( abs `  (
0  /  C ) ) )
28016, 17div0d 10098 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  /  C
)  =  0 )
281280abs00bd 12772 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
0  /  C ) )  =  0 )
282281adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( 0  /  C ) )  =  0 )
283279, 282eqtrd 2470 . . . . . . . . 9  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  ( abs `  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  /  C ) )  =  0 )
284283sq0id 11951 . . . . . . . 8  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  =  0 )
285284oveq1d 6101 . . . . . . 7  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  (
( ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) ) ^ 2 )  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) )  =  ( 0  -  ( D  x.  ( ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) ) ^ 2 ) ) ) )
286276, 285eqtr3d 2472 . . . . . 6  |-  ( (
ph  /\  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F
) ) )  =  0 )  ->  1  =  ( 0  -  ( D  x.  (
( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) ) ^ 2 ) ) ) )
287126, 286mtand 659 . . . . 5  |-  ( ph  ->  -.  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  =  0 )
288287neneqad 2676 . . . 4  |-  ( ph  ->  ( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  =/=  0 )
28914, 16, 288, 17divne0d 10115 . . 3  |-  ( ph  ->  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )
290 nnabscl 12805 . . 3  |-  ( ( ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  e.  ZZ  /\  ( ( ( A  x.  E )  -  ( D  x.  ( B  x.  F )
) )  /  C
)  =/=  0 )  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
291106, 289, 290syl2anc 661 . 2  |-  ( ph  ->  ( abs `  (
( ( A  x.  E )  -  ( D  x.  ( B  x.  F ) ) )  /  C ) )  e.  NN )
292113, 16, 17absdivd 12933 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  =  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F ) ) )  /  ( abs `  C
) ) )
293 negsub 9649 . . . . . . . . . . . 12  |-  ( ( ( B  x.  E
)  e.  CC  /\  ( A  x.  F
)  e.  CC )  ->  ( ( B  x.  E )  + 
-u ( A  x.  F ) )  =  ( ( B  x.  E )  -  ( A  x.  F )
) )
294293eqcomd 2443 . . . . . . . . . . 11  |-  ( ( ( B  x.  E
)  e.  CC  /\  ( A  x.  F
)  e.  CC )  ->  ( ( B  x.  E )  -  ( A  x.  F
) )  =  ( ( B  x.  E
)  +  -u ( A  x.  F )
) )
295111, 112, 294syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  -  ( A  x.  F )
)  =  ( ( B  x.  E )  +  -u ( A  x.  F ) ) )
296295oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) ) )
297134renegcld 9767 . . . . . . . . . 10  |-  ( ph  -> 
-u ( A  x.  F )  e.  RR )
29811, 4mulcomd 9399 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  E
)  =  ( E  x.  F ) )
299298oveq1d 6101 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F  x.  E )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
300 modmul1 11744 . . . . . . . . . . . 12  |-  ( ( ( B  e.  RR  /\  F  e.  RR )  /\  ( E  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( B  mod  ( abs `  C ) )  =  ( F  mod  ( abs `  C
) ) )  -> 
( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
30126, 27, 32, 31, 80, 300syl221anc 1229 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( F  x.  E )  mod  ( abs `  C
) ) )
302 modmul1 11744 . . . . . . . . . . . 12  |-  ( ( ( A  e.  RR  /\  E  e.  RR )  /\  ( F  e.  ZZ  /\  ( abs `  C )  e.  RR+ )  /\  ( A  mod  ( abs `  C ) )  =  ( E  mod  ( abs `  C
) ) )  -> 
( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
30322, 23, 78, 31, 33, 302syl221anc 1229 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A  x.  F )  mod  ( abs `  C ) )  =  ( ( E  x.  F )  mod  ( abs `  C
) ) )
304299, 301, 3033eqtr4d 2480 . . . . . . . . . 10  |-  ( ph  ->  ( ( B  x.  E )  mod  ( abs `  C ) )  =  ( ( A  x.  F )  mod  ( abs `  C
) ) )
305 modadd1 11737 . . . . . . . . . 10  |-  ( ( ( ( B  x.  E )  e.  RR  /\  ( A  x.  F
)  e.  RR )  /\  ( -u ( A  x.  F )  e.  RR  /\  ( abs `  C )  e.  RR+ )  /\  ( ( B  x.  E )  mod  ( abs `  C
) )  =  ( ( A  x.  F
)  mod  ( abs `  C ) ) )  ->  ( ( ( B  x.  E )  +  -u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
306133, 134, 297, 31, 304, 305syl221anc 1229 . . . . . . . . 9  |-  ( ph  ->  ( ( ( B  x.  E )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( ( ( A  x.  F )  +  -u ( A  x.  F
) )  mod  ( abs `  C ) ) )
307112negidd 9701 . . . . . . . . . 10  |-  ( ph  ->  ( ( A  x.  F )  +  -u ( A  x.  F
) )  =  0 )
308307oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A  x.  F )  + 
-u ( A  x.  F ) )  mod  ( abs `  C
) )  =  ( 0  mod  ( abs `  C ) ) )
309296, 306, 3083eqtrd 2474 . . . . . . . 8  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  ( 0  mod  ( abs `  C
) ) )
310309, 66eqtrd 2470 . . . . . . 7  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0 )
311 absmod0 12784 . . . . . . . 8  |-  ( ( ( ( B  x.  E )  -  ( A  x.  F )
)  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( ( B  x.  E )  -  ( A  x.  F
) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F
) ) )  mod  ( abs `  C
) )  =  0 ) )
312135, 31, 311syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  mod  ( abs `  C
) )  =  0  <-> 
( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 ) )
313310, 312mpbid 210 . . . . . 6  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0 )
314113abscld 12914 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR )
315 mod0 11707 . . . . . . 7  |-  ( ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  e.  RR  /\  ( abs `  C )  e.  RR+ )  ->  (
( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F )
) )  /  ( abs `  C ) )  e.  ZZ ) )
316314, 31, 315syl2anc 661 . . . . . 6  |-  ( ph  ->  ( ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F )
) )  mod  ( abs `  C ) )  =  0  <->  ( ( abs `  ( ( B  x.  E )  -  ( A  x.  F
) ) )  / 
( abs `  C
) )  e.  ZZ ) )
317313, 316mpbid 210 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( B  x.  E
)  -  ( A  x.  F ) ) )  /  ( abs `  C ) )  e.  ZZ )
318292, 317eqeltrd 2512 . . . 4  |-  ( ph  ->  ( abs `  (
( ( B  x.  E )  -  ( A  x.  F )
)  /  C ) )  e.  ZZ )
319 absz 12792 . . . . 5  |-  ( ( ( ( B  x.  E )  -  ( A  x.  F )
)  /  C )  e.  RR  ->  (
( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ  <->  ( abs `  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
) )  e.  ZZ ) )
320136, 319syl 16 . . . 4  |-  ( ph  ->  ( ( ( ( B  x.  E )  -  ( A  x.  F ) )  /  C )  e.  ZZ  <->  ( abs `  ( ( ( B  x.  E
)  -  ( A  x.  F ) )  /  C ) )  e.  ZZ ) )
321318, 320mpbird 232 . . 3  |-  ( ph  ->  ( ( ( B  x.  E )  -  ( A  x.  F
) )  /  C
)  e.  ZZ )
322 pellex.neq . . . . . . 7  |-  ( ph  ->  -.  ( A  =  E  /\  B  =  F ) )
32310nnne0d 10358 . . . . . . . . 9  |-  ( ph  ->  F  =/=  0 )
3243nnne0d 10358 . . . . . . . . 9  |-  ( ph  ->  E  =/=  0 )
3259, 11, 2, 4, 323, 324divmuleqd 10145 . . . . . . . 8  |-  ( ph  ->  ( ( B  /  F )  =  ( A  /  E )  <-> 
( B  x.  E
)  =  ( A  x.  F ) ) )
32663adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) )  =  C )
327326eqcomd 2443 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  C  =  ( ( E ^
2 )  -  ( D  x.  ( F ^ 2 ) ) ) )
328327oveq2d 6102 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  C )  =  ( ( ( B  /  F ) ^
2 )  x.  (
( E ^ 2 )  -  ( D  x.  ( F ^
2 ) ) ) ) )
3299, 11, 323divcld 10099 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  F
)  e.  CC )
330329sqcld 11998 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( B  /  F ) ^ 2 )  e.  CC )
331330adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  e.  CC )
33236adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  e.  CC )
33338adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( F ^ 2 ) )  e.  CC )
334331, 332, 333subdid 9792 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( ( E ^ 2 )  -  ( D  x.  ( F ^ 2 ) ) ) )  =  ( ( ( ( B  /  F ) ^
2 )  x.  ( E ^ 2 ) )  -  ( ( ( B  /  F ) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) ) ) )
335 oveq1 6093 . . . . . . . . . . . . . . . . 17  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( B  /  F
) ^ 2 )  =  ( ( A  /  E ) ^
2 ) )
336335oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( ( B  /  F )  =  ( A  /  E )  ->  (
( ( B  /  F ) ^ 2 )  x.  ( E ^ 2 ) )  =  ( ( ( A  /  E ) ^ 2 )  x.  ( E ^ 2 ) ) )
337336adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A  /  E ) ^
2 )  x.  ( E ^ 2 ) ) )
3382adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  A  e.  CC )
3394adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  e.  CC )
340324adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  E  =/=  0 )
341338, 339, 340sqdivd 12013 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( A  /  E ) ^
2 )  =  ( ( A ^ 2 )  /  ( E ^ 2 ) ) )
342341oveq1d 6101 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A  /  E
) ^ 2 )  x.  ( E ^
2 ) )  =  ( ( ( A ^ 2 )  / 
( E ^ 2 ) )  x.  ( E ^ 2 ) ) )
343220adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( A ^ 2 )  e.  CC )
344 sqne0 11924 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  CC  ->  (
( E ^ 2 )  =/=  0  <->  E  =/=  0 ) )
3454, 344syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( E ^
2 )  =/=  0  <->  E  =/=  0 ) )
346324, 345mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( E ^ 2 )  =/=  0 )
347346adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( E ^ 2 )  =/=  0 )
348343, 332, 347divcan1d 10100 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( A ^ 2 )  /  ( E ^ 2 ) )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
349337, 342, 3483eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( E ^
2 ) )  =  ( A ^ 2 ) )
3507adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  D  e.  CC )
35137adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  e.  CC )
352331, 350, 351mul12d 9570 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( D  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B  /  F
) ^ 2 )  x.  ( F ^
2 ) ) ) )
3539adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  B  e.  CC )
35411adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  e.  CC )
355323adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  F  =/=  0 )
356353, 354, 355sqdivd 12013 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( ( B  /  F ) ^
2 )  =  ( ( B ^ 2 )  /  ( F ^ 2 ) ) )
357356oveq1d 6101 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B  /  F
) ^ 2 )  x.  ( F ^
2 ) )  =  ( ( ( B ^ 2 )  / 
( F ^ 2 ) )  x.  ( F ^ 2 ) ) )
358357oveq2d 6102 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( D  x.  ( ( ( B  /  F ) ^
2 )  x.  ( F ^ 2 ) ) )  =  ( D  x.  ( ( ( B ^ 2 )  /  ( F ^
2 ) )  x.  ( F ^ 2 ) ) ) )
359207adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( B ^ 2 )  e.  CC )
360 sqne0 11924 . . . . . . . . . . . . . . . . . . . 20  |-  ( F  e.  CC  ->  (
( F ^ 2 )  =/=  0  <->  F  =/=  0 ) )
36111, 360syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( F ^
2 )  =/=  0  <->  F  =/=  0 ) )
362323, 361mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( F ^ 2 )  =/=  0 )
363362adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( F ^ 2 )  =/=  0 )
364359, 351, 363divcan1d 10100 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( B  /  F )  =  ( A  /  E ) )  ->  ( (
( B ^ 2 )  /  ( F ^ 2 ) )