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	⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
	stoweidlem12.2	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
	stoweidlem12.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	stoweidlem12.4	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	stoweidlem12	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem12.1	⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
2		stoweidlem12.2	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
3		stoweidlem12.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		stoweidlem12.4	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
6		1red	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
7	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℕ0 )
9	7 8	reexpcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ )
10	6 9	resubcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ )
11	4 3	jca	⊢ ( 𝜑 → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
13		nn0expcl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
15	10 14	reexpcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ )
16	1	fvmpt2	⊢ ( ( 𝑡 ∈ 𝑇 ∧ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
17	5 15 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )