Metamath Proof Explorer

Theorem quartlem1

Description: Lemma for quart . (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quartlem1.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚ )
quartlem1.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚ )
quartlem1.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„‚ )
quartlem1.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ( ๐‘ƒ โ†‘ 2 ) + ( 1 2 ยท ๐‘… ) ) )
quartlem1.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
Assertion quartlem1 ( ๐œ‘ โ†’ ( ๐‘ˆ = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) โˆง ๐‘‰ = ( ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) + ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quartlem1.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚ )
2 quartlem1.q โŠข ( ๐œ‘ โ†’ ๐‘„ โˆˆ โ„‚ )
3 quartlem1.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„‚ )
4 quartlem1.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ( ๐‘ƒ โ†‘ 2 ) + ( 1 2 ยท ๐‘… ) ) )
5 quartlem1.v โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
6 2cn โŠข 2 โˆˆ โ„‚
7 sqmul โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ ) โ†’ ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) = ( ( 2 โ†‘ 2 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) )
8 6 1 7 sylancr โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) = ( ( 2 โ†‘ 2 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) )
9 sq2 โŠข ( 2 โ†‘ 2 ) = 4
10 9 oveq1i โŠข ( ( 2 โ†‘ 2 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( 4 ยท ( ๐‘ƒ โ†‘ 2 ) )
11 8 10 eqtrdi โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) = ( 4 ยท ( ๐‘ƒ โ†‘ 2 ) ) )
12 11 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) = ( ( 4 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) )
13 4cn โŠข 4 โˆˆ โ„‚
14 13 a1i โŠข ( ๐œ‘ โ†’ 4 โˆˆ โ„‚ )
15 3cn โŠข 3 โˆˆ โ„‚
16 15 a1i โŠข ( ๐œ‘ โ†’ 3 โˆˆ โ„‚ )
17 1 sqcld โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โ†‘ 2 ) โˆˆ โ„‚ )
18 14 16 17 subdird โŠข ( ๐œ‘ โ†’ ( ( 4 โˆ’ 3 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( ( 4 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) )
19 12 18 eqtr4d โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) = ( ( 4 โˆ’ 3 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) )
20 ax-1cn โŠข 1 โˆˆ โ„‚
21 3p1e4 โŠข ( 3 + 1 ) = 4
22 13 15 20 21 subaddrii โŠข ( 4 โˆ’ 3 ) = 1
23 22 oveq1i โŠข ( ( 4 โˆ’ 3 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( 1 ยท ( ๐‘ƒ โ†‘ 2 ) )
24 mullid โŠข ( ( ๐‘ƒ โ†‘ 2 ) โˆˆ โ„‚ โ†’ ( 1 ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( ๐‘ƒ โ†‘ 2 ) )
25 23 24 eqtrid โŠข ( ( ๐‘ƒ โ†‘ 2 ) โˆˆ โ„‚ โ†’ ( ( 4 โˆ’ 3 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( ๐‘ƒ โ†‘ 2 ) )
26 17 25 syl โŠข ( ๐œ‘ โ†’ ( ( 4 โˆ’ 3 ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( ๐‘ƒ โ†‘ 2 ) )
27 19 26 eqtr2d โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โ†‘ 2 ) = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) )
28 27 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ โ†‘ 2 ) + ( 1 2 ยท ๐‘… ) ) = ( ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) + ( 1 2 ยท ๐‘… ) ) )
29 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘ƒ โˆˆ โ„‚ ) โ†’ ( 2 ยท ๐‘ƒ ) โˆˆ โ„‚ )
30 6 1 29 sylancr โŠข ( ๐œ‘ โ†’ ( 2 ยท ๐‘ƒ ) โˆˆ โ„‚ )
31 30 sqcld โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆˆ โ„‚ )
32 mulcl โŠข ( ( 3 โˆˆ โ„‚ โˆง ( ๐‘ƒ โ†‘ 2 ) โˆˆ โ„‚ ) โ†’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆˆ โ„‚ )
33 15 17 32 sylancr โŠข ( ๐œ‘ โ†’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆˆ โ„‚ )
34 1nn0 โŠข 1 โˆˆ โ„•0
35 2nn โŠข 2 โˆˆ โ„•
36 34 35 decnncl โŠข 1 2 โˆˆ โ„•
37 36 nncni โŠข 1 2 โˆˆ โ„‚
38 mulcl โŠข ( ( 1 2 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚ ) โ†’ ( 1 2 ยท ๐‘… ) โˆˆ โ„‚ )
39 37 3 38 sylancr โŠข ( ๐œ‘ โ†’ ( 1 2 ยท ๐‘… ) โˆˆ โ„‚ )
40 31 33 39 subsubd โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 1 2 ยท ๐‘… ) ) ) = ( ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) ) + ( 1 2 ยท ๐‘… ) ) )
41 28 40 eqtr4d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ โ†‘ 2 ) + ( 1 2 ยท ๐‘… ) ) = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 1 2 ยท ๐‘… ) ) ) )
42 mulcl โŠข ( ( 4 โˆˆ โ„‚ โˆง ๐‘… โˆˆ โ„‚ ) โ†’ ( 4 ยท ๐‘… ) โˆˆ โ„‚ )
43 13 3 42 sylancr โŠข ( ๐œ‘ โ†’ ( 4 ยท ๐‘… ) โˆˆ โ„‚ )
44 16 17 43 subdid โŠข ( ๐œ‘ โ†’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) = ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 3 ยท ( 4 ยท ๐‘… ) ) ) )
45 4t3e12 โŠข ( 4 ยท 3 ) = 1 2
46 13 15 45 mulcomli โŠข ( 3 ยท 4 ) = 1 2
47 46 oveq1i โŠข ( ( 3 ยท 4 ) ยท ๐‘… ) = ( 1 2 ยท ๐‘… )
48 16 14 3 mulassd โŠข ( ๐œ‘ โ†’ ( ( 3 ยท 4 ) ยท ๐‘… ) = ( 3 ยท ( 4 ยท ๐‘… ) ) )
49 47 48 eqtr3id โŠข ( ๐œ‘ โ†’ ( 1 2 ยท ๐‘… ) = ( 3 ยท ( 4 ยท ๐‘… ) ) )
50 49 oveq2d โŠข ( ๐œ‘ โ†’ ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 1 2 ยท ๐‘… ) ) = ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 3 ยท ( 4 ยท ๐‘… ) ) ) )
51 44 50 eqtr4d โŠข ( ๐œ‘ โ†’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) = ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 1 2 ยท ๐‘… ) ) )
52 51 oveq2d โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( ( 3 ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( 1 2 ยท ๐‘… ) ) ) )
53 41 4 52 3eqtr4d โŠข ( ๐œ‘ โ†’ ๐‘ˆ = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) )
54 6 a1i โŠข ( ๐œ‘ โ†’ 2 โˆˆ โ„‚ )
55 3nn0 โŠข 3 โˆˆ โ„•0
56 55 a1i โŠข ( ๐œ‘ โ†’ 3 โˆˆ โ„•0 )
57 54 1 56 mulexpd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) = ( ( 2 โ†‘ 3 ) ยท ( ๐‘ƒ โ†‘ 3 ) ) )
58 cu2 โŠข ( 2 โ†‘ 3 ) = 8
59 58 oveq1i โŠข ( ( 2 โ†‘ 3 ) ยท ( ๐‘ƒ โ†‘ 3 ) ) = ( 8 ยท ( ๐‘ƒ โ†‘ 3 ) )
60 57 59 eqtrdi โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) = ( 8 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
61 60 oveq2d โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) = ( 2 ยท ( 8 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) )
62 8cn โŠข 8 โˆˆ โ„‚
63 62 a1i โŠข ( ๐œ‘ โ†’ 8 โˆˆ โ„‚ )
64 expcl โŠข ( ( ๐‘ƒ โˆˆ โ„‚ โˆง 3 โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ โ†‘ 3 ) โˆˆ โ„‚ )
65 1 55 64 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โ†‘ 3 ) โˆˆ โ„‚ )
66 54 63 65 mul12d โŠข ( ๐œ‘ โ†’ ( 2 ยท ( 8 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) = ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) )
67 61 66 eqtrd โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) = ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) )
68 9cn โŠข 9 โˆˆ โ„‚
69 68 a1i โŠข ( ๐œ‘ โ†’ 9 โˆˆ โ„‚ )
70 mulcl โŠข ( ( 2 โˆˆ โ„‚ โˆง ( ๐‘ƒ โ†‘ 3 ) โˆˆ โ„‚ ) โ†’ ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆˆ โ„‚ )
71 6 65 70 sylancr โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆˆ โ„‚ )
72 1 3 mulcld โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ๐‘… ) โˆˆ โ„‚ )
73 mulcl โŠข ( ( 8 โˆˆ โ„‚ โˆง ( ๐‘ƒ ยท ๐‘… ) โˆˆ โ„‚ ) โ†’ ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) โˆˆ โ„‚ )
74 62 72 73 sylancr โŠข ( ๐œ‘ โ†’ ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) โˆˆ โ„‚ )
75 69 71 74 subdid โŠข ( ๐œ‘ โ†’ ( 9 ยท ( ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) ) = ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 9 ยท ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) ) )
76 30 17 43 subdid โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) = ( ( ( 2 ยท ๐‘ƒ ) ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( ( 2 ยท ๐‘ƒ ) ยท ( 4 ยท ๐‘… ) ) ) )
77 54 1 17 mulassd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( 2 ยท ( ๐‘ƒ ยท ( ๐‘ƒ โ†‘ 2 ) ) ) )
78 1 17 mulcomd โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( ( ๐‘ƒ โ†‘ 2 ) ยท ๐‘ƒ ) )
79 df-3 โŠข 3 = ( 2 + 1 )
80 79 oveq2i โŠข ( ๐‘ƒ โ†‘ 3 ) = ( ๐‘ƒ โ†‘ ( 2 + 1 ) )
81 2nn0 โŠข 2 โˆˆ โ„•0
82 expp1 โŠข ( ( ๐‘ƒ โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0 ) โ†’ ( ๐‘ƒ โ†‘ ( 2 + 1 ) ) = ( ( ๐‘ƒ โ†‘ 2 ) ยท ๐‘ƒ ) )
83 1 81 82 sylancl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โ†‘ ( 2 + 1 ) ) = ( ( ๐‘ƒ โ†‘ 2 ) ยท ๐‘ƒ ) )
84 80 83 eqtrid โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โ†‘ 3 ) = ( ( ๐‘ƒ โ†‘ 2 ) ยท ๐‘ƒ ) )
85 78 84 eqtr4d โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( ๐‘ƒ โ†‘ 3 ) )
86 85 oveq2d โŠข ( ๐œ‘ โ†’ ( 2 ยท ( ๐‘ƒ ยท ( ๐‘ƒ โ†‘ 2 ) ) ) = ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
87 77 86 eqtrd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) ยท ( ๐‘ƒ โ†‘ 2 ) ) = ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
88 54 1 14 3 mul4d โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) ยท ( 4 ยท ๐‘… ) ) = ( ( 2 ยท 4 ) ยท ( ๐‘ƒ ยท ๐‘… ) ) )
89 4t2e8 โŠข ( 4 ยท 2 ) = 8
90 13 6 89 mulcomli โŠข ( 2 ยท 4 ) = 8
91 90 oveq1i โŠข ( ( 2 ยท 4 ) ยท ( ๐‘ƒ ยท ๐‘… ) ) = ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) )
92 88 91 eqtrdi โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) ยท ( 4 ยท ๐‘… ) ) = ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) )
93 87 92 oveq12d โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ๐‘ƒ ) ยท ( ๐‘ƒ โ†‘ 2 ) ) โˆ’ ( ( 2 ยท ๐‘ƒ ) ยท ( 4 ยท ๐‘… ) ) ) = ( ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
94 76 93 eqtrd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) = ( ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
95 94 oveq2d โŠข ( ๐œ‘ โ†’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) = ( 9 ยท ( ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) ) )
96 9t8e72 โŠข ( 9 ยท 8 ) = 7 2
97 96 oveq1i โŠข ( ( 9 ยท 8 ) ยท ( ๐‘ƒ ยท ๐‘… ) ) = ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) )
98 69 63 72 mulassd โŠข ( ๐œ‘ โ†’ ( ( 9 ยท 8 ) ยท ( ๐‘ƒ ยท ๐‘… ) ) = ( 9 ยท ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
99 97 98 eqtr3id โŠข ( ๐œ‘ โ†’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) = ( 9 ยท ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
100 99 oveq2d โŠข ( ๐œ‘ โ†’ ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) = ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 9 ยท ( 8 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) ) )
101 75 95 100 3eqtr4d โŠข ( ๐œ‘ โ†’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) = ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
102 67 101 oveq12d โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) = ( ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) ) )
103 mulcl โŠข ( ( 8 โˆˆ โ„‚ โˆง ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆˆ โ„‚ ) โ†’ ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆˆ โ„‚ )
104 62 71 103 sylancr โŠข ( ๐œ‘ โ†’ ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆˆ โ„‚ )
105 mulcl โŠข ( ( 9 โˆˆ โ„‚ โˆง ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆˆ โ„‚ ) โ†’ ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆˆ โ„‚ )
106 68 71 105 sylancr โŠข ( ๐œ‘ โ†’ ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆˆ โ„‚ )
107 7nn0 โŠข 7 โˆˆ โ„•0
108 107 35 decnncl โŠข 7 2 โˆˆ โ„•
109 108 nncni โŠข 7 2 โˆˆ โ„‚
110 mulcl โŠข ( ( 7 2 โˆˆ โ„‚ โˆง ( ๐‘ƒ ยท ๐‘… ) โˆˆ โ„‚ ) โ†’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) โˆˆ โ„‚ )
111 109 72 110 sylancr โŠข ( ๐œ‘ โ†’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) โˆˆ โ„‚ )
112 104 106 111 subsubd โŠข ( ๐œ‘ โ†’ ( ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) ) = ( ( ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
113 106 104 negsubdi2d โŠข ( ๐œ‘ โ†’ - ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) = ( ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) )
114 69 63 71 subdird โŠข ( ๐œ‘ โ†’ ( ( 9 โˆ’ 8 ) ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) = ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) )
115 8p1e9 โŠข ( 8 + 1 ) = 9
116 68 62 20 115 subaddrii โŠข ( 9 โˆ’ 8 ) = 1
117 116 oveq1i โŠข ( ( 9 โˆ’ 8 ) ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) = ( 1 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
118 71 mullidd โŠข ( ๐œ‘ โ†’ ( 1 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) = ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
119 117 118 eqtrid โŠข ( ๐œ‘ โ†’ ( ( 9 โˆ’ 8 ) ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) = ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
120 114 119 eqtr3d โŠข ( ๐œ‘ โ†’ ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) = ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
121 120 negeqd โŠข ( ๐œ‘ โ†’ - ( ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) = - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
122 113 121 eqtr3d โŠข ( ๐œ‘ โ†’ ( ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) = - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) )
123 122 oveq1d โŠข ( ๐œ‘ โ†’ ( ( ( 8 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) โˆ’ ( 9 ยท ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) = ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
124 102 112 123 3eqtrd โŠข ( ๐œ‘ โ†’ ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) = ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
125 7nn โŠข 7 โˆˆ โ„•
126 81 125 decnncl โŠข 2 7 โˆˆ โ„•
127 126 nncni โŠข 2 7 โˆˆ โ„‚
128 2 sqcld โŠข ( ๐œ‘ โ†’ ( ๐‘„ โ†‘ 2 ) โˆˆ โ„‚ )
129 mulneg2 โŠข ( ( 2 7 โˆˆ โ„‚ โˆง ( ๐‘„ โ†‘ 2 ) โˆˆ โ„‚ ) โ†’ ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) = - ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) )
130 127 128 129 sylancr โŠข ( ๐œ‘ โ†’ ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) = - ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) )
131 124 130 oveq12d โŠข ( ๐œ‘ โ†’ ( ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) + ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) ) = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) + - ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) )
132 71 negcld โŠข ( ๐œ‘ โ†’ - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆˆ โ„‚ )
133 mulcl โŠข ( ( 2 7 โˆˆ โ„‚ โˆง ( ๐‘„ โ†‘ 2 ) โˆˆ โ„‚ ) โ†’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) โˆˆ โ„‚ )
134 127 128 133 sylancr โŠข ( ๐œ‘ โ†’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) โˆˆ โ„‚ )
135 132 111 134 addsubd โŠข ( ๐œ‘ โ†’ ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) )
136 132 111 addcld โŠข ( ๐œ‘ โ†’ ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) โˆˆ โ„‚ )
137 136 134 negsubd โŠข ( ๐œ‘ โ†’ ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) + - ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) = ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) โˆ’ ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) )
138 135 137 5 3eqtr4d โŠข ( ๐œ‘ โ†’ ( ( - ( 2 ยท ( ๐‘ƒ โ†‘ 3 ) ) + ( 7 2 ยท ( ๐‘ƒ ยท ๐‘… ) ) ) + - ( 2 7 ยท ( ๐‘„ โ†‘ 2 ) ) ) = ๐‘‰ )
139 131 138 eqtr2d โŠข ( ๐œ‘ โ†’ ๐‘‰ = ( ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) + ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) ) )
140 53 139 jca โŠข ( ๐œ‘ โ†’ ( ๐‘ˆ = ( ( ( 2 ยท ๐‘ƒ ) โ†‘ 2 ) โˆ’ ( 3 ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) โˆง ๐‘‰ = ( ( ( 2 ยท ( ( 2 ยท ๐‘ƒ ) โ†‘ 3 ) ) โˆ’ ( 9 ยท ( ( 2 ยท ๐‘ƒ ) ยท ( ( ๐‘ƒ โ†‘ 2 ) โˆ’ ( 4 ยท ๐‘… ) ) ) ) ) + ( 2 7 ยท - ( ๐‘„ โ†‘ 2 ) ) ) ) )