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 φ0A
cxpaddle.3 φB
cxpaddle.4 φ0B
cxpaddle.5 φC+
cxpaddle.6 φC1
Assertion cxpaddle φA+BCAC+BC

Proof

Step Hyp Ref Expression
1 cxpaddle.1 φA
2 cxpaddle.2 φ0A
3 cxpaddle.3 φB
4 cxpaddle.4 φ0B
5 cxpaddle.5 φC+
6 cxpaddle.6 φC1
7 1 3 readdcld φA+B
8 1 3 2 4 addge0d φ0A+B
9 5 rpred φC
10 7 8 9 recxpcld φA+BC
11 10 adantr φ0<A+BA+BC
12 11 recnd φ0<A+BA+BC
13 12 mulid2d φ0<A+B1A+BC=A+BC
14 1 adantr φ0<A+BA
15 7 anim1i φ0<A+BA+B0<A+B
16 elrp A+B+A+B0<A+B
17 15 16 sylibr φ0<A+BA+B+
18 14 17 rerpdivcld φ0<A+BAA+B
19 3 adantr φ0<A+BB
20 19 17 rerpdivcld φ0<A+BBA+B
21 2 adantr φ0<A+B0A
22 7 adantr φ0<A+BA+B
23 simpr φ0<A+B0<A+B
24 divge0 A0AA+B0<A+B0AA+B
25 14 21 22 23 24 syl22anc φ0<A+B0AA+B
26 9 adantr φ0<A+BC
27 18 25 26 recxpcld φ0<A+BAA+BC
28 4 adantr φ0<A+B0B
29 divge0 B0BA+B0<A+B0BA+B
30 19 28 22 23 29 syl22anc φ0<A+B0BA+B
31 20 30 26 recxpcld φ0<A+BBA+BC
32 1 3 addge01d φ0BAA+B
33 4 32 mpbid φAA+B
34 33 adantr φ0<A+BAA+B
35 22 recnd φ0<A+BA+B
36 35 mulid1d φ0<A+BA+B1=A+B
37 34 36 breqtrrd φ0<A+BAA+B1
38 1red φ0<A+B1
39 ledivmul A1A+B0<A+BAA+B1AA+B1
40 14 38 22 23 39 syl112anc φ0<A+BAA+B1AA+B1
41 37 40 mpbird φ0<A+BAA+B1
42 5 adantr φ0<A+BC+
43 6 adantr φ0<A+BC1
44 18 25 41 42 43 cxpaddlelem φ0<A+BAA+BAA+BC
45 3 1 addge02d φ0ABA+B
46 2 45 mpbid φBA+B
47 46 adantr φ0<A+BBA+B
48 47 36 breqtrrd φ0<A+BBA+B1
49 ledivmul B1A+B0<A+BBA+B1BA+B1
50 19 38 22 23 49 syl112anc φ0<A+BBA+B1BA+B1
51 48 50 mpbird φ0<A+BBA+B1
52 20 30 51 42 43 cxpaddlelem φ0<A+BBA+BBA+BC
53 18 20 27 31 44 52 le2addd φ0<A+BAA+B+BA+BAA+BC+BA+BC
54 14 recnd φ0<A+BA
55 19 recnd φ0<A+BB
56 17 rpne0d φ0<A+BA+B0
57 54 55 35 56 divdird φ0<A+BA+BA+B=AA+B+BA+B
58 35 56 dividd φ0<A+BA+BA+B=1
59 57 58 eqtr3d φ0<A+BAA+B+BA+B=1
60 9 recnd φC
61 60 adantr φ0<A+BC
62 14 21 17 61 divcxpd φ0<A+BAA+BC=ACA+BC
63 19 28 17 61 divcxpd φ0<A+BBA+BC=BCA+BC
64 62 63 oveq12d φ0<A+BAA+BC+BA+BC=ACA+BC+BCA+BC
65 1 2 9 recxpcld φAC
66 65 recnd φAC
67 66 adantr φ0<A+BAC
68 3 4 9 recxpcld φBC
69 68 recnd φBC
70 69 adantr φ0<A+BBC
71 17 26 rpcxpcld φ0<A+BA+BC+
72 71 rpne0d φ0<A+BA+BC0
73 67 70 12 72 divdird φ0<A+BAC+BCA+BC=ACA+BC+BCA+BC
74 64 73 eqtr4d φ0<A+BAA+BC+BA+BC=AC+BCA+BC
75 53 59 74 3brtr3d φ0<A+B1AC+BCA+BC
76 65 68 readdcld φAC+BC
77 76 adantr φ0<A+BAC+BC
78 38 77 71 lemuldivd φ0<A+B1A+BCAC+BC1AC+BCA+BC
79 75 78 mpbird φ0<A+B1A+BCAC+BC
80 13 79 eqbrtrrd φ0<A+BA+BCAC+BC
81 5 rpne0d φC0
82 60 81 0cxpd φ0C=0
83 1 2 9 cxpge0d φ0AC
84 3 4 9 cxpge0d φ0BC
85 65 68 83 84 addge0d φ0AC+BC
86 82 85 eqbrtrd φ0CAC+BC
87 oveq1 0=A+B0C=A+BC
88 87 breq1d 0=A+B0CAC+BCA+BCAC+BC
89 86 88 syl5ibcom φ0=A+BA+BCAC+BC
90 89 imp φ0=A+BA+BCAC+BC
91 0re 0
92 leloe 0A+B0A+B0<A+B0=A+B
93 91 7 92 sylancr φ0A+B0<A+B0=A+B
94 8 93 mpbid φ0<A+B0=A+B
95 80 90 94 mpjaodan φA+BCAC+BC