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 ⁡ K K + 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 → K K + 1 ⊆ D
24 22 7 23 syl2anc ⊢ K ∈ ℕ ∧ K + 1 ∈ D → K K + 1 ⊆ D
25 12 ltp1d ⊢ K ∈ ℕ ∧ K + 1 ∈ D → K < K + 1
26 12 25 ltned ⊢ K ∈ ℕ ∧ K + 1 ∈ D → K ≠ K + 1
27 pr2nelem ⊢ K ∈ D ∧ K + 1 ∈ D ∧ K ≠ K + 1 → K K + 1 ≈ 2 𝑜
28 22 7 26 27 syl3anc ⊢ K ∈ ℕ ∧ K + 1 ∈ D → K K + 1 ≈ 2 𝑜
29 eqid ⊢ ran ⁡ T = ran ⁡ T
30 2 29 pmtrrn ⊢ D ∈ Fin ∧ K K + 1 ⊆ D ∧ K K + 1 ≈ 2 𝑜 → T ⁡ K K + 1 ∈ ran ⁡ T
31 5 24 28 30 syl3anc ⊢ K ∈ ℕ ∧ K + 1 ∈ D → T ⁡ K K + 1 ∈ ran ⁡ T