abvcxp

Description: Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvcxp.a	$⊢ A = AbsVal (R)$
	abvcxp.b	$⊢ B = {Base}_{R}$
	abvcxp.f	$⊢ G = (x \in B ⟼ {F (x)}^{S})$
Assertion	abvcxp	$⊢ (F \in A \land S \in (0, 1]) \to G \in A$

Proof

Step	Hyp	Ref	Expression
1		abvcxp.a	$⊢ A = AbsVal (R)$
2		abvcxp.b	$⊢ B = {Base}_{R}$
3		abvcxp.f	$⊢ G = (x \in B ⟼ {F (x)}^{S})$
4	1	a1i	$⊢ (F \in A \land S \in (0, 1]) \to A = AbsVal (R)$
5	2	a1i	$⊢ (F \in A \land S \in (0, 1]) \to B = {Base}_{R}$
6		eqidd	$⊢ (F \in A \land S \in (0, 1]) \to +_{R} = +_{R}$
7		eqidd	$⊢ (F \in A \land S \in (0, 1]) \to \cdot_{R} = \cdot_{R}$
8		eqidd	$⊢ (F \in A \land S \in (0, 1]) \to 0_{R} = 0_{R}$
9	1	abvrcl	$⊢ F \in A \to R \in Ring$
10	9	adantr	$⊢ (F \in A \land S \in (0, 1]) \to R \in Ring$
11	1 2	abvcl	$⊢ (F \in A \land x \in B) \to F (x) \in ℝ$
12	11	adantlr	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to F (x) \in ℝ$
13	1 2	abvge0	$⊢ (F \in A \land x \in B) \to 0 \leq F (x)$
14	13	adantlr	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to 0 \leq F (x)$
15		0xr	$⊢ 0 \in ℝ^{*}$
16		1re	$⊢ 1 \in ℝ$
17		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (S \in (0, 1] \leftrightarrow (S \in ℝ \land 0 < S \land S \leq 1))$
18	15 16 17	mp2an	$⊢ S \in (0, 1] \leftrightarrow (S \in ℝ \land 0 < S \land S \leq 1)$
19	18	bilani	$⊢ (F \in A \land S \in (0, 1]) \to (S \in ℝ \land 0 < S \land S \leq 1)$
20	19	simp1d	$⊢ (F \in A \land S \in (0, 1]) \to S \in ℝ$
21	20	adantr	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to S \in ℝ$
22	12 14 21	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to {F (x)}^{S} \in ℝ$
23	22 3	fmptd	$⊢ (F \in A \land S \in (0, 1]) \to G : B ⟶ ℝ$
24		eqid	$⊢ 0_{R} = 0_{R}$
25	2 24	ring0cl	$⊢ R \in Ring \to 0_{R} \in B$
26	10 25	syl	$⊢ (F \in A \land S \in (0, 1]) \to 0_{R} \in B$
27		fveq2	$⊢ x = 0_{R} \to F (x) = F (0_{R})$
28	27	oveq1d	$⊢ x = 0_{R} \to {F (x)}^{S} = {F (0_{R})}^{S}$
29		ovex	$⊢ {F (0_{R})}^{S} \in V$
30	28 3 29	fvmpt	$⊢ 0_{R} \in B \to G (0_{R}) = {F (0_{R})}^{S}$
31	26 30	syl	$⊢ (F \in A \land S \in (0, 1]) \to G (0_{R}) = {F (0_{R})}^{S}$
32	1 24	abv0	$⊢ F \in A \to F (0_{R}) = 0$
33	32	adantr	$⊢ (F \in A \land S \in (0, 1]) \to F (0_{R}) = 0$
34	33	oveq1d	$⊢ (F \in A \land S \in (0, 1]) \to {F (0_{R})}^{S} = 0^{S}$
35	20	recnd	$⊢ (F \in A \land S \in (0, 1]) \to S \in ℂ$
36	19	simp2d	$⊢ (F \in A \land S \in (0, 1]) \to 0 < S$
37	36	gt0ne0d	$⊢ (F \in A \land S \in (0, 1]) \to S \neq 0$
38	35 37	0cxpd	$⊢ (F \in A \land S \in (0, 1]) \to 0^{S} = 0$
39	34 38	eqtrd	$⊢ (F \in A \land S \in (0, 1]) \to {F (0_{R})}^{S} = 0$
40	31 39	eqtrd	$⊢ (F \in A \land S \in (0, 1]) \to G (0_{R}) = 0$
41		simp1l	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to F \in A$
42		simp2	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to y \in B$
43	1 2	abvcl	$⊢ (F \in A \land y \in B) \to F (y) \in ℝ$
44	41 42 43	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to F (y) \in ℝ$
45	1 2 24	abvgt0	$⊢ (F \in A \land y \in B \land y \neq 0_{R}) \to 0 < F (y)$
46	45	3adant1r	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to 0 < F (y)$
47	44 46	elrpd	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to F (y) \in ℝ^{+}$
48	20	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to S \in ℝ$
49	47 48	rpcxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to {F (y)}^{S} \in ℝ^{+}$
50	49	rpgt0d	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to 0 < {F (y)}^{S}$
51		fveq2	$⊢ x = y \to F (x) = F (y)$
52	51	oveq1d	$⊢ x = y \to {F (x)}^{S} = {F (y)}^{S}$
53		ovex	$⊢ {F (y)}^{S} \in V$
54	52 3 53	fvmpt	$⊢ y \in B \to G (y) = {F (y)}^{S}$
55	42 54	syl	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to G (y) = {F (y)}^{S}$
56	50 55	breqtrrd	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to 0 < G (y)$
57		simp1l	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F \in A$
58		simp2l	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to y \in B$
59		simp3l	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to z \in B$
60		eqid	$⊢ \cdot_{R} = \cdot_{R}$
61	1 2 60	abvmul	$⊢ (F \in A \land y \in B \land z \in B) \to F (y \cdot_{R} z) = F (y) F (z)$
62	57 58 59 61	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y \cdot_{R} z) = F (y) F (z)$
63	62	oveq1d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y \cdot_{R} z)}^{S} = {F (y) F (z)}^{S}$
64	57 58 43	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y) \in ℝ$
65	1 2	abvge0	$⊢ (F \in A \land y \in B) \to 0 \leq F (y)$
66	57 58 65	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (y)$
67	1 2	abvcl	$⊢ (F \in A \land z \in B) \to F (z) \in ℝ$
68	57 59 67	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (z) \in ℝ$
69	1 2	abvge0	$⊢ (F \in A \land z \in B) \to 0 \leq F (z)$
70	57 59 69	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (z)$
71	35	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \in ℂ$
72	64 66 68 70 71	mulcxpd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y) F (z)}^{S} = {F (y)}^{S} {F (z)}^{S}$
73	63 72	eqtrd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y \cdot_{R} z)}^{S} = {F (y)}^{S} {F (z)}^{S}$
74	10	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to R \in Ring$
75	2 60	ringcl	$⊢ (R \in Ring \land y \in B \land z \in B) \to y \cdot_{R} z \in B$
76	74 58 59 75	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to y \cdot_{R} z \in B$
77		fveq2	$⊢ x = y \cdot_{R} z \to F (x) = F (y \cdot_{R} z)$
78	77	oveq1d	$⊢ x = y \cdot_{R} z \to {F (x)}^{S} = {F (y \cdot_{R} z)}^{S}$
79		ovex	$⊢ {F (y \cdot_{R} z)}^{S} \in V$
80	78 3 79	fvmpt	$⊢ y \cdot_{R} z \in B \to G (y \cdot_{R} z) = {F (y \cdot_{R} z)}^{S}$
81	76 80	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y \cdot_{R} z) = {F (y \cdot_{R} z)}^{S}$
82	58 54	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y) = {F (y)}^{S}$
83		fveq2	$⊢ x = z \to F (x) = F (z)$
84	83	oveq1d	$⊢ x = z \to {F (x)}^{S} = {F (z)}^{S}$
85		ovex	$⊢ {F (z)}^{S} \in V$
86	84 3 85	fvmpt	$⊢ z \in B \to G (z) = {F (z)}^{S}$
87	59 86	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (z) = {F (z)}^{S}$
88	82 87	oveq12d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y) G (z) = {F (y)}^{S} {F (z)}^{S}$
89	73 81 88	3eqtr4d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y \cdot_{R} z) = G (y) G (z)$
90		ringgrp	$⊢ R \in Ring \to R \in Grp$
91	74 90	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to R \in Grp$
92		eqid	$⊢ +_{R} = +_{R}$
93	2 92	grpcl	$⊢ (R \in Grp \land y \in B \land z \in B) \to y +_{R} z \in B$
94	91 58 59 93	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to y +_{R} z \in B$
95	1 2	abvcl	$⊢ (F \in A \land y +_{R} z \in B) \to F (y +_{R} z) \in ℝ$
96	57 94 95	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y +_{R} z) \in ℝ$
97	1 2	abvge0	$⊢ (F \in A \land y +_{R} z \in B) \to 0 \leq F (y +_{R} z)$
98	57 94 97	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (y +_{R} z)$
99	19	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to (S \in ℝ \land 0 < S \land S \leq 1)$
100	99	simp1d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \in ℝ$
101	96 98 100	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y +_{R} z)}^{S} \in ℝ$
102	64 68	readdcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y) + F (z) \in ℝ$
103	64 68 66 70	addge0d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (y) + F (z)$
104	102 103 100	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {(F (y) + F (z))}^{S} \in ℝ$
105	64 66 100	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y)}^{S} \in ℝ$
106	68 70 100	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (z)}^{S} \in ℝ$
107	105 106	readdcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y)}^{S} + {F (z)}^{S} \in ℝ$
108	1 2 92	abvtri	$⊢ (F \in A \land y \in B \land z \in B) \to F (y +_{R} z) \leq F (y) + F (z)$
109	57 58 59 108	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y +_{R} z) \leq F (y) + F (z)$
110	99	simp2d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 < S$
111	100 110	elrpd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \in ℝ^{+}$
112	96 98 102 103 111	cxple2d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to (F (y +_{R} z) \leq F (y) + F (z) \leftrightarrow {F (y +_{R} z)}^{S} \leq {(F (y) + F (z))}^{S})$
113	109 112	mpbid	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y +_{R} z)}^{S} \leq {(F (y) + F (z))}^{S}$
114	99	simp3d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \leq 1$
115	64 66 68 70 111 114	cxpaddle	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {(F (y) + F (z))}^{S} \leq {F (y)}^{S} + {F (z)}^{S}$
116	101 104 107 113 115	letrd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y +_{R} z)}^{S} \leq {F (y)}^{S} + {F (z)}^{S}$
117		fveq2	$⊢ x = y +_{R} z \to F (x) = F (y +_{R} z)$
118	117	oveq1d	$⊢ x = y +_{R} z \to {F (x)}^{S} = {F (y +_{R} z)}^{S}$
119		ovex	$⊢ {F (y +_{R} z)}^{S} \in V$
120	118 3 119	fvmpt	$⊢ y +_{R} z \in B \to G (y +_{R} z) = {F (y +_{R} z)}^{S}$
121	94 120	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y +_{R} z) = {F (y +_{R} z)}^{S}$
122	82 87	oveq12d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y) + G (z) = {F (y)}^{S} + {F (z)}^{S}$
123	116 121 122	3brtr4d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y +_{R} z) \leq G (y) + G (z)$
124	4 5 6 7 8 10 23 40 56 89 123	isabvd	$⊢ (F \in A \land S \in (0, 1]) \to G \in A$

Metamath Proof Explorer

Theorem abvcxp

Proof