Step | Hyp | Ref
| Expression |
1 | | eropr.3 |
. . . . . . . . . . . 12
âĒ (ð â ð â ð) |
2 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) ⧠(ð â ðī ⧠ð â ðĩ)) â ð â ð) |
3 | | eropr.10 |
. . . . . . . . . . . . 13
âĒ (ð â + :(ðī Ã ðĩ)âķðķ) |
4 | 3 | adantr 482 |
. . . . . . . . . . . 12
âĒ ((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) â + :(ðī à ðĩ)âķðķ) |
5 | 4 | fovcdmda 7475 |
. . . . . . . . . . 11
âĒ (((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) ⧠(ð â ðī ⧠ð â ðĩ)) â (ð + ð) â ðķ) |
6 | | ecelqsg 8592 |
. . . . . . . . . . 11
âĒ ((ð â ð ⧠(ð + ð) â ðķ) â [(ð + ð)]ð â (ðķ / ð)) |
7 | 2, 5, 6 | syl2anc 585 |
. . . . . . . . . 10
âĒ (((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) ⧠(ð â ðī ⧠ð â ðĩ)) â [(ð + ð)]ð â (ðķ / ð)) |
8 | | eropr.15 |
. . . . . . . . . 10
âĒ ðŋ = (ðķ / ð) |
9 | 7, 8 | eleqtrrdi 2848 |
. . . . . . . . 9
âĒ (((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) ⧠(ð â ðī ⧠ð â ðĩ)) â [(ð + ð)]ð â ðŋ) |
10 | | eleq1a 2832 |
. . . . . . . . 9
âĒ ([(ð + ð)]ð â ðŋ â (ð§ = [(ð + ð)]ð â ð§ â ðŋ)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
âĒ (((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) ⧠(ð â ðī ⧠ð â ðĩ)) â (ð§ = [(ð + ð)]ð â ð§ â ðŋ)) |
12 | 11 | adantld 492 |
. . . . . . 7
âĒ (((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) ⧠(ð â ðī ⧠ð â ðĩ)) â (((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð) â ð§ â ðŋ)) |
13 | 12 | rexlimdvva 3202 |
. . . . . 6
âĒ ((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) â (âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð) â ð§ â ðŋ)) |
14 | 13 | abssdv 4007 |
. . . . 5
âĒ ((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) â {ð§ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)} â ðŋ) |
15 | | eropr.1 |
. . . . . . 7
âĒ ð― = (ðī / ð
) |
16 | | eropr.2 |
. . . . . . 7
âĒ ðū = (ðĩ / ð) |
17 | | eropr.4 |
. . . . . . 7
âĒ (ð â ð
Er ð) |
18 | | eropr.5 |
. . . . . . 7
âĒ (ð â ð Er ð) |
19 | | eropr.6 |
. . . . . . 7
âĒ (ð â ð Er ð) |
20 | | eropr.7 |
. . . . . . 7
âĒ (ð â ðī â ð) |
21 | | eropr.8 |
. . . . . . 7
âĒ (ð â ðĩ â ð) |
22 | | eropr.9 |
. . . . . . 7
âĒ (ð â ðķ â ð) |
23 | | eropr.11 |
. . . . . . 7
âĒ ((ð ⧠((ð â ðī ⧠ð â ðī) ⧠(ðĄ â ðĩ ⧠ðĒ â ðĩ))) â ((ðð
ð ⧠ðĄððĒ) â (ð + ðĄ)ð(ð + ðĒ))) |
24 | 15, 16, 1, 17, 18, 19, 20, 21, 22, 3, 23 | eroveu 8632 |
. . . . . 6
âĒ ((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) â â!ð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)) |
25 | | iotacl 6444 |
. . . . . 6
âĒ
(â!ð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð) â (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)) â {ð§ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)}) |
26 | 24, 25 | syl 17 |
. . . . 5
âĒ ((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) â (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)) â {ð§ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)}) |
27 | 14, 26 | sseldd 3927 |
. . . 4
âĒ ((ð ⧠(ðĨ â ð― ⧠ðĶ â ðū)) â (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)) â ðŋ) |
28 | 27 | ralrimivva 3194 |
. . 3
âĒ (ð â âðĨ â ð― âðĶ â ðū (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)) â ðŋ) |
29 | | eqid 2736 |
. . . 4
âĒ (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð))) = (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð))) |
30 | 29 | fmpo 7940 |
. . 3
âĒ
(âðĨ â
ð― âðĶ â ðū (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)) â ðŋ â (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð))):(ð― à ðū)âķðŋ) |
31 | 28, 30 | sylib 217 |
. 2
âĒ (ð â (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð))):(ð― à ðū)âķðŋ) |
32 | | eropr.12 |
. . . 4
âĒ âĻĢ =
{âĻâĻðĨ, ðĶâĐ, ð§âĐ âĢ âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)} |
33 | 15, 16, 1, 17, 18, 19, 20, 21, 22, 3, 23, 32 | erovlem 8633 |
. . 3
âĒ (ð â âĻĢ = (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð)))) |
34 | 33 | feq1d 6615 |
. 2
âĒ (ð â ( âĻĢ :(ð― à ðū)âķðŋ â (ðĨ â ð―, ðĶ â ðū âĶ (âĐð§âð â ðī âð â ðĩ ((ðĨ = [ð]ð
⧠ðĶ = [ð]ð) ⧠ð§ = [(ð + ð)]ð))):(ð― à ðū)âķðŋ)) |
35 | 31, 34 | mpbird 257 |
1
âĒ (ð â âĻĢ :(ð― Ã ðū)âķðŋ) |