nn0opthlem1

Description: A rather pretty lemma for nn0opthi . (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Hypotheses	nn0opthlem1.1	$⊢ A \in ℕ_{0}$
	nn0opthlem1.2	$⊢ C \in ℕ_{0}$
Assertion	nn0opthlem1	$⊢ A < C \leftrightarrow A A + 2 A < C C$

Proof

Step	Hyp	Ref	Expression
1		nn0opthlem1.1	$⊢ A \in ℕ_{0}$
2		nn0opthlem1.2	$⊢ C \in ℕ_{0}$
3		1nn0	$⊢ 1 \in ℕ_{0}$
4	1 3	nn0addcli	$⊢ A + 1 \in ℕ_{0}$
5	4 2	nn0le2msqi	$⊢ A + 1 \leq C \leftrightarrow (A + 1) (A + 1) \leq C C$
6		nn0ltp1le	$⊢ (A \in ℕ_{0} \land C \in ℕ_{0}) \to (A < C \leftrightarrow A + 1 \leq C)$
7	1 2 6	mp2an	$⊢ A < C \leftrightarrow A + 1 \leq C$
8	1 1	nn0mulcli	$⊢ A A \in ℕ_{0}$
9		2nn0	$⊢ 2 \in ℕ_{0}$
10	9 1	nn0mulcli	$⊢ 2 A \in ℕ_{0}$
11	8 10	nn0addcli	$⊢ A A + 2 A \in ℕ_{0}$
12	2 2	nn0mulcli	$⊢ C C \in ℕ_{0}$
13		nn0ltp1le	$⊢ (A A + 2 A \in ℕ_{0} \land C C \in ℕ_{0}) \to (A A + 2 A < C C \leftrightarrow A A + 2 A + 1 \leq C C)$
14	11 12 13	mp2an	$⊢ A A + 2 A < C C \leftrightarrow A A + 2 A + 1 \leq C C$
15	1	nn0cni	$⊢ A \in ℂ$
16		ax-1cn	$⊢ 1 \in ℂ$
17	15 16	binom2i	$⊢ {(A + 1)}^{2} = A^{2} + 2 A \cdot 1 + 1^{2}$
18	15 16	addcli	$⊢ A + 1 \in ℂ$
19	18	sqvali	$⊢ {(A + 1)}^{2} = (A + 1) (A + 1)$
20	15	sqvali	$⊢ A^{2} = A A$
21	20	oveq1i	$⊢ A^{2} + 2 A \cdot 1 = A A + 2 A \cdot 1$
22	16	sqvali	$⊢ 1^{2} = 1 \cdot 1$
23	21 22	oveq12i	$⊢ A^{2} + 2 A \cdot 1 + 1^{2} = A A + 2 A \cdot 1 + 1 \cdot 1$
24	17 19 23	3eqtr3i	$⊢ (A + 1) (A + 1) = A A + 2 A \cdot 1 + 1 \cdot 1$
25	15	mulid1i	$⊢ A \cdot 1 = A$
26	25	oveq2i	$⊢ 2 A \cdot 1 = 2 A$
27	26	oveq2i	$⊢ A A + 2 A \cdot 1 = A A + 2 A$
28	16	mulid1i	$⊢ 1 \cdot 1 = 1$
29	27 28	oveq12i	$⊢ A A + 2 A \cdot 1 + 1 \cdot 1 = A A + 2 A + 1$
30	24 29	eqtri	$⊢ (A + 1) (A + 1) = A A + 2 A + 1$
31	30	breq1i	$⊢ (A + 1) (A + 1) \leq C C \leftrightarrow A A + 2 A + 1 \leq C C$
32	14 31	bitr4i	$⊢ A A + 2 A < C C \leftrightarrow (A + 1) (A + 1) \leq C C$
33	5 7 32	3bitr4i	$⊢ A < C \leftrightarrow A A + 2 A < C C$

Metamath Proof Explorer

Theorem nn0opthlem1

Proof