Metamath Proof Explorer

Theorem cxpaddlelem

Description: Lemma for cxpaddle . (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Hypotheses cxpaddlelem.1 
|- ( ph -> A e. RR )
cxpaddlelem.2 
|- ( ph -> 0 <_ A )
cxpaddlelem.3 
|- ( ph -> A <_ 1 )
cxpaddlelem.4 
|- ( ph -> B e. RR+ )
cxpaddlelem.5 
|- ( ph -> B <_ 1 )
Assertion cxpaddlelem 
|- ( ph -> A <_ ( A ^c B ) )

Proof

Step Hyp Ref Expression
1 cxpaddlelem.1 
 |-  ( ph -> A e. RR )
2 cxpaddlelem.2 
 |-  ( ph -> 0 <_ A )
3 cxpaddlelem.3 
 |-  ( ph -> A <_ 1 )
4 cxpaddlelem.4 
 |-  ( ph -> B e. RR+ )
5 cxpaddlelem.5 
 |-  ( ph -> B <_ 1 )
6 1re 
 |-  1 e. RR
7 4 rpred 
 |-  ( ph -> B e. RR )
8 resubcl 
 |-  ( ( 1 e. RR /\ B e. RR ) -> ( 1 - B ) e. RR )
9 6 7 8 sylancr 
 |-  ( ph -> ( 1 - B ) e. RR )
10 1 2 9 recxpcld 
 |-  ( ph -> ( A ^c ( 1 - B ) ) e. RR )
11 10 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( A ^c ( 1 - B ) ) e. RR )
12 1red 
 |-  ( ( ph /\ 0 < A ) -> 1 e. RR )
13 recxpcl 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )
14 cxpge0 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> 0 <_ ( A ^c B ) )
15 13 14 jca 
 |-  ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( ( A ^c B ) e. RR /\ 0 <_ ( A ^c B ) ) )
16 1 2 7 15 syl3anc 
 |-  ( ph -> ( ( A ^c B ) e. RR /\ 0 <_ ( A ^c B ) ) )
17 16 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( ( A ^c B ) e. RR /\ 0 <_ ( A ^c B ) ) )
18 3 ad2antrr 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> A <_ 1 )
19 1 ad2antrr 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> A e. RR )
20 2 ad2antrr 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> 0 <_ A )
21 1red 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> 1 e. RR )
22 0le1 
 |-  0 <_ 1
23 22 a1i 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> 0 <_ 1 )
24 difrp 
 |-  ( ( B e. RR /\ 1 e. RR ) -> ( B < 1 <-> ( 1 - B ) e. RR+ ) )
25 7 6 24 sylancl 
 |-  ( ph -> ( B < 1 <-> ( 1 - B ) e. RR+ ) )
26 25 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( B < 1 <-> ( 1 - B ) e. RR+ ) )
27 26 biimpa 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> ( 1 - B ) e. RR+ )
28 19 20 21 23 27 cxple2d 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> ( A <_ 1 <-> ( A ^c ( 1 - B ) ) <_ ( 1 ^c ( 1 - B ) ) ) )
29 18 28 mpbid 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> ( A ^c ( 1 - B ) ) <_ ( 1 ^c ( 1 - B ) ) )
30 9 recnd 
 |-  ( ph -> ( 1 - B ) e. CC )
31 30 1cxpd 
 |-  ( ph -> ( 1 ^c ( 1 - B ) ) = 1 )
32 31 ad2antrr 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> ( 1 ^c ( 1 - B ) ) = 1 )
33 29 32 breqtrd 
 |-  ( ( ( ph /\ 0 < A ) /\ B < 1 ) -> ( A ^c ( 1 - B ) ) <_ 1 )
34 simpr 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> B = 1 )
35 34 oveq2d 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> ( 1 - B ) = ( 1 - 1 ) )
36 1m1e0 
 |-  ( 1 - 1 ) = 0
37 35 36 eqtrdi 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> ( 1 - B ) = 0 )
38 37 oveq2d 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> ( A ^c ( 1 - B ) ) = ( A ^c 0 ) )
39 1 recnd 
 |-  ( ph -> A e. CC )
40 39 ad2antrr 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> A e. CC )
41 40 cxp0d 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> ( A ^c 0 ) = 1 )
42 38 41 eqtrd 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> ( A ^c ( 1 - B ) ) = 1 )
43 1le1 
 |-  1 <_ 1
44 42 43 eqbrtrdi 
 |-  ( ( ( ph /\ 0 < A ) /\ B = 1 ) -> ( A ^c ( 1 - B ) ) <_ 1 )
