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	$$⊢\phi \to A\in \mathbb{Q}$$
Assertion	3cubeslem2	$$⊢\phi \to \neg 3^3{A}^2+3^{2}A+3=0$$

Proof

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