Metamath Proof Explorer


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 T 1 P t N K N
stoweidlem12.2 φ P : T
stoweidlem12.3 φ N 0
stoweidlem12.4 φ K 0
Assertion stoweidlem12 φ t T Q t = 1 P t N K N

Proof

Step Hyp Ref Expression
1 stoweidlem12.1 Q = t T 1 P t N K N
2 stoweidlem12.2 φ P : T
3 stoweidlem12.3 φ N 0
4 stoweidlem12.4 φ K 0
5 simpr φ t T t T
6 1red φ t T 1
7 2 ffvelrnda φ t T P t
8 3 adantr φ t T N 0
9 7 8 reexpcld φ t T P t N
10 6 9 resubcld φ t T 1 P t N
11 4 3 jca φ K 0 N 0
12 11 adantr φ t T K 0 N 0
13 nn0expcl K 0 N 0 K N 0
14 12 13 syl φ t T K N 0
15 10 14 reexpcld φ t T 1 P t N K N
16 1 fvmpt2 t T 1 P t N K N Q t = 1 P t N K N
17 5 15 16 syl2anc φ t T Q t = 1 P t N K N