Metamath Proof Explorer

Theorem cxpaddle

Description: Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses cxpaddle.1 ⊢ φ → A ∈ ℝ
cxpaddle.2 ⊢ φ → 0 ≤ A
cxpaddle.3 ⊢ φ → B ∈ ℝ
cxpaddle.4 ⊢ φ → 0 ≤ B
cxpaddle.5 ⊢ φ → C ∈ ℝ +
cxpaddle.6 ⊢ φ → C ≤ 1
Assertion cxpaddle ⊢ φ → A + B C ≤ A C + B C

Proof

Step Hyp Ref Expression
1 cxpaddle.1 ⊢ φ → A ∈ ℝ
2 cxpaddle.2 ⊢ φ → 0 ≤ A
3 cxpaddle.3 ⊢ φ → B ∈ ℝ
4 cxpaddle.4 ⊢ φ → 0 ≤ B
5 cxpaddle.5 ⊢ φ → C ∈ ℝ +
6 cxpaddle.6 ⊢ φ → C ≤ 1
7 1 3 readdcld ⊢ φ → A + B ∈ ℝ
8 1 3 2 4 addge0d ⊢ φ → 0 ≤ A + B
9 5 rpred ⊢ φ → C ∈ ℝ
10 7 8 9 recxpcld ⊢ φ → A + B C ∈ ℝ
11 10 adantr ⊢ φ ∧ 0 < A + B → A + B C ∈ ℝ
12 11 recnd ⊢ φ ∧ 0 < A + B → A + B C ∈ ℂ
13 12 mulid2d ⊢ φ ∧ 0 < A + B → 1 ⁢ A + B C = A + B C
14 1 adantr ⊢ φ ∧ 0 < A + B → A ∈ ℝ
15 7 anim1i ⊢ φ ∧ 0 < A + B → A + B ∈ ℝ ∧ 0 < A + B
16 elrp ⊢ A + B ∈ ℝ + ↔ A + B ∈ ℝ ∧ 0 < A + B
17 15 16 sylibr ⊢ φ ∧ 0 < A + B → A + B ∈ ℝ +
18 14 17 rerpdivcld ⊢ φ ∧ 0 < A + B → A A + B ∈ ℝ
19 3 adantr ⊢ φ ∧ 0 < A + B → B ∈ ℝ
20 19 17 rerpdivcld ⊢ φ ∧ 0 < A + B → B A + B ∈ ℝ
21 2 adantr ⊢ φ ∧ 0 < A + B → 0 ≤ A
22 7 adantr ⊢ φ ∧ 0 < A + B → A + B ∈ ℝ
23 simpr ⊢ φ ∧ 0 < A + B → 0 < A + B
24 divge0 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ A + B ∈ ℝ ∧ 0 < A + B → 0 ≤ A A + B
25 14 21 22 23 24 syl22anc ⊢ φ ∧ 0 < A + B → 0 ≤ A A + B
26 9 adantr ⊢ φ ∧ 0 < A + B → C ∈ ℝ
27 18 25 26 recxpcld ⊢ φ ∧ 0 < A + B → A A + B C ∈ ℝ
28 4 adantr ⊢ φ ∧ 0 < A + B → 0 ≤ B
29 divge0 ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A + B ∈ ℝ ∧ 0 < A + B → 0 ≤ B A + B
30 19 28 22 23 29 syl22anc ⊢ φ ∧ 0 < A + B → 0 ≤ B A + B
31 20 30 26 recxpcld ⊢ φ ∧ 0 < A + B → B A + B C ∈ ℝ
32 1 3 addge01d ⊢ φ → 0 ≤ B ↔ A ≤ A + B
33 4 32 mpbid ⊢ φ → A ≤ A + B
34 33 adantr ⊢ φ ∧ 0 < A + B → A ≤ A + B
35 22 recnd ⊢ φ ∧ 0 < A + B → A + B ∈ ℂ
36 35 mulid1d ⊢ φ ∧ 0 < A + B → A + B ⋅ 1 = A + B
37 34 36 breqtrrd ⊢ φ ∧ 0 < A + B → A ≤ A + B ⋅ 1
38 1red ⊢ φ ∧ 0 < A + B → 1 ∈ ℝ
39 ledivmul ⊢ A ∈ ℝ ∧ 1 ∈ ℝ ∧ A + B ∈ ℝ ∧ 0 < A + B → A A + B ≤ 1 ↔ A ≤ A + B ⋅ 1
40 14 38 22 23 39 syl112anc ⊢ φ ∧ 0 < A + B → A A + B ≤ 1 ↔ A ≤ A + B ⋅ 1
41 37 40 mpbird ⊢ φ ∧ 0 < A + B → A A + B ≤ 1
42 5 adantr ⊢ φ ∧ 0 < A + B → C ∈ ℝ +
43 6 adantr ⊢ φ ∧ 0 < A + B → C ≤ 1
44 18 25 41 42 43 cxpaddlelem ⊢ φ ∧ 0 < A + B → A A + B ≤ A A + B C
45 3 1 addge02d ⊢ φ → 0 ≤ A ↔ B ≤ A + B
46 2 45 mpbid ⊢ φ → B ≤ A + B
47 46 adantr ⊢ φ ∧ 0 < A + B → B ≤ A + B
48 47 36 breqtrrd ⊢ φ ∧ 0 < A + B → B ≤ A + B ⋅ 1
49 ledivmul ⊢ B ∈ ℝ ∧ 1 ∈ ℝ ∧ A + B ∈ ℝ ∧ 0 < A + B → B A + B ≤ 1 ↔ B ≤ A + B ⋅ 1
50 19 38 22 23 49 syl112anc ⊢ φ ∧ 0 < A + B → B A + B ≤ 1 ↔ B ≤ A + B ⋅ 1
51 48 50 mpbird ⊢ φ ∧ 0 < A + B → B A + B ≤ 1
52 20 30 51 42 43 cxpaddlelem ⊢ φ ∧ 0 < A + B → B A + B ≤ B A + B C
53 18 20 27 31 44 52 le2addd ⊢ φ ∧ 0 < A + B → A A + B + B A + B ≤ A A + B C + B A + B C
54 14 recnd ⊢ φ ∧ 0 < A + B → A ∈ ℂ
55 19 recnd ⊢ φ ∧ 0 < A + B → B ∈ ℂ
56 17 rpne0d ⊢ φ ∧ 0 < A + B → A + B ≠ 0
57 54 55 35 56 divdird ⊢ φ ∧ 0 < A + B → A + B A + B = A A + B + B A + B
58 35 56 dividd ⊢ φ ∧ 0 < A + B → A + B A + B = 1
59 57 58 eqtr3d ⊢ φ ∧ 0 < A + B → A A + B + B A + B = 1
60 9 recnd ⊢ φ → C ∈ ℂ
61 60 adantr ⊢ φ ∧ 0 < A + B → C ∈ ℂ
62 14 21 17 61 divcxpd ⊢ φ ∧ 0 < A + B → A A + B C = A C A + B C
63 19 28 17 61 divcxpd ⊢ φ ∧ 0 < A + B → B A + B C = B C A + B C
64 62 63 oveq12d ⊢ φ ∧ 0 < A + B → A A + B C + B A + B C = A C A + B C + B C A + B C
65 1 2 9 recxpcld ⊢ φ → A C ∈ ℝ
66 65 recnd ⊢ φ → A C ∈ ℂ
67 66 adantr ⊢ φ ∧ 0 < A + B → A C ∈ ℂ
68 3 4 9 recxpcld ⊢ φ → B C ∈ ℝ
69 68 recnd ⊢ φ → B C ∈ ℂ
70 69 adantr ⊢ φ ∧ 0 < A + B → B C ∈ ℂ
71 17 26 rpcxpcld ⊢ φ ∧ 0 < A + B → A + B C ∈ ℝ +
72 71 rpne0d ⊢ φ ∧ 0 < A + B → A + B C ≠ 0
73 67 70 12 72 divdird ⊢ φ ∧ 0 < A + B → A C + B C A + B C = A C A + B C + B C A + B C
74 64 73 eqtr4d ⊢ φ ∧ 0 < A + B → A A + B C + B A + B C = A C + B C A + B C
75 53 59 74 3brtr3d ⊢ φ ∧ 0 < A + B → 1 ≤ A C + B C A + B C
76 65 68 readdcld ⊢ φ → A C + B C ∈ ℝ
77 76 adantr ⊢ φ ∧ 0 < A + B → A C + B C ∈ ℝ
78 38 77 71 lemuldivd ⊢ φ ∧ 0 < A + B → 1 ⁢ A + B C ≤ A C + B C ↔ 1 ≤ A C + B C A + B C
79 75 78 mpbird ⊢ φ ∧ 0 < A + B → 1 ⁢ A + B C ≤ A C + B C
80 13 79 eqbrtrrd ⊢ φ ∧ 0 < A + B → A + B C ≤ A C + B C
81 5 rpne0d ⊢ φ → C ≠ 0
82 60 81 0cxpd ⊢ φ → 0 C = 0
83 1 2 9 cxpge0d ⊢ φ → 0 ≤ A C
84 3 4 9 cxpge0d ⊢ φ → 0 ≤ B C
85 65 68 83 84 addge0d ⊢ φ → 0 ≤ A C + B C
86 82 85 eqbrtrd ⊢ φ → 0 C ≤ A C + B C
87 oveq1 ⊢ 0 = A + B → 0 C = A + B C
88 87 breq1d ⊢ 0 = A + B → 0 C ≤ A C + B C ↔ A + B C ≤ A C + B C
89 86 88 syl5ibcom ⊢ φ → 0 = A + B → A + B C ≤ A C + B C
90 89 imp ⊢ φ ∧ 0 = A + B → A + B C ≤ A C + B C
91 0re ⊢ 0 ∈ ℝ
92 leloe ⊢ 0 ∈ ℝ ∧ A + B ∈ ℝ → 0 ≤ A + B ↔ 0 < A + B ∨ 0 = A + B
93 91 7 92 sylancr ⊢ φ → 0 ≤ A + B ↔ 0 < A + B ∨ 0 = A + B
94 8 93 mpbid ⊢ φ → 0 < A + B ∨ 0 = A + B
95 80 90 94 mpjaodan ⊢ φ → A + B C ≤ A C + B C