Metamath Proof Explorer

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 {ℕ}_{0}$
nn0opth.2 ${⊢}{B}\in {ℕ}_{0}$
nn0opth.3 ${⊢}{C}\in {ℕ}_{0}$
nn0opth.4 ${⊢}{D}\in {ℕ}_{0}$
Assertion nn0opthlem2 ${⊢}{A}+{B}<{C}\to {C}{C}+{D}\ne \left({A}+{B}\right)\left({A}+{B}\right)+{B}$

Proof

Step Hyp Ref Expression
1 nn0opth.1 ${⊢}{A}\in {ℕ}_{0}$
2 nn0opth.2 ${⊢}{B}\in {ℕ}_{0}$
3 nn0opth.3 ${⊢}{C}\in {ℕ}_{0}$
4 nn0opth.4 ${⊢}{D}\in {ℕ}_{0}$
5 1 2 nn0addcli ${⊢}{A}+{B}\in {ℕ}_{0}$
6 5 3 nn0opthlem1 ${⊢}{A}+{B}<{C}↔\left({A}+{B}\right)\left({A}+{B}\right)+2\left({A}+{B}\right)<{C}{C}$
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)↔\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 ${⊢}{C}{C}\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)<{C}{C}\right)\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}$
22 16 21 mpan ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+2\left({A}+{B}\right)<{C}{C}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}$
23 6 22 sylbi ${⊢}{A}+{B}<{C}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}$
24 20 4 nn0addge1i ${⊢}{C}{C}\le {C}{C}+{D}$
25 4 nn0rei ${⊢}{D}\in ℝ$
26 20 25 readdcli ${⊢}{C}{C}+{D}\in ℝ$
27 17 20 26 ltletri ${⊢}\left(\left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}\wedge {C}{C}\le {C}{C}+{D}\right)\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}+{D}$
28 24 27 mpan2 ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}\to \left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}+{D}$
29 17 26 ltnei ${⊢}\left({A}+{B}\right)\left({A}+{B}\right)+{B}<{C}{C}+{D}\to {C}{C}+{D}\ne \left({A}+{B}\right)\left({A}+{B}\right)+{B}$
30 23 28 29 3syl ${⊢}{A}+{B}<{C}\to {C}{C}+{D}\ne \left({A}+{B}\right)\left({A}+{B}\right)+{B}$