Theorem stoweidlem12

Description: Lemma for stoweid . This Lemma is used by other three Lemmas. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem12.1	|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
	stoweidlem12.2	|- ( ph -> P : T --> RR )
	stoweidlem12.3	|- ( ph -> N e. NN0 )
	stoweidlem12.4	|- ( ph -> K e. NN0 )
Assertion	stoweidlem12	|- ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem12.1	|- Q = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
2		stoweidlem12.2	|- ( ph -> P : T --> RR )
3		stoweidlem12.3	|- ( ph -> N e. NN0 )
4		stoweidlem12.4	|- ( ph -> K e. NN0 )
5		simpr	|- ( ( ph /\ t e. T ) -> t e. T )
6		1red	|- ( ( ph /\ t e. T ) -> 1 e. RR )
7	2	ffvelrnda	|- ( ( ph /\ t e. T ) -> ( P ` t ) e. RR )
8	3	adantr	|- ( ( ph /\ t e. T ) -> N e. NN0 )
9	7 8	reexpcld	|- ( ( ph /\ t e. T ) -> ( ( P ` t ) ^ N ) e. RR )
10	6 9	resubcld	|- ( ( ph /\ t e. T ) -> ( 1 - ( ( P ` t ) ^ N ) ) e. RR )
11	4 3	jca	|- ( ph -> ( K e. NN0 /\ N e. NN0 ) )
12	11	adantr	|- ( ( ph /\ t e. T ) -> ( K e. NN0 /\ N e. NN0 ) )
13		nn0expcl	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( K ^ N ) e. NN0 )
14	12 13	syl	|- ( ( ph /\ t e. T ) -> ( K ^ N ) e. NN0 )
15	10 14	reexpcld	|- ( ( ph /\ t e. T ) -> ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR )
16	1	fvmpt2	|- ( ( t e. T /\ ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) e. RR ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )
17	5 15 16	syl2anc	|- ( ( ph /\ t e. T ) -> ( Q ` t ) = ( ( 1 - ( ( P ` t ) ^ N ) ) ^ ( K ^ N ) ) )