Step |
Hyp |
Ref |
Expression |
1 |
|
pellex.ann |
|- ( ph -> A e. NN ) |
2 |
|
pellex.bnn |
|- ( ph -> B e. NN ) |
3 |
|
pellex.cz |
|- ( ph -> C e. ZZ ) |
4 |
|
pellex.dnn |
|- ( ph -> D e. NN ) |
5 |
|
pellex.irr |
|- ( ph -> -. ( sqrt ` D ) e. QQ ) |
6 |
|
pellex.enn |
|- ( ph -> E e. NN ) |
7 |
|
pellex.fnn |
|- ( ph -> F e. NN ) |
8 |
|
pellex.neq |
|- ( ph -> -. ( A = E /\ B = F ) ) |
9 |
|
pellex.cn0 |
|- ( ph -> C =/= 0 ) |
10 |
|
pellex.no1 |
|- ( ph -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = C ) |
11 |
|
pellex.no2 |
|- ( ph -> ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) = C ) |
12 |
|
pellex.xcg |
|- ( ph -> ( A mod ( abs ` C ) ) = ( E mod ( abs ` C ) ) ) |
13 |
|
pellex.ycg |
|- ( ph -> ( B mod ( abs ` C ) ) = ( F mod ( abs ` C ) ) ) |
14 |
1
|
nncnd |
|- ( ph -> A e. CC ) |
15 |
6
|
nncnd |
|- ( ph -> E e. CC ) |
16 |
14 15
|
mulcld |
|- ( ph -> ( A x. E ) e. CC ) |
17 |
4
|
nncnd |
|- ( ph -> D e. CC ) |
18 |
2
|
nncnd |
|- ( ph -> B e. CC ) |
19 |
7
|
nncnd |
|- ( ph -> F e. CC ) |
20 |
18 19
|
mulcld |
|- ( ph -> ( B x. F ) e. CC ) |
21 |
17 20
|
mulcld |
|- ( ph -> ( D x. ( B x. F ) ) e. CC ) |
22 |
16 21
|
subcld |
|- ( ph -> ( ( A x. E ) - ( D x. ( B x. F ) ) ) e. CC ) |
23 |
3
|
zcnd |
|- ( ph -> C e. CC ) |
24 |
22 23 9
|
absdivd |
|- ( ph -> ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) = ( ( abs ` ( ( A x. E ) - ( D x. ( B x. F ) ) ) ) / ( abs ` C ) ) ) |
25 |
16 21
|
negsubd |
|- ( ph -> ( ( A x. E ) + -u ( D x. ( B x. F ) ) ) = ( ( A x. E ) - ( D x. ( B x. F ) ) ) ) |
26 |
25
|
eqcomd |
|- ( ph -> ( ( A x. E ) - ( D x. ( B x. F ) ) ) = ( ( A x. E ) + -u ( D x. ( B x. F ) ) ) ) |
27 |
26
|
oveq1d |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) mod ( abs ` C ) ) = ( ( ( A x. E ) + -u ( D x. ( B x. F ) ) ) mod ( abs ` C ) ) ) |
28 |
1
|
nnred |
|- ( ph -> A e. RR ) |
29 |
6
|
nnred |
|- ( ph -> E e. RR ) |
30 |
28 29
|
remulcld |
|- ( ph -> ( A x. E ) e. RR ) |
31 |
4
|
nnred |
|- ( ph -> D e. RR ) |
32 |
2
|
nnred |
|- ( ph -> B e. RR ) |
33 |
7
|
nnred |
|- ( ph -> F e. RR ) |
34 |
32 33
|
remulcld |
|- ( ph -> ( B x. F ) e. RR ) |
35 |
31 34
|
remulcld |
|- ( ph -> ( D x. ( B x. F ) ) e. RR ) |
36 |
35
|
renegcld |
|- ( ph -> -u ( D x. ( B x. F ) ) e. RR ) |
37 |
23 9
|
absrpcld |
|- ( ph -> ( abs ` C ) e. RR+ ) |
38 |
6
|
nnzd |
|- ( ph -> E e. ZZ ) |
39 |
|
modmul1 |
|- ( ( ( 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 ) ) ) |
40 |
28 29 38 37 12 39
|
syl221anc |
|- ( ph -> ( ( A x. E ) mod ( abs ` C ) ) = ( ( E x. E ) mod ( abs ` C ) ) ) |
41 |
15
|
sqcld |
|- ( ph -> ( E ^ 2 ) e. CC ) |
42 |
19
|
sqcld |
|- ( ph -> ( F ^ 2 ) e. CC ) |
43 |
17 42
|
mulcld |
|- ( ph -> ( D x. ( F ^ 2 ) ) e. CC ) |
44 |
41 43
|
npcand |
|- ( ph -> ( ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) + ( D x. ( F ^ 2 ) ) ) = ( E ^ 2 ) ) |
45 |
15
|
sqvald |
|- ( ph -> ( E ^ 2 ) = ( E x. E ) ) |
46 |
44 45
|
eqtr2d |
|- ( ph -> ( E x. E ) = ( ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) + ( D x. ( F ^ 2 ) ) ) ) |
47 |
46
|
oveq1d |
|- ( ph -> ( ( E x. E ) mod ( abs ` C ) ) = ( ( ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) + ( D x. ( F ^ 2 ) ) ) mod ( abs ` C ) ) ) |
48 |
29
|
resqcld |
|- ( ph -> ( E ^ 2 ) e. RR ) |
49 |
33
|
resqcld |
|- ( ph -> ( F ^ 2 ) e. RR ) |
50 |
31 49
|
remulcld |
|- ( ph -> ( D x. ( F ^ 2 ) ) e. RR ) |
51 |
48 50
|
resubcld |
|- ( ph -> ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) e. RR ) |
52 |
|
0red |
|- ( ph -> 0 e. RR ) |
53 |
23
|
abscld |
|- ( ph -> ( abs ` C ) e. RR ) |
54 |
53
|
recnd |
|- ( ph -> ( abs ` C ) e. CC ) |
55 |
23 9
|
absne0d |
|- ( ph -> ( abs ` C ) =/= 0 ) |
56 |
54 55
|
dividd |
|- ( ph -> ( ( abs ` C ) / ( abs ` C ) ) = 1 ) |
57 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
58 |
56 57
|
eqeltrd |
|- ( ph -> ( ( abs ` C ) / ( abs ` C ) ) e. ZZ ) |
59 |
|
mod0 |
|- ( ( ( abs ` C ) e. RR /\ ( abs ` C ) e. RR+ ) -> ( ( ( abs ` C ) mod ( abs ` C ) ) = 0 <-> ( ( abs ` C ) / ( abs ` C ) ) e. ZZ ) ) |
60 |
53 37 59
|
syl2anc |
|- ( ph -> ( ( ( abs ` C ) mod ( abs ` C ) ) = 0 <-> ( ( abs ` C ) / ( abs ` C ) ) e. ZZ ) ) |
61 |
58 60
|
mpbird |
|- ( ph -> ( ( abs ` C ) mod ( abs ` C ) ) = 0 ) |
62 |
3
|
zred |
|- ( ph -> C e. RR ) |
63 |
|
absmod0 |
|- ( ( C e. RR /\ ( abs ` C ) e. RR+ ) -> ( ( C mod ( abs ` C ) ) = 0 <-> ( ( abs ` C ) mod ( abs ` C ) ) = 0 ) ) |
64 |
62 37 63
|
syl2anc |
|- ( ph -> ( ( C mod ( abs ` C ) ) = 0 <-> ( ( abs ` C ) mod ( abs ` C ) ) = 0 ) ) |
65 |
61 64
|
mpbird |
|- ( ph -> ( C mod ( abs ` C ) ) = 0 ) |
66 |
11
|
oveq1d |
|- ( ph -> ( ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) mod ( abs ` C ) ) = ( C mod ( abs ` C ) ) ) |
67 |
|
0mod |
|- ( ( abs ` C ) e. RR+ -> ( 0 mod ( abs ` C ) ) = 0 ) |
68 |
37 67
|
syl |
|- ( ph -> ( 0 mod ( abs ` C ) ) = 0 ) |
69 |
65 66 68
|
3eqtr4d |
|- ( ph -> ( ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) mod ( abs ` C ) ) = ( 0 mod ( abs ` C ) ) ) |
70 |
|
modadd1 |
|- ( ( ( ( ( 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 ) ) ) |
71 |
51 52 50 37 69 70
|
syl221anc |
|- ( ph -> ( ( ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) + ( D x. ( F ^ 2 ) ) ) mod ( abs ` C ) ) = ( ( 0 + ( D x. ( F ^ 2 ) ) ) mod ( abs ` C ) ) ) |
72 |
43
|
addid2d |
|- ( ph -> ( 0 + ( D x. ( F ^ 2 ) ) ) = ( D x. ( F ^ 2 ) ) ) |
73 |
19
|
sqvald |
|- ( ph -> ( F ^ 2 ) = ( F x. F ) ) |
74 |
73
|
oveq2d |
|- ( ph -> ( D x. ( F ^ 2 ) ) = ( D x. ( F x. F ) ) ) |
75 |
17 19 19
|
mul12d |
|- ( ph -> ( D x. ( F x. F ) ) = ( F x. ( D x. F ) ) ) |
76 |
72 74 75
|
3eqtrd |
|- ( ph -> ( 0 + ( D x. ( F ^ 2 ) ) ) = ( F x. ( D x. F ) ) ) |
77 |
76
|
oveq1d |
|- ( ph -> ( ( 0 + ( D x. ( F ^ 2 ) ) ) mod ( abs ` C ) ) = ( ( F x. ( D x. F ) ) mod ( abs ` C ) ) ) |
78 |
47 71 77
|
3eqtrd |
|- ( ph -> ( ( E x. E ) mod ( abs ` C ) ) = ( ( F x. ( D x. F ) ) mod ( abs ` C ) ) ) |
79 |
4
|
nnzd |
|- ( ph -> D e. ZZ ) |
80 |
7
|
nnzd |
|- ( ph -> F e. ZZ ) |
81 |
79 80
|
zmulcld |
|- ( ph -> ( D x. F ) e. ZZ ) |
82 |
13
|
eqcomd |
|- ( ph -> ( F mod ( abs ` C ) ) = ( B mod ( abs ` C ) ) ) |
83 |
|
modmul1 |
|- ( ( ( 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 ) ) ) |
84 |
33 32 81 37 82 83
|
syl221anc |
|- ( ph -> ( ( F x. ( D x. F ) ) mod ( abs ` C ) ) = ( ( B x. ( D x. F ) ) mod ( abs ` C ) ) ) |
85 |
18 17 19
|
mul12d |
|- ( ph -> ( B x. ( D x. F ) ) = ( D x. ( B x. F ) ) ) |
86 |
85
|
oveq1d |
|- ( ph -> ( ( B x. ( D x. F ) ) mod ( abs ` C ) ) = ( ( D x. ( B x. F ) ) mod ( abs ` C ) ) ) |
87 |
84 86
|
eqtrd |
|- ( ph -> ( ( F x. ( D x. F ) ) mod ( abs ` C ) ) = ( ( D x. ( B x. F ) ) mod ( abs ` C ) ) ) |
88 |
40 78 87
|
3eqtrd |
|- ( ph -> ( ( A x. E ) mod ( abs ` C ) ) = ( ( D x. ( B x. F ) ) mod ( abs ` C ) ) ) |
89 |
|
modadd1 |
|- ( ( ( ( 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 ) ) ) |
90 |
30 35 36 37 88 89
|
syl221anc |
|- ( 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 ) ) ) |
91 |
21
|
negidd |
|- ( ph -> ( ( D x. ( B x. F ) ) + -u ( D x. ( B x. F ) ) ) = 0 ) |
92 |
91
|
oveq1d |
|- ( ph -> ( ( ( D x. ( B x. F ) ) + -u ( D x. ( B x. F ) ) ) mod ( abs ` C ) ) = ( 0 mod ( abs ` C ) ) ) |
93 |
27 90 92
|
3eqtrd |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) mod ( abs ` C ) ) = ( 0 mod ( abs ` C ) ) ) |
94 |
93 68
|
eqtrd |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) mod ( abs ` C ) ) = 0 ) |
95 |
30 35
|
resubcld |
|- ( ph -> ( ( A x. E ) - ( D x. ( B x. F ) ) ) e. RR ) |
96 |
|
absmod0 |
|- ( ( ( ( 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 ) ) |
97 |
95 37 96
|
syl2anc |
|- ( 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 ) ) |
98 |
94 97
|
mpbid |
|- ( ph -> ( ( abs ` ( ( A x. E ) - ( D x. ( B x. F ) ) ) ) mod ( abs ` C ) ) = 0 ) |
99 |
22
|
abscld |
|- ( ph -> ( abs ` ( ( A x. E ) - ( D x. ( B x. F ) ) ) ) e. RR ) |
100 |
|
mod0 |
|- ( ( ( 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 ) ) |
101 |
99 37 100
|
syl2anc |
|- ( 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 ) ) |
102 |
98 101
|
mpbid |
|- ( ph -> ( ( abs ` ( ( A x. E ) - ( D x. ( B x. F ) ) ) ) / ( abs ` C ) ) e. ZZ ) |
103 |
24 102
|
eqeltrd |
|- ( ph -> ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) e. ZZ ) |
104 |
95 62 9
|
redivcld |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) e. RR ) |
105 |
|
absz |
|- ( ( ( ( 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 ) ) |
106 |
104 105
|
syl |
|- ( ph -> ( ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) e. ZZ <-> ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) e. ZZ ) ) |
107 |
103 106
|
mpbird |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) e. ZZ ) |
108 |
|
0lt1 |
|- 0 < 1 |
109 |
|
0re |
|- 0 e. RR |
110 |
|
1re |
|- 1 e. RR |
111 |
109 110
|
ltnlei |
|- ( 0 < 1 <-> -. 1 <_ 0 ) |
112 |
108 111
|
mpbi |
|- -. 1 <_ 0 |
113 |
18 15
|
mulcld |
|- ( ph -> ( B x. E ) e. CC ) |
114 |
14 19
|
mulcld |
|- ( ph -> ( A x. F ) e. CC ) |
115 |
113 114
|
subcld |
|- ( ph -> ( ( B x. E ) - ( A x. F ) ) e. CC ) |
116 |
115 23 9
|
divcld |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) / C ) e. CC ) |
117 |
116
|
abscld |
|- ( ph -> ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) e. RR ) |
118 |
117
|
resqcld |
|- ( ph -> ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) e. RR ) |
119 |
4
|
nnnn0d |
|- ( ph -> D e. NN0 ) |
120 |
119
|
nn0ge0d |
|- ( ph -> 0 <_ D ) |
121 |
117
|
sqge0d |
|- ( ph -> 0 <_ ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) |
122 |
31 118 120 121
|
mulge0d |
|- ( ph -> 0 <_ ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) |
123 |
31 118
|
remulcld |
|- ( ph -> ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) e. RR ) |
124 |
52 123
|
suble0d |
|- ( 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 ) ) ) ) |
125 |
122 124
|
mpbird |
|- ( ph -> ( 0 - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) <_ 0 ) |
126 |
|
breq1 |
|- ( 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 ) ) |
127 |
125 126
|
syl5ibrcom |
|- ( ph -> ( 1 = ( 0 - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) -> 1 <_ 0 ) ) |
128 |
112 127
|
mtoi |
|- ( ph -> -. 1 = ( 0 - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) ) |
129 |
|
absresq |
|- ( ( ( ( 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 ) ) |
130 |
104 129
|
syl |
|- ( ph -> ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) = ( ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ^ 2 ) ) |
131 |
22 23 9
|
sqdivd |
|- ( ph -> ( ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ^ 2 ) = ( ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) ^ 2 ) / ( C ^ 2 ) ) ) |
132 |
22
|
sqvald |
|- ( 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 ) ) ) ) ) |
133 |
132
|
oveq1d |
|- ( 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 ) ) ) |
134 |
130 131 133
|
3eqtrd |
|- ( 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 ) ) ) |
135 |
32 29
|
remulcld |
|- ( ph -> ( B x. E ) e. RR ) |
136 |
28 33
|
remulcld |
|- ( ph -> ( A x. F ) e. RR ) |
137 |
135 136
|
resubcld |
|- ( ph -> ( ( B x. E ) - ( A x. F ) ) e. RR ) |
138 |
137 62 9
|
redivcld |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) / C ) e. RR ) |
139 |
|
absresq |
|- ( ( ( ( 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 ) ) |
140 |
138 139
|
syl |
|- ( ph -> ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) = ( ( ( ( B x. E ) - ( A x. F ) ) / C ) ^ 2 ) ) |
141 |
115 23 9
|
sqdivd |
|- ( ph -> ( ( ( ( B x. E ) - ( A x. F ) ) / C ) ^ 2 ) = ( ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) / ( C ^ 2 ) ) ) |
142 |
140 141
|
eqtrd |
|- ( ph -> ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) = ( ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) / ( C ^ 2 ) ) ) |
143 |
142
|
oveq2d |
|- ( ph -> ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) = ( D x. ( ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) / ( C ^ 2 ) ) ) ) |
144 |
115
|
sqcld |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) e. CC ) |
145 |
23
|
sqcld |
|- ( ph -> ( C ^ 2 ) e. CC ) |
146 |
|
sqne0 |
|- ( C e. CC -> ( ( C ^ 2 ) =/= 0 <-> C =/= 0 ) ) |
147 |
23 146
|
syl |
|- ( ph -> ( ( C ^ 2 ) =/= 0 <-> C =/= 0 ) ) |
148 |
9 147
|
mpbird |
|- ( ph -> ( C ^ 2 ) =/= 0 ) |
149 |
17 144 145 148
|
divassd |
|- ( ph -> ( ( D x. ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) ) / ( C ^ 2 ) ) = ( D x. ( ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) / ( C ^ 2 ) ) ) ) |
150 |
115
|
sqvald |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) ^ 2 ) = ( ( ( B x. E ) - ( A x. F ) ) x. ( ( B x. E ) - ( A x. F ) ) ) ) |
151 |
150
|
oveq2d |
|- ( 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 ) ) ) ) ) |
152 |
151
|
oveq1d |
|- ( 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 ) ) ) |
153 |
143 149 152
|
3eqtr2d |
|- ( 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 ) ) ) |
154 |
134 153
|
oveq12d |
|- ( 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 ) ) ) ) |
155 |
22 22
|
mulcld |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) x. ( ( A x. E ) - ( D x. ( B x. F ) ) ) ) e. CC ) |
156 |
115 115
|
mulcld |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) x. ( ( B x. E ) - ( A x. F ) ) ) e. CC ) |
157 |
17 156
|
mulcld |
|- ( ph -> ( D x. ( ( ( B x. E ) - ( A x. F ) ) x. ( ( B x. E ) - ( A x. F ) ) ) ) e. CC ) |
158 |
155 157 145 148
|
divsubdird |
|- ( 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 ) ) ) ) |
159 |
16 21 16 21
|
mulsubd |
|- ( 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 ) ) ) ) ) ) |
160 |
113 114 113 114
|
mulsubd |
|- ( 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 ) ) ) ) ) |
161 |
160
|
oveq2d |
|- ( 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 ) ) ) ) ) ) |
162 |
113 113
|
mulcld |
|- ( ph -> ( ( B x. E ) x. ( B x. E ) ) e. CC ) |
163 |
114 114
|
mulcld |
|- ( ph -> ( ( A x. F ) x. ( A x. F ) ) e. CC ) |
164 |
162 163
|
addcld |
|- ( ph -> ( ( ( B x. E ) x. ( B x. E ) ) + ( ( A x. F ) x. ( A x. F ) ) ) e. CC ) |
165 |
113 114
|
mulcld |
|- ( ph -> ( ( B x. E ) x. ( A x. F ) ) e. CC ) |
166 |
165 165
|
addcld |
|- ( ph -> ( ( ( B x. E ) x. ( A x. F ) ) + ( ( B x. E ) x. ( A x. F ) ) ) e. CC ) |
167 |
17 164 166
|
subdid |
|- ( 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 ) ) ) ) ) ) |
168 |
17 162 163
|
adddid |
|- ( 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 ) ) ) ) ) |
169 |
17 165 165
|
adddid |
|- ( 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 ) ) ) ) ) |
170 |
168 169
|
oveq12d |
|- ( 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 ) ) ) ) ) ) |
171 |
161 167 170
|
3eqtrd |
|- ( 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 ) ) ) ) ) ) |
172 |
159 171
|
oveq12d |
|- ( 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 ) ) ) ) ) ) ) |
173 |
172
|
oveq1d |
|- ( 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 ) ) ) |
174 |
16 21
|
mulcomd |
|- ( ph -> ( ( A x. E ) x. ( D x. ( B x. F ) ) ) = ( ( D x. ( B x. F ) ) x. ( A x. E ) ) ) |
175 |
17 20 16
|
mulassd |
|- ( ph -> ( ( D x. ( B x. F ) ) x. ( A x. E ) ) = ( D x. ( ( B x. F ) x. ( A x. E ) ) ) ) |
176 |
14 15
|
mulcomd |
|- ( ph -> ( A x. E ) = ( E x. A ) ) |
177 |
176
|
oveq2d |
|- ( ph -> ( ( B x. F ) x. ( A x. E ) ) = ( ( B x. F ) x. ( E x. A ) ) ) |
178 |
18 19 15 14
|
mul4d |
|- ( ph -> ( ( B x. F ) x. ( E x. A ) ) = ( ( B x. E ) x. ( F x. A ) ) ) |
179 |
19 14
|
mulcomd |
|- ( ph -> ( F x. A ) = ( A x. F ) ) |
180 |
179
|
oveq2d |
|- ( ph -> ( ( B x. E ) x. ( F x. A ) ) = ( ( B x. E ) x. ( A x. F ) ) ) |
181 |
177 178 180
|
3eqtrd |
|- ( ph -> ( ( B x. F ) x. ( A x. E ) ) = ( ( B x. E ) x. ( A x. F ) ) ) |
182 |
181
|
oveq2d |
|- ( ph -> ( D x. ( ( B x. F ) x. ( A x. E ) ) ) = ( D x. ( ( B x. E ) x. ( A x. F ) ) ) ) |
183 |
174 175 182
|
3eqtrd |
|- ( ph -> ( ( A x. E ) x. ( D x. ( B x. F ) ) ) = ( D x. ( ( B x. E ) x. ( A x. F ) ) ) ) |
184 |
183 183
|
oveq12d |
|- ( 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 ) ) ) ) ) |
185 |
184
|
oveq2d |
|- ( 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 ) ) ) ) ) ) |
186 |
185
|
oveq1d |
|- ( 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 ) ) ) ) ) ) ) |
187 |
16 16
|
mulcld |
|- ( ph -> ( ( A x. E ) x. ( A x. E ) ) e. CC ) |
188 |
21 21
|
mulcld |
|- ( ph -> ( ( D x. ( B x. F ) ) x. ( D x. ( B x. F ) ) ) e. CC ) |
189 |
187 188
|
addcld |
|- ( ph -> ( ( ( A x. E ) x. ( A x. E ) ) + ( ( D x. ( B x. F ) ) x. ( D x. ( B x. F ) ) ) ) e. CC ) |
190 |
17 162
|
mulcld |
|- ( ph -> ( D x. ( ( B x. E ) x. ( B x. E ) ) ) e. CC ) |
191 |
17 163
|
mulcld |
|- ( ph -> ( D x. ( ( A x. F ) x. ( A x. F ) ) ) e. CC ) |
192 |
190 191
|
addcld |
|- ( ph -> ( ( D x. ( ( B x. E ) x. ( B x. E ) ) ) + ( D x. ( ( A x. F ) x. ( A x. F ) ) ) ) e. CC ) |
193 |
17 165
|
mulcld |
|- ( ph -> ( D x. ( ( B x. E ) x. ( A x. F ) ) ) e. CC ) |
194 |
193 193
|
addcld |
|- ( ph -> ( ( D x. ( ( B x. E ) x. ( A x. F ) ) ) + ( D x. ( ( B x. E ) x. ( A x. F ) ) ) ) e. CC ) |
195 |
189 192 194
|
nnncan2d |
|- ( 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 ) ) ) ) ) ) |
196 |
187 188 190 191
|
addsub4d |
|- ( 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 ) ) ) ) ) ) |
197 |
16
|
sqvald |
|- ( ph -> ( ( A x. E ) ^ 2 ) = ( ( A x. E ) x. ( A x. E ) ) ) |
198 |
113
|
sqvald |
|- ( ph -> ( ( B x. E ) ^ 2 ) = ( ( B x. E ) x. ( B x. E ) ) ) |
199 |
198
|
oveq2d |
|- ( ph -> ( D x. ( ( B x. E ) ^ 2 ) ) = ( D x. ( ( B x. E ) x. ( B x. E ) ) ) ) |
200 |
197 199
|
oveq12d |
|- ( 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 ) ) ) ) ) |
201 |
21
|
sqvald |
|- ( ph -> ( ( D x. ( B x. F ) ) ^ 2 ) = ( ( D x. ( B x. F ) ) x. ( D x. ( B x. F ) ) ) ) |
202 |
114
|
sqvald |
|- ( ph -> ( ( A x. F ) ^ 2 ) = ( ( A x. F ) x. ( A x. F ) ) ) |
203 |
202
|
oveq2d |
|- ( ph -> ( D x. ( ( A x. F ) ^ 2 ) ) = ( D x. ( ( A x. F ) x. ( A x. F ) ) ) ) |
204 |
201 203
|
oveq12d |
|- ( 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 ) ) ) ) ) |
205 |
200 204
|
oveq12d |
|- ( 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 ) ) ) ) ) ) |
206 |
14 15
|
sqmuld |
|- ( ph -> ( ( A x. E ) ^ 2 ) = ( ( A ^ 2 ) x. ( E ^ 2 ) ) ) |
207 |
18 15
|
sqmuld |
|- ( ph -> ( ( B x. E ) ^ 2 ) = ( ( B ^ 2 ) x. ( E ^ 2 ) ) ) |
208 |
207
|
oveq2d |
|- ( ph -> ( D x. ( ( B x. E ) ^ 2 ) ) = ( D x. ( ( B ^ 2 ) x. ( E ^ 2 ) ) ) ) |
209 |
18
|
sqcld |
|- ( ph -> ( B ^ 2 ) e. CC ) |
210 |
17 209 41
|
mulassd |
|- ( ph -> ( ( D x. ( B ^ 2 ) ) x. ( E ^ 2 ) ) = ( D x. ( ( B ^ 2 ) x. ( E ^ 2 ) ) ) ) |
211 |
208 210
|
eqtr4d |
|- ( ph -> ( D x. ( ( B x. E ) ^ 2 ) ) = ( ( D x. ( B ^ 2 ) ) x. ( E ^ 2 ) ) ) |
212 |
206 211
|
oveq12d |
|- ( ph -> ( ( ( A x. E ) ^ 2 ) - ( D x. ( ( B x. E ) ^ 2 ) ) ) = ( ( ( A ^ 2 ) x. ( E ^ 2 ) ) - ( ( D x. ( B ^ 2 ) ) x. ( E ^ 2 ) ) ) ) |
213 |
17
|
sqvald |
|- ( ph -> ( D ^ 2 ) = ( D x. D ) ) |
214 |
18 19
|
sqmuld |
|- ( ph -> ( ( B x. F ) ^ 2 ) = ( ( B ^ 2 ) x. ( F ^ 2 ) ) ) |
215 |
213 214
|
oveq12d |
|- ( ph -> ( ( D ^ 2 ) x. ( ( B x. F ) ^ 2 ) ) = ( ( D x. D ) x. ( ( B ^ 2 ) x. ( F ^ 2 ) ) ) ) |
216 |
17 20
|
sqmuld |
|- ( ph -> ( ( D x. ( B x. F ) ) ^ 2 ) = ( ( D ^ 2 ) x. ( ( B x. F ) ^ 2 ) ) ) |
217 |
17 17
|
mulcld |
|- ( ph -> ( D x. D ) e. CC ) |
218 |
217 209 42
|
mulassd |
|- ( ph -> ( ( ( D x. D ) x. ( B ^ 2 ) ) x. ( F ^ 2 ) ) = ( ( D x. D ) x. ( ( B ^ 2 ) x. ( F ^ 2 ) ) ) ) |
219 |
215 216 218
|
3eqtr4d |
|- ( ph -> ( ( D x. ( B x. F ) ) ^ 2 ) = ( ( ( D x. D ) x. ( B ^ 2 ) ) x. ( F ^ 2 ) ) ) |
220 |
14 19
|
sqmuld |
|- ( ph -> ( ( A x. F ) ^ 2 ) = ( ( A ^ 2 ) x. ( F ^ 2 ) ) ) |
221 |
220
|
oveq2d |
|- ( ph -> ( D x. ( ( A x. F ) ^ 2 ) ) = ( D x. ( ( A ^ 2 ) x. ( F ^ 2 ) ) ) ) |
222 |
14
|
sqcld |
|- ( ph -> ( A ^ 2 ) e. CC ) |
223 |
17 222 42
|
mulassd |
|- ( ph -> ( ( D x. ( A ^ 2 ) ) x. ( F ^ 2 ) ) = ( D x. ( ( A ^ 2 ) x. ( F ^ 2 ) ) ) ) |
224 |
221 223
|
eqtr4d |
|- ( ph -> ( D x. ( ( A x. F ) ^ 2 ) ) = ( ( D x. ( A ^ 2 ) ) x. ( F ^ 2 ) ) ) |
225 |
219 224
|
oveq12d |
|- ( 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 ) ) ) ) |
226 |
212 225
|
oveq12d |
|- ( 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 ) ) ) ) ) |
227 |
17 209
|
mulcld |
|- ( ph -> ( D x. ( B ^ 2 ) ) e. CC ) |
228 |
222 227 41
|
subdird |
|- ( ph -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) x. ( E ^ 2 ) ) = ( ( ( A ^ 2 ) x. ( E ^ 2 ) ) - ( ( D x. ( B ^ 2 ) ) x. ( E ^ 2 ) ) ) ) |
229 |
10
|
oveq1d |
|- ( ph -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) x. ( E ^ 2 ) ) = ( C x. ( E ^ 2 ) ) ) |
230 |
228 229
|
eqtr3d |
|- ( ph -> ( ( ( A ^ 2 ) x. ( E ^ 2 ) ) - ( ( D x. ( B ^ 2 ) ) x. ( E ^ 2 ) ) ) = ( C x. ( E ^ 2 ) ) ) |
231 |
17 17 209
|
mulassd |
|- ( ph -> ( ( D x. D ) x. ( B ^ 2 ) ) = ( D x. ( D x. ( B ^ 2 ) ) ) ) |
232 |
231
|
oveq1d |
|- ( ph -> ( ( ( D x. D ) x. ( B ^ 2 ) ) - ( D x. ( A ^ 2 ) ) ) = ( ( D x. ( D x. ( B ^ 2 ) ) ) - ( D x. ( A ^ 2 ) ) ) ) |
233 |
232
|
oveq1d |
|- ( 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 ) ) ) |
234 |
217 209
|
mulcld |
|- ( ph -> ( ( D x. D ) x. ( B ^ 2 ) ) e. CC ) |
235 |
17 222
|
mulcld |
|- ( ph -> ( D x. ( A ^ 2 ) ) e. CC ) |
236 |
234 235 42
|
subdird |
|- ( 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 ) ) ) ) |
237 |
|
subdi |
|- ( ( 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 ) ) ) ) |
238 |
237
|
eqcomd |
|- ( ( 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 ) ) ) ) |
239 |
17 227 222 238
|
syl3anc |
|- ( ph -> ( ( D x. ( D x. ( B ^ 2 ) ) ) - ( D x. ( A ^ 2 ) ) ) = ( D x. ( ( D x. ( B ^ 2 ) ) - ( A ^ 2 ) ) ) ) |
240 |
|
negsubdi2 |
|- ( ( ( A ^ 2 ) e. CC /\ ( D x. ( B ^ 2 ) ) e. CC ) -> -u ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = ( ( D x. ( B ^ 2 ) ) - ( A ^ 2 ) ) ) |
241 |
240
|
eqcomd |
|- ( ( ( A ^ 2 ) e. CC /\ ( D x. ( B ^ 2 ) ) e. CC ) -> ( ( D x. ( B ^ 2 ) ) - ( A ^ 2 ) ) = -u ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) |
242 |
222 227 241
|
syl2anc |
|- ( ph -> ( ( D x. ( B ^ 2 ) ) - ( A ^ 2 ) ) = -u ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) |
243 |
10
|
negeqd |
|- ( ph -> -u ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = -u C ) |
244 |
242 243
|
eqtrd |
|- ( ph -> ( ( D x. ( B ^ 2 ) ) - ( A ^ 2 ) ) = -u C ) |
245 |
244
|
oveq2d |
|- ( ph -> ( D x. ( ( D x. ( B ^ 2 ) ) - ( A ^ 2 ) ) ) = ( D x. -u C ) ) |
246 |
17 23
|
mulneg2d |
|- ( ph -> ( D x. -u C ) = -u ( D x. C ) ) |
247 |
239 245 246
|
3eqtrd |
|- ( ph -> ( ( D x. ( D x. ( B ^ 2 ) ) ) - ( D x. ( A ^ 2 ) ) ) = -u ( D x. C ) ) |
248 |
247
|
oveq1d |
|- ( ph -> ( ( ( D x. ( D x. ( B ^ 2 ) ) ) - ( D x. ( A ^ 2 ) ) ) x. ( F ^ 2 ) ) = ( -u ( D x. C ) x. ( F ^ 2 ) ) ) |
249 |
233 236 248
|
3eqtr3d |
|- ( ph -> ( ( ( ( D x. D ) x. ( B ^ 2 ) ) x. ( F ^ 2 ) ) - ( ( D x. ( A ^ 2 ) ) x. ( F ^ 2 ) ) ) = ( -u ( D x. C ) x. ( F ^ 2 ) ) ) |
250 |
230 249
|
oveq12d |
|- ( 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 ) ) ) ) |
251 |
17 23
|
mulcld |
|- ( ph -> ( D x. C ) e. CC ) |
252 |
251 42
|
mulneg1d |
|- ( ph -> ( -u ( D x. C ) x. ( F ^ 2 ) ) = -u ( ( D x. C ) x. ( F ^ 2 ) ) ) |
253 |
17 23
|
mulcomd |
|- ( ph -> ( D x. C ) = ( C x. D ) ) |
254 |
253
|
oveq1d |
|- ( ph -> ( ( D x. C ) x. ( F ^ 2 ) ) = ( ( C x. D ) x. ( F ^ 2 ) ) ) |
255 |
23 17 42
|
mulassd |
|- ( ph -> ( ( C x. D ) x. ( F ^ 2 ) ) = ( C x. ( D x. ( F ^ 2 ) ) ) ) |
256 |
254 255
|
eqtrd |
|- ( ph -> ( ( D x. C ) x. ( F ^ 2 ) ) = ( C x. ( D x. ( F ^ 2 ) ) ) ) |
257 |
256
|
negeqd |
|- ( ph -> -u ( ( D x. C ) x. ( F ^ 2 ) ) = -u ( C x. ( D x. ( F ^ 2 ) ) ) ) |
258 |
252 257
|
eqtrd |
|- ( ph -> ( -u ( D x. C ) x. ( F ^ 2 ) ) = -u ( C x. ( D x. ( F ^ 2 ) ) ) ) |
259 |
258
|
oveq2d |
|- ( ph -> ( ( C x. ( E ^ 2 ) ) + ( -u ( D x. C ) x. ( F ^ 2 ) ) ) = ( ( C x. ( E ^ 2 ) ) + -u ( C x. ( D x. ( F ^ 2 ) ) ) ) ) |
260 |
23 41
|
mulcld |
|- ( ph -> ( C x. ( E ^ 2 ) ) e. CC ) |
261 |
23 43
|
mulcld |
|- ( ph -> ( C x. ( D x. ( F ^ 2 ) ) ) e. CC ) |
262 |
260 261
|
negsubd |
|- ( ph -> ( ( C x. ( E ^ 2 ) ) + -u ( C x. ( D x. ( F ^ 2 ) ) ) ) = ( ( C x. ( E ^ 2 ) ) - ( C x. ( D x. ( F ^ 2 ) ) ) ) ) |
263 |
11
|
oveq2d |
|- ( ph -> ( C x. ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) ) = ( C x. C ) ) |
264 |
|
subdi |
|- ( ( 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 ) ) ) ) ) |
265 |
264
|
eqcomd |
|- ( ( 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 ) ) ) ) ) |
266 |
23 41 43 265
|
syl3anc |
|- ( ph -> ( ( C x. ( E ^ 2 ) ) - ( C x. ( D x. ( F ^ 2 ) ) ) ) = ( C x. ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) ) ) |
267 |
23
|
sqvald |
|- ( ph -> ( C ^ 2 ) = ( C x. C ) ) |
268 |
263 266 267
|
3eqtr4d |
|- ( ph -> ( ( C x. ( E ^ 2 ) ) - ( C x. ( D x. ( F ^ 2 ) ) ) ) = ( C ^ 2 ) ) |
269 |
259 262 268
|
3eqtrd |
|- ( ph -> ( ( C x. ( E ^ 2 ) ) + ( -u ( D x. C ) x. ( F ^ 2 ) ) ) = ( C ^ 2 ) ) |
270 |
226 250 269
|
3eqtrd |
|- ( 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 ) ) |
271 |
196 205 270
|
3eqtr2d |
|- ( 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 ) ) |
272 |
186 195 271
|
3eqtrd |
|- ( 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 ) ) |
273 |
272
|
oveq1d |
|- ( 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 ) ) ) |
274 |
145 148
|
dividd |
|- ( ph -> ( ( C ^ 2 ) / ( C ^ 2 ) ) = 1 ) |
275 |
173 273 274
|
3eqtrd |
|- ( 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 ) |
276 |
154 158 275
|
3eqtr2d |
|- ( ph -> ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) = 1 ) |
277 |
276
|
adantr |
|- ( ( 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 ) |
278 |
|
simpr |
|- ( ( ph /\ ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) -> ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) |
279 |
278
|
fvoveq1d |
|- ( ( ph /\ ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) -> ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) = ( abs ` ( 0 / C ) ) ) |
280 |
23 9
|
div0d |
|- ( ph -> ( 0 / C ) = 0 ) |
281 |
280
|
abs00bd |
|- ( ph -> ( abs ` ( 0 / C ) ) = 0 ) |
282 |
281
|
adantr |
|- ( ( ph /\ ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) -> ( abs ` ( 0 / C ) ) = 0 ) |
283 |
279 282
|
eqtrd |
|- ( ( ph /\ ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) -> ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) = 0 ) |
284 |
283
|
sq0id |
|- ( ( ph /\ ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) -> ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) = 0 ) |
285 |
284
|
oveq1d |
|- ( ( 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 ) ) ) ) |
286 |
277 285
|
eqtr3d |
|- ( ( ph /\ ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) -> 1 = ( 0 - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) ) |
287 |
128 286
|
mtand |
|- ( ph -> -. ( ( A x. E ) - ( D x. ( B x. F ) ) ) = 0 ) |
288 |
287
|
neqned |
|- ( ph -> ( ( A x. E ) - ( D x. ( B x. F ) ) ) =/= 0 ) |
289 |
22 23 288 9
|
divne0d |
|- ( ph -> ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) =/= 0 ) |
290 |
|
nnabscl |
|- ( ( ( ( ( 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 ) |
291 |
107 289 290
|
syl2anc |
|- ( ph -> ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) e. NN ) |
292 |
115 23 9
|
absdivd |
|- ( ph -> ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) = ( ( abs ` ( ( B x. E ) - ( A x. F ) ) ) / ( abs ` C ) ) ) |
293 |
|
negsub |
|- ( ( ( B x. E ) e. CC /\ ( A x. F ) e. CC ) -> ( ( B x. E ) + -u ( A x. F ) ) = ( ( B x. E ) - ( A x. F ) ) ) |
294 |
293
|
eqcomd |
|- ( ( ( B x. E ) e. CC /\ ( A x. F ) e. CC ) -> ( ( B x. E ) - ( A x. F ) ) = ( ( B x. E ) + -u ( A x. F ) ) ) |
295 |
113 114 294
|
syl2anc |
|- ( ph -> ( ( B x. E ) - ( A x. F ) ) = ( ( B x. E ) + -u ( A x. F ) ) ) |
296 |
295
|
oveq1d |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) mod ( abs ` C ) ) = ( ( ( B x. E ) + -u ( A x. F ) ) mod ( abs ` C ) ) ) |
297 |
136
|
renegcld |
|- ( ph -> -u ( A x. F ) e. RR ) |
298 |
19 15
|
mulcomd |
|- ( ph -> ( F x. E ) = ( E x. F ) ) |
299 |
298
|
oveq1d |
|- ( ph -> ( ( F x. E ) mod ( abs ` C ) ) = ( ( E x. F ) mod ( abs ` C ) ) ) |
300 |
|
modmul1 |
|- ( ( ( 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 ) ) ) |
301 |
32 33 38 37 13 300
|
syl221anc |
|- ( ph -> ( ( B x. E ) mod ( abs ` C ) ) = ( ( F x. E ) mod ( abs ` C ) ) ) |
302 |
|
modmul1 |
|- ( ( ( 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 ) ) ) |
303 |
28 29 80 37 12 302
|
syl221anc |
|- ( ph -> ( ( A x. F ) mod ( abs ` C ) ) = ( ( E x. F ) mod ( abs ` C ) ) ) |
304 |
299 301 303
|
3eqtr4d |
|- ( ph -> ( ( B x. E ) mod ( abs ` C ) ) = ( ( A x. F ) mod ( abs ` C ) ) ) |
305 |
|
modadd1 |
|- ( ( ( ( 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 ) ) ) |
306 |
135 136 297 37 304 305
|
syl221anc |
|- ( ph -> ( ( ( B x. E ) + -u ( A x. F ) ) mod ( abs ` C ) ) = ( ( ( A x. F ) + -u ( A x. F ) ) mod ( abs ` C ) ) ) |
307 |
114
|
negidd |
|- ( ph -> ( ( A x. F ) + -u ( A x. F ) ) = 0 ) |
308 |
307
|
oveq1d |
|- ( ph -> ( ( ( A x. F ) + -u ( A x. F ) ) mod ( abs ` C ) ) = ( 0 mod ( abs ` C ) ) ) |
309 |
296 306 308
|
3eqtrd |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) mod ( abs ` C ) ) = ( 0 mod ( abs ` C ) ) ) |
310 |
309 68
|
eqtrd |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) mod ( abs ` C ) ) = 0 ) |
311 |
|
absmod0 |
|- ( ( ( ( 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 ) ) |
312 |
137 37 311
|
syl2anc |
|- ( ph -> ( ( ( ( B x. E ) - ( A x. F ) ) mod ( abs ` C ) ) = 0 <-> ( ( abs ` ( ( B x. E ) - ( A x. F ) ) ) mod ( abs ` C ) ) = 0 ) ) |
313 |
310 312
|
mpbid |
|- ( ph -> ( ( abs ` ( ( B x. E ) - ( A x. F ) ) ) mod ( abs ` C ) ) = 0 ) |
314 |
115
|
abscld |
|- ( ph -> ( abs ` ( ( B x. E ) - ( A x. F ) ) ) e. RR ) |
315 |
|
mod0 |
|- ( ( ( 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 ) ) |
316 |
314 37 315
|
syl2anc |
|- ( ph -> ( ( ( abs ` ( ( B x. E ) - ( A x. F ) ) ) mod ( abs ` C ) ) = 0 <-> ( ( abs ` ( ( B x. E ) - ( A x. F ) ) ) / ( abs ` C ) ) e. ZZ ) ) |
317 |
313 316
|
mpbid |
|- ( ph -> ( ( abs ` ( ( B x. E ) - ( A x. F ) ) ) / ( abs ` C ) ) e. ZZ ) |
318 |
292 317
|
eqeltrd |
|- ( ph -> ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) e. ZZ ) |
319 |
|
absz |
|- ( ( ( ( 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 ) ) |
320 |
138 319
|
syl |
|- ( ph -> ( ( ( ( B x. E ) - ( A x. F ) ) / C ) e. ZZ <-> ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) e. ZZ ) ) |
321 |
318 320
|
mpbird |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) / C ) e. ZZ ) |
322 |
7
|
nnne0d |
|- ( ph -> F =/= 0 ) |
323 |
6
|
nnne0d |
|- ( ph -> E =/= 0 ) |
324 |
18 19 14 15 322 323
|
divmuleqd |
|- ( ph -> ( ( B / F ) = ( A / E ) <-> ( B x. E ) = ( A x. F ) ) ) |
325 |
11
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) = C ) |
326 |
325
|
eqcomd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> C = ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) ) |
327 |
326
|
oveq2d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. C ) = ( ( ( B / F ) ^ 2 ) x. ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) ) ) |
328 |
18 19 322
|
divcld |
|- ( ph -> ( B / F ) e. CC ) |
329 |
328
|
sqcld |
|- ( ph -> ( ( B / F ) ^ 2 ) e. CC ) |
330 |
329
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( B / F ) ^ 2 ) e. CC ) |
331 |
41
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( E ^ 2 ) e. CC ) |
332 |
43
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( D x. ( F ^ 2 ) ) e. CC ) |
333 |
330 331 332
|
subdid |
|- ( ( 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 |
|- ( ( B / F ) = ( A / E ) -> ( ( B / F ) ^ 2 ) = ( ( A / E ) ^ 2 ) ) |
335 |
334
|
oveq1d |
|- ( ( B / F ) = ( A / E ) -> ( ( ( B / F ) ^ 2 ) x. ( E ^ 2 ) ) = ( ( ( A / E ) ^ 2 ) x. ( E ^ 2 ) ) ) |
336 |
335
|
adantl |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. ( E ^ 2 ) ) = ( ( ( A / E ) ^ 2 ) x. ( E ^ 2 ) ) ) |
337 |
14
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> A e. CC ) |
338 |
15
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> E e. CC ) |
339 |
323
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> E =/= 0 ) |
340 |
337 338 339
|
sqdivd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( A / E ) ^ 2 ) = ( ( A ^ 2 ) / ( E ^ 2 ) ) ) |
341 |
340
|
oveq1d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( A / E ) ^ 2 ) x. ( E ^ 2 ) ) = ( ( ( A ^ 2 ) / ( E ^ 2 ) ) x. ( E ^ 2 ) ) ) |
342 |
222
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( A ^ 2 ) e. CC ) |
343 |
|
sqne0 |
|- ( E e. CC -> ( ( E ^ 2 ) =/= 0 <-> E =/= 0 ) ) |
344 |
15 343
|
syl |
|- ( ph -> ( ( E ^ 2 ) =/= 0 <-> E =/= 0 ) ) |
345 |
323 344
|
mpbird |
|- ( ph -> ( E ^ 2 ) =/= 0 ) |
346 |
345
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( E ^ 2 ) =/= 0 ) |
347 |
342 331 346
|
divcan1d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( A ^ 2 ) / ( E ^ 2 ) ) x. ( E ^ 2 ) ) = ( A ^ 2 ) ) |
348 |
336 341 347
|
3eqtrd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. ( E ^ 2 ) ) = ( A ^ 2 ) ) |
349 |
17
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> D e. CC ) |
350 |
42
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( F ^ 2 ) e. CC ) |
351 |
330 349 350
|
mul12d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. ( D x. ( F ^ 2 ) ) ) = ( D x. ( ( ( B / F ) ^ 2 ) x. ( F ^ 2 ) ) ) ) |
352 |
18
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> B e. CC ) |
353 |
19
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> F e. CC ) |
354 |
322
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> F =/= 0 ) |
355 |
352 353 354
|
sqdivd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( B / F ) ^ 2 ) = ( ( B ^ 2 ) / ( F ^ 2 ) ) ) |
356 |
355
|
oveq1d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. ( F ^ 2 ) ) = ( ( ( B ^ 2 ) / ( F ^ 2 ) ) x. ( F ^ 2 ) ) ) |
357 |
356
|
oveq2d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( D x. ( ( ( B / F ) ^ 2 ) x. ( F ^ 2 ) ) ) = ( D x. ( ( ( B ^ 2 ) / ( F ^ 2 ) ) x. ( F ^ 2 ) ) ) ) |
358 |
209
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( B ^ 2 ) e. CC ) |
359 |
|
sqne0 |
|- ( F e. CC -> ( ( F ^ 2 ) =/= 0 <-> F =/= 0 ) ) |
360 |
19 359
|
syl |
|- ( ph -> ( ( F ^ 2 ) =/= 0 <-> F =/= 0 ) ) |
361 |
322 360
|
mpbird |
|- ( ph -> ( F ^ 2 ) =/= 0 ) |
362 |
361
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( F ^ 2 ) =/= 0 ) |
363 |
358 350 362
|
divcan1d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B ^ 2 ) / ( F ^ 2 ) ) x. ( F ^ 2 ) ) = ( B ^ 2 ) ) |
364 |
363
|
oveq2d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( D x. ( ( ( B ^ 2 ) / ( F ^ 2 ) ) x. ( F ^ 2 ) ) ) = ( D x. ( B ^ 2 ) ) ) |
365 |
351 357 364
|
3eqtrd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. ( D x. ( F ^ 2 ) ) ) = ( D x. ( B ^ 2 ) ) ) |
366 |
348 365
|
oveq12d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( ( B / F ) ^ 2 ) x. ( E ^ 2 ) ) - ( ( ( B / F ) ^ 2 ) x. ( D x. ( F ^ 2 ) ) ) ) = ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) |
367 |
327 333 366
|
3eqtrd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) x. C ) = ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) |
368 |
10
|
eqcomd |
|- ( ph -> C = ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) |
369 |
368
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> C = ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) |
370 |
367 369
|
oveq12d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( ( B / F ) ^ 2 ) x. C ) / C ) = ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) / ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) ) |
371 |
23
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> C e. CC ) |
372 |
9
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> C =/= 0 ) |
373 |
330 371 372
|
divcan4d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( ( B / F ) ^ 2 ) x. C ) / C ) = ( ( B / F ) ^ 2 ) ) |
374 |
10 10
|
oveq12d |
|- ( ph -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) / ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) = ( C / C ) ) |
375 |
23 9
|
dividd |
|- ( ph -> ( C / C ) = 1 ) |
376 |
374 375
|
eqtrd |
|- ( ph -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) / ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) = 1 ) |
377 |
376
|
adantr |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) / ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) = 1 ) |
378 |
370 373 377
|
3eqtr3d |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( B / F ) ^ 2 ) = 1 ) |
379 |
32 33 322
|
redivcld |
|- ( ph -> ( B / F ) e. RR ) |
380 |
2
|
nnnn0d |
|- ( ph -> B e. NN0 ) |
381 |
380
|
nn0ge0d |
|- ( ph -> 0 <_ B ) |
382 |
7
|
nngt0d |
|- ( ph -> 0 < F ) |
383 |
|
divge0 |
|- ( ( ( B e. RR /\ 0 <_ B ) /\ ( F e. RR /\ 0 < F ) ) -> 0 <_ ( B / F ) ) |
384 |
32 381 33 382 383
|
syl22anc |
|- ( ph -> 0 <_ ( B / F ) ) |
385 |
379 384
|
sqrtsqd |
|- ( ph -> ( sqrt ` ( ( B / F ) ^ 2 ) ) = ( B / F ) ) |
386 |
385
|
eqcomd |
|- ( ph -> ( B / F ) = ( sqrt ` ( ( B / F ) ^ 2 ) ) ) |
387 |
386
|
ad2antrr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( ( B / F ) ^ 2 ) = 1 ) -> ( B / F ) = ( sqrt ` ( ( B / F ) ^ 2 ) ) ) |
388 |
|
fveq2 |
|- ( ( ( B / F ) ^ 2 ) = 1 -> ( sqrt ` ( ( B / F ) ^ 2 ) ) = ( sqrt ` 1 ) ) |
389 |
388
|
adantl |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( ( B / F ) ^ 2 ) = 1 ) -> ( sqrt ` ( ( B / F ) ^ 2 ) ) = ( sqrt ` 1 ) ) |
390 |
|
sqrt1 |
|- ( sqrt ` 1 ) = 1 |
391 |
390
|
a1i |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( ( B / F ) ^ 2 ) = 1 ) -> ( sqrt ` 1 ) = 1 ) |
392 |
387 389 391
|
3eqtrd |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( ( B / F ) ^ 2 ) = 1 ) -> ( B / F ) = 1 ) |
393 |
392
|
ex |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) = 1 -> ( B / F ) = 1 ) ) |
394 |
|
simplr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( B / F ) = ( A / E ) ) |
395 |
|
simpr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( B / F ) = 1 ) |
396 |
394 395
|
eqtr3d |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( A / E ) = 1 ) |
397 |
396
|
oveq1d |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( ( A / E ) x. E ) = ( 1 x. E ) ) |
398 |
14 15 323
|
divcan1d |
|- ( ph -> ( ( A / E ) x. E ) = A ) |
399 |
398
|
ad2antrr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( ( A / E ) x. E ) = A ) |
400 |
15
|
mulid2d |
|- ( ph -> ( 1 x. E ) = E ) |
401 |
400
|
ad2antrr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( 1 x. E ) = E ) |
402 |
397 399 401
|
3eqtr3d |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> A = E ) |
403 |
395
|
oveq1d |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( ( B / F ) x. F ) = ( 1 x. F ) ) |
404 |
18 19 322
|
divcan1d |
|- ( ph -> ( ( B / F ) x. F ) = B ) |
405 |
404
|
ad2antrr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( ( B / F ) x. F ) = B ) |
406 |
19
|
mulid2d |
|- ( ph -> ( 1 x. F ) = F ) |
407 |
406
|
ad2antrr |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( 1 x. F ) = F ) |
408 |
403 405 407
|
3eqtr3d |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> B = F ) |
409 |
402 408
|
jca |
|- ( ( ( ph /\ ( B / F ) = ( A / E ) ) /\ ( B / F ) = 1 ) -> ( A = E /\ B = F ) ) |
410 |
409
|
ex |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( B / F ) = 1 -> ( A = E /\ B = F ) ) ) |
411 |
393 410
|
syld |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( ( ( B / F ) ^ 2 ) = 1 -> ( A = E /\ B = F ) ) ) |
412 |
378 411
|
mpd |
|- ( ( ph /\ ( B / F ) = ( A / E ) ) -> ( A = E /\ B = F ) ) |
413 |
412
|
ex |
|- ( ph -> ( ( B / F ) = ( A / E ) -> ( A = E /\ B = F ) ) ) |
414 |
324 413
|
sylbird |
|- ( ph -> ( ( B x. E ) = ( A x. F ) -> ( A = E /\ B = F ) ) ) |
415 |
8 414
|
mtod |
|- ( ph -> -. ( B x. E ) = ( A x. F ) ) |
416 |
415
|
neqned |
|- ( ph -> ( B x. E ) =/= ( A x. F ) ) |
417 |
113 114 416
|
subne0d |
|- ( ph -> ( ( B x. E ) - ( A x. F ) ) =/= 0 ) |
418 |
115 23 417 9
|
divne0d |
|- ( ph -> ( ( ( B x. E ) - ( A x. F ) ) / C ) =/= 0 ) |
419 |
|
nnabscl |
|- ( ( ( ( ( B x. E ) - ( A x. F ) ) / C ) e. ZZ /\ ( ( ( B x. E ) - ( A x. F ) ) / C ) =/= 0 ) -> ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) e. NN ) |
420 |
321 418 419
|
syl2anc |
|- ( ph -> ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) e. NN ) |
421 |
|
oveq1 |
|- ( a = ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) -> ( a ^ 2 ) = ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) ) |
422 |
421
|
oveq1d |
|- ( a = ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) -> ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( b ^ 2 ) ) ) ) |
423 |
422
|
eqeq1d |
|- ( a = ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) -> ( ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) ) |
424 |
|
oveq1 |
|- ( b = ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) -> ( b ^ 2 ) = ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) |
425 |
424
|
oveq2d |
|- ( b = ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) -> ( D x. ( b ^ 2 ) ) = ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) |
426 |
425
|
oveq2d |
|- ( b = ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) -> ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) ) |
427 |
426
|
eqeq1d |
|- ( b = ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) -> ( ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 <-> ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) = 1 ) ) |
428 |
423 427
|
rspc2ev |
|- ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) e. NN /\ ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) e. NN /\ ( ( ( abs ` ( ( ( A x. E ) - ( D x. ( B x. F ) ) ) / C ) ) ^ 2 ) - ( D x. ( ( abs ` ( ( ( B x. E ) - ( A x. F ) ) / C ) ) ^ 2 ) ) ) = 1 ) -> E. a e. NN E. b e. NN ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) |
429 |
291 420 276 428
|
syl3anc |
|- ( ph -> E. a e. NN E. b e. NN ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 ) |