Step |
Hyp |
Ref |
Expression |
1 |
|
eropr.1 |
âĒ ð― = ( ðī / ð
) |
2 |
|
eropr.2 |
âĒ ðū = ( ðĩ / ð ) |
3 |
|
eropr.3 |
âĒ ( ð â ð â ð ) |
4 |
|
eropr.4 |
âĒ ( ð â ð
Er ð ) |
5 |
|
eropr.5 |
âĒ ( ð â ð Er ð ) |
6 |
|
eropr.6 |
âĒ ( ð â ð Er ð ) |
7 |
|
eropr.7 |
âĒ ( ð â ðī â ð ) |
8 |
|
eropr.8 |
âĒ ( ð â ðĩ â ð ) |
9 |
|
eropr.9 |
âĒ ( ð â ðķ â ð ) |
10 |
|
eropr.10 |
âĒ ( ð â + : ( ðī Ã ðĩ ) âķ ðķ ) |
11 |
|
eropr.11 |
âĒ ( ( ð ⧠( ( ð â ðī ⧠ð â ðī ) ⧠( ðĄ â ðĩ ⧠ðĒ â ðĩ ) ) ) â ( ( ð ð
ð ⧠ðĄ ð ðĒ ) â ( ð + ðĄ ) ð ( ð + ðĒ ) ) ) |
12 |
|
eropr.12 |
âĒ âĻĢ = { âĻ âĻ ðĨ , ðĶ âĐ , ð§ âĐ âĢ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) } |
13 |
|
simpl |
âĒ ( ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ) |
14 |
13
|
reximi |
âĒ ( â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â â ð â ðĩ ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ) |
15 |
14
|
reximi |
âĒ ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â â ð â ðī â ð â ðĩ ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ) |
16 |
1
|
eleq2i |
âĒ ( ðĨ â ð― â ðĨ â ( ðī / ð
) ) |
17 |
|
vex |
âĒ ðĨ â V |
18 |
17
|
elqs |
âĒ ( ðĨ â ( ðī / ð
) â â ð â ðī ðĨ = [ ð ] ð
) |
19 |
16 18
|
bitri |
âĒ ( ðĨ â ð― â â ð â ðī ðĨ = [ ð ] ð
) |
20 |
2
|
eleq2i |
âĒ ( ðĶ â ðū â ðĶ â ( ðĩ / ð ) ) |
21 |
|
vex |
âĒ ðĶ â V |
22 |
21
|
elqs |
âĒ ( ðĶ â ( ðĩ / ð ) â â ð â ðĩ ðĶ = [ ð ] ð ) |
23 |
20 22
|
bitri |
âĒ ( ðĶ â ðū â â ð â ðĩ ðĶ = [ ð ] ð ) |
24 |
19 23
|
anbi12i |
âĒ ( ( ðĨ â ð― ⧠ðĶ â ðū ) â ( â ð â ðī ðĨ = [ ð ] ð
⧠â ð â ðĩ ðĶ = [ ð ] ð ) ) |
25 |
|
reeanv |
âĒ ( â ð â ðī â ð â ðĩ ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) â ( â ð â ðī ðĨ = [ ð ] ð
⧠â ð â ðĩ ðĶ = [ ð ] ð ) ) |
26 |
24 25
|
bitr4i |
âĒ ( ( ðĨ â ð― ⧠ðĶ â ðū ) â â ð â ðī â ð â ðĩ ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ) |
27 |
15 26
|
sylibr |
âĒ ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( ðĨ â ð― ⧠ðĶ â ðū ) ) |
28 |
27
|
pm4.71ri |
âĒ ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) |
29 |
1 2 3 4 5 6 7 8 9 10 11
|
eroveu |
âĒ ( ( ð ⧠( ðĨ â ð― ⧠ðĶ â ðū ) ) â â! ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) |
30 |
|
iota1 |
âĒ ( â! ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) = ð§ ) ) |
31 |
29 30
|
syl |
âĒ ( ( ð ⧠( ðĨ â ð― ⧠ðĶ â ðū ) ) â ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) = ð§ ) ) |
32 |
|
eqcom |
âĒ ( ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) = ð§ â ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) |
33 |
31 32
|
bitrdi |
âĒ ( ( ð ⧠( ðĨ â ð― ⧠ðĶ â ðū ) ) â ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) ) |
34 |
33
|
pm5.32da |
âĒ ( ð â ( ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) â ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) ) ) |
35 |
28 34
|
bitrid |
âĒ ( ð â ( â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) â ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) ) ) |
36 |
35
|
oprabbidv |
âĒ ( ð â { âĻ âĻ ðĨ , ðĶ âĐ , ð§ âĐ âĢ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) } = { âĻ âĻ ðĨ , ðĶ âĐ , ð§ âĐ âĢ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) } ) |
37 |
|
df-mpo |
âĒ ( ðĨ â ð― , ðĶ â ðū âĶ ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) = { âĻ âĻ ðĨ , ðĶ âĐ , ðĪ âĐ âĢ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ðĪ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) } |
38 |
|
nfv |
âĒ âē ðĪ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) |
39 |
|
nfv |
âĒ âē ð§ ( ðĨ â ð― ⧠ðĶ â ðū ) |
40 |
|
nfiota1 |
âĒ âē ð§ ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) |
41 |
40
|
nfeq2 |
âĒ âē ð§ ðĪ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) |
42 |
39 41
|
nfan |
âĒ âē ð§ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ðĪ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) |
43 |
|
eqeq1 |
âĒ ( ð§ = ðĪ â ( ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) â ðĪ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) ) |
44 |
43
|
anbi2d |
âĒ ( ð§ = ðĪ â ( ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) â ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ðĪ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) ) ) |
45 |
38 42 44
|
cbvoprab3 |
âĒ { âĻ âĻ ðĨ , ðĶ âĐ , ð§ âĐ âĢ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) } = { âĻ âĻ ðĨ , ðĶ âĐ , ðĪ âĐ âĢ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ðĪ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) } |
46 |
37 45
|
eqtr4i |
âĒ ( ðĨ â ð― , ðĶ â ðū âĶ ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) = { âĻ âĻ ðĨ , ðĶ âĐ , ð§ âĐ âĢ ( ( ðĨ â ð― ⧠ðĶ â ðū ) ⧠ð§ = ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) } |
47 |
36 12 46
|
3eqtr4g |
âĒ ( ð â âĻĢ = ( ðĨ â ð― , ðĶ â ðū âĶ ( âĐ ð§ â ð â ðī â ð â ðĩ ( ( ðĨ = [ ð ] ð
⧠ðĶ = [ ð ] ð ) ⧠ð§ = [ ( ð + ð ) ] ð ) ) ) ) |