Metamath Proof Explorer

Theorem cxpaddlelem

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

Ref Expression
Hypotheses cxpaddlelem.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
cxpaddlelem.2 ⊢ ( 𝜑 → 0 ≤ 𝐴 )
cxpaddlelem.3 ⊢ ( 𝜑 → 𝐴 ≤ 1 )
cxpaddlelem.4 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
cxpaddlelem.5 ⊢ ( 𝜑 → 𝐵 ≤ 1 )
Assertion cxpaddlelem ( 𝜑 → 𝐴 ≤ ( 𝐴 ↑𝑐 𝐵 ) )

Proof

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