Metamath Proof Explorer

Theorem 3cubeslem2

Description: Lemma for 3cubes . Used to show that the denominators in 3cubeslem4 are nonzero. (Contributed by Igor Ieskov, 22-Jan-2024)

Ref Expression
Hypothesis 3cubeslem1.a 
|- ( ph -> A e. QQ )
Assertion 3cubeslem2 
|- ( ph -> -. ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = 0 )

Proof

Step Hyp Ref Expression
1 3cubeslem1.a 
 |-  ( ph -> A e. QQ )
2 3re 
 |-  3 e. RR
3 2 a1i 
 |-  ( ph -> 3 e. RR )
4 3 recnd 
 |-  ( ph -> 3 e. CC )
5 4 mulid2d 
 |-  ( ph -> ( 1 x. 3 ) = 3 )
6 5 oveq2d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) x. 3 ) + ( 1 x. 3 ) ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) x. 3 ) + 3 ) )
7 4 sqcld 
 |-  ( ph -> ( 3 ^ 2 ) e. CC )
8 qre 
 |-  ( A e. QQ -> A e. RR )
9 1 8 syl 
 |-  ( ph -> A e. RR )
10 9 resqcld 
 |-  ( ph -> ( A ^ 2 ) e. RR )
11 10 recnd 
 |-  ( ph -> ( A ^ 2 ) e. CC )
12 7 11 mulcld 
 |-  ( ph -> ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) e. CC )
13 9 recnd 
 |-  ( ph -> A e. CC )
14 4 13 mulcld 
 |-  ( ph -> ( 3 x. A ) e. CC )
15 12 14 addcld 
 |-  ( ph -> ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) e. CC )
16 1cnd 
 |-  ( ph -> 1 e. CC )
17 15 16 4 adddird 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) x. 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) x. 3 ) + ( 1 x. 3 ) ) )
18 4 13 4 mulassd 
 |-  ( ph -> ( ( 3 x. A ) x. 3 ) = ( 3 x. ( A x. 3 ) ) )
19 18 oveq2d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. A ) x. 3 ) ) = ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( A x. 3 ) ) ) )
20 19 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. A ) x. 3 ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( A x. 3 ) ) ) + 3 ) )
21 12 14 4 adddird 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) x. 3 ) = ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. A ) x. 3 ) ) )
22 21 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) x. 3 ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. A ) x. 3 ) ) + 3 ) )
23 4 4 13 mulassd 
 |-  ( ph -> ( ( 3 x. 3 ) x. A ) = ( 3 x. ( 3 x. A ) ) )
24 23 oveq2d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. 3 ) x. A ) ) = ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( 3 x. A ) ) ) )
25 24 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( 3 x. A ) ) ) + 3 ) )
26 11 4 mulcomd 
 |-  ( ph -> ( ( A ^ 2 ) x. 3 ) = ( 3 x. ( A ^ 2 ) ) )
27 26 oveq2d 
 |-  ( ph -> ( ( 3 ^ 2 ) x. ( ( A ^ 2 ) x. 3 ) ) = ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) )
28 27 oveq1d 
 |-  ( ph -> ( ( ( 3 ^ 2 ) x. ( ( A ^ 2 ) x. 3 ) ) + ( ( 3 x. 3 ) x. A ) ) = ( ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) + ( ( 3 x. 3 ) x. A ) ) )
29 28 oveq1d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( ( A ^ 2 ) x. 3 ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) = ( ( ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
30 7 11 4 mulassd 
 |-  ( ph -> ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) = ( ( 3 ^ 2 ) x. ( ( A ^ 2 ) x. 3 ) ) )
31 30 oveq1d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. 3 ) x. A ) ) = ( ( ( 3 ^ 2 ) x. ( ( A ^ 2 ) x. 3 ) ) + ( ( 3 x. 3 ) x. A ) ) )
32 31 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) = ( ( ( ( 3 ^ 2 ) x. ( ( A ^ 2 ) x. 3 ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
33 df-3 
 |-  3 = ( 2 + 1 )
34 33 a1i 
 |-  ( ph -> 3 = ( 2 + 1 ) )
35 34 oveq2d 
 |-  ( ph -> ( 3 ^ 3 ) = ( 3 ^ ( 2 + 1 ) ) )
36 35 oveq1d 
 |-  ( ph -> ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) = ( ( 3 ^ ( 2 + 1 ) ) x. ( A ^ 2 ) ) )
37 36 oveq1d 
 |-  ( ph -> ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) = ( ( ( 3 ^ ( 2 + 1 ) ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) )
38 37 oveq1d 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( 3 ^ ( 2 + 1 ) ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) )
39 2nn0 
 |-  2 e. NN0
40 39 a1i 
 |-  ( ph -> 2 e. NN0 )
41 4 40 expp1d 
 |-  ( ph -> ( 3 ^ ( 2 + 1 ) ) = ( ( 3 ^ 2 ) x. 3 ) )
42 41 oveq1d 
 |-  ( ph -> ( ( 3 ^ ( 2 + 1 ) ) x. ( A ^ 2 ) ) = ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) )
43 42 oveq1d 
 |-  ( ph -> ( ( ( 3 ^ ( 2 + 1 ) ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) = ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) )
44 43 oveq1d 
 |-  ( ph -> ( ( ( ( 3 ^ ( 2 + 1 ) ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) )
45 38 44 eqtrd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) )
46 4 sqvald 
 |-  ( ph -> ( 3 ^ 2 ) = ( 3 x. 3 ) )
47 46 oveq1d 
 |-  ( ph -> ( ( 3 ^ 2 ) x. A ) = ( ( 3 x. 3 ) x. A ) )
48 47 oveq2d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) = ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 x. 3 ) x. A ) ) )
49 48 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
50 45 49 eqtrd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
51 7 4 11 mulassd 
 |-  ( ph -> ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) = ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) )
