3cubeslem1

		Ref	Expression
	Hypothesis	3cubeslem1.a	$⊢ φ \to A \in ℚ$
	Assertion	3cubeslem1	$⊢ φ \to 0 < {(A + 1)}^{2} - A$

Proof

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

Metamath Proof Explorer

Theorem 3cubeslem1

Proof