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=\left(t\in T⟼{\left(1-{P\left(t\right)}^N\right)}^{K^N}\right)$$
	stoweidlem12.2	$$⊢\phi \to P:T⟶ℝ$$
	stoweidlem12.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	stoweidlem12.4	$$⊢\phi \to K\in {\mathbb{N}}_0$$
Assertion	stoweidlem12	$$⊢\left(\phi \wedge t\in T\right)\to Q\left(t\right)={\left(1-{P\left(t\right)}^N\right)}^{K^N}$$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem12.1	$$⊢Q=\left(t\in T⟼{\left(1-{P\left(t\right)}^N\right)}^{K^N}\right)$$
2		stoweidlem12.2	$$⊢\phi \to P:T⟶ℝ$$
3		stoweidlem12.3	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		stoweidlem12.4	$$⊢\phi \to K\in {\mathbb{N}}_0$$
5		simpr	$$⊢\left(\phi \wedge t\in T\right)\to t\in T$$
6		1red	$$⊢\left(\phi \wedge t\in T\right)\to 1\in ℝ$$
7	2	ffvelcdmda	$$⊢\left(\phi \wedge t\in T\right)\to P\left(t\right)\in ℝ$$
8	3	adantr	$$⊢\left(\phi \wedge t\in T\right)\to N\in {\mathbb{N}}_0$$
9	7 8	reexpcld	$$⊢\left(\phi \wedge t\in T\right)\to {P\left(t\right)}^N\in ℝ$$
10	6 9	resubcld	$$⊢\left(\phi \wedge t\in T\right)\to 1-{P\left(t\right)}^N\in ℝ$$
11	4 3	jca	$$⊢\phi \to \left(K\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)$$
12	11	adantr	$$⊢\left(\phi \wedge t\in T\right)\to \left(K\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)$$
13		nn0expcl	$$⊢\left(K\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to K^N\in {\mathbb{N}}_0$$
14	12 13	syl	$$⊢\left(\phi \wedge t\in T\right)\to K^N\in {\mathbb{N}}_0$$
15	10 14	reexpcld	$$⊢\left(\phi \wedge t\in T\right)\to {\left(1-{P\left(t\right)}^N\right)}^{K^N}\in ℝ$$
16	1	fvmpt2	$$⊢\left(t\in T\wedge {\left(1-{P\left(t\right)}^N\right)}^{K^N}\in ℝ\right)\to Q\left(t\right)={\left(1-{P\left(t\right)}^N\right)}^{K^N}$$
17	5 15 16	syl2anc	$$⊢\left(\phi \wedge t\in T\right)\to Q\left(t\right)={\left(1-{P\left(t\right)}^N\right)}^{K^N}$$