52 51 oveq1d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 x. 3 ) x. A ) ) = ( ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) + ( ( 3 x. 3 ) x. A ) ) )
53 52 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. 3 ) x. ( A ^ 2 ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) = ( ( ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
54 50 53 eqtrd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( 3 ^ 2 ) x. ( 3 x. ( A ^ 2 ) ) ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
55 29 32 54 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( ( 3 x. 3 ) x. A ) ) + 3 ) )
56 13 4 mulcomd 
 |-  ( ph -> ( A x. 3 ) = ( 3 x. A ) )
57 56 oveq2d 
 |-  ( ph -> ( 3 x. ( A x. 3 ) ) = ( 3 x. ( 3 x. A ) ) )
58 57 oveq2d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( A x. 3 ) ) ) = ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( 3 x. A ) ) ) )
59 58 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( A x. 3 ) ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( 3 x. A ) ) ) + 3 ) )
60 25 55 59 3eqtr4d 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) x. 3 ) + ( 3 x. ( A x. 3 ) ) ) + 3 ) )
61 20 22 60 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) x. 3 ) + 3 ) )
62 6 17 61 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) x. 3 ) )
63 14 mulid1d 
 |-  ( ph -> ( ( 3 x. A ) x. 1 ) = ( 3 x. A ) )
64 63 oveq2d 
 |-  ( ph -> ( 2 x. ( ( 3 x. A ) x. 1 ) ) = ( 2 x. ( 3 x. A ) ) )
65 64 oveq2d 
 |-  ( ph -> ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( ( 3 x. A ) x. 1 ) ) ) = ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) )
66 65 oveq1d 
 |-  ( ph -> ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( ( 3 x. A ) x. 1 ) ) ) + ( 1 ^ 2 ) ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + ( 1 ^ 2 ) ) )
67 66 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( ( 3 x. A ) x. 1 ) ) ) + ( 1 ^ 2 ) ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + ( 1 ^ 2 ) ) - ( 3 x. A ) ) )
68 14 16 binom2d 
 |-  ( ph -> ( ( ( 3 x. A ) + 1 ) ^ 2 ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( ( 3 x. A ) x. 1 ) ) ) + ( 1 ^ 2 ) ) )
69 68 oveq1d 
 |-  ( ph -> ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( ( 3 x. A ) x. 1 ) ) ) + ( 1 ^ 2 ) ) - ( 3 x. A ) ) )
70 14 2timesd 
 |-  ( ph -> ( 2 x. ( 3 x. A ) ) = ( ( 3 x. A ) + ( 3 x. A ) ) )
71 70 oveq2d 
 |-  ( ph -> ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) = ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) )
72 71 oveq1d 
 |-  ( ph -> ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + 1 ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) + 1 ) )
73 72 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + 1 ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) + 1 ) - ( 3 x. A ) ) )
74 sq1 
 |-  ( 1 ^ 2 ) = 1
75 74 a1i 
 |-  ( ph -> ( 1 ^ 2 ) = 1 )
76 75 oveq2d 
 |-  ( ph -> ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + ( 1 ^ 2 ) ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + 1 ) )
77 76 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + ( 1 ^ 2 ) ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + 1 ) - ( 3 x. A ) ) )
78 14 16 addcomd 
 |-  ( ph -> ( ( 3 x. A ) + 1 ) = ( 1 + ( 3 x. A ) ) )
79 78 oveq2d 
 |-  ( ph -> ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( ( 3 x. A ) + 1 ) ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 1 + ( 3 x. A ) ) ) )
80 79 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( ( 3 x. A ) + 1 ) ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 1 + ( 3 x. A ) ) ) - ( 3 x. A ) ) )
81 4 13 sqmuld 
 |-  ( ph -> ( ( 3 x. A ) ^ 2 ) = ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) )
