Metamath Proof Explorer

Theorem nn0opthlem1

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

Ref Expression
Hypotheses nn0opthlem1.1 
|- A e. NN0
nn0opthlem1.2 
|- C e. NN0
Assertion nn0opthlem1 
|- ( A < C <-> ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) )

Proof

Step Hyp Ref Expression
1 nn0opthlem1.1 
 |-  A e. NN0
2 nn0opthlem1.2 
 |-  C e. NN0
3 1nn0 
 |-  1 e. NN0
4 1 3 nn0addcli 
 |-  ( A + 1 ) e. NN0
5 4 2 nn0le2msqi 
 |-  ( ( A + 1 ) <_ C <-> ( ( A + 1 ) x. ( A + 1 ) ) <_ ( C x. C ) )
6 nn0ltp1le 
 |-  ( ( A e. NN0 /\ C e. NN0 ) -> ( A < C <-> ( A + 1 ) <_ C ) )
7 1 2 6 mp2an 
 |-  ( A < C <-> ( A + 1 ) <_ C )
8 1 1 nn0mulcli 
 |-  ( A x. A ) e. NN0
9 2nn0 
 |-  2 e. NN0
10 9 1 nn0mulcli 
 |-  ( 2 x. A ) e. NN0
11 8 10 nn0addcli 
 |-  ( ( A x. A ) + ( 2 x. A ) ) e. NN0
12 2 2 nn0mulcli 
 |-  ( C x. C ) e. NN0
13 nn0ltp1le 
 |-  ( ( ( ( A x. A ) + ( 2 x. A ) ) e. NN0 /\ ( C x. C ) e. NN0 ) -> ( ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) <-> ( ( ( A x. A ) + ( 2 x. A ) ) + 1 ) <_ ( C x. C ) ) )
14 11 12 13 mp2an 
 |-  ( ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) <-> ( ( ( A x. A ) + ( 2 x. A ) ) + 1 ) <_ ( C x. C ) )
15 1 nn0cni 
 |-  A e. CC
16 ax-1cn 
 |-  1 e. CC
17 15 16 binom2i 
 |-  ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 ^ 2 ) )
18 15 16 addcli 
 |-  ( A + 1 ) e. CC
19 18 sqvali 
 |-  ( ( A + 1 ) ^ 2 ) = ( ( A + 1 ) x. ( A + 1 ) )
20 15 sqvali 
 |-  ( A ^ 2 ) = ( A x. A )
21 20 oveq1i 
 |-  ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) = ( ( A x. A ) + ( 2 x. ( A x. 1 ) ) )
22 16 sqvali 
 |-  ( 1 ^ 2 ) = ( 1 x. 1 )
23 21 22 oveq12i 
 |-  ( ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 ^ 2 ) ) = ( ( ( A x. A ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 x. 1 ) )
24 17 19 23 3eqtr3i 
 |-  ( ( A + 1 ) x. ( A + 1 ) ) = ( ( ( A x. A ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 x. 1 ) )
25 15 mulid1i 
 |-  ( A x. 1 ) = A
26 25 oveq2i 
 |-  ( 2 x. ( A x. 1 ) ) = ( 2 x. A )
27 26 oveq2i 
 |-  ( ( A x. A ) + ( 2 x. ( A x. 1 ) ) ) = ( ( A x. A ) + ( 2 x. A ) )
28 16 mulid1i 
 |-  ( 1 x. 1 ) = 1
29 27 28 oveq12i 
 |-  ( ( ( A x. A ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 x. 1 ) ) = ( ( ( A x. A ) + ( 2 x. A ) ) + 1 )
30 24 29 eqtri 
 |-  ( ( A + 1 ) x. ( A + 1 ) ) = ( ( ( A x. A ) + ( 2 x. A ) ) + 1 )
31 30 breq1i 
 |-  ( ( ( A + 1 ) x. ( A + 1 ) ) <_ ( C x. C ) <-> ( ( ( A x. A ) + ( 2 x. A ) ) + 1 ) <_ ( C x. C ) )
32 14 31 bitr4i 
 |-  ( ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) <-> ( ( A + 1 ) x. ( A + 1 ) ) <_ ( C x. C ) )
33 5 7 32 3bitr4i 
 |-  ( A < C <-> ( ( A x. A ) + ( 2 x. A ) ) < ( C x. C ) )