| Step |
Hyp |
Ref |
Expression |
| 1 |
|
modadd12d.1 |
|- ( ph -> A e. RR ) |
| 2 |
|
modadd12d.2 |
|- ( ph -> B e. RR ) |
| 3 |
|
modadd12d.3 |
|- ( ph -> C e. RR ) |
| 4 |
|
modadd12d.4 |
|- ( ph -> D e. RR ) |
| 5 |
|
modadd12d.5 |
|- ( ph -> E e. RR+ ) |
| 6 |
|
modadd12d.6 |
|- ( ph -> ( A mod E ) = ( B mod E ) ) |
| 7 |
|
modadd12d.7 |
|- ( ph -> ( C mod E ) = ( D mod E ) ) |
| 8 |
3
|
renegcld |
|- ( ph -> -u C e. RR ) |
| 9 |
4
|
renegcld |
|- ( ph -> -u D e. RR ) |
| 10 |
3 4 5 7
|
modnegd |
|- ( ph -> ( -u C mod E ) = ( -u D mod E ) ) |
| 11 |
1 2 8 9 5 6 10
|
modadd12d |
|- ( ph -> ( ( A + -u C ) mod E ) = ( ( B + -u D ) mod E ) ) |
| 12 |
1
|
recnd |
|- ( ph -> A e. CC ) |
| 13 |
3
|
recnd |
|- ( ph -> C e. CC ) |
| 14 |
12 13
|
negsubd |
|- ( ph -> ( A + -u C ) = ( A - C ) ) |
| 15 |
14
|
oveq1d |
|- ( ph -> ( ( A + -u C ) mod E ) = ( ( A - C ) mod E ) ) |
| 16 |
2
|
recnd |
|- ( ph -> B e. CC ) |
| 17 |
4
|
recnd |
|- ( ph -> D e. CC ) |
| 18 |
16 17
|
negsubd |
|- ( ph -> ( B + -u D ) = ( B - D ) ) |
| 19 |
18
|
oveq1d |
|- ( ph -> ( ( B + -u D ) mod E ) = ( ( B - D ) mod E ) ) |
| 20 |
11 15 19
|
3eqtr3d |
|- ( ph -> ( ( A - C ) mod E ) = ( ( B - D ) mod E ) ) |