82 81 12 eqeltrd 
 |-  ( ph -> ( ( 3 x. A ) ^ 2 ) e. CC )
83 82 14 addcld 
 |-  ( ph -> ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) e. CC )
84 83 14 16 addassd 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( ( 3 x. A ) + 1 ) ) )
85 84 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 3 x. A ) ) + 1 ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( ( 3 x. A ) + 1 ) ) - ( 3 x. A ) ) )
86 15 16 addcld 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) e. CC )
87 86 14 14 addsubassd 
 |-  ( ph -> ( ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) - ( 3 x. A ) ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + ( ( 3 x. A ) - ( 3 x. A ) ) ) )
88 81 oveq1d 
 |-  ( ph -> ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) = ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) )
89 88 oveq1d 
 |-  ( ph -> ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) )
90 89 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) )
91 90 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) - ( 3 x. A ) ) = ( ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) - ( 3 x. A ) ) )
92 14 subidd 
 |-  ( ph -> ( ( 3 x. A ) - ( 3 x. A ) ) = 0 )
93 92 oveq2d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + ( ( 3 x. A ) - ( 3 x. A ) ) ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + 0 ) )
94 86 addid1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + 0 ) = ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) )
95 93 94 eqtr2d 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) + ( ( 3 x. A ) - ( 3 x. A ) ) ) )
96 87 91 95 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) - ( 3 x. A ) ) )
97 83 16 14 addassd 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 1 + ( 3 x. A ) ) ) )
98 97 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + 1 ) + ( 3 x. A ) ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 1 + ( 3 x. A ) ) ) - ( 3 x. A ) ) )
99 96 98 eqtrd 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 1 + ( 3 x. A ) ) ) - ( 3 x. A ) ) )
100 80 85 99 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 3 x. A ) ) + 1 ) - ( 3 x. A ) ) )
101 82 14 14 addassd 
 |-  ( ph -> ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 3 x. A ) ) = ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) )
102 101 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) + 1 ) )
103 102 oveq1d 
 |-  ( ph -> ( ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 3 x. A ) ) + ( 3 x. A ) ) + 1 ) - ( 3 x. A ) ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) + 1 ) - ( 3 x. A ) ) )
104 100 103 eqtrd 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( ( 3 x. A ) + ( 3 x. A ) ) ) + 1 ) - ( 3 x. A ) ) )
105 73 77 104 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( ( 3 x. A ) ^ 2 ) + ( 2 x. ( 3 x. A ) ) ) + ( 1 ^ 2 ) ) - ( 3 x. A ) ) )
106 67 69 105 3eqtr4rd 
 |-  ( ph -> ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) = ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) )
107 106 oveq1d 
 |-  ( ph -> ( ( ( ( ( 3 ^ 2 ) x. ( A ^ 2 ) ) + ( 3 x. A ) ) + 1 ) x. 3 ) = ( ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) x. 3 ) )
108 62 107 eqtrd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = ( ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) x. 3 ) )
109 3 9 remulcld 
 |-  ( ph -> ( 3 x. A ) e. RR )
110 peano2re 
 |-  ( ( 3 x. A ) e. RR -> ( ( 3 x. A ) + 1 ) e. RR )
111 109 110 syl 
 |-  ( ph -> ( ( 3 x. A ) + 1 ) e. RR )
112 111 resqcld 
 |-  ( ph -> ( ( ( 3 x. A ) + 1 ) ^ 2 ) e. RR )
113 112 109 resubcld 
 |-  ( ph -> ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) e. RR )
114 113 recnd 
 |-  ( ph -> ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) e. CC )
115 3nn 
 |-  3 e. NN
116 nnq 
 |-  ( 3 e. NN -> 3 e. QQ )
117 115 116 ax-mp 
 |-  3 e. QQ
118 qmulcl 
 |-  ( ( 3 e. QQ /\ A e. QQ ) -> ( 3 x. A ) e. QQ )
119 117 1 118 sylancr 
 |-  ( ph -> ( 3 x. A ) e. QQ )
120 119 3cubeslem1 
 |-  ( ph -> 0 < ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) )
121 120 gt0ne0d 
 |-  ( ph -> ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) =/= 0 )
122 3ne0 
 |-  3 =/= 0
123 122 a1i 
 |-  ( ph -> 3 =/= 0 )
124 114 4 121 123 mulne0d 
 |-  ( ph -> ( ( ( ( ( 3 x. A ) + 1 ) ^ 2 ) - ( 3 x. A ) ) x. 3 ) =/= 0 )
125 108 124 eqnetrd 
 |-  ( ph -> ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) =/= 0 )
126 125 neneqd 
 |-  ( ph -> -. ( ( ( ( 3 ^ 3 ) x. ( A ^ 2 ) ) + ( ( 3 ^ 2 ) x. A ) ) + 3 ) = 0 )