This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. NN0
nn0opth.2 
|- B e. NN0
nn0opth.3 
|- C e. NN0
nn0opth.4 
|- D e. NN0
Assertion nn0opthlem2 
|- ( ( A + B ) < C -> ( ( C x. C ) + D ) =/= ( ( ( A + B ) x. ( A + B ) ) + B ) )

Proof

Step Hyp Ref Expression
1 nn0opth.1 
 |-  A e. NN0
2 nn0opth.2 
 |-  B e. NN0
3 nn0opth.3 
 |-  C e. NN0
4 nn0opth.4 
 |-  D e. NN0
5 1 2 nn0addcli 
 |-  ( A + B ) e. NN0
6 5 3 nn0opthlem1 
 |-  ( ( A + B ) < C <-> ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) < ( C x. C ) )
7 2 nn0rei 
 |-  B e. RR
8 7 1 nn0addge2i 
 |-  B <_ ( A + B )
9 5 2 nn0lele2xi 
 |-  ( B <_ ( A + B ) -> B <_ ( 2 x. ( A + B ) ) )
10 2re 
 |-  2 e. RR
11 5 nn0rei 
 |-  ( A + B ) e. RR
12 10 11 remulcli 
 |-  ( 2 x. ( A + B ) ) e. RR
13 11 11 remulcli 
 |-  ( ( A + B ) x. ( A + B ) ) e. RR
14 7 12 13 leadd2i 
 |-  ( B <_ ( 2 x. ( A + B ) ) <-> ( ( ( A + B ) x. ( A + B ) ) + B ) <_ ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) )
15 9 14 sylib 
 |-  ( B <_ ( A + B ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) <_ ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) )
16 8 15 ax-mp 
 |-  ( ( ( A + B ) x. ( A + B ) ) + B ) <_ ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) )
17 13 7 readdcli 
 |-  ( ( ( A + B ) x. ( A + B ) ) + B ) e. RR
18 13 12 readdcli 
 |-  ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) e. RR
19 3 nn0rei 
 |-  C e. RR
20 19 19 remulcli 
 |-  ( C x. C ) e. RR
21 17 18 20 lelttri 
 |-  ( ( ( ( ( A + B ) x. ( A + B ) ) + B ) <_ ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) /\ ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) < ( C x. C ) ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) < ( C x. C ) )
22 16 21 mpan 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + ( 2 x. ( A + B ) ) ) < ( C x. C ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) < ( C x. C ) )
23 6 22 sylbi 
 |-  ( ( A + B ) < C -> ( ( ( A + B ) x. ( A + B ) ) + B ) < ( C x. C ) )
24 20 4 nn0addge1i 
 |-  ( C x. C ) <_ ( ( C x. C ) + D )
25 4 nn0rei 
 |-  D e. RR
26 20 25 readdcli 
 |-  ( ( C x. C ) + D ) e. RR
27 17 20 26 ltletri 
 |-  ( ( ( ( ( A + B ) x. ( A + B ) ) + B ) < ( C x. C ) /\ ( C x. C ) <_ ( ( C x. C ) + D ) ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) < ( ( C x. C ) + D ) )
28 24 27 mpan2 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) < ( C x. C ) -> ( ( ( A + B ) x. ( A + B ) ) + B ) < ( ( C x. C ) + D ) )
29 17 26 ltnei 
 |-  ( ( ( ( A + B ) x. ( A + B ) ) + B ) < ( ( C x. C ) + D ) -> ( ( C x. C ) + D ) =/= ( ( ( A + B ) x. ( A + B ) ) + B ) )
30 23 28 29 3syl 
 |-  ( ( A + B ) < C -> ( ( C x. C ) + D ) =/= ( ( ( A + B ) x. ( A + B ) ) + B ) )