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 ⊢ ( 𝜑 → 𝐴 ∈ ℚ )
Assertion 3cubeslem2 ( 𝜑 → ¬ ( ( ( ( 3 ↑ 3 ) · ( 𝐴 ↑ 2 ) ) + ( ( 3 ↑ 2 ) · 𝐴 ) ) + 3 ) = 0 )

Proof

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