Theorem 3cubeslem1

Description: Lemma for 3cubes . (Contributed by Igor Ieskov, 22-Jan-2024)

	Ref	Expression
Hypothesis	3cubeslem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
Assertion	3cubeslem1	⊢ ( 𝜑 → 0 < ( ( ( 𝐴 + 1 ) ↑ 2 ) − 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		3cubeslem1.a	⊢ ( 𝜑 → 𝐴 ∈ ℚ )
2		qre	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℝ )
3	1 2	syl	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
5	3 4	lttri4d	⊢ ( 𝜑 → ( 𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴 ) )
6		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ )
7		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 0 ∈ ℝ )
8		peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ( 𝐴 + 1 ) ∈ ℝ )
10	9	resqcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ( ( 𝐴 + 1 ) ↑ 2 ) ∈ ℝ )
11		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 𝐴 < 0 )
12	9	sqge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 0 ≤ ( ( 𝐴 + 1 ) ↑ 2 ) )
13	6 7 10 11 12	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) )
14	13	a1i	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ) )
15	3 14	mpand	⊢ ( 𝜑 → ( 𝐴 < 0 → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ) )
16		0lt1	⊢ 0 < 1
17	16	a1i	⊢ ( 𝐴 = 0 → 0 < 1 )
18		id	⊢ ( 𝐴 = 0 → 𝐴 = 0 )
19		sq1	⊢ ( 1 ↑ 2 ) = 1
20	19	a1i	⊢ ( 𝐴 = 0 → ( 1 ↑ 2 ) = 1 )
21	17 18 20	3brtr4d	⊢ ( 𝐴 = 0 → 𝐴 < ( 1 ↑ 2 ) )
22		0cnd	⊢ ( 𝐴 = 0 → 0 ∈ ℂ )
23		1cnd	⊢ ( 𝐴 = 0 → 1 ∈ ℂ )
24	18	oveq1d	⊢ ( 𝐴 = 0 → ( 𝐴 + 1 ) = ( 0 + 1 ) )
25	22 23 24	comraddd	⊢ ( 𝐴 = 0 → ( 𝐴 + 1 ) = ( 1 + 0 ) )
26		1p0e1	⊢ ( 1 + 0 ) = 1
27	25 26	eqtrdi	⊢ ( 𝐴 = 0 → ( 𝐴 + 1 ) = 1 )
28	27	oveq1d	⊢ ( 𝐴 = 0 → ( ( 𝐴 + 1 ) ↑ 2 ) = ( 1 ↑ 2 ) )
29	21 28	breqtrrd	⊢ ( 𝐴 = 0 → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) )
30	29	a1i	⊢ ( 𝜑 → ( 𝐴 = 0 → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ) )
31		ax-1rid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
32	31	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 · 1 ) = 𝐴 )
33		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
34		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 1 ∈ ℝ )
35	33 34	readdcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 + 1 ) ∈ ℝ )
36		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < 𝐴 )
37		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ∈ ℝ )
38		ltle	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
39	37 33 38	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 0 < 𝐴 → 0 ≤ 𝐴 ) )
40	33	ltp1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 < ( 𝐴 + 1 ) )
41	39 40	jctird	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 0 < 𝐴 → ( 0 ≤ 𝐴 ∧ 𝐴 < ( 𝐴 + 1 ) ) ) )
42	36 41	mpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 0 ≤ 𝐴 ∧ 𝐴 < ( 𝐴 + 1 ) ) )
43	34 35	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) )
44		0le1	⊢ 0 ≤ 1
45	44	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 ≤ 1 )
46		1e0p1	⊢ 1 = ( 0 + 1 )
47	37 33 34 36	ltadd1dd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 0 + 1 ) < ( 𝐴 + 1 ) )
48	46 47	eqbrtrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 1 < ( 𝐴 + 1 ) )
49	43 45 48	jca32	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 1 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) ∧ ( 0 ≤ 1 ∧ 1 < ( 𝐴 + 1 ) ) ) )
50		ltmul12a	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) ∧ ( 0 ≤ 𝐴 ∧ 𝐴 < ( 𝐴 + 1 ) ) ) ∧ ( ( 1 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ) ∧ ( 0 ≤ 1 ∧ 1 < ( 𝐴 + 1 ) ) ) ) → ( 𝐴 · 1 ) < ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) )
51	33 35 42 49 50	syl1111anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 · 1 ) < ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) )
52	32 51	eqbrtrrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 < ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) )
53	35	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 + 1 ) ∈ ℂ )
54	53	sqvald	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 𝐴 + 1 ) ↑ 2 ) = ( ( 𝐴 + 1 ) · ( 𝐴 + 1 ) ) )
55	52 54	breqtrrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) )
56	55	a1i	⊢ ( 𝜑 → ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ) )
57	3 56	mpand	⊢ ( 𝜑 → ( 0 < 𝐴 → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ) )
58	15 30 57	3jaod	⊢ ( 𝜑 → ( ( 𝐴 < 0 ∨ 𝐴 = 0 ∨ 0 < 𝐴 ) → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ) )
59	5 58	mpd	⊢ ( 𝜑 → 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) )
60	3 8	syl	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ )
61	60	resqcld	⊢ ( 𝜑 → ( ( 𝐴 + 1 ) ↑ 2 ) ∈ ℝ )
62	3 61	posdifd	⊢ ( 𝜑 → ( 𝐴 < ( ( 𝐴 + 1 ) ↑ 2 ) ↔ 0 < ( ( ( 𝐴 + 1 ) ↑ 2 ) − 𝐴 ) ) )
63	59 62	mpbid	⊢ ( 𝜑 → 0 < ( ( ( 𝐴 + 1 ) ↑ 2 ) − 𝐴 ) )