Step |
Hyp |
Ref |
Expression |
1 |
|
cju |
โข ( ๐ด โ โ โ โ! ๐ฅ โ โ ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) |
2 |
|
riotasbc |
โข ( โ! ๐ฅ โ โ ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) โ [ ( โฉ ๐ฅ โ โ ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) / ๐ฅ ] ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) |
3 |
1 2
|
syl |
โข ( ๐ด โ โ โ [ ( โฉ ๐ฅ โ โ ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) / ๐ฅ ] ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) |
4 |
|
cjval |
โข ( ๐ด โ โ โ ( โ โ ๐ด ) = ( โฉ ๐ฅ โ โ ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) ) |
5 |
4
|
sbceq1d |
โข ( ๐ด โ โ โ ( [ ( โ โ ๐ด ) / ๐ฅ ] ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) โ [ ( โฉ ๐ฅ โ โ ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) / ๐ฅ ] ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) ) |
6 |
3 5
|
mpbird |
โข ( ๐ด โ โ โ [ ( โ โ ๐ด ) / ๐ฅ ] ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) ) |
7 |
|
fvex |
โข ( โ โ ๐ด ) โ V |
8 |
|
oveq2 |
โข ( ๐ฅ = ( โ โ ๐ด ) โ ( ๐ด + ๐ฅ ) = ( ๐ด + ( โ โ ๐ด ) ) ) |
9 |
8
|
eleq1d |
โข ( ๐ฅ = ( โ โ ๐ด ) โ ( ( ๐ด + ๐ฅ ) โ โ โ ( ๐ด + ( โ โ ๐ด ) ) โ โ ) ) |
10 |
|
oveq2 |
โข ( ๐ฅ = ( โ โ ๐ด ) โ ( ๐ด โ ๐ฅ ) = ( ๐ด โ ( โ โ ๐ด ) ) ) |
11 |
10
|
oveq2d |
โข ( ๐ฅ = ( โ โ ๐ด ) โ ( i ยท ( ๐ด โ ๐ฅ ) ) = ( i ยท ( ๐ด โ ( โ โ ๐ด ) ) ) ) |
12 |
11
|
eleq1d |
โข ( ๐ฅ = ( โ โ ๐ด ) โ ( ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ โ ( i ยท ( ๐ด โ ( โ โ ๐ด ) ) ) โ โ ) ) |
13 |
9 12
|
anbi12d |
โข ( ๐ฅ = ( โ โ ๐ด ) โ ( ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) โ ( ( ๐ด + ( โ โ ๐ด ) ) โ โ โง ( i ยท ( ๐ด โ ( โ โ ๐ด ) ) ) โ โ ) ) ) |
14 |
7 13
|
sbcie |
โข ( [ ( โ โ ๐ด ) / ๐ฅ ] ( ( ๐ด + ๐ฅ ) โ โ โง ( i ยท ( ๐ด โ ๐ฅ ) ) โ โ ) โ ( ( ๐ด + ( โ โ ๐ด ) ) โ โ โง ( i ยท ( ๐ด โ ( โ โ ๐ด ) ) ) โ โ ) ) |
15 |
6 14
|
sylib |
โข ( ๐ด โ โ โ ( ( ๐ด + ( โ โ ๐ด ) ) โ โ โง ( i ยท ( ๐ด โ ( โ โ ๐ด ) ) ) โ โ ) ) |