rpabscxpbnd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > rpabscxpbnd		Unicode version

Theorem rpabscxpbnd 14026

Description: Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.)

**Hypotheses**
Ref	Expression
rpabscxpbnd.1
abscxpbnd.2
rpabscxpbnd.3
abscxpbnd.4
abscxpbnd.5

**Assertion**
Ref	Expression
rpabscxpbnd

**Proof of Theorem rpabscxpbnd**
Step	Hyp	Ref	Expression
1		rpabscxpbnd.1	. . . . 5
2		abscxpbnd.2	. . . . 5
3		rpcxpef 13982	. . . . 5 $/\$
4	1, 2, 3	syl2anc 411	. . . 4
5	4	fveq2d 5515	. . 3
6	1	relogcld 13970	. . . . . 6
7	6	recnd 7976	. . . . 5
8	2, 7	mulcld 7968	. . . 4
9		absef 11761	. . . 4
10	8, 9	syl 14	. . 3
11	2	recld 10931	. . . . . . 7
12	7	recld 10931	. . . . . . 7
13	11, 12	remulcld 7978	. . . . . 6
14	13	recnd 7976	. . . . 5
15	2	imcld 10932	. . . . . . 7
16	7	imcld 10932	. . . . . . . 8
17	16	renegcld 8327	. . . . . . 7
18	15, 17	remulcld 7978	. . . . . 6
19	18	recnd 7976	. . . . 5
20		efadd 11667	. . . . 5 $/\$
21	14, 19, 20	syl2anc 411	. . . 4
22	15, 16	remulcld 7978	. . . . . . . 8
23	22	recnd 7976	. . . . . . 7
24	14, 23	negsubd 8264	. . . . . 6
25	15	recnd 7976	. . . . . . . 8
26	16	recnd 7976	. . . . . . . 8
27	25, 26	mulneg2d 8359	. . . . . . 7
28	27	oveq2d 5885	. . . . . 6
29	2, 7	remuld 10956	. . . . . 6
30	24, 28, 29	3eqtr4d 2220	. . . . 5
31	30	fveq2d 5515	. . . 4
32	6	rered 10962	. . . . . . . . 9
33	1	rpred 9683	. . . . . . . . . . 11
34	1	rpge0d 9687	. . . . . . . . . . 11
35	33, 34	absidd 11160	. . . . . . . . . 10
36	35	fveq2d 5515	. . . . . . . . 9
37	32, 36	eqtr4d 2213	. . . . . . . 8
38	37	oveq2d 5885	. . . . . . 7
39	38	fveq2d 5515	. . . . . 6
40	35, 1	eqeltrd 2254	. . . . . . 7
41	11	recnd 7976	. . . . . . 7
42		rpcxpef 13982	. . . . . . 7 $/\$
43	40, 41, 42	syl2anc 411	. . . . . 6
44	39, 43	eqtr4d 2213	. . . . 5
45	44	oveq1d 5884	. . . 4
46	21, 31, 45	3eqtr3d 2218	. . 3
47	5, 10, 46	3eqtrd 2214	. 2
48	40, 11	rpcxpcld 14019	. . . . 5
49	48	rpred 9683	. . . 4
50	18	reefcld 11661	. . . 4
51	49, 50	remulcld 7978	. . 3
52		abscxpbnd.4	. . . . . . 7
53		abscxpbnd.5	. . . . . . 7
54	52, 40, 53	rpgecld 9723	. . . . . 6
55	54, 11	rpcxpcld 14019	. . . . 5
56	55	rpred 9683	. . . 4
57	56, 50	remulcld 7978	. . 3
58	2	abscld 11174	. . . . . 6
59		pire 13874	. . . . . 6
60		remulcl 7930	. . . . . 6 $/\$
61	58, 59, 60	sylancl 413	. . . . 5
62	61	reefcld 11661	. . . 4
63	56, 62	remulcld 7978	. . 3
64	18	rpefcld 11678	. . . . 5
65	64	rpge0d 9687	. . . 4
66	1	rpcnd 9685	. . . . . . 7
67	1	rpap0d 9689	. . . . . . 7 #
68	66, 67	absrpclapd 11181	. . . . . 6
69	52, 68, 53	rpgecld 9723	. . . . . 6
70		rpabscxpbnd.3	. . . . . . 7
71	11, 70	elrpd 9680	. . . . . 6
72		rpcxple2 14005	. . . . . 6 $/\$ $/\$
73	68, 69, 71, 72	syl3anc 1238	. . . . 5
74	53, 73	mpbid 147	. . . 4
75	49, 56, 50, 65, 74	lemul1ad 8885	. . 3
76	55	rpge0d 9687	. . . 4
77	25	abscld 11174	. . . . . . 7
78	17	recnd 7976	. . . . . . . 8
79	78	abscld 11174	. . . . . . 7
80	77, 79	remulcld 7978	. . . . . 6
81	18	leabsd 11154	. . . . . . 7
82	25, 78	absmuld 11187	. . . . . . 7
83	81, 82	breqtrd 4026	. . . . . 6
84	58, 79	remulcld 7978	. . . . . . 7
85	78	absge0d 11177	. . . . . . . 8
86		absimle 11077	. . . . . . . . 9
87	2, 86	syl 14	. . . . . . . 8
88	77, 58, 79, 85, 87	lemul1ad 8885	. . . . . . 7
89	59	a1i 9	. . . . . . . 8
90	2	absge0d 11177	. . . . . . . 8
91	26	absnegd 11182	. . . . . . . . 9
92	59	renegcli 8209	. . . . . . . . . . . 12
93		0re 7948	. . . . . . . . . . . 12
94		pipos 13876	. . . . . . . . . . . . 13
95		lt0neg2 8416	. . . . . . . . . . . . . 14
96	59, 95	ax-mp 5	. . . . . . . . . . . . 13
97	94, 96	mpbi 145	. . . . . . . . . . . 12
98	92, 93, 97	ltleii 8050	. . . . . . . . . . 11
99	6	reim0d 10963	. . . . . . . . . . 11
100	98, 99	breqtrrid 4038	. . . . . . . . . 10
101	93, 59, 94	ltleii 8050	. . . . . . . . . . 11
102	99, 101	eqbrtrdi 4039	. . . . . . . . . 10
103		absle 11082	. . . . . . . . . . 11 $/\$ $/\$
104	16, 59, 103	sylancl 413	. . . . . . . . . 10 $/\$
105	100, 102, 104	mpbir2and 944	. . . . . . . . 9
106	91, 105	eqbrtrd 4022	. . . . . . . 8
107	79, 89, 58, 90, 106	lemul2ad 8886	. . . . . . 7
108	80, 84, 61, 88, 107	letrd 8071	. . . . . 6
109	18, 80, 61, 83, 108	letrd 8071	. . . . 5
110		efle 13864	. . . . . 6 $/\$
111	18, 61, 110	syl2anc 411	. . . . 5
112	109, 111	mpbid 147	. . . 4
113	50, 62, 56, 76, 112	lemul2ad 8886	. . 3
114	51, 57, 63, 75, 113	letrd 8071	. 2
115	47, 114	eqbrtrd 4022	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105

wceq 1353

wcel 2148 class class class wbr 4000

cfv 5212 (class class class)co 5869

cc 7800

cr 7801

cc0 7802

caddc 7805

cmul 7807

clt 7982

cle 7983

cmin 8118

cneg 8119

crp 9640

cre 10833

cim 10834

cabs 10990

ce 11634

cpi 11639

clog 13944

ccxp 13945

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4115 ax-sep 4118 ax-nul 4126 ax-pow 4171 ax-pr 4206 ax-un 4430 ax-setind 4533 ax-iinf 4584 ax-cnex 7893 ax-resscn 7894 ax-1cn 7895 ax-1re 7896 ax-icn 7897 ax-addcl 7898 ax-addrcl 7899 ax-mulcl 7900 ax-mulrcl 7901 ax-addcom 7902 ax-mulcom 7903 ax-addass 7904 ax-mulass 7905 ax-distr 7906 ax-i2m1 7907 ax-0lt1 7908 ax-1rid 7909 ax-0id 7910 ax-rnegex 7911 ax-precex 7912 ax-cnre 7913 ax-pre-ltirr 7914 ax-pre-ltwlin 7915 ax-pre-lttrn 7916 ax-pre-apti 7917 ax-pre-ltadd 7918 ax-pre-mulgt0 7919 ax-pre-mulext 7920 ax-arch 7921 ax-caucvg 7922 ax-pre-suploc 7923 ax-addf 7924 ax-mulf 7925

This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2739 df-sbc 2963 df-csb 3058 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-if 3535 df-pw 3576 df-sn 3597 df-pr 3598 df-op 3600 df-uni 3808 df-int 3843 df-iun 3886 df-disj 3978 df-br 4001 df-opab 4062 df-mpt 4063 df-tr 4099 df-id 4290 df-po 4293 df-iso 4294 df-iord 4363 df-on 4365 df-ilim 4366 df-suc 4368 df-iom 4587 df-xp 4629 df-rel 4630 df-cnv 4631 df-co 4632 df-dm 4633 df-rn 4634 df-res 4635 df-ima 4636 df-iota 5174 df-fun 5214 df-fn 5215 df-f 5216 df-f1 5217 df-fo 5218 df-f1o 5219 df-fv 5220 df-isom 5221 df-riota 5825 df-ov 5872 df-oprab 5873 df-mpo 5874 df-of 6077 df-1st 6135 df-2nd 6136 df-recs 6300 df-irdg 6365 df-frec 6386 df-1o 6411 df-oadd 6415 df-er 6529 df-map 6644 df-pm 6645 df-en 6735 df-dom 6736 df-fin 6737 df-sup 6977 df-inf 6978 df-pnf 7984 df-mnf 7985 df-xr 7986 df-ltxr 7987 df-le 7988 df-sub 8120 df-neg 8121 df-reap 8522 df-ap 8529 df-div 8619 df-inn 8909 df-2 8967 df-3 8968 df-4 8969 df-5 8970 df-6 8971 df-7 8972 df-8 8973 df-9 8974 df-n0 9166 df-z 9243 df-uz 9518 df-q 9609 df-rp 9641 df-xneg 9759 df-xadd 9760 df-ioo 9879 df-ioc 9880 df-ico 9881 df-icc 9882 df-fz 9996 df-fzo 10129 df-seqfrec 10432 df-exp 10506 df-fac 10690 df-bc 10712 df-ihash 10740 df-shft 10808 df-cj 10835 df-re 10836 df-im 10837 df-rsqrt 10991 df-abs 10992 df-clim 11271 df-sumdc 11346 df-ef 11640 df-e 11641 df-sin 11642 df-cos 11643 df-pi 11645 df-rest 12638 df-topgen 12657 df-psmet 13154 df-xmet 13155 df-met 13156 df-bl 13157 df-mopn 13158 df-top 13163 df-topon 13176 df-bases 13208 df-ntr 13263 df-cn 13355 df-cnp 13356 df-tx 13420 df-cncf 13725 df-limced 13792 df-dvap 13793 df-relog 13946 df-rpcxp 13947

This theorem is referenced by: (None)

W3C validator