Step | Hyp | Ref
| Expression |
1 | | cnre 7953 |
. . 3
โข (๐ด โ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
๐ด = (๐ฆ + (i ยท ๐ง))) |
2 | | recn 7944 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
3 | | ax-icn 7906 |
. . . . . . . 8
โข i โ
โ |
4 | | recn 7944 |
. . . . . . . 8
โข (๐ง โ โ โ ๐ง โ
โ) |
5 | | mulcl 7938 |
. . . . . . . 8
โข ((i
โ โ โง ๐ง
โ โ) โ (i ยท ๐ง) โ โ) |
6 | 3, 4, 5 | sylancr 414 |
. . . . . . 7
โข (๐ง โ โ โ (i
ยท ๐ง) โ
โ) |
7 | | subcl 8156 |
. . . . . . 7
โข ((๐ฆ โ โ โง (i
ยท ๐ง) โ โ)
โ (๐ฆ โ (i
ยท ๐ง)) โ
โ) |
8 | 2, 6, 7 | syl2an 289 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ โ (i ยท ๐ง)) โ
โ) |
9 | 2 | adantr 276 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ๐ฆ โ
โ) |
10 | 6 | adantl 277 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ๐ง) โ
โ) |
11 | 9, 10, 9 | ppncand 8308 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) = (๐ฆ + ๐ฆ)) |
12 | | readdcl 7937 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ฆ โ โ) โ (๐ฆ + ๐ฆ) โ โ) |
13 | 12 | anidms 397 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐ฆ + ๐ฆ) โ โ) |
14 | 13 | adantr 276 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ + ๐ฆ) โ โ) |
15 | 11, 14 | eqeltrd 2254 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ) |
16 | 9, 10, 10 | pnncand 8307 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง))) = ((i ยท ๐ง) + (i ยท ๐ง))) |
17 | 3 | a1i 9 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ง โ โ) โ i โ
โ) |
18 | 4 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ๐ง โ
โ) |
19 | 17, 18, 18 | adddid 7982 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท (๐ง + ๐ง)) = ((i ยท ๐ง) + (i ยท ๐ง))) |
20 | 16, 19 | eqtr4d 2213 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง))) = (i ยท (๐ง + ๐ง))) |
21 | 20 | oveq2d 5891 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ((๐ฆ + (i ยท
๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) = (i ยท (i ยท
(๐ง + ๐ง)))) |
22 | 18, 18 | addcld 7977 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ง + ๐ง) โ โ) |
23 | | mulass 7942 |
. . . . . . . . . 10
โข ((i
โ โ โง i โ โ โง (๐ง + ๐ง) โ โ) โ ((i ยท i)
ยท (๐ง + ๐ง)) = (i ยท (i ยท
(๐ง + ๐ง)))) |
24 | 3, 3, 23 | mp3an12 1327 |
. . . . . . . . 9
โข ((๐ง + ๐ง) โ โ โ ((i ยท i)
ยท (๐ง + ๐ง)) = (i ยท (i ยท
(๐ง + ๐ง)))) |
25 | 22, 24 | syl 14 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((i
ยท i) ยท (๐ง +
๐ง)) = (i ยท (i
ยท (๐ง + ๐ง)))) |
26 | 21, 25 | eqtr4d 2213 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ((๐ฆ + (i ยท
๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) = ((i ยท i) ยท
(๐ง + ๐ง))) |
27 | | ixi 8540 |
. . . . . . . . 9
โข (i
ยท i) = -1 |
28 | | 1re 7956 |
. . . . . . . . . 10
โข 1 โ
โ |
29 | 28 | renegcli 8219 |
. . . . . . . . 9
โข -1 โ
โ |
30 | 27, 29 | eqeltri 2250 |
. . . . . . . 8
โข (i
ยท i) โ โ |
31 | | simpr 110 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ๐ง โ
โ) |
32 | 31, 31 | readdcld 7987 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ง + ๐ง) โ โ) |
33 | | remulcl 7939 |
. . . . . . . 8
โข (((i
ยท i) โ โ โง (๐ง + ๐ง) โ โ) โ ((i ยท i)
ยท (๐ง + ๐ง)) โ
โ) |
34 | 30, 32, 33 | sylancr 414 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((i
ยท i) ยท (๐ง +
๐ง)) โ
โ) |
35 | 26, 34 | eqeltrd 2254 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ((๐ฆ + (i ยท
๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ
โ) |
36 | | oveq2 5883 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((๐ฆ + (i ยท ๐ง)) + ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง)))) |
37 | 36 | eleq1d 2246 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โ ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ)) |
38 | | oveq2 5883 |
. . . . . . . . . 10
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) |
39 | 38 | oveq2d 5891 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) = (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง))))) |
40 | 39 | eleq1d 2246 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ โ (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ โ)) |
41 | 37, 40 | anbi12d 473 |
. . . . . . 7
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ) โ (((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ โ))) |
42 | 41 | rspcev 2842 |
. . . . . 6
โข (((๐ฆ โ (i ยท ๐ง)) โ โ โง (((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ โ)) โ โ๐ฅ โ โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ)) |
43 | 8, 15, 35, 42 | syl12anc 1236 |
. . . . 5
โข ((๐ฆ โ โ โง ๐ง โ โ) โ
โ๐ฅ โ โ
(((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ)) |
44 | | oveq1 5882 |
. . . . . . . 8
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (๐ด + ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) + ๐ฅ)) |
45 | 44 | eleq1d 2246 |
. . . . . . 7
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ ((๐ด + ๐ฅ) โ โ โ ((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ)) |
46 | | oveq1 5882 |
. . . . . . . . 9
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (๐ด โ ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) |
47 | 46 | oveq2d 5891 |
. . . . . . . 8
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (i ยท (๐ด โ ๐ฅ)) = (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ))) |
48 | 47 | eleq1d 2246 |
. . . . . . 7
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ ((i ยท (๐ด โ ๐ฅ)) โ โ โ (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ)) |
49 | 45, 48 | anbi12d 473 |
. . . . . 6
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ))) |
50 | 49 | rexbidv 2478 |
. . . . 5
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (โ๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ โ๐ฅ โ โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ))) |
51 | 43, 50 | syl5ibrcom 157 |
. . . 4
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ด = (๐ฆ + (i ยท ๐ง)) โ โ๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ))) |
52 | 51 | rexlimivv 2600 |
. . 3
โข
(โ๐ฆ โ
โ โ๐ง โ
โ ๐ด = (๐ฆ + (i ยท ๐ง)) โ โ๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |
53 | 1, 52 | syl 14 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |
54 | | an4 586 |
. . . 4
โข ((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ (((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โง ((i ยท (๐ด โ ๐ฅ)) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ))) |
55 | | resubcl 8221 |
. . . . . . 7
โข (((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โ ((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) โ โ) |
56 | | pnpcan 8196 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) = (๐ฅ โ ๐ฆ)) |
57 | 56 | 3expb 1204 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) = (๐ฅ โ ๐ฆ)) |
58 | 57 | eleq1d 2246 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) โ โ โ (๐ฅ โ ๐ฆ) โ โ)) |
59 | 55, 58 | imbitrid 154 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โ (๐ฅ โ ๐ฆ) โ โ)) |
60 | | resubcl 8221 |
. . . . . . . 8
โข (((i
ยท (๐ด โ ๐ฆ)) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ) โ ((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) โ โ) |
61 | 60 | ancoms 268 |
. . . . . . 7
โข (((i
ยท (๐ด โ ๐ฅ)) โ โ โง (i
ยท (๐ด โ ๐ฆ)) โ โ) โ ((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) โ โ) |
62 | 3 | a1i 9 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ i
โ โ) |
63 | | subcl 8156 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฆ โ โ) โ (๐ด โ ๐ฆ) โ โ) |
64 | 63 | adantrl 478 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด โ ๐ฆ) โ โ) |
65 | | subcl 8156 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฅ โ โ) โ (๐ด โ ๐ฅ) โ โ) |
66 | 65 | adantrr 479 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด โ ๐ฅ) โ โ) |
67 | 62, 64, 66 | subdid 8371 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (i
ยท ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ))) = ((i ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ)))) |
68 | | nnncan1 8193 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ฆ โ โ โง ๐ฅ โ โ) โ ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ)) = (๐ฅ โ ๐ฆ)) |
69 | 68 | 3com23 1209 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ)) = (๐ฅ โ ๐ฆ)) |
70 | 69 | 3expb 1204 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ)) = (๐ฅ โ ๐ฆ)) |
71 | 70 | oveq2d 5891 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (i
ยท ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ))) = (i ยท (๐ฅ โ ๐ฆ))) |
72 | 67, 71 | eqtr3d 2212 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) = (i ยท (๐ฅ โ ๐ฆ))) |
73 | 72 | eleq1d 2246 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) โ โ โ (i ยท (๐ฅ โ ๐ฆ)) โ โ)) |
74 | 61, 73 | imbitrid 154 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((i
ยท (๐ด โ ๐ฅ)) โ โ โง (i
ยท (๐ด โ ๐ฆ)) โ โ) โ (i
ยท (๐ฅ โ ๐ฆ)) โ
โ)) |
75 | 59, 74 | anim12d 335 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โง ((i ยท (๐ด โ ๐ฅ)) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ((๐ฅ โ ๐ฆ) โ โ โง (i ยท (๐ฅ โ ๐ฆ)) โ โ))) |
76 | | rimul 8542 |
. . . . . 6
โข (((๐ฅ โ ๐ฆ) โ โ โง (i ยท (๐ฅ โ ๐ฆ)) โ โ) โ (๐ฅ โ ๐ฆ) = 0) |
77 | 76 | a1i 9 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ฅ โ ๐ฆ) โ โ โง (i
ยท (๐ฅ โ ๐ฆ)) โ โ) โ (๐ฅ โ ๐ฆ) = 0)) |
78 | | subeq0 8183 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ โ ๐ฆ) = 0 โ ๐ฅ = ๐ฆ)) |
79 | 78 | biimpd 144 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ โ ๐ฆ) = 0 โ ๐ฅ = ๐ฆ)) |
80 | 79 | adantl 277 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฅ โ ๐ฆ) = 0 โ ๐ฅ = ๐ฆ)) |
81 | 75, 77, 80 | 3syld 57 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โง ((i ยท (๐ด โ ๐ฅ)) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ)) |
82 | 54, 81 | biimtrid 152 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ)) |
83 | 82 | ralrimivva 2559 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ)) |
84 | | oveq2 5883 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด + ๐ฅ) = (๐ด + ๐ฆ)) |
85 | 84 | eleq1d 2246 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด + ๐ฅ) โ โ โ (๐ด + ๐ฆ) โ โ)) |
86 | | oveq2 5883 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด โ ๐ฅ) = (๐ด โ ๐ฆ)) |
87 | 86 | oveq2d 5891 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (i ยท (๐ด โ ๐ฅ)) = (i ยท (๐ด โ ๐ฆ))) |
88 | 87 | eleq1d 2246 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((i ยท (๐ด โ ๐ฅ)) โ โ โ (i ยท (๐ด โ ๐ฆ)) โ โ)) |
89 | 85, 88 | anbi12d 473 |
. . 3
โข (๐ฅ = ๐ฆ โ (((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ))) |
90 | 89 | reu4 2932 |
. 2
โข
(โ!๐ฅ โ
โ ((๐ด + ๐ฅ) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ) โ
(โ๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง โ๐ฅ โ โ โ๐ฆ โ โ ((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ))) |
91 | 53, 83, 90 | sylanbrc 417 |
1
โข (๐ด โ โ โ
โ!๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |