psgnfzto1stlem - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > psgnfzto1stlem		Structured version Visualization version GIF version

Theorem psgnfzto1stlem 33488

Description: Lemma for psgnfzto1st 33493. Our permutation of rank (𝑛 + 1) can be written as a permutation of rank 𝑛 composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.)

**Hypothesis**
Ref	Expression
psgnfzto1st.d	⊢ 𝐷 = (1...𝑁)

**Assertion**
Ref	Expression
psgnfzto1stlem	⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))))

Distinct variable groups: 𝐷,𝑖 𝑖,𝐾 Allowed substitution hint: 𝑁(𝑖)

Proof of Theorem psgnfzto1stlem Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 7452	. . . . 5 ⊢ (𝐾 + 1) ∈ V
2		ovex 7452	. . . . . 6 ⊢ (𝑖 − 1) ∈ V
3		vex 3461	. . . . . 6 ⊢ 𝑖 ∈ V
4	2, 3	ifex 4540	. . . . 5 ⊢ if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) ∈ V
5	1, 4	ifex 4540	. . . 4 ⊢ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) ∈ V
6		eqid 2765	. . . 4 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))
7	5, 6	fnmpti 6682	. . 3 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) Fn 𝐷
8	7	a1i 11	. 2 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) Fn 𝐷)
9		psgnfzto1st.d	. . . . 5 ⊢ 𝐷 = (1...𝑁)
10		eqid 2765	. . . . 5 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
11	9, 10	pmtrto1cl 33487	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷))
12		eqid 2765	. . . . 5 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
13	10, 12	pmtrff1o 19581	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷)
14		f1ofn 6825	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷 → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) Fn 𝐷)
15	11, 13, 14	3syl 19	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) Fn 𝐷)
16		simpr 490	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝑖 = 1)
17	16	iftrued 4497	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = 𝐾)
18		simpl 488	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℕ)
19	18	nnred 12267	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℝ)
20		fz1ssnn 13604	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
21	9	eleq2i 2857	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ 𝐷 ↔ (𝐾 + 1) ∈ (1...𝑁))
22	21	biimpi 219	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ 𝐷 → (𝐾 + 1) ∈ (1...𝑁))
23	22	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ (1...𝑁))
24	20, 23	sselid 3936	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℕ)
25	24	nnred 12267	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℝ)
26		elfz1b 13642	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ (1...𝑁) ↔ ((𝐾 + 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾 + 1) ≤ 𝑁))
27	26	simp2bi 1164	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → 𝑁 ∈ ℕ)
28	22, 27	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ 𝐷 → 𝑁 ∈ ℕ)
29	28	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℕ)
30	29	nnred 12267	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℝ)
31	19	lep1d 12165	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ (𝐾 + 1))
32		elfzle2 13576	. . . . . . . . . . . 12 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → (𝐾 + 1) ≤ 𝑁)
33	23, 32	syl 18	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ≤ 𝑁)
34	19, 25, 30, 31, 33	letrd 11386	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ 𝑁)
35	29	nnzd 12636	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℤ)
36		fznn 13641	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
37	35, 36	syl 18	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
38	18, 34, 37	mpbir2and 726	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ (1...𝑁))
39	38, 9	eleqtrrdi 2876	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ 𝐷)
40	39	ad2antrr 739	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝐾 ∈ 𝐷)
41	17, 40	eqeltrd 2865	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
42		simpr 490	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → ¬ 𝑖 = 1)
43	42	iffalsed 4500	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))
44		simpr 490	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝐾)
45	44	iftrued 4497	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = (𝑖 − 1))
46	42	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ¬ 𝑖 = 1)
47	9, 20	eqsstri 3984	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ⊆ ℕ
48		simpllr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
49	47, 48	sselid 3936	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℕ)
50		nn1m1nn 12273	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ℕ → (𝑖 = 1 ∨ (𝑖 − 1) ∈ ℕ))
51	49, 50	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 = 1 ∨ (𝑖 − 1) ∈ ℕ))
52	51	ord 878	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (¬ 𝑖 = 1 → (𝑖 − 1) ∈ ℕ))
53	46, 52	mpd 16	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℕ)
54	53	nnred 12267	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℝ)
55	49	nnred 12267	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℝ)
56	30	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑁 ∈ ℝ)
57	55	lem1d 12167	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑖)
58	48, 9	eleqtrdi 2875	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ (1...𝑁))
59		elfzle2 13576	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ≤ 𝑁)
60	58, 59	syl 18	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝑁)
61	54, 55, 56, 57, 60	letrd 11386	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑁)
62	53, 61	jca 521	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁))
63		fznn 13641	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
64	35, 63	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
65	64	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
66	62, 65	mpbird 260	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ (1...𝑁))
67	66, 9	eleqtrrdi 2876	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ 𝐷)
68	45, 67	eqeltrd 2865	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
69		simpr 490	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → ¬ 𝑖 ≤ 𝐾)
70	69	iffalsed 4500	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = 𝑖)
71		simpllr 788	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
72	70, 71	eqeltrd 2865	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
73	68, 72	pm2.61dan 825	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
74	43, 73	eqeltrd 2865	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
75	41, 74	pm2.61dan 825	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
76	75	ralrimiva 3159	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
77		eqid 2765	. . . . 5 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
78	77	fnmpt 6679	. . . 4 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) Fn 𝐷)
79	76, 78	syl 18	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) Fn 𝐷)
80	77	rnmptss 7122	. . . 4 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
81	76, 80	syl 18	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
82		fnco 6657	. . 3 ⊢ ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) Fn 𝐷 ∧ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) Fn 𝐷 ∧ ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))) Fn 𝐷)
83	15, 79, 81, 82	syl3anc 1398	. 2 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))) Fn 𝐷)
84		simpr 490	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → 𝑥 = 1)
85	84	iftrued 4497	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = 𝐾)
86	85	fveq2d 6889	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾))
87		fzfi 14030	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
88	9, 87	eqeltri 2861	. . . . . . . . 9 ⊢ 𝐷 ∈ Fin
89	88	a1i 11	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐷 ∈ Fin)
90	23, 21	sylibr 237	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ 𝐷)
91	19	ltp1d 12164	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 < (𝐾 + 1))
92	19, 91	ltned 11365	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≠ (𝐾 + 1))
93	10	pmtrprfv 19571	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
94	89, 39, 90, 92, 93	syl13anc 1399	. . . . . . 7 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
95	94	ad2antrr 739	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
96	86, 95	eqtr2d 2801	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (𝐾 + 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
97	88	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐷 ∈ Fin)
98	39	ad4antr 745	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ 𝐷)
99	90	ad4antr 745	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
100	92	ad4antr 745	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
101	10	pmtrprfv2 33476	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
102	97, 98, 99, 100, 101	syl13anc 1399	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
103	91	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < (𝐾 + 1))
104		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 = (𝐾 + 1))
105	103, 104	breqtrrd 5141	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < 𝑥)
106	19	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
107		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
108	47, 107	sselid 3936	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℕ)
109	108	nnred 12267	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℝ)
110	109	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 ∈ ℝ)
111	106, 110	ltnled 11376	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐾))
112	105, 111	mpbid 235	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
113	112	iffalsed 4500	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
114	113, 104	eqtrd 2800	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = (𝐾 + 1))
115	114	fveq2d 6889	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)))
116	104	oveq1d 7434	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = ((𝐾 + 1) − 1))
117	106	recnd 11256	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℂ)
118		1cnd 11221	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 1 ∈ ℂ)
119	117, 118	pncand 11589	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) − 1) = 𝐾)
120	116, 119	eqtrd 2800	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = 𝐾)
121	102, 115, 120	3eqtr4rd 2811	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
122		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ (𝐾 + 1))
123		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≠ (𝐾 + 1))
124	123	necomd 3015	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
125	109	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ ℝ)
126	25	ad4antr 745	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
127	125, 126	ltlend 11374	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 < (𝐾 + 1) ↔ (𝑥 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑥)))
128	122, 124, 127	mpbir2and 726	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 < (𝐾 + 1))
129	108	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ ℕ)
130		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝐾 ∈ ℕ)
131	130	ad3antrrr 743	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ∈ ℕ)
132		nnleltp1 12671	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑥 ≤ 𝐾 ↔ 𝑥 < (𝐾 + 1)))
133	129, 131, 132	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 ≤ 𝐾 ↔ 𝑥 < (𝐾 + 1)))
134	128, 133	mpbird 260	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝐾)
135	134	iftrued 4497	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = (𝑥 − 1))
136	135	fveq2d 6889	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)))
137	88	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐷 ∈ Fin)
138	39	ad4antr 745	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ∈ 𝐷)
139		simp-5r 798	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
140		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → ¬ 𝑥 = 1)
141	140	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ¬ 𝑥 = 1)
142		elnn1uz2 12969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ ↔ (𝑥 = 1 ∨ 𝑥 ∈ (ℤ_≥‘2)))
143	129, 142	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 = 1 ∨ 𝑥 ∈ (ℤ_≥‘2)))
144	143	ord 878	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (¬ 𝑥 = 1 → 𝑥 ∈ (ℤ_≥‘2)))
145	141, 144	mpd 16	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (ℤ_≥‘2))
146		uz2m1nn 12967	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℤ_≥‘2) → (𝑥 − 1) ∈ ℕ)
147	145, 146	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℕ)
148	139, 28	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℕ)
149	147	nnred 12267	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℝ)
150	131, 139, 30	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℝ)
151	125	lem1d 12167	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑥)
152	107	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
153	152, 9	eleqtrdi 2875	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (1...𝑁))
154		elfzle2 13576	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
155	153, 154	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝑁)
156	149, 125, 150, 151, 155	letrd 11386	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑁)
157	147, 148, 156	3jca 1146	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
158		elfz1b 13642	. . . . . . . . . . . . 13 ⊢ ((𝑥 − 1) ∈ (1...𝑁) ↔ ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
159	157, 158	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ (1...𝑁))
160	159, 9	eleqtrrdi 2876	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ 𝐷)
161	138, 139, 160	3jca 1146	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷))
162	131, 139, 92	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
163		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝐾 = (𝑥 − 1))
164	163	oveq1d 7434	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → (𝐾 + 1) = ((𝑥 − 1) + 1))
165	109	recnd 11256	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
166	165	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 ∈ ℂ)
167		1cnd 11221	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 1 ∈ ℂ)
168	166, 167	npcand 11592	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → ((𝑥 − 1) + 1) = 𝑥)
169	164, 168	eqtr2d 2801	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 = (𝐾 + 1))
170	169	ex 418	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝐾 = (𝑥 − 1) → 𝑥 = (𝐾 + 1)))
171	170	necon3d 2981	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 ≠ (𝐾 + 1) → 𝐾 ≠ (𝑥 − 1)))
172	171	imp 412	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝑥 − 1))
173	149, 125, 126, 151, 128	lelttrd 11387	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) < (𝐾 + 1))
174	149, 173	ltned 11365	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≠ (𝐾 + 1))
175	174	necomd 3015	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ≠ (𝑥 − 1))
176	162, 172, 175	3jca 1146	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1)))
177	10	pmtrprfv3 19572	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
178	137, 161, 176, 177	syl3anc 1398	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
179	136, 178	eqtr2d 2801	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
180	121, 179	pm2.61dane 3047	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
181	109	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ∈ ℝ)
182	19	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝐾 ∈ ℝ)
183	25	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → (𝐾 + 1) ∈ ℝ)
184		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ≤ 𝐾)
185	31	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝐾 ≤ (𝐾 + 1))
186	181, 182, 183, 184, 185	letrd 11386	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ≤ (𝐾 + 1))
187	186	ex 418	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (𝑥 ≤ 𝐾 → 𝑥 ≤ (𝐾 + 1)))
188	187	con3d 153	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (¬ 𝑥 ≤ (𝐾 + 1) → ¬ 𝑥 ≤ 𝐾))
189	188	imp 412	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
190	189	iffalsed 4500	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
191	190	fveq2d 6889	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥))
192	88	a1i 11	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐷 ∈ Fin)
193	39	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ∈ 𝐷)
194	90	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
195	107	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
196	193, 194, 195	3jca 1146	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷))
197	92	ad3antrrr 743	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
198	19	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ∈ ℝ)
199	25	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
200	109	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 ∈ ℝ)
201	91	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < (𝐾 + 1))
202		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ¬ 𝑥 ≤ (𝐾 + 1))
203	199, 200	ltnled 11376	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ((𝐾 + 1) < 𝑥 ↔ ¬ 𝑥 ≤ (𝐾 + 1)))
204	202, 203	mpbird 260	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) < 𝑥)
205	198, 199, 200, 201, 204	lttrd 11390	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < 𝑥)
206	198, 205	ltned 11365	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ 𝑥)
207	199, 204	ltned 11365	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
208	197, 206, 207	3jca 1146	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥))
209	10	pmtrprfv3 19572	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
210	192, 196, 208, 209	syl3anc 1398	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
211	191, 210	eqtr2d 2801	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
212	180, 211	ifeqda 4526	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
213	140	iffalsed 4500	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
214	213	fveq2d 6889	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
215	212, 214	eqtr4d 2803	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
216	96, 215	ifeqda 4526	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
217		eqidd 2766	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
218		eqeq1 2769	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1))
219		breq1 5114	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐾 ↔ 𝑥 ≤ 𝐾))
220		oveq1 7426	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1))
221		id 23	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥)
222	219, 220, 221	ifbieq12d 4518	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
223	218, 222	ifbieq2d 4516	. . . . . . 7 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
224	223	adantl 487	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 = 𝑥) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
225		ovex 7452	. . . . . . . . 9 ⊢ (𝑥 − 1) ∈ V
226		vex 3461	. . . . . . . . 9 ⊢ 𝑥 ∈ V
227	225, 226	ifcli 4537	. . . . . . . 8 ⊢ if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V
228	227	a1i 11	. . . . . . 7 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V)
229	130, 228	ifexd 4538	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) ∈ V)
230	217, 224, 107, 229	fvmptd 7001	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
231	230	fveq2d 6889	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
232	216, 231	eqtr4d 2803	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
233		breq1 5114	. . . . . . 7 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ (𝐾 + 1) ↔ 𝑥 ≤ (𝐾 + 1)))
234	233, 220, 221	ifbieq12d 4518	. . . . . 6 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) = if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥))
235	218, 234	ifbieq2d 4516	. . . . 5 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
236	225, 226	ifex 4540	. . . . . 6 ⊢ if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) ∈ V
237	1, 236	ifex 4540	. . . . 5 ⊢ if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) ∈ V
238	235, 6, 237	fvmpt 6993	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
239	238	adantl 487	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
240		funmpt 6578	. . . . 5 ⊢ Fun (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
241	240	a1i 11	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → Fun (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
242	76	adantr 486	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
243		dmmptg 6245	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = 𝐷)
244	242, 243	syl 18	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = 𝐷)
245	107, 244	eleqtrrd 2868	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
246		fvco 6983	. . . 4 ⊢ ((Fun (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ∧ 𝑥 ∈ dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))) → ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
247	241, 245, 246	syl2anc 596	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
248	232, 239, 247	3eqtr4d 2810	. 2 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥))
249	8, 83, 248	eqfnfvd 7032	1 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 Vcvv 3457 ⊆ wss 3906 ifcif 4489 {cpr 4593 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ran crn 5664 ∘ ccom 5667 Fun wfun 6534 Fn wfn 6535 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7419 Fincfn 8949 ℂcc 11117 ℝcr 11118 1c1 11120 + caddc 11122 < clt 11262 ≤ cle 11263 − cmin 11460 ℕcn 12252 2c2 12314 ℤcz 12610 ℤ_≥cuz 12882 ...cfz 13555 pmTrspcpmtr 19559

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11175 ax-resscn 11176 ax-1cn 11177 ax-icn 11178 ax-addcl 11179 ax-addrcl 11180 ax-mulcl 11181 ax-mulrcl 11182 ax-mulcom 11183 ax-addass 11184 ax-mulass 11185 ax-distr 11186 ax-i2m1 11187 ax-1ne0 11188 ax-1rid 11189 ax-rnegex 11190 ax-rrecex 11191 ax-cnre 11192 ax-pre-lttri 11193 ax-pre-lttrn 11194 ax-pre-ltadd 11195 ax-pre-mulgt0 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-pnf 11264 df-mnf 11265 df-xr 11266 df-ltxr 11267 df-le 11268 df-sub 11462 df-neg 11463 df-nn 12253 df-2 12322 df-n0 12524 df-z 12611 df-uz 12883 df-fz 13556 df-pmtr 19560

This theorem is used by: fzto1st 33491 psgnfzto1st 33493

W3C validator