Metamath Proof Explorer

Theorem pmtrto1cl

Description: Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypotheses psgnfzto1st.d ⊢D=1…N
pmtrto1cl.t ⊢T=pmTrsp⁡D
Assertion pmtrto1cl ⊢K∈ℕ∧K+1∈D→T⁡KK+1∈ran⁡T

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢D=1…N
2 pmtrto1cl.t ⊢T=pmTrsp⁡D
3 fzfi ⊢1…N∈Fin
4 1 3 eqeltri ⊢D∈Fin
5 4 a1i ⊢K∈ℕ∧K+1∈D→D∈Fin
6 simpl ⊢K∈ℕ∧K+1∈D→K∈ℕ
7 simpr ⊢K∈ℕ∧K+1∈D→K+1∈D
8 7 1 eleqtrdi ⊢K∈ℕ∧K+1∈D→K+1∈1…N
9 elfz1b ⊢K+1∈1…N↔K+1∈ℕ∧N∈ℕ∧K+1≤N
10 8 9 sylib ⊢K∈ℕ∧K+1∈D→K+1∈ℕ∧N∈ℕ∧K+1≤N
11 10 simp2d ⊢K∈ℕ∧K+1∈D→N∈ℕ
12 6 nnred ⊢K∈ℕ∧K+1∈D→K∈ℝ
13 1red ⊢K∈ℕ∧K+1∈D→1∈ℝ
14 12 13 readdcld ⊢K∈ℕ∧K+1∈D→K+1∈ℝ
15 11 nnred ⊢K∈ℕ∧K+1∈D→N∈ℝ
16 12 lep1d ⊢K∈ℕ∧K+1∈D→K≤K+1
17 10 simp3d ⊢K∈ℕ∧K+1∈D→K+1≤N
18 12 14 15 16 17 letrd ⊢K∈ℕ∧K+1∈D→K≤N
19 6 11 18 3jca ⊢K∈ℕ∧K+1∈D→K∈ℕ∧N∈ℕ∧K≤N
20 elfz1b ⊢K∈1…N↔K∈ℕ∧N∈ℕ∧K≤N
21 19 20 sylibr ⊢K∈ℕ∧K+1∈D→K∈1…N
22 21 1 eleqtrrdi ⊢K∈ℕ∧K+1∈D→K∈D
23 prssi ⊢K∈D∧K+1∈D→KK+1⊆D
24 22 7 23 syl2anc ⊢K∈ℕ∧K+1∈D→KK+1⊆D
25 12 ltp1d ⊢K∈ℕ∧K+1∈D→K<K+1
26 12 25 ltned ⊢K∈ℕ∧K+1∈D→K≠K+1
27 enpr2 ⊢K∈D∧K+1∈D∧K≠K+1→KK+1≈2𝑜
28 22 7 26 27 syl3anc ⊢K∈ℕ∧K+1∈D→KK+1≈2𝑜
29 eqid ⊢ran⁡T=ran⁡T
30 2 29 pmtrrn ⊢D∈Fin∧KK+1⊆D∧KK+1≈2𝑜→T⁡KK+1∈ran⁡T
31 5 24 28 30 syl3anc ⊢K∈ℕ∧K+1∈D→T⁡KK+1∈ran⁡T