Step | Hyp | Ref
| Expression |
1 | | 2cn 12235 |
. . . . . . . . . 10
โข 2 โ
โ |
2 | | quartlem1.p |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
3 | | sqmul 14031 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ) โ ((2 ยท ๐)โ2) = ((2โ2) ยท (๐โ2))) |
4 | 1, 2, 3 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ2) = ((2โ2) ยท
(๐โ2))) |
5 | | sq2 14108 |
. . . . . . . . . 10
โข
(2โ2) = 4 |
6 | 5 | oveq1i 7372 |
. . . . . . . . 9
โข
((2โ2) ยท (๐โ2)) = (4 ยท (๐โ2)) |
7 | 4, 6 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐)โ2) = (4 ยท (๐โ2))) |
8 | 7 | oveq1d 7377 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐)โ2) โ (3 ยท
(๐โ2))) = ((4 ยท
(๐โ2)) โ (3
ยท (๐โ2)))) |
9 | | 4cn 12245 |
. . . . . . . . 9
โข 4 โ
โ |
10 | 9 | a1i 11 |
. . . . . . . 8
โข (๐ โ 4 โ
โ) |
11 | | 3cn 12241 |
. . . . . . . . 9
โข 3 โ
โ |
12 | 11 | a1i 11 |
. . . . . . . 8
โข (๐ โ 3 โ
โ) |
13 | 2 | sqcld 14056 |
. . . . . . . 8
โข (๐ โ (๐โ2) โ โ) |
14 | 10, 12, 13 | subdird 11619 |
. . . . . . 7
โข (๐ โ ((4 โ 3) ยท
(๐โ2)) = ((4 ยท
(๐โ2)) โ (3
ยท (๐โ2)))) |
15 | 8, 14 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ (((2 ยท ๐)โ2) โ (3 ยท
(๐โ2))) = ((4 โ
3) ยท (๐โ2))) |
16 | | ax-1cn 11116 |
. . . . . . . . . 10
โข 1 โ
โ |
17 | | 3p1e4 12305 |
. . . . . . . . . 10
โข (3 + 1) =
4 |
18 | 9, 11, 16, 17 | subaddrii 11497 |
. . . . . . . . 9
โข (4
โ 3) = 1 |
19 | 18 | oveq1i 7372 |
. . . . . . . 8
โข ((4
โ 3) ยท (๐โ2)) = (1 ยท (๐โ2)) |
20 | | mulid2 11161 |
. . . . . . . 8
โข ((๐โ2) โ โ โ
(1 ยท (๐โ2)) =
(๐โ2)) |
21 | 19, 20 | eqtrid 2789 |
. . . . . . 7
โข ((๐โ2) โ โ โ
((4 โ 3) ยท (๐โ2)) = (๐โ2)) |
22 | 13, 21 | syl 17 |
. . . . . 6
โข (๐ โ ((4 โ 3) ยท
(๐โ2)) = (๐โ2)) |
23 | 15, 22 | eqtr2d 2778 |
. . . . 5
โข (๐ โ (๐โ2) = (((2 ยท ๐)โ2) โ (3 ยท (๐โ2)))) |
24 | 23 | oveq1d 7377 |
. . . 4
โข (๐ โ ((๐โ2) + (;12 ยท ๐
)) = ((((2 ยท ๐)โ2) โ (3 ยท (๐โ2))) + (;12 ยท ๐
))) |
25 | | mulcl 11142 |
. . . . . . 7
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
26 | 1, 2, 25 | sylancr 588 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
27 | 26 | sqcld 14056 |
. . . . 5
โข (๐ โ ((2 ยท ๐)โ2) โ
โ) |
28 | | mulcl 11142 |
. . . . . 6
โข ((3
โ โ โง (๐โ2) โ โ) โ (3 ยท
(๐โ2)) โ
โ) |
29 | 11, 13, 28 | sylancr 588 |
. . . . 5
โข (๐ โ (3 ยท (๐โ2)) โ
โ) |
30 | | 1nn0 12436 |
. . . . . . . 8
โข 1 โ
โ0 |
31 | | 2nn 12233 |
. . . . . . . 8
โข 2 โ
โ |
32 | 30, 31 | decnncl 12645 |
. . . . . . 7
โข ;12 โ โ |
33 | 32 | nncni 12170 |
. . . . . 6
โข ;12 โ โ |
34 | | quartlem1.r |
. . . . . 6
โข (๐ โ ๐
โ โ) |
35 | | mulcl 11142 |
. . . . . 6
โข ((;12 โ โ โง ๐
โ โ) โ (;12 ยท ๐
) โ โ) |
36 | 33, 34, 35 | sylancr 588 |
. . . . 5
โข (๐ โ (;12 ยท ๐
) โ โ) |
37 | 27, 29, 36 | subsubd 11547 |
. . . 4
โข (๐ โ (((2 ยท ๐)โ2) โ ((3 ยท
(๐โ2)) โ (;12 ยท ๐
))) = ((((2 ยท ๐)โ2) โ (3 ยท (๐โ2))) + (;12 ยท ๐
))) |
38 | 24, 37 | eqtr4d 2780 |
. . 3
โข (๐ โ ((๐โ2) + (;12 ยท ๐
)) = (((2 ยท ๐)โ2) โ ((3 ยท (๐โ2)) โ (;12 ยท ๐
)))) |
39 | | quartlem1.u |
. . 3
โข (๐ โ ๐ = ((๐โ2) + (;12 ยท ๐
))) |
40 | | mulcl 11142 |
. . . . . . 7
โข ((4
โ โ โง ๐
โ โ) โ (4 ยท ๐
) โ โ) |
41 | 9, 34, 40 | sylancr 588 |
. . . . . 6
โข (๐ โ (4 ยท ๐
) โ
โ) |
42 | 12, 13, 41 | subdid 11618 |
. . . . 5
โข (๐ โ (3 ยท ((๐โ2) โ (4 ยท
๐
))) = ((3 ยท (๐โ2)) โ (3 ยท (4
ยท ๐
)))) |
43 | | 4t3e12 12723 |
. . . . . . . . 9
โข (4
ยท 3) = ;12 |
44 | 9, 11, 43 | mulcomli 11171 |
. . . . . . . 8
โข (3
ยท 4) = ;12 |
45 | 44 | oveq1i 7372 |
. . . . . . 7
โข ((3
ยท 4) ยท ๐
) =
(;12 ยท ๐
) |
46 | 12, 10, 34 | mulassd 11185 |
. . . . . . 7
โข (๐ โ ((3 ยท 4) ยท
๐
) = (3 ยท (4
ยท ๐
))) |
47 | 45, 46 | eqtr3id 2791 |
. . . . . 6
โข (๐ โ (;12 ยท ๐
) = (3 ยท (4 ยท ๐
))) |
48 | 47 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((3 ยท (๐โ2)) โ (;12 ยท ๐
)) = ((3 ยท (๐โ2)) โ (3 ยท (4 ยท
๐
)))) |
49 | 42, 48 | eqtr4d 2780 |
. . . 4
โข (๐ โ (3 ยท ((๐โ2) โ (4 ยท
๐
))) = ((3 ยท (๐โ2)) โ (;12 ยท ๐
))) |
50 | 49 | oveq2d 7378 |
. . 3
โข (๐ โ (((2 ยท ๐)โ2) โ (3 ยท
((๐โ2) โ (4
ยท ๐
)))) = (((2
ยท ๐)โ2) โ
((3 ยท (๐โ2))
โ (;12 ยท ๐
)))) |
51 | 38, 39, 50 | 3eqtr4d 2787 |
. 2
โข (๐ โ ๐ = (((2 ยท ๐)โ2) โ (3 ยท ((๐โ2) โ (4 ยท
๐
))))) |
52 | 1 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ) |
53 | | 3nn0 12438 |
. . . . . . . . . . 11
โข 3 โ
โ0 |
54 | 53 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 3 โ
โ0) |
55 | 52, 2, 54 | mulexpd 14073 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐)โ3) = ((2โ3) ยท
(๐โ3))) |
56 | | cu2 14111 |
. . . . . . . . . 10
โข
(2โ3) = 8 |
57 | 56 | oveq1i 7372 |
. . . . . . . . 9
โข
((2โ3) ยท (๐โ3)) = (8 ยท (๐โ3)) |
58 | 55, 57 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐)โ3) = (8 ยท (๐โ3))) |
59 | 58 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (2 ยท ((2 ยท
๐)โ3)) = (2 ยท
(8 ยท (๐โ3)))) |
60 | | 8cn 12257 |
. . . . . . . . 9
โข 8 โ
โ |
61 | 60 | a1i 11 |
. . . . . . . 8
โข (๐ โ 8 โ
โ) |
62 | | expcl 13992 |
. . . . . . . . 9
โข ((๐ โ โ โง 3 โ
โ0) โ (๐โ3) โ โ) |
63 | 2, 53, 62 | sylancl 587 |
. . . . . . . 8
โข (๐ โ (๐โ3) โ โ) |
64 | 52, 61, 63 | mul12d 11371 |
. . . . . . 7
โข (๐ โ (2 ยท (8 ยท
(๐โ3))) = (8 ยท
(2 ยท (๐โ3)))) |
65 | 59, 64 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (2 ยท ((2 ยท
๐)โ3)) = (8 ยท
(2 ยท (๐โ3)))) |
66 | | 9cn 12260 |
. . . . . . . . 9
โข 9 โ
โ |
67 | 66 | a1i 11 |
. . . . . . . 8
โข (๐ โ 9 โ
โ) |
68 | | mulcl 11142 |
. . . . . . . . 9
โข ((2
โ โ โง (๐โ3) โ โ) โ (2 ยท
(๐โ3)) โ
โ) |
69 | 1, 63, 68 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (2 ยท (๐โ3)) โ
โ) |
70 | 2, 34 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ (๐ ยท ๐
) โ โ) |
71 | | mulcl 11142 |
. . . . . . . . 9
โข ((8
โ โ โง (๐
ยท ๐
) โ โ)
โ (8 ยท (๐
ยท ๐
)) โ
โ) |
72 | 60, 70, 71 | sylancr 588 |
. . . . . . . 8
โข (๐ โ (8 ยท (๐ ยท ๐
)) โ โ) |
73 | 67, 69, 72 | subdid 11618 |
. . . . . . 7
โข (๐ โ (9 ยท ((2 ยท
(๐โ3)) โ (8
ยท (๐ ยท ๐
)))) = ((9 ยท (2 ยท
(๐โ3))) โ (9
ยท (8 ยท (๐
ยท ๐
))))) |
74 | 26, 13, 41 | subdid 11618 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) ยท ((๐โ2) โ (4 ยท ๐
))) = (((2 ยท ๐) ยท (๐โ2)) โ ((2 ยท ๐) ยท (4 ยท ๐
)))) |
75 | 52, 2, 13 | mulassd 11185 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) ยท (๐โ2)) = (2 ยท (๐ ยท (๐โ2)))) |
76 | 2, 13 | mulcomd 11183 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ ยท (๐โ2)) = ((๐โ2) ยท ๐)) |
77 | | df-3 12224 |
. . . . . . . . . . . . . . 15
โข 3 = (2 +
1) |
78 | 77 | oveq2i 7373 |
. . . . . . . . . . . . . 14
โข (๐โ3) = (๐โ(2 + 1)) |
79 | | 2nn0 12437 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ0 |
80 | | expp1 13981 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง 2 โ
โ0) โ (๐โ(2 + 1)) = ((๐โ2) ยท ๐)) |
81 | 2, 79, 80 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐โ(2 + 1)) = ((๐โ2) ยท ๐)) |
82 | 78, 81 | eqtrid 2789 |
. . . . . . . . . . . . 13
โข (๐ โ (๐โ3) = ((๐โ2) ยท ๐)) |
83 | 76, 82 | eqtr4d 2780 |
. . . . . . . . . . . 12
โข (๐ โ (๐ ยท (๐โ2)) = (๐โ3)) |
84 | 83 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท (๐ ยท (๐โ2))) = (2 ยท (๐โ3))) |
85 | 75, 84 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) ยท (๐โ2)) = (2 ยท (๐โ3))) |
86 | 52, 2, 10, 34 | mul4d 11374 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) ยท (4 ยท ๐
)) = ((2 ยท 4) ยท
(๐ ยท ๐
))) |
87 | | 4t2e8 12328 |
. . . . . . . . . . . . 13
โข (4
ยท 2) = 8 |
88 | 9, 1, 87 | mulcomli 11171 |
. . . . . . . . . . . 12
โข (2
ยท 4) = 8 |
89 | 88 | oveq1i 7372 |
. . . . . . . . . . 11
โข ((2
ยท 4) ยท (๐
ยท ๐
)) = (8 ยท
(๐ ยท ๐
)) |
90 | 86, 89 | eqtrdi 2793 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) ยท (4 ยท ๐
)) = (8 ยท (๐ ยท ๐
))) |
91 | 85, 90 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) ยท (๐โ2)) โ ((2 ยท ๐) ยท (4 ยท ๐
))) = ((2 ยท (๐โ3)) โ (8 ยท
(๐ ยท ๐
)))) |
92 | 74, 91 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ ((2 ยท ๐) ยท ((๐โ2) โ (4 ยท ๐
))) = ((2 ยท (๐โ3)) โ (8 ยท
(๐ ยท ๐
)))) |
93 | 92 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (9 ยท ((2 ยท
๐) ยท ((๐โ2) โ (4 ยท
๐
)))) = (9 ยท ((2
ยท (๐โ3))
โ (8 ยท (๐
ยท ๐
))))) |
94 | | 9t8e72 12753 |
. . . . . . . . . 10
โข (9
ยท 8) = ;72 |
95 | 94 | oveq1i 7372 |
. . . . . . . . 9
โข ((9
ยท 8) ยท (๐
ยท ๐
)) = (;72 ยท (๐ ยท ๐
)) |
96 | 67, 61, 70 | mulassd 11185 |
. . . . . . . . 9
โข (๐ โ ((9 ยท 8) ยท
(๐ ยท ๐
)) = (9 ยท (8 ยท
(๐ ยท ๐
)))) |
97 | 95, 96 | eqtr3id 2791 |
. . . . . . . 8
โข (๐ โ (;72 ยท (๐ ยท ๐
)) = (9 ยท (8 ยท (๐ ยท ๐
)))) |
98 | 97 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ ((9 ยท (2 ยท
(๐โ3))) โ (;72 ยท (๐ ยท ๐
))) = ((9 ยท (2 ยท (๐โ3))) โ (9 ยท
(8 ยท (๐ ยท
๐
))))) |
99 | 73, 93, 98 | 3eqtr4d 2787 |
. . . . . 6
โข (๐ โ (9 ยท ((2 ยท
๐) ยท ((๐โ2) โ (4 ยท
๐
)))) = ((9 ยท (2
ยท (๐โ3)))
โ (;72 ยท (๐ ยท ๐
)))) |
100 | 65, 99 | oveq12d 7380 |
. . . . 5
โข (๐ โ ((2 ยท ((2 ยท
๐)โ3)) โ (9
ยท ((2 ยท ๐)
ยท ((๐โ2)
โ (4 ยท ๐
)))))
= ((8 ยท (2 ยท (๐โ3))) โ ((9 ยท (2 ยท
(๐โ3))) โ (;72 ยท (๐ ยท ๐
))))) |
101 | | mulcl 11142 |
. . . . . . 7
โข ((8
โ โ โง (2 ยท (๐โ3)) โ โ) โ (8 ยท
(2 ยท (๐โ3)))
โ โ) |
102 | 60, 69, 101 | sylancr 588 |
. . . . . 6
โข (๐ โ (8 ยท (2 ยท
(๐โ3))) โ
โ) |
103 | | mulcl 11142 |
. . . . . . 7
โข ((9
โ โ โง (2 ยท (๐โ3)) โ โ) โ (9 ยท
(2 ยท (๐โ3)))
โ โ) |
104 | 66, 69, 103 | sylancr 588 |
. . . . . 6
โข (๐ โ (9 ยท (2 ยท
(๐โ3))) โ
โ) |
105 | | 7nn0 12442 |
. . . . . . . . 9
โข 7 โ
โ0 |
106 | 105, 31 | decnncl 12645 |
. . . . . . . 8
โข ;72 โ โ |
107 | 106 | nncni 12170 |
. . . . . . 7
โข ;72 โ โ |
108 | | mulcl 11142 |
. . . . . . 7
โข ((;72 โ โ โง (๐ ยท ๐
) โ โ) โ (;72 ยท (๐ ยท ๐
)) โ โ) |
109 | 107, 70, 108 | sylancr 588 |
. . . . . 6
โข (๐ โ (;72 ยท (๐ ยท ๐
)) โ โ) |
110 | 102, 104,
109 | subsubd 11547 |
. . . . 5
โข (๐ โ ((8 ยท (2 ยท
(๐โ3))) โ ((9
ยท (2 ยท (๐โ3))) โ (;72 ยท (๐ ยท ๐
)))) = (((8 ยท (2 ยท (๐โ3))) โ (9 ยท
(2 ยท (๐โ3)))) +
(;72 ยท (๐ ยท ๐
)))) |
111 | 104, 102 | negsubdi2d 11535 |
. . . . . . 7
โข (๐ โ -((9 ยท (2 ยท
(๐โ3))) โ (8
ยท (2 ยท (๐โ3)))) = ((8 ยท (2 ยท
(๐โ3))) โ (9
ยท (2 ยท (๐โ3))))) |
112 | 67, 61, 69 | subdird 11619 |
. . . . . . . . 9
โข (๐ โ ((9 โ 8) ยท (2
ยท (๐โ3))) = ((9
ยท (2 ยท (๐โ3))) โ (8 ยท (2 ยท
(๐โ3))))) |
113 | | 8p1e9 12310 |
. . . . . . . . . . . 12
โข (8 + 1) =
9 |
114 | 66, 60, 16, 113 | subaddrii 11497 |
. . . . . . . . . . 11
โข (9
โ 8) = 1 |
115 | 114 | oveq1i 7372 |
. . . . . . . . . 10
โข ((9
โ 8) ยท (2 ยท (๐โ3))) = (1 ยท (2 ยท (๐โ3))) |
116 | 69 | mulid2d 11180 |
. . . . . . . . . 10
โข (๐ โ (1 ยท (2 ยท
(๐โ3))) = (2 ยท
(๐โ3))) |
117 | 115, 116 | eqtrid 2789 |
. . . . . . . . 9
โข (๐ โ ((9 โ 8) ยท (2
ยท (๐โ3))) = (2
ยท (๐โ3))) |
118 | 112, 117 | eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ ((9 ยท (2 ยท
(๐โ3))) โ (8
ยท (2 ยท (๐โ3)))) = (2 ยท (๐โ3))) |
119 | 118 | negeqd 11402 |
. . . . . . 7
โข (๐ โ -((9 ยท (2 ยท
(๐โ3))) โ (8
ยท (2 ยท (๐โ3)))) = -(2 ยท (๐โ3))) |
120 | 111, 119 | eqtr3d 2779 |
. . . . . 6
โข (๐ โ ((8 ยท (2 ยท
(๐โ3))) โ (9
ยท (2 ยท (๐โ3)))) = -(2 ยท (๐โ3))) |
121 | 120 | oveq1d 7377 |
. . . . 5
โข (๐ โ (((8 ยท (2 ยท
(๐โ3))) โ (9
ยท (2 ยท (๐โ3)))) + (;72 ยท (๐ ยท ๐
))) = (-(2 ยท (๐โ3)) + (;72 ยท (๐ ยท ๐
)))) |
122 | 100, 110,
121 | 3eqtrd 2781 |
. . . 4
โข (๐ โ ((2 ยท ((2 ยท
๐)โ3)) โ (9
ยท ((2 ยท ๐)
ยท ((๐โ2)
โ (4 ยท ๐
)))))
= (-(2 ยท (๐โ3))
+ (;72 ยท (๐ ยท ๐
)))) |
123 | | 7nn 12252 |
. . . . . . 7
โข 7 โ
โ |
124 | 79, 123 | decnncl 12645 |
. . . . . 6
โข ;27 โ โ |
125 | 124 | nncni 12170 |
. . . . 5
โข ;27 โ โ |
126 | | quartlem1.q |
. . . . . 6
โข (๐ โ ๐ โ โ) |
127 | 126 | sqcld 14056 |
. . . . 5
โข (๐ โ (๐โ2) โ โ) |
128 | | mulneg2 11599 |
. . . . 5
โข ((;27 โ โ โง (๐โ2) โ โ) โ
(;27 ยท -(๐โ2)) = -(;27 ยท (๐โ2))) |
129 | 125, 127,
128 | sylancr 588 |
. . . 4
โข (๐ โ (;27 ยท -(๐โ2)) = -(;27 ยท (๐โ2))) |
130 | 122, 129 | oveq12d 7380 |
. . 3
โข (๐ โ (((2 ยท ((2 ยท
๐)โ3)) โ (9
ยท ((2 ยท ๐)
ยท ((๐โ2)
โ (4 ยท ๐
)))))
+ (;27 ยท -(๐โ2))) = ((-(2 ยท
(๐โ3)) + (;72 ยท (๐ ยท ๐
))) + -(;27 ยท (๐โ2)))) |
131 | 69 | negcld 11506 |
. . . . 5
โข (๐ โ -(2 ยท (๐โ3)) โ
โ) |
132 | | mulcl 11142 |
. . . . . 6
โข ((;27 โ โ โง (๐โ2) โ โ) โ
(;27 ยท (๐โ2)) โ โ) |
133 | 125, 127,
132 | sylancr 588 |
. . . . 5
โข (๐ โ (;27 ยท (๐โ2)) โ โ) |
134 | 131, 109,
133 | addsubd 11540 |
. . . 4
โข (๐ โ ((-(2 ยท (๐โ3)) + (;72 ยท (๐ ยท ๐
))) โ (;27 ยท (๐โ2))) = ((-(2 ยท (๐โ3)) โ (;27 ยท (๐โ2))) + (;72 ยท (๐ ยท ๐
)))) |
135 | 131, 109 | addcld 11181 |
. . . . 5
โข (๐ โ (-(2 ยท (๐โ3)) + (;72 ยท (๐ ยท ๐
))) โ โ) |
136 | 135, 133 | negsubd 11525 |
. . . 4
โข (๐ โ ((-(2 ยท (๐โ3)) + (;72 ยท (๐ ยท ๐
))) + -(;27 ยท (๐โ2))) = ((-(2 ยท (๐โ3)) + (;72 ยท (๐ ยท ๐
))) โ (;27 ยท (๐โ2)))) |
137 | | quartlem1.v |
. . . 4
โข (๐ โ ๐ = ((-(2 ยท (๐โ3)) โ (;27 ยท (๐โ2))) + (;72 ยท (๐ ยท ๐
)))) |
138 | 134, 136,
137 | 3eqtr4d 2787 |
. . 3
โข (๐ โ ((-(2 ยท (๐โ3)) + (;72 ยท (๐ ยท ๐
))) + -(;27 ยท (๐โ2))) = ๐) |
139 | 130, 138 | eqtr2d 2778 |
. 2
โข (๐ โ ๐ = (((2 ยท ((2 ยท ๐)โ3)) โ (9 ยท
((2 ยท ๐) ยท
((๐โ2) โ (4
ยท ๐
))))) + (;27 ยท -(๐โ2)))) |
140 | 51, 139 | jca 513 |
1
โข (๐ โ (๐ = (((2 ยท ๐)โ2) โ (3 ยท ((๐โ2) โ (4 ยท
๐
)))) โง ๐ = (((2 ยท ((2 ยท
๐)โ3)) โ (9
ยท ((2 ยท ๐)
ยท ((๐โ2)
โ (4 ยท ๐
)))))
+ (;27 ยท -(๐โ2))))) |