Theorem nn0opthlem2

Description: Lemma for nn0opthi . (Contributed by Raph Levien, 10-Dec-2002) (Revised by Scott Fenton, 8-Sep-2010)

	Ref	Expression
Hypotheses	nn0opth.1	$$⊢A\in {\mathbb{N}}_0$$
	nn0opth.2	$$⊢B\in {\mathbb{N}}_0$$
	nn0opth.3	$$⊢C\in {\mathbb{N}}_0$$
	nn0opth.4	$$⊢D\in {\mathbb{N}}_0$$
Assertion	nn0opthlem2	$$⊢A+B<C\to CC+D\ne \left(A+B\right)\left(A+B\right)+B$$

Proof

Step	Hyp	Ref	Expression
1		nn0opth.1	$$⊢A\in {\mathbb{N}}_0$$
2		nn0opth.2	$$⊢B\in {\mathbb{N}}_0$$
3		nn0opth.3	$$⊢C\in {\mathbb{N}}_0$$
4		nn0opth.4	$$⊢D\in {\mathbb{N}}_0$$
5	1 2	nn0addcli	$$⊢A+B\in {\mathbb{N}}_0$$
6	5 3	nn0opthlem1	$$⊢A+B<C\leftrightarrow \left(A+B\right)\left(A+B\right)+2\left(A+B\right)<CC$$
7	2	nn0rei	$$⊢B\in ℝ$$
8	7 1	nn0addge2i	$$⊢B\le A+B$$
9	5 2	nn0lele2xi	$$⊢B\le A+B\to B\le 2\left(A+B\right)$$
10		2re	$$⊢2\in ℝ$$
11	5	nn0rei	$$⊢A+B\in ℝ$$
12	10 11	remulcli	$$⊢2\left(A+B\right)\in ℝ$$
13	11 11	remulcli	$$⊢\left(A+B\right)\left(A+B\right)\in ℝ$$
14	7 12 13	leadd2i	$$⊢B\le 2\left(A+B\right)\leftrightarrow \left(A+B\right)\left(A+B\right)+B\le \left(A+B\right)\left(A+B\right)+2\left(A+B\right)$$
15	9 14	sylib	$$⊢B\le A+B\to \left(A+B\right)\left(A+B\right)+B\le \left(A+B\right)\left(A+B\right)+2\left(A+B\right)$$
16	8 15	ax-mp	$$⊢\left(A+B\right)\left(A+B\right)+B\le \left(A+B\right)\left(A+B\right)+2\left(A+B\right)$$
17	13 7	readdcli	$$⊢\left(A+B\right)\left(A+B\right)+B\in ℝ$$
18	13 12	readdcli	$$⊢\left(A+B\right)\left(A+B\right)+2\left(A+B\right)\in ℝ$$
19	3	nn0rei	$$⊢C\in ℝ$$
20	19 19	remulcli	$$⊢CC\in ℝ$$
21	17 18 20	lelttri	$$⊢\left(\left(A+B\right)\left(A+B\right)+B\le \left(A+B\right)\left(A+B\right)+2\left(A+B\right)\wedge \left(A+B\right)\left(A+B\right)+2\left(A+B\right)<CC\right)\to \left(A+B\right)\left(A+B\right)+B<CC$$
22	16 21	mpan	$$⊢\left(A+B\right)\left(A+B\right)+2\left(A+B\right)<CC\to \left(A+B\right)\left(A+B\right)+B<CC$$
23	6 22	sylbi	$$⊢A+B<C\to \left(A+B\right)\left(A+B\right)+B<CC$$
24	20 4	nn0addge1i	$$⊢CC\le CC+D$$
25	4	nn0rei	$$⊢D\in ℝ$$
26	20 25	readdcli	$$⊢CC+D\in ℝ$$
27	17 20 26	ltletri	$$⊢\left(\left(A+B\right)\left(A+B\right)+B<CC\wedge CC\le CC+D\right)\to \left(A+B\right)\left(A+B\right)+B<CC+D$$
28	24 27	mpan2	$$⊢\left(A+B\right)\left(A+B\right)+B<CC\to \left(A+B\right)\left(A+B\right)+B<CC+D$$
29	17 26	ltnei	$$⊢\left(A+B\right)\left(A+B\right)+B<CC+D\to CC+D\ne \left(A+B\right)\left(A+B\right)+B$$
30	23 28 29	3syl	$$⊢A+B<C\to CC+D\ne \left(A+B\right)\left(A+B\right)+B$$