Step | Hyp | Ref
| Expression |
1 | | cnre 11160 |
. . 3
โข (๐ด โ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
๐ด = (๐ฆ + (i ยท ๐ง))) |
2 | | recn 11149 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
3 | | ax-icn 11118 |
. . . . . . . 8
โข i โ
โ |
4 | | recn 11149 |
. . . . . . . 8
โข (๐ง โ โ โ ๐ง โ
โ) |
5 | | mulcl 11143 |
. . . . . . . 8
โข ((i
โ โ โง ๐ง
โ โ) โ (i ยท ๐ง) โ โ) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . . 7
โข (๐ง โ โ โ (i
ยท ๐ง) โ
โ) |
7 | | subcl 11408 |
. . . . . . 7
โข ((๐ฆ โ โ โง (i
ยท ๐ง) โ โ)
โ (๐ฆ โ (i
ยท ๐ง)) โ
โ) |
8 | 2, 6, 7 | syl2an 597 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ โ (i ยท ๐ง)) โ
โ) |
9 | 2 | adantr 482 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ๐ฆ โ
โ) |
10 | 6 | adantl 483 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ๐ง) โ
โ) |
11 | 9, 10, 9 | ppncand 11560 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) = (๐ฆ + ๐ฆ)) |
12 | | readdcl 11142 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ฆ โ โ) โ (๐ฆ + ๐ฆ) โ โ) |
13 | 12 | anidms 568 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐ฆ + ๐ฆ) โ โ) |
14 | 13 | adantr 482 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ + ๐ฆ) โ โ) |
15 | 11, 14 | eqeltrd 2834 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ) |
16 | 9, 10, 10 | pnncand 11559 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง))) = ((i ยท ๐ง) + (i ยท ๐ง))) |
17 | 3 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ง โ โ) โ i โ
โ) |
18 | 4 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ๐ง โ
โ) |
19 | 17, 18, 18 | adddid 11187 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท (๐ง + ๐ง)) = ((i ยท ๐ง) + (i ยท ๐ง))) |
20 | 16, 19 | eqtr4d 2776 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง))) = (i ยท (๐ง + ๐ง))) |
21 | 20 | oveq2d 7377 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ((๐ฆ + (i ยท
๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) = (i ยท (i ยท
(๐ง + ๐ง)))) |
22 | 18, 18 | addcld 11182 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ง + ๐ง) โ โ) |
23 | | mulass 11147 |
. . . . . . . . 9
โข ((i
โ โ โง i โ โ โง (๐ง + ๐ง) โ โ) โ ((i ยท i)
ยท (๐ง + ๐ง)) = (i ยท (i ยท
(๐ง + ๐ง)))) |
24 | 3, 3, 22, 23 | mp3an12i 1466 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((i
ยท i) ยท (๐ง +
๐ง)) = (i ยท (i
ยท (๐ง + ๐ง)))) |
25 | 21, 24 | eqtr4d 2776 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ((๐ฆ + (i ยท
๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) = ((i ยท i) ยท
(๐ง + ๐ง))) |
26 | | ixi 11792 |
. . . . . . . . 9
โข (i
ยท i) = -1 |
27 | | 1re 11163 |
. . . . . . . . . 10
โข 1 โ
โ |
28 | 27 | renegcli 11470 |
. . . . . . . . 9
โข -1 โ
โ |
29 | 26, 28 | eqeltri 2830 |
. . . . . . . 8
โข (i
ยท i) โ โ |
30 | | simpr 486 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ๐ง โ
โ) |
31 | 30, 30 | readdcld 11192 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ง + ๐ง) โ โ) |
32 | | remulcl 11144 |
. . . . . . . 8
โข (((i
ยท i) โ โ โง (๐ง + ๐ง) โ โ) โ ((i ยท i)
ยท (๐ง + ๐ง)) โ
โ) |
33 | 29, 31, 32 | sylancr 588 |
. . . . . . 7
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((i
ยท i) ยท (๐ง +
๐ง)) โ
โ) |
34 | 25, 33 | eqeltrd 2834 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (i
ยท ((๐ฆ + (i ยท
๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ
โ) |
35 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((๐ฆ + (i ยท ๐ง)) + ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง)))) |
36 | 35 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โ ((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ)) |
37 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) |
38 | 37 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) = (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง))))) |
39 | 38 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ โ (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ โ)) |
40 | 36, 39 | anbi12d 632 |
. . . . . . 7
โข (๐ฅ = (๐ฆ โ (i ยท ๐ง)) โ ((((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ) โ (((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ โ))) |
41 | 40 | rspcev 3583 |
. . . . . 6
โข (((๐ฆ โ (i ยท ๐ง)) โ โ โง (((๐ฆ + (i ยท ๐ง)) + (๐ฆ โ (i ยท ๐ง))) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ (๐ฆ โ (i ยท ๐ง)))) โ โ)) โ โ๐ฅ โ โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ)) |
42 | 8, 15, 34, 41 | syl12anc 836 |
. . . . 5
โข ((๐ฆ โ โ โง ๐ง โ โ) โ
โ๐ฅ โ โ
(((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ)) |
43 | | oveq1 7368 |
. . . . . . . 8
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (๐ด + ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) + ๐ฅ)) |
44 | 43 | eleq1d 2819 |
. . . . . . 7
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ ((๐ด + ๐ฅ) โ โ โ ((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ)) |
45 | | oveq1 7368 |
. . . . . . . . 9
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (๐ด โ ๐ฅ) = ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) |
46 | 45 | oveq2d 7377 |
. . . . . . . 8
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (i ยท (๐ด โ ๐ฅ)) = (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ))) |
47 | 46 | eleq1d 2819 |
. . . . . . 7
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ ((i ยท (๐ด โ ๐ฅ)) โ โ โ (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ)) |
48 | 44, 47 | anbi12d 632 |
. . . . . 6
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ))) |
49 | 48 | rexbidv 3172 |
. . . . 5
โข (๐ด = (๐ฆ + (i ยท ๐ง)) โ (โ๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ โ๐ฅ โ โ (((๐ฆ + (i ยท ๐ง)) + ๐ฅ) โ โ โง (i ยท ((๐ฆ + (i ยท ๐ง)) โ ๐ฅ)) โ โ))) |
50 | 42, 49 | syl5ibrcom 247 |
. . . 4
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ด = (๐ฆ + (i ยท ๐ง)) โ โ๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ))) |
51 | 50 | rexlimivv 3193 |
. . 3
โข
(โ๐ฆ โ
โ โ๐ง โ
โ ๐ด = (๐ฆ + (i ยท ๐ง)) โ โ๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |
52 | 1, 51 | syl 17 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |
53 | | an4 655 |
. . . 4
โข ((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ (((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โง ((i ยท (๐ด โ ๐ฅ)) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ))) |
54 | | resubcl 11473 |
. . . . . . 7
โข (((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โ ((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) โ โ) |
55 | | pnpcan 11448 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) = (๐ฅ โ ๐ฆ)) |
56 | 55 | 3expb 1121 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) = (๐ฅ โ ๐ฆ)) |
57 | 56 | eleq1d 2819 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ด + ๐ฅ) โ (๐ด + ๐ฆ)) โ โ โ (๐ฅ โ ๐ฆ) โ โ)) |
58 | 54, 57 | imbitrid 243 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โ (๐ฅ โ ๐ฆ) โ โ)) |
59 | | resubcl 11473 |
. . . . . . . 8
โข (((i
ยท (๐ด โ ๐ฆ)) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ) โ ((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) โ โ) |
60 | 59 | ancoms 460 |
. . . . . . 7
โข (((i
ยท (๐ด โ ๐ฅ)) โ โ โง (i
ยท (๐ด โ ๐ฆ)) โ โ) โ ((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) โ โ) |
61 | 3 | a1i 11 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ i
โ โ) |
62 | | subcl 11408 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฆ โ โ) โ (๐ด โ ๐ฆ) โ โ) |
63 | 62 | adantrl 715 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด โ ๐ฆ) โ โ) |
64 | | subcl 11408 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฅ โ โ) โ (๐ด โ ๐ฅ) โ โ) |
65 | 64 | adantrr 716 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด โ ๐ฅ) โ โ) |
66 | 61, 63, 65 | subdid 11619 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (i
ยท ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ))) = ((i ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ)))) |
67 | | nnncan1 11445 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ฆ โ โ โง ๐ฅ โ โ) โ ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ)) = (๐ฅ โ ๐ฆ)) |
68 | 67 | 3com23 1127 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ)) = (๐ฅ โ ๐ฆ)) |
69 | 68 | 3expb 1121 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ)) = (๐ฅ โ ๐ฆ)) |
70 | 69 | oveq2d 7377 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (i
ยท ((๐ด โ ๐ฆ) โ (๐ด โ ๐ฅ))) = (i ยท (๐ฅ โ ๐ฆ))) |
71 | 66, 70 | eqtr3d 2775 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) = (i ยท (๐ฅ โ ๐ฆ))) |
72 | 71 | eleq1d 2819 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((i
ยท (๐ด โ ๐ฆ)) โ (i ยท (๐ด โ ๐ฅ))) โ โ โ (i ยท (๐ฅ โ ๐ฆ)) โ โ)) |
73 | 60, 72 | imbitrid 243 |
. . . . . 6
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((i
ยท (๐ด โ ๐ฅ)) โ โ โง (i
ยท (๐ด โ ๐ฆ)) โ โ) โ (i
ยท (๐ฅ โ ๐ฆ)) โ
โ)) |
74 | 58, 73 | anim12d 610 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โง ((i ยท (๐ด โ ๐ฅ)) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ((๐ฅ โ ๐ฆ) โ โ โง (i ยท (๐ฅ โ ๐ฆ)) โ โ))) |
75 | | rimul 12152 |
. . . . . 6
โข (((๐ฅ โ ๐ฆ) โ โ โง (i ยท (๐ฅ โ ๐ฆ)) โ โ) โ (๐ฅ โ ๐ฆ) = 0) |
76 | 75 | a1i 11 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ฅ โ ๐ฆ) โ โ โง (i
ยท (๐ฅ โ ๐ฆ)) โ โ) โ (๐ฅ โ ๐ฆ) = 0)) |
77 | | subeq0 11435 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ โ ๐ฆ) = 0 โ ๐ฅ = ๐ฆ)) |
78 | 77 | biimpd 228 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐ฅ โ ๐ฆ) = 0 โ ๐ฅ = ๐ฆ)) |
79 | 78 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฅ โ ๐ฆ) = 0 โ ๐ฅ = ๐ฆ)) |
80 | 74, 76, 79 | 3syld 60 |
. . . 4
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((((๐ด + ๐ฅ) โ โ โง (๐ด + ๐ฆ) โ โ) โง ((i ยท (๐ด โ ๐ฅ)) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ)) |
81 | 53, 80 | biimtrid 241 |
. . 3
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ)) |
82 | 81 | ralrimivva 3194 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ)) |
83 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด + ๐ฅ) = (๐ด + ๐ฆ)) |
84 | 83 | eleq1d 2819 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด + ๐ฅ) โ โ โ (๐ด + ๐ฆ) โ โ)) |
85 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด โ ๐ฅ) = (๐ด โ ๐ฆ)) |
86 | 85 | oveq2d 7377 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (i ยท (๐ด โ ๐ฅ)) = (i ยท (๐ด โ ๐ฆ))) |
87 | 86 | eleq1d 2819 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((i ยท (๐ด โ ๐ฅ)) โ โ โ (i ยท (๐ด โ ๐ฆ)) โ โ)) |
88 | 84, 87 | anbi12d 632 |
. . 3
โข (๐ฅ = ๐ฆ โ (((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ))) |
89 | 88 | reu4 3693 |
. 2
โข
(โ!๐ฅ โ
โ ((๐ด + ๐ฅ) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ) โ
(โ๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง โ๐ฅ โ โ โ๐ฆ โ โ ((((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โง ((๐ด + ๐ฆ) โ โ โง (i ยท (๐ด โ ๐ฆ)) โ โ)) โ ๐ฅ = ๐ฆ))) |
90 | 52, 82, 89 | sylanbrc 584 |
1
โข (๐ด โ โ โ
โ!๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |