MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  quartlem1 Structured version   Visualization version   GIF version

Theorem quartlem1 26223
Description: Lemma for quart 26227. (Contributed by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
quartlem1.p (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
quartlem1.q (๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚)
quartlem1.r (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
quartlem1.u (๐œ‘ โ†’ ๐‘ˆ = ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)))
quartlem1.v (๐œ‘ โ†’ ๐‘‰ = ((-(2 ยท (๐‘ƒโ†‘3)) โˆ’ (27 ยท (๐‘„โ†‘2))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
Assertion
Ref Expression
quartlem1 (๐œ‘ โ†’ (๐‘ˆ = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) โˆง ๐‘‰ = (((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) + (27 ยท -(๐‘„โ†‘2)))))

Proof of Theorem quartlem1
StepHypRef Expression
1 2cn 12235 . . . . . . . . . 10 2 โˆˆ โ„‚
2 quartlem1.p . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
3 sqmul 14031 . . . . . . . . . 10 ((2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚) โ†’ ((2 ยท ๐‘ƒ)โ†‘2) = ((2โ†‘2) ยท (๐‘ƒโ†‘2)))
41, 2, 3sylancr 588 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘2) = ((2โ†‘2) ยท (๐‘ƒโ†‘2)))
5 sq2 14108 . . . . . . . . . 10 (2โ†‘2) = 4
65oveq1i 7372 . . . . . . . . 9 ((2โ†‘2) ยท (๐‘ƒโ†‘2)) = (4 ยท (๐‘ƒโ†‘2))
74, 6eqtrdi 2793 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘2) = (4 ยท (๐‘ƒโ†‘2)))
87oveq1d 7377 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) = ((4 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (๐‘ƒโ†‘2))))
9 4cn 12245 . . . . . . . . 9 4 โˆˆ โ„‚
109a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 4 โˆˆ โ„‚)
11 3cn 12241 . . . . . . . . 9 3 โˆˆ โ„‚
1211a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
132sqcld 14056 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒโ†‘2) โˆˆ โ„‚)
1410, 12, 13subdird 11619 . . . . . . 7 (๐œ‘ โ†’ ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = ((4 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (๐‘ƒโ†‘2))))
158, 14eqtr4d 2780 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) = ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)))
16 ax-1cn 11116 . . . . . . . . . 10 1 โˆˆ โ„‚
17 3p1e4 12305 . . . . . . . . . 10 (3 + 1) = 4
189, 11, 16, 17subaddrii 11497 . . . . . . . . 9 (4 โˆ’ 3) = 1
1918oveq1i 7372 . . . . . . . 8 ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = (1 ยท (๐‘ƒโ†‘2))
20 mulid2 11161 . . . . . . . 8 ((๐‘ƒโ†‘2) โˆˆ โ„‚ โ†’ (1 ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘2))
2119, 20eqtrid 2789 . . . . . . 7 ((๐‘ƒโ†‘2) โˆˆ โ„‚ โ†’ ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘2))
2213, 21syl 17 . . . . . 6 (๐œ‘ โ†’ ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘2))
2315, 22eqtr2d 2778 . . . . 5 (๐œ‘ โ†’ (๐‘ƒโ†‘2) = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))))
2423oveq1d 7377 . . . 4 (๐œ‘ โ†’ ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)) = ((((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) + (12 ยท ๐‘…)))
25 mulcl 11142 . . . . . . 7 ((2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚) โ†’ (2 ยท ๐‘ƒ) โˆˆ โ„‚)
261, 2, 25sylancr 588 . . . . . 6 (๐œ‘ โ†’ (2 ยท ๐‘ƒ) โˆˆ โ„‚)
2726sqcld 14056 . . . . 5 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘2) โˆˆ โ„‚)
28 mulcl 11142 . . . . . 6 ((3 โˆˆ โ„‚ โˆง (๐‘ƒโ†‘2) โˆˆ โ„‚) โ†’ (3 ยท (๐‘ƒโ†‘2)) โˆˆ โ„‚)
2911, 13, 28sylancr 588 . . . . 5 (๐œ‘ โ†’ (3 ยท (๐‘ƒโ†‘2)) โˆˆ โ„‚)
30 1nn0 12436 . . . . . . . 8 1 โˆˆ โ„•0
31 2nn 12233 . . . . . . . 8 2 โˆˆ โ„•
3230, 31decnncl 12645 . . . . . . 7 12 โˆˆ โ„•
3332nncni 12170 . . . . . 6 12 โˆˆ โ„‚
34 quartlem1.r . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
35 mulcl 11142 . . . . . 6 ((12 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚) โ†’ (12 ยท ๐‘…) โˆˆ โ„‚)
3633, 34, 35sylancr 588 . . . . 5 (๐œ‘ โ†’ (12 ยท ๐‘…) โˆˆ โ„‚)
3727, 29, 36subsubd 11547 . . . 4 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…))) = ((((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) + (12 ยท ๐‘…)))
3824, 37eqtr4d 2780 . . 3 (๐œ‘ โ†’ ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)) = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…))))
39 quartlem1.u . . 3 (๐œ‘ โ†’ ๐‘ˆ = ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)))
40 mulcl 11142 . . . . . . 7 ((4 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚) โ†’ (4 ยท ๐‘…) โˆˆ โ„‚)
419, 34, 40sylancr 588 . . . . . 6 (๐œ‘ โ†’ (4 ยท ๐‘…) โˆˆ โ„‚)
4212, 13, 41subdid 11618 . . . . 5 (๐œ‘ โ†’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (4 ยท ๐‘…))))
43 4t3e12 12723 . . . . . . . . 9 (4 ยท 3) = 12
449, 11, 43mulcomli 11171 . . . . . . . 8 (3 ยท 4) = 12
4544oveq1i 7372 . . . . . . 7 ((3 ยท 4) ยท ๐‘…) = (12 ยท ๐‘…)
4612, 10, 34mulassd 11185 . . . . . . 7 (๐œ‘ โ†’ ((3 ยท 4) ยท ๐‘…) = (3 ยท (4 ยท ๐‘…)))
4745, 46eqtr3id 2791 . . . . . 6 (๐œ‘ โ†’ (12 ยท ๐‘…) = (3 ยท (4 ยท ๐‘…)))
4847oveq2d 7378 . . . . 5 (๐œ‘ โ†’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…)) = ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (4 ยท ๐‘…))))
4942, 48eqtr4d 2780 . . . 4 (๐œ‘ โ†’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…)))
5049oveq2d 7378 . . 3 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…))))
5138, 39, 503eqtr4d 2787 . 2 (๐œ‘ โ†’ ๐‘ˆ = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))))
521a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
53 3nn0 12438 . . . . . . . . . . 11 3 โˆˆ โ„•0
5453a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
5552, 2, 54mulexpd 14073 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘3) = ((2โ†‘3) ยท (๐‘ƒโ†‘3)))
56 cu2 14111 . . . . . . . . . 10 (2โ†‘3) = 8
5756oveq1i 7372 . . . . . . . . 9 ((2โ†‘3) ยท (๐‘ƒโ†‘3)) = (8 ยท (๐‘ƒโ†‘3))
5855, 57eqtrdi 2793 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘3) = (8 ยท (๐‘ƒโ†‘3)))
5958oveq2d 7378 . . . . . . 7 (๐œ‘ โ†’ (2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) = (2 ยท (8 ยท (๐‘ƒโ†‘3))))
60 8cn 12257 . . . . . . . . 9 8 โˆˆ โ„‚
6160a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 8 โˆˆ โ„‚)
62 expcl 13992 . . . . . . . . 9 ((๐‘ƒ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘ƒโ†‘3) โˆˆ โ„‚)
632, 53, 62sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒโ†‘3) โˆˆ โ„‚)
6452, 61, 63mul12d 11371 . . . . . . 7 (๐œ‘ โ†’ (2 ยท (8 ยท (๐‘ƒโ†‘3))) = (8 ยท (2 ยท (๐‘ƒโ†‘3))))
6559, 64eqtrd 2777 . . . . . 6 (๐œ‘ โ†’ (2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) = (8 ยท (2 ยท (๐‘ƒโ†‘3))))
66 9cn 12260 . . . . . . . . 9 9 โˆˆ โ„‚
6766a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 9 โˆˆ โ„‚)
68 mulcl 11142 . . . . . . . . 9 ((2 โˆˆ โ„‚ โˆง (๐‘ƒโ†‘3) โˆˆ โ„‚) โ†’ (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚)
691, 63, 68sylancr 588 . . . . . . . 8 (๐œ‘ โ†’ (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚)
702, 34mulcld 11182 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘…) โˆˆ โ„‚)
71 mulcl 11142 . . . . . . . . 9 ((8 โˆˆ โ„‚ โˆง (๐‘ƒ ยท ๐‘…) โˆˆ โ„‚) โ†’ (8 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
7260, 70, 71sylancr 588 . . . . . . . 8 (๐œ‘ โ†’ (8 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
7367, 69, 72subdid 11618 . . . . . . 7 (๐œ‘ โ†’ (9 ยท ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…)))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…)))))
7426, 13, 41subdid 11618 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = (((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) โˆ’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…))))
7552, 2, 13mulassd 11185 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) = (2 ยท (๐‘ƒ ยท (๐‘ƒโ†‘2))))
762, 13mulcomd 11183 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ƒ ยท (๐‘ƒโ†‘2)) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
77 df-3 12224 . . . . . . . . . . . . . . 15 3 = (2 + 1)
7877oveq2i 7373 . . . . . . . . . . . . . 14 (๐‘ƒโ†‘3) = (๐‘ƒโ†‘(2 + 1))
79 2nn0 12437 . . . . . . . . . . . . . . 15 2 โˆˆ โ„•0
80 expp1 13981 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (๐‘ƒโ†‘(2 + 1)) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
812, 79, 80sylancl 587 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ƒโ†‘(2 + 1)) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
8278, 81eqtrid 2789 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ƒโ†‘3) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
8376, 82eqtr4d 2780 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ƒ ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘3))
8483oveq2d 7378 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (๐‘ƒ ยท (๐‘ƒโ†‘2))) = (2 ยท (๐‘ƒโ†‘3)))
8575, 84eqtrd 2777 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) = (2 ยท (๐‘ƒโ†‘3)))
8652, 2, 10, 34mul4d 11374 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…)) = ((2 ยท 4) ยท (๐‘ƒ ยท ๐‘…)))
87 4t2e8 12328 . . . . . . . . . . . . 13 (4 ยท 2) = 8
889, 1, 87mulcomli 11171 . . . . . . . . . . . 12 (2 ยท 4) = 8
8988oveq1i 7372 . . . . . . . . . . 11 ((2 ยท 4) ยท (๐‘ƒ ยท ๐‘…)) = (8 ยท (๐‘ƒ ยท ๐‘…))
9086, 89eqtrdi 2793 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…)) = (8 ยท (๐‘ƒ ยท ๐‘…)))
9185, 90oveq12d 7380 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) โˆ’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…))) = ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…))))
9274, 91eqtrd 2777 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…))))
9392oveq2d 7378 . . . . . . 7 (๐œ‘ โ†’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) = (9 ยท ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…)))))
94 9t8e72 12753 . . . . . . . . . 10 (9 ยท 8) = 72
9594oveq1i 7372 . . . . . . . . 9 ((9 ยท 8) ยท (๐‘ƒ ยท ๐‘…)) = (72 ยท (๐‘ƒ ยท ๐‘…))
9667, 61, 70mulassd 11185 . . . . . . . . 9 (๐œ‘ โ†’ ((9 ยท 8) ยท (๐‘ƒ ยท ๐‘…)) = (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…))))
9795, 96eqtr3id 2791 . . . . . . . 8 (๐œ‘ โ†’ (72 ยท (๐‘ƒ ยท ๐‘…)) = (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…))))
9897oveq2d 7378 . . . . . . 7 (๐œ‘ โ†’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…)))))
9973, 93, 983eqtr4d 2787 . . . . . 6 (๐œ‘ โ†’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…))))
10065, 99oveq12d 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))) โˆˆ โ„‚)
10260, 69, 101sylancr 588 . . . . . 6 (๐œ‘ โ†’ (8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
103 mulcl 11142 . . . . . . 7 ((9 โˆˆ โ„‚ โˆง (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚) โ†’ (9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
10466, 69, 103sylancr 588 . . . . . 6 (๐œ‘ โ†’ (9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
105 7nn0 12442 . . . . . . . . 9 7 โˆˆ โ„•0
106105, 31decnncl 12645 . . . . . . . 8 72 โˆˆ โ„•
107106nncni 12170 . . . . . . 7 72 โˆˆ โ„‚
108 mulcl 11142 . . . . . . 7 ((72 โˆˆ โ„‚ โˆง (๐‘ƒ ยท ๐‘…) โˆˆ โ„‚) โ†’ (72 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
109107, 70, 108sylancr 588 . . . . . 6 (๐œ‘ โ†’ (72 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
110102, 104, 109subsubd 11547 . . . . 5 (๐œ‘ โ†’ ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…)))) = (((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
111104, 102negsubdi2d 11535 . . . . . . 7 (๐œ‘ โ†’ -((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))) = ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))))
11267, 61, 69subdird 11619 . . . . . . . . 9 (๐œ‘ โ†’ ((9 โˆ’ 8) ยท (2 ยท (๐‘ƒโ†‘3))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))))
113 8p1e9 12310 . . . . . . . . . . . 12 (8 + 1) = 9
11466, 60, 16, 113subaddrii 11497 . . . . . . . . . . 11 (9 โˆ’ 8) = 1
115114oveq1i 7372 . . . . . . . . . 10 ((9 โˆ’ 8) ยท (2 ยท (๐‘ƒโ†‘3))) = (1 ยท (2 ยท (๐‘ƒโ†‘3)))
11669mulid2d 11180 . . . . . . . . . 10 (๐œ‘ โ†’ (1 ยท (2 ยท (๐‘ƒโ†‘3))) = (2 ยท (๐‘ƒโ†‘3)))
117115, 116eqtrid 2789 . . . . . . . . 9 (๐œ‘ โ†’ ((9 โˆ’ 8) ยท (2 ยท (๐‘ƒโ†‘3))) = (2 ยท (๐‘ƒโ†‘3)))
118112, 117eqtr3d 2779 . . . . . . . 8 (๐œ‘ โ†’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))) = (2 ยท (๐‘ƒโ†‘3)))
119118negeqd 11402 . . . . . . 7 (๐œ‘ โ†’ -((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))) = -(2 ยท (๐‘ƒโ†‘3)))
120111, 119eqtr3d 2779 . . . . . 6 (๐œ‘ โ†’ ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))) = -(2 ยท (๐‘ƒโ†‘3)))
121120oveq1d 7377 . . . . 5 (๐œ‘ โ†’ (((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))) + (72 ยท (๐‘ƒ ยท ๐‘…))) = (-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))))
122100, 110, 1213eqtrd 2781 . . . 4 (๐œ‘ โ†’ ((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) = (-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))))
123 7nn 12252 . . . . . . 7 7 โˆˆ โ„•
12479, 123decnncl 12645 . . . . . 6 27 โˆˆ โ„•
125124nncni 12170 . . . . 5 27 โˆˆ โ„‚
126 quartlem1.q . . . . . 6 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚)
127126sqcld 14056 . . . . 5 (๐œ‘ โ†’ (๐‘„โ†‘2) โˆˆ โ„‚)
128 mulneg2 11599 . . . . 5 ((27 โˆˆ โ„‚ โˆง (๐‘„โ†‘2) โˆˆ โ„‚) โ†’ (27 ยท -(๐‘„โ†‘2)) = -(27 ยท (๐‘„โ†‘2)))
129125, 127, 128sylancr 588 . . . 4 (๐œ‘ โ†’ (27 ยท -(๐‘„โ†‘2)) = -(27 ยท (๐‘„โ†‘2)))
130122, 129oveq12d 7380 . . 3 (๐œ‘ โ†’ (((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) + (27 ยท -(๐‘„โ†‘2))) = ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) + -(27 ยท (๐‘„โ†‘2))))
13169negcld 11506 . . . . 5 (๐œ‘ โ†’ -(2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚)
132 mulcl 11142 . . . . . 6 ((27 โˆˆ โ„‚ โˆง (๐‘„โ†‘2) โˆˆ โ„‚) โ†’ (27 ยท (๐‘„โ†‘2)) โˆˆ โ„‚)
133125, 127, 132sylancr 588 . . . . 5 (๐œ‘ โ†’ (27 ยท (๐‘„โ†‘2)) โˆˆ โ„‚)
134131, 109, 133addsubd 11540 . . . 4 (๐œ‘ โ†’ ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) โˆ’ (27 ยท (๐‘„โ†‘2))) = ((-(2 ยท (๐‘ƒโ†‘3)) โˆ’ (27 ยท (๐‘„โ†‘2))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
135131, 109addcld 11181 . . . . 5 (๐œ‘ โ†’ (-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) โˆˆ โ„‚)
136135, 133negsubd 11525 . . . 4 (๐œ‘ โ†’ ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) + -(27 ยท (๐‘„โ†‘2))) = ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) โˆ’ (27 ยท (๐‘„โ†‘2))))
137 quartlem1.v . . . 4 (๐œ‘ โ†’ ๐‘‰ = ((-(2 ยท (๐‘ƒโ†‘3)) โˆ’ (27 ยท (๐‘„โ†‘2))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
138134, 136, 1373eqtr4d 2787 . . 3 (๐œ‘ โ†’ ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) + -(27 ยท (๐‘„โ†‘2))) = ๐‘‰)
139130, 138eqtr2d 2778 . 2 (๐œ‘ โ†’ ๐‘‰ = (((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) + (27 ยท -(๐‘„โ†‘2))))
14051, 139jca 513 1 (๐œ‘ โ†’ (๐‘ˆ = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) โˆง ๐‘‰ = (((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) + (27 ยท -(๐‘„โ†‘2)))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7362  โ„‚cc 11056  1c1 11059   + caddc 11061   ยท cmul 11063   โˆ’ cmin 11392  -cneg 11393  2c2 12215  3c3 12216  4c4 12217  7c7 12220  8c8 12221  9c9 12222  โ„•0cn0 12420  cdc 12625  โ†‘cexp 13974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-seq 13914  df-exp 13975
This theorem is referenced by:  quart  26227
  Copyright terms: Public domain W3C validator