45 leloe 
 |-  ( ( B e. RR /\ 1 e. RR ) -> ( B <_ 1 <-> ( B < 1 \/ B = 1 ) ) )
46 7 6 45 sylancl 
 |-  ( ph -> ( B <_ 1 <-> ( B < 1 \/ B = 1 ) ) )
47 5 46 mpbid 
 |-  ( ph -> ( B < 1 \/ B = 1 ) )
48 47 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( B < 1 \/ B = 1 ) )
49 33 44 48 mpjaodan 
 |-  ( ( ph /\ 0 < A ) -> ( A ^c ( 1 - B ) ) <_ 1 )
50 lemul1a 
 |-  ( ( ( ( A ^c ( 1 - B ) ) e. RR /\ 1 e. RR /\ ( ( A ^c B ) e. RR /\ 0 <_ ( A ^c B ) ) ) /\ ( A ^c ( 1 - B ) ) <_ 1 ) -> ( ( A ^c ( 1 - B ) ) x. ( A ^c B ) ) <_ ( 1 x. ( A ^c B ) ) )
51 11 12 17 49 50 syl31anc 
 |-  ( ( ph /\ 0 < A ) -> ( ( A ^c ( 1 - B ) ) x. ( A ^c B ) ) <_ ( 1 x. ( A ^c B ) ) )
52 ax-1cn 
 |-  1 e. CC
53 7 recnd 
 |-  ( ph -> B e. CC )
54 npcan 
 |-  ( ( 1 e. CC /\ B e. CC ) -> ( ( 1 - B ) + B ) = 1 )
55 52 53 54 sylancr 
 |-  ( ph -> ( ( 1 - B ) + B ) = 1 )
56 55 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( ( 1 - B ) + B ) = 1 )
57 56 oveq2d 
 |-  ( ( ph /\ 0 < A ) -> ( A ^c ( ( 1 - B ) + B ) ) = ( A ^c 1 ) )
58 39 adantr 
 |-  ( ( ph /\ 0 < A ) -> A e. CC )
59 1 anim1i 
 |-  ( ( ph /\ 0 < A ) -> ( A e. RR /\ 0 < A ) )
60 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
61 59 60 sylibr 
 |-  ( ( ph /\ 0 < A ) -> A e. RR+ )
62 61 rpne0d 
 |-  ( ( ph /\ 0 < A ) -> A =/= 0 )
63 30 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( 1 - B ) e. CC )
64 53 adantr 
 |-  ( ( ph /\ 0 < A ) -> B e. CC )
65 58 62 63 64 cxpaddd 
 |-  ( ( ph /\ 0 < A ) -> ( A ^c ( ( 1 - B ) + B ) ) = ( ( A ^c ( 1 - B ) ) x. ( A ^c B ) ) )
66 39 cxp1d 
 |-  ( ph -> ( A ^c 1 ) = A )
67 66 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( A ^c 1 ) = A )
68 57 65 67 3eqtr3d 
 |-  ( ( ph /\ 0 < A ) -> ( ( A ^c ( 1 - B ) ) x. ( A ^c B ) ) = A )
69 39 53 cxpcld 
 |-  ( ph -> ( A ^c B ) e. CC )
70 69 mullidd 
 |-  ( ph -> ( 1 x. ( A ^c B ) ) = ( A ^c B ) )
71 70 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( 1 x. ( A ^c B ) ) = ( A ^c B ) )
72 51 68 71 3brtr3d 
 |-  ( ( ph /\ 0 < A ) -> A <_ ( A ^c B ) )
73 1 2 7 cxpge0d 
 |-  ( ph -> 0 <_ ( A ^c B ) )
74 breq1 
 |-  ( 0 = A -> ( 0 <_ ( A ^c B ) <-> A <_ ( A ^c B ) ) )
75 73 74 syl5ibcom 
 |-  ( ph -> ( 0 = A -> A <_ ( A ^c B ) ) )
76 75 imp 
 |-  ( ( ph /\ 0 = A ) -> A <_ ( A ^c B ) )
77 0re 
 |-  0 e. RR
78 leloe 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
79 77 1 78 sylancr 
 |-  ( ph -> ( 0 <_ A <-> ( 0 < A \/ 0 = A ) ) )
80 2 79 mpbid 
 |-  ( ph -> ( 0 < A \/ 0 = A ) )
81 72 76 80 mpjaodan 
 |-  ( ph -> A <_ ( A ^c B ) )