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

Theorem quartlem1 26362
Description: Lemma for quart 26366. (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 12287 . . . . . . . . . 10 2 โˆˆ โ„‚
2 quartlem1.p . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
3 sqmul 14084 . . . . . . . . . 10 ((2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚) โ†’ ((2 ยท ๐‘ƒ)โ†‘2) = ((2โ†‘2) ยท (๐‘ƒโ†‘2)))
41, 2, 3sylancr 588 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘2) = ((2โ†‘2) ยท (๐‘ƒโ†‘2)))
5 sq2 14161 . . . . . . . . . 10 (2โ†‘2) = 4
65oveq1i 7419 . . . . . . . . 9 ((2โ†‘2) ยท (๐‘ƒโ†‘2)) = (4 ยท (๐‘ƒโ†‘2))
74, 6eqtrdi 2789 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘2) = (4 ยท (๐‘ƒโ†‘2)))
87oveq1d 7424 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) = ((4 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (๐‘ƒโ†‘2))))
9 4cn 12297 . . . . . . . . 9 4 โˆˆ โ„‚
109a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 4 โˆˆ โ„‚)
11 3cn 12293 . . . . . . . . 9 3 โˆˆ โ„‚
1211a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
132sqcld 14109 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒโ†‘2) โˆˆ โ„‚)
1410, 12, 13subdird 11671 . . . . . . 7 (๐œ‘ โ†’ ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = ((4 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (๐‘ƒโ†‘2))))
158, 14eqtr4d 2776 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) = ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)))
16 ax-1cn 11168 . . . . . . . . . 10 1 โˆˆ โ„‚
17 3p1e4 12357 . . . . . . . . . 10 (3 + 1) = 4
189, 11, 16, 17subaddrii 11549 . . . . . . . . 9 (4 โˆ’ 3) = 1
1918oveq1i 7419 . . . . . . . 8 ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = (1 ยท (๐‘ƒโ†‘2))
20 mullid 11213 . . . . . . . 8 ((๐‘ƒโ†‘2) โˆˆ โ„‚ โ†’ (1 ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘2))
2119, 20eqtrid 2785 . . . . . . 7 ((๐‘ƒโ†‘2) โˆˆ โ„‚ โ†’ ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘2))
2213, 21syl 17 . . . . . 6 (๐œ‘ โ†’ ((4 โˆ’ 3) ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘2))
2315, 22eqtr2d 2774 . . . . 5 (๐œ‘ โ†’ (๐‘ƒโ†‘2) = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))))
2423oveq1d 7424 . . . 4 (๐œ‘ โ†’ ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)) = ((((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) + (12 ยท ๐‘…)))
25 mulcl 11194 . . . . . . 7 ((2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚) โ†’ (2 ยท ๐‘ƒ) โˆˆ โ„‚)
261, 2, 25sylancr 588 . . . . . 6 (๐œ‘ โ†’ (2 ยท ๐‘ƒ) โˆˆ โ„‚)
2726sqcld 14109 . . . . 5 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘2) โˆˆ โ„‚)
28 mulcl 11194 . . . . . 6 ((3 โˆˆ โ„‚ โˆง (๐‘ƒโ†‘2) โˆˆ โ„‚) โ†’ (3 ยท (๐‘ƒโ†‘2)) โˆˆ โ„‚)
2911, 13, 28sylancr 588 . . . . 5 (๐œ‘ โ†’ (3 ยท (๐‘ƒโ†‘2)) โˆˆ โ„‚)
30 1nn0 12488 . . . . . . . 8 1 โˆˆ โ„•0
31 2nn 12285 . . . . . . . 8 2 โˆˆ โ„•
3230, 31decnncl 12697 . . . . . . 7 12 โˆˆ โ„•
3332nncni 12222 . . . . . 6 12 โˆˆ โ„‚
34 quartlem1.r . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
35 mulcl 11194 . . . . . 6 ((12 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚) โ†’ (12 ยท ๐‘…) โˆˆ โ„‚)
3633, 34, 35sylancr 588 . . . . 5 (๐œ‘ โ†’ (12 ยท ๐‘…) โˆˆ โ„‚)
3727, 29, 36subsubd 11599 . . . 4 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…))) = ((((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท (๐‘ƒโ†‘2))) + (12 ยท ๐‘…)))
3824, 37eqtr4d 2776 . . 3 (๐œ‘ โ†’ ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)) = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…))))
39 quartlem1.u . . 3 (๐œ‘ โ†’ ๐‘ˆ = ((๐‘ƒโ†‘2) + (12 ยท ๐‘…)))
40 mulcl 11194 . . . . . . 7 ((4 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚) โ†’ (4 ยท ๐‘…) โˆˆ โ„‚)
419, 34, 40sylancr 588 . . . . . 6 (๐œ‘ โ†’ (4 ยท ๐‘…) โˆˆ โ„‚)
4212, 13, 41subdid 11670 . . . . 5 (๐œ‘ โ†’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (4 ยท ๐‘…))))
43 4t3e12 12775 . . . . . . . . 9 (4 ยท 3) = 12
449, 11, 43mulcomli 11223 . . . . . . . 8 (3 ยท 4) = 12
4544oveq1i 7419 . . . . . . 7 ((3 ยท 4) ยท ๐‘…) = (12 ยท ๐‘…)
4612, 10, 34mulassd 11237 . . . . . . 7 (๐œ‘ โ†’ ((3 ยท 4) ยท ๐‘…) = (3 ยท (4 ยท ๐‘…)))
4745, 46eqtr3id 2787 . . . . . 6 (๐œ‘ โ†’ (12 ยท ๐‘…) = (3 ยท (4 ยท ๐‘…)))
4847oveq2d 7425 . . . . 5 (๐œ‘ โ†’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…)) = ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (3 ยท (4 ยท ๐‘…))))
4942, 48eqtr4d 2776 . . . 4 (๐œ‘ โ†’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…)))
5049oveq2d 7425 . . 3 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ ((3 ยท (๐‘ƒโ†‘2)) โˆ’ (12 ยท ๐‘…))))
5138, 39, 503eqtr4d 2783 . 2 (๐œ‘ โ†’ ๐‘ˆ = (((2 ยท ๐‘ƒ)โ†‘2) โˆ’ (3 ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))))
521a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
53 3nn0 12490 . . . . . . . . . . 11 3 โˆˆ โ„•0
5453a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
5552, 2, 54mulexpd 14126 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘3) = ((2โ†‘3) ยท (๐‘ƒโ†‘3)))
56 cu2 14164 . . . . . . . . . 10 (2โ†‘3) = 8
5756oveq1i 7419 . . . . . . . . 9 ((2โ†‘3) ยท (๐‘ƒโ†‘3)) = (8 ยท (๐‘ƒโ†‘3))
5855, 57eqtrdi 2789 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ)โ†‘3) = (8 ยท (๐‘ƒโ†‘3)))
5958oveq2d 7425 . . . . . . 7 (๐œ‘ โ†’ (2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) = (2 ยท (8 ยท (๐‘ƒโ†‘3))))
60 8cn 12309 . . . . . . . . 9 8 โˆˆ โ„‚
6160a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 8 โˆˆ โ„‚)
62 expcl 14045 . . . . . . . . 9 ((๐‘ƒ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0) โ†’ (๐‘ƒโ†‘3) โˆˆ โ„‚)
632, 53, 62sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ƒโ†‘3) โˆˆ โ„‚)
6452, 61, 63mul12d 11423 . . . . . . 7 (๐œ‘ โ†’ (2 ยท (8 ยท (๐‘ƒโ†‘3))) = (8 ยท (2 ยท (๐‘ƒโ†‘3))))
6559, 64eqtrd 2773 . . . . . 6 (๐œ‘ โ†’ (2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) = (8 ยท (2 ยท (๐‘ƒโ†‘3))))
66 9cn 12312 . . . . . . . . 9 9 โˆˆ โ„‚
6766a1i 11 . . . . . . . 8 (๐œ‘ โ†’ 9 โˆˆ โ„‚)
68 mulcl 11194 . . . . . . . . 9 ((2 โˆˆ โ„‚ โˆง (๐‘ƒโ†‘3) โˆˆ โ„‚) โ†’ (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚)
691, 63, 68sylancr 588 . . . . . . . 8 (๐œ‘ โ†’ (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚)
702, 34mulcld 11234 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘…) โˆˆ โ„‚)
71 mulcl 11194 . . . . . . . . 9 ((8 โˆˆ โ„‚ โˆง (๐‘ƒ ยท ๐‘…) โˆˆ โ„‚) โ†’ (8 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
7260, 70, 71sylancr 588 . . . . . . . 8 (๐œ‘ โ†’ (8 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
7367, 69, 72subdid 11670 . . . . . . 7 (๐œ‘ โ†’ (9 ยท ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…)))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…)))))
7426, 13, 41subdid 11670 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = (((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) โˆ’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…))))
7552, 2, 13mulassd 11237 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) = (2 ยท (๐‘ƒ ยท (๐‘ƒโ†‘2))))
762, 13mulcomd 11235 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ƒ ยท (๐‘ƒโ†‘2)) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
77 df-3 12276 . . . . . . . . . . . . . . 15 3 = (2 + 1)
7877oveq2i 7420 . . . . . . . . . . . . . 14 (๐‘ƒโ†‘3) = (๐‘ƒโ†‘(2 + 1))
79 2nn0 12489 . . . . . . . . . . . . . . 15 2 โˆˆ โ„•0
80 expp1 14034 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (๐‘ƒโ†‘(2 + 1)) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
812, 79, 80sylancl 587 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ƒโ†‘(2 + 1)) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
8278, 81eqtrid 2785 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘ƒโ†‘3) = ((๐‘ƒโ†‘2) ยท ๐‘ƒ))
8376, 82eqtr4d 2776 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ƒ ยท (๐‘ƒโ†‘2)) = (๐‘ƒโ†‘3))
8483oveq2d 7425 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (๐‘ƒ ยท (๐‘ƒโ†‘2))) = (2 ยท (๐‘ƒโ†‘3)))
8575, 84eqtrd 2773 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) = (2 ยท (๐‘ƒโ†‘3)))
8652, 2, 10, 34mul4d 11426 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…)) = ((2 ยท 4) ยท (๐‘ƒ ยท ๐‘…)))
87 4t2e8 12380 . . . . . . . . . . . . 13 (4 ยท 2) = 8
889, 1, 87mulcomli 11223 . . . . . . . . . . . 12 (2 ยท 4) = 8
8988oveq1i 7419 . . . . . . . . . . 11 ((2 ยท 4) ยท (๐‘ƒ ยท ๐‘…)) = (8 ยท (๐‘ƒ ยท ๐‘…))
9086, 89eqtrdi 2789 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…)) = (8 ยท (๐‘ƒ ยท ๐‘…)))
9185, 90oveq12d 7427 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘ƒ) ยท (๐‘ƒโ†‘2)) โˆ’ ((2 ยท ๐‘ƒ) ยท (4 ยท ๐‘…))) = ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…))))
9274, 91eqtrd 2773 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))) = ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…))))
9392oveq2d 7425 . . . . . . 7 (๐œ‘ โ†’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) = (9 ยท ((2 ยท (๐‘ƒโ†‘3)) โˆ’ (8 ยท (๐‘ƒ ยท ๐‘…)))))
94 9t8e72 12805 . . . . . . . . . 10 (9 ยท 8) = 72
9594oveq1i 7419 . . . . . . . . 9 ((9 ยท 8) ยท (๐‘ƒ ยท ๐‘…)) = (72 ยท (๐‘ƒ ยท ๐‘…))
9667, 61, 70mulassd 11237 . . . . . . . . 9 (๐œ‘ โ†’ ((9 ยท 8) ยท (๐‘ƒ ยท ๐‘…)) = (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…))))
9795, 96eqtr3id 2787 . . . . . . . 8 (๐œ‘ โ†’ (72 ยท (๐‘ƒ ยท ๐‘…)) = (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…))))
9897oveq2d 7425 . . . . . . 7 (๐œ‘ โ†’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (8 ยท (๐‘ƒ ยท ๐‘…)))))
9973, 93, 983eqtr4d 2783 . . . . . 6 (๐œ‘ โ†’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…)))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…))))
10065, 99oveq12d 7427 . . . . 5 (๐œ‘ โ†’ ((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) = ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…)))))
101 mulcl 11194 . . . . . . 7 ((8 โˆˆ โ„‚ โˆง (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚) โ†’ (8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
10260, 69, 101sylancr 588 . . . . . 6 (๐œ‘ โ†’ (8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
103 mulcl 11194 . . . . . . 7 ((9 โˆˆ โ„‚ โˆง (2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚) โ†’ (9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
10466, 69, 103sylancr 588 . . . . . 6 (๐œ‘ โ†’ (9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆˆ โ„‚)
105 7nn0 12494 . . . . . . . . 9 7 โˆˆ โ„•0
106105, 31decnncl 12697 . . . . . . . 8 72 โˆˆ โ„•
107106nncni 12222 . . . . . . 7 72 โˆˆ โ„‚
108 mulcl 11194 . . . . . . 7 ((72 โˆˆ โ„‚ โˆง (๐‘ƒ ยท ๐‘…) โˆˆ โ„‚) โ†’ (72 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
109107, 70, 108sylancr 588 . . . . . 6 (๐œ‘ โ†’ (72 ยท (๐‘ƒ ยท ๐‘…)) โˆˆ โ„‚)
110102, 104, 109subsubd 11599 . . . . 5 (๐œ‘ โ†’ ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (72 ยท (๐‘ƒ ยท ๐‘…)))) = (((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
111104, 102negsubdi2d 11587 . . . . . . 7 (๐œ‘ โ†’ -((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))) = ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))))
11267, 61, 69subdird 11671 . . . . . . . . 9 (๐œ‘ โ†’ ((9 โˆ’ 8) ยท (2 ยท (๐‘ƒโ†‘3))) = ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))))
113 8p1e9 12362 . . . . . . . . . . . 12 (8 + 1) = 9
11466, 60, 16, 113subaddrii 11549 . . . . . . . . . . 11 (9 โˆ’ 8) = 1
115114oveq1i 7419 . . . . . . . . . 10 ((9 โˆ’ 8) ยท (2 ยท (๐‘ƒโ†‘3))) = (1 ยท (2 ยท (๐‘ƒโ†‘3)))
11669mullidd 11232 . . . . . . . . . 10 (๐œ‘ โ†’ (1 ยท (2 ยท (๐‘ƒโ†‘3))) = (2 ยท (๐‘ƒโ†‘3)))
117115, 116eqtrid 2785 . . . . . . . . 9 (๐œ‘ โ†’ ((9 โˆ’ 8) ยท (2 ยท (๐‘ƒโ†‘3))) = (2 ยท (๐‘ƒโ†‘3)))
118112, 117eqtr3d 2775 . . . . . . . 8 (๐œ‘ โ†’ ((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))) = (2 ยท (๐‘ƒโ†‘3)))
119118negeqd 11454 . . . . . . 7 (๐œ‘ โ†’ -((9 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (8 ยท (2 ยท (๐‘ƒโ†‘3)))) = -(2 ยท (๐‘ƒโ†‘3)))
120111, 119eqtr3d 2775 . . . . . 6 (๐œ‘ โ†’ ((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))) = -(2 ยท (๐‘ƒโ†‘3)))
121120oveq1d 7424 . . . . 5 (๐œ‘ โ†’ (((8 ยท (2 ยท (๐‘ƒโ†‘3))) โˆ’ (9 ยท (2 ยท (๐‘ƒโ†‘3)))) + (72 ยท (๐‘ƒ ยท ๐‘…))) = (-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))))
122100, 110, 1213eqtrd 2777 . . . 4 (๐œ‘ โ†’ ((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) = (-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))))
123 7nn 12304 . . . . . . 7 7 โˆˆ โ„•
12479, 123decnncl 12697 . . . . . 6 27 โˆˆ โ„•
125124nncni 12222 . . . . 5 27 โˆˆ โ„‚
126 quartlem1.q . . . . . 6 (๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚)
127126sqcld 14109 . . . . 5 (๐œ‘ โ†’ (๐‘„โ†‘2) โˆˆ โ„‚)
128 mulneg2 11651 . . . . 5 ((27 โˆˆ โ„‚ โˆง (๐‘„โ†‘2) โˆˆ โ„‚) โ†’ (27 ยท -(๐‘„โ†‘2)) = -(27 ยท (๐‘„โ†‘2)))
129125, 127, 128sylancr 588 . . . 4 (๐œ‘ โ†’ (27 ยท -(๐‘„โ†‘2)) = -(27 ยท (๐‘„โ†‘2)))
130122, 129oveq12d 7427 . . 3 (๐œ‘ โ†’ (((2 ยท ((2 ยท ๐‘ƒ)โ†‘3)) โˆ’ (9 ยท ((2 ยท ๐‘ƒ) ยท ((๐‘ƒโ†‘2) โˆ’ (4 ยท ๐‘…))))) + (27 ยท -(๐‘„โ†‘2))) = ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) + -(27 ยท (๐‘„โ†‘2))))
13169negcld 11558 . . . . 5 (๐œ‘ โ†’ -(2 ยท (๐‘ƒโ†‘3)) โˆˆ โ„‚)
132 mulcl 11194 . . . . . 6 ((27 โˆˆ โ„‚ โˆง (๐‘„โ†‘2) โˆˆ โ„‚) โ†’ (27 ยท (๐‘„โ†‘2)) โˆˆ โ„‚)
133125, 127, 132sylancr 588 . . . . 5 (๐œ‘ โ†’ (27 ยท (๐‘„โ†‘2)) โˆˆ โ„‚)
134131, 109, 133addsubd 11592 . . . 4 (๐œ‘ โ†’ ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) โˆ’ (27 ยท (๐‘„โ†‘2))) = ((-(2 ยท (๐‘ƒโ†‘3)) โˆ’ (27 ยท (๐‘„โ†‘2))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
135131, 109addcld 11233 . . . . 5 (๐œ‘ โ†’ (-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) โˆˆ โ„‚)
136135, 133negsubd 11577 . . . 4 (๐œ‘ โ†’ ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) + -(27 ยท (๐‘„โ†‘2))) = ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) โˆ’ (27 ยท (๐‘„โ†‘2))))
137 quartlem1.v . . . 4 (๐œ‘ โ†’ ๐‘‰ = ((-(2 ยท (๐‘ƒโ†‘3)) โˆ’ (27 ยท (๐‘„โ†‘2))) + (72 ยท (๐‘ƒ ยท ๐‘…))))
138134, 136, 1373eqtr4d 2783 . . 3 (๐œ‘ โ†’ ((-(2 ยท (๐‘ƒโ†‘3)) + (72 ยท (๐‘ƒ ยท ๐‘…))) + -(27 ยท (๐‘„โ†‘2))) = ๐‘‰)
139130, 138eqtr2d 2774 . 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 7409  โ„‚cc 11108  1c1 11111   + caddc 11113   ยท cmul 11115   โˆ’ cmin 11444  -cneg 11445  2c2 12267  3c3 12268  4c4 12269  7c7 12272  8c8 12273  9c9 12274  โ„•0cn0 12472  cdc 12677  โ†‘cexp 14027
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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-seq 13967  df-exp 14028
This theorem is referenced by:  quart  26366
  Copyright terms: Public domain W3C validator