Metamath Proof Explorer

Theorem dchrisum0lem1a

Description: Lemma for dchrisum0lem1 . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Assertion dchrisum0lem1a 
|- ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X <_ ( ( X ^ 2 ) / D ) /\ ( |_ ` ( ( X ^ 2 ) / D ) ) e. ( ZZ>= ` ( |_ ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 elfznn 
 |-  ( D e. ( 1 ... ( |_ ` X ) ) -> D e. NN )
2 1 adantl 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> D e. NN )
3 2 nnred 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> D e. RR )
4 simpr 
 |-  ( ( ph /\ X e. RR+ ) -> X e. RR+ )
5 4 rpregt0d 
 |-  ( ( ph /\ X e. RR+ ) -> ( X e. RR /\ 0 < X ) )
6 5 adantr 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X e. RR /\ 0 < X ) )
7 6 simpld 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> X e. RR )
8 4 adantr 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> X e. RR+ )
9 8 rpge0d 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> 0 <_ X )
10 4 rpred 
 |-  ( ( ph /\ X e. RR+ ) -> X e. RR )
11 fznnfl 
 |-  ( X e. RR -> ( D e. ( 1 ... ( |_ ` X ) ) <-> ( D e. NN /\ D <_ X ) ) )
12 10 11 syl 
 |-  ( ( ph /\ X e. RR+ ) -> ( D e. ( 1 ... ( |_ ` X ) ) <-> ( D e. NN /\ D <_ X ) ) )
13 12 simplbda 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> D <_ X )
14 3 7 7 9 13 lemul2ad 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X x. D ) <_ ( X x. X ) )
15 rpcn 
 |-  ( X e. RR+ -> X e. CC )
16 15 adantl 
 |-  ( ( ph /\ X e. RR+ ) -> X e. CC )
17 16 sqvald 
 |-  ( ( ph /\ X e. RR+ ) -> ( X ^ 2 ) = ( X x. X ) )
18 17 adantr 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X ^ 2 ) = ( X x. X ) )
19 14 18 breqtrrd 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X x. D ) <_ ( X ^ 2 ) )
20 2z 
 |-  2 e. ZZ
21 rpexpcl 
 |-  ( ( X e. RR+ /\ 2 e. ZZ ) -> ( X ^ 2 ) e. RR+ )
22 4 20 21 sylancl 
 |-  ( ( ph /\ X e. RR+ ) -> ( X ^ 2 ) e. RR+ )
23 22 rpred 
 |-  ( ( ph /\ X e. RR+ ) -> ( X ^ 2 ) e. RR )
24 23 adantr 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X ^ 2 ) e. RR )
25 2 nnrpd 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> D e. RR+ )
26 7 24 25 lemuldivd 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( ( X x. D ) <_ ( X ^ 2 ) <-> X <_ ( ( X ^ 2 ) / D ) ) )
27 19 26 mpbid 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> X <_ ( ( X ^ 2 ) / D ) )
28 nndivre 
 |-  ( ( ( X ^ 2 ) e. RR /\ D e. NN ) -> ( ( X ^ 2 ) / D ) e. RR )
29 23 1 28 syl2an 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( ( X ^ 2 ) / D ) e. RR )
30 flword2 
 |-  ( ( X e. RR /\ ( ( X ^ 2 ) / D ) e. RR /\ X <_ ( ( X ^ 2 ) / D ) ) -> ( |_ ` ( ( X ^ 2 ) / D ) ) e. ( ZZ>= ` ( |_ ` X ) ) )
31 7 29 27 30 syl3anc 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( |_ ` ( ( X ^ 2 ) / D ) ) e. ( ZZ>= ` ( |_ ` X ) ) )
32 27 31 jca 
 |-  ( ( ( ph /\ X e. RR+ ) /\ D e. ( 1 ... ( |_ ` X ) ) ) -> ( X <_ ( ( X ^ 2 ) / D ) /\ ( |_ ` ( ( X ^ 2 ) / D ) ) e. ( ZZ>= ` ( |_ ` X ) ) ) )