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 33050

Description: Lemma for psgnfzto1st 33055. 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 7445	. . . . 5 ⊢ (𝐾 + 1) ∈ V
2		ovex 7445	. . . . . 6 ⊢ (𝑖 − 1) ∈ V
3		vex 3467	. . . . . 6 ⊢ 𝑖 ∈ V
4	2, 3	ifex 4556	. . . . 5 ⊢ if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) ∈ V
5	1, 4	ifex 4556	. . . 4 ⊢ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) ∈ V
6		eqid 2734	. . . 4 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))
7	5, 6	fnmpti 6690	. . 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 2734	. . . . 5 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
11	9, 10	pmtrto1cl 33049	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷))
12		eqid 2734	. . . . 5 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
13	10, 12	pmtrff1o 19448	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷)
14		f1ofn 6828	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷 → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) Fn 𝐷)
15	11, 13, 14	3syl 18	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) Fn 𝐷)
16		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝑖 = 1)
17	16	iftrued 4513	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = 𝐾)
18		simpl 482	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℕ)
19	18	nnred 12262	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℝ)
20		fz1ssnn 13576	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
21	9	eleq2i 2825	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ 𝐷 ↔ (𝐾 + 1) ∈ (1...𝑁))
22	21	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ 𝐷 → (𝐾 + 1) ∈ (1...𝑁))
23	22	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ (1...𝑁))
24	20, 23	sselid 3961	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℕ)
25	24	nnred 12262	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℝ)
26		elfz1b 13614	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ (1...𝑁) ↔ ((𝐾 + 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾 + 1) ≤ 𝑁))
27	26	simp2bi 1146	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → 𝑁 ∈ ℕ)
28	22, 27	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ 𝐷 → 𝑁 ∈ ℕ)
29	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℕ)
30	29	nnred 12262	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℝ)
31	19	lep1d 12180	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ (𝐾 + 1))
32		elfzle2 13549	. . . . . . . . . . . 12 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → (𝐾 + 1) ≤ 𝑁)
33	23, 32	syl 17	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ≤ 𝑁)
34	19, 25, 30, 31, 33	letrd 11399	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ 𝑁)
35	29	nnzd 12622	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℤ)
36		fznn 13613	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
38	18, 34, 37	mpbir2and 713	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ (1...𝑁))
39	38, 9	eleqtrrdi 2844	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ 𝐷)
40	39	ad2antrr 726	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝐾 ∈ 𝐷)
41	17, 40	eqeltrd 2833	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
42		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → ¬ 𝑖 = 1)
43	42	iffalsed 4516	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))
44		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝐾)
45	44	iftrued 4513	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = (𝑖 − 1))
46	42	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ¬ 𝑖 = 1)
47	9, 20	eqsstri 4010	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ⊆ ℕ
48		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
49	47, 48	sselid 3961	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℕ)
50		nn1m1nn 12268	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ℕ → (𝑖 = 1 ∨ (𝑖 − 1) ∈ ℕ))
51	49, 50	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 = 1 ∨ (𝑖 − 1) ∈ ℕ))
52	51	ord 864	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (¬ 𝑖 = 1 → (𝑖 − 1) ∈ ℕ))
53	46, 52	mpd 15	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℕ)
54	53	nnred 12262	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℝ)
55	49	nnred 12262	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℝ)
56	30	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑁 ∈ ℝ)
57	55	lem1d 12182	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑖)
58	48, 9	eleqtrdi 2843	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ (1...𝑁))
59		elfzle2 13549	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ≤ 𝑁)
60	58, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝑁)
61	54, 55, 56, 57, 60	letrd 11399	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑁)
62	53, 61	jca 511	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁))
63		fznn 13613	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
64	35, 63	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
65	64	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
66	62, 65	mpbird 257	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ (1...𝑁))
67	66, 9	eleqtrrdi 2844	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ 𝐷)
68	45, 67	eqeltrd 2833	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
69		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → ¬ 𝑖 ≤ 𝐾)
70	69	iffalsed 4516	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = 𝑖)
71		simpllr 775	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
72	70, 71	eqeltrd 2833	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
73	68, 72	pm2.61dan 812	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
74	43, 73	eqeltrd 2833	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
75	41, 74	pm2.61dan 812	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
76	75	ralrimiva 3133	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
77		eqid 2734	. . . . 5 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
78	77	fnmpt 6687	. . . 4 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) Fn 𝐷)
79	76, 78	syl 17	. . 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 17	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
82		fnco 6665	. . 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 1372	. 2 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))) Fn 𝐷)
84		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → 𝑥 = 1)
85	84	iftrued 4513	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = 𝐾)
86	85	fveq2d 6889	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾))
87		fzfi 13994	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
88	9, 87	eqeltri 2829	. . . . . . . . 9 ⊢ 𝐷 ∈ Fin
89	88	a1i 11	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐷 ∈ Fin)
90	23, 21	sylibr 234	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ 𝐷)
91	19	ltp1d 12179	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 < (𝐾 + 1))
92	19, 91	ltned 11378	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≠ (𝐾 + 1))
93	10	pmtrprfv 19438	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
94	89, 39, 90, 92, 93	syl13anc 1373	. . . . . . 7 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
95	94	ad2antrr 726	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
96	86, 95	eqtr2d 2770	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (𝐾 + 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
97	88	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐷 ∈ Fin)
98	39	ad4antr 732	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ 𝐷)
99	90	ad4antr 732	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
100	92	ad4antr 732	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
101	10	pmtrprfv2 33038	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
102	97, 98, 99, 100, 101	syl13anc 1373	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
103	91	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < (𝐾 + 1))
104		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 = (𝐾 + 1))
105	103, 104	breqtrrd 5151	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < 𝑥)
106	19	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
107		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
108	47, 107	sselid 3961	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℕ)
109	108	nnred 12262	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℝ)
110	109	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 ∈ ℝ)
111	106, 110	ltnled 11389	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐾))
112	105, 111	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
113	112	iffalsed 4516	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
114	113, 104	eqtrd 2769	. . . . . . . . . 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 7427	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = ((𝐾 + 1) − 1))
117	106	recnd 11270	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℂ)
118		1cnd 11237	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 1 ∈ ℂ)
119	117, 118	pncand 11602	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) − 1) = 𝐾)
120	116, 119	eqtrd 2769	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = 𝐾)
121	102, 115, 120	3eqtr4rd 2780	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
122		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ (𝐾 + 1))
123		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≠ (𝐾 + 1))
124	123	necomd 2986	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
125	109	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ ℝ)
126	25	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
127	125, 126	ltlend 11387	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 < (𝐾 + 1) ↔ (𝑥 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑥)))
128	122, 124, 127	mpbir2and 713	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 < (𝐾 + 1))
129	108	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ ℕ)
130		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝐾 ∈ ℕ)
131	130	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ∈ ℕ)
132		nnleltp1 12655	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑥 ≤ 𝐾 ↔ 𝑥 < (𝐾 + 1)))
133	129, 131, 132	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 ≤ 𝐾 ↔ 𝑥 < (𝐾 + 1)))
134	128, 133	mpbird 257	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝐾)
135	134	iftrued 4513	. . . . . . . . . 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 732	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ∈ 𝐷)
139		simp-5r 785	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
140		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → ¬ 𝑥 = 1)
141	140	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ¬ 𝑥 = 1)
142		elnn1uz2 12948	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ ↔ (𝑥 = 1 ∨ 𝑥 ∈ (ℤ_≥‘2)))
143	129, 142	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 = 1 ∨ 𝑥 ∈ (ℤ_≥‘2)))
144	143	ord 864	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (¬ 𝑥 = 1 → 𝑥 ∈ (ℤ_≥‘2)))
145	141, 144	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (ℤ_≥‘2))
146		uz2m1nn 12946	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℤ_≥‘2) → (𝑥 − 1) ∈ ℕ)
147	145, 146	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℕ)
148	139, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℕ)
149	147	nnred 12262	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℝ)
150	131, 139, 30	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℝ)
151	125	lem1d 12182	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑥)
152	107	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
153	152, 9	eleqtrdi 2843	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (1...𝑁))
154		elfzle2 13549	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
155	153, 154	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝑁)
156	149, 125, 150, 151, 155	letrd 11399	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑁)
157	147, 148, 156	3jca 1128	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
158		elfz1b 13614	. . . . . . . . . . . . 13 ⊢ ((𝑥 − 1) ∈ (1...𝑁) ↔ ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
159	157, 158	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ (1...𝑁))
160	159, 9	eleqtrrdi 2844	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ 𝐷)
161	138, 139, 160	3jca 1128	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷))
162	131, 139, 92	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
163		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝐾 = (𝑥 − 1))
164	163	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → (𝐾 + 1) = ((𝑥 − 1) + 1))
165	109	recnd 11270	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
166	165	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 ∈ ℂ)
167		1cnd 11237	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 1 ∈ ℂ)
168	166, 167	npcand 11605	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → ((𝑥 − 1) + 1) = 𝑥)
169	164, 168	eqtr2d 2770	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 = (𝐾 + 1))
170	169	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝐾 = (𝑥 − 1) → 𝑥 = (𝐾 + 1)))
171	170	necon3d 2952	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 ≠ (𝐾 + 1) → 𝐾 ≠ (𝑥 − 1)))
172	171	imp 406	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝑥 − 1))
173	149, 125, 126, 151, 128	lelttrd 11400	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) < (𝐾 + 1))
174	149, 173	ltned 11378	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≠ (𝐾 + 1))
175	174	necomd 2986	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ≠ (𝑥 − 1))
176	162, 172, 175	3jca 1128	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1)))
177	10	pmtrprfv3 19439	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
178	137, 161, 176, 177	syl3anc 1372	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
179	136, 178	eqtr2d 2770	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
180	121, 179	pm2.61dane 3018	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
181	109	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ∈ ℝ)
182	19	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝐾 ∈ ℝ)
183	25	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → (𝐾 + 1) ∈ ℝ)
184		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ≤ 𝐾)
185	31	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝐾 ≤ (𝐾 + 1))
186	181, 182, 183, 184, 185	letrd 11399	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ≤ (𝐾 + 1))
187	186	ex 412	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (𝑥 ≤ 𝐾 → 𝑥 ≤ (𝐾 + 1)))
188	187	con3d 152	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (¬ 𝑥 ≤ (𝐾 + 1) → ¬ 𝑥 ≤ 𝐾))
189	188	imp 406	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
190	189	iffalsed 4516	. . . . . . . . 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 730	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ∈ 𝐷)
194	90	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
195	107	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
196	193, 194, 195	3jca 1128	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷))
197	92	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
198	19	ad3antrrr 730	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ∈ ℝ)
199	25	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
200	109	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 ∈ ℝ)
201	91	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < (𝐾 + 1))
202		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ¬ 𝑥 ≤ (𝐾 + 1))
203	199, 200	ltnled 11389	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ((𝐾 + 1) < 𝑥 ↔ ¬ 𝑥 ≤ (𝐾 + 1)))
204	202, 203	mpbird 257	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) < 𝑥)
205	198, 199, 200, 201, 204	lttrd 11403	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < 𝑥)
206	198, 205	ltned 11378	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ 𝑥)
207	199, 204	ltned 11378	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
208	197, 206, 207	3jca 1128	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥))
209	10	pmtrprfv3 19439	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
210	192, 196, 208, 209	syl3anc 1372	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
211	191, 210	eqtr2d 2770	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
212	180, 211	ifeqda 4542	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
213	140	iffalsed 4516	. . . . . . 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 2772	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
216	96, 215	ifeqda 4542	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
217		eqidd 2735	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
218		eqeq1 2738	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1))
219		breq1 5126	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐾 ↔ 𝑥 ≤ 𝐾))
220		oveq1 7419	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1))
221		id 22	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥)
222	219, 220, 221	ifbieq12d 4534	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
223	218, 222	ifbieq2d 4532	. . . . . . 7 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
224	223	adantl 481	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑖 = 𝑥) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
225		ovex 7445	. . . . . . . . 9 ⊢ (𝑥 − 1) ∈ V
226		vex 3467	. . . . . . . . 9 ⊢ 𝑥 ∈ V
227	225, 226	ifcli 4553	. . . . . . . 8 ⊢ if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V
228	227	a1i 11	. . . . . . 7 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V)
229	130, 228	ifexd 4554	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) ∈ V)
230	217, 224, 107, 229	fvmptd 7002	. . . . 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 2772	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
233		breq1 5126	. . . . . . 7 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ (𝐾 + 1) ↔ 𝑥 ≤ (𝐾 + 1)))
234	233, 220, 221	ifbieq12d 4534	. . . . . 6 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) = if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥))
235	218, 234	ifbieq2d 4532	. . . . 5 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
236	225, 226	ifex 4556	. . . . . 6 ⊢ if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) ∈ V
237	1, 236	ifex 4556	. . . . 5 ⊢ if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) ∈ V
238	235, 6, 237	fvmpt 6995	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
239	238	adantl 481	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
240		funmpt 6583	. . . . 5 ⊢ Fun (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
241	240	a1i 11	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → Fun (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
242	76	adantr 480	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
243		dmmptg 6242	. . . . . 6 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = 𝐷)
244	242, 243	syl 17	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = 𝐷)
245	107, 244	eleqtrrd 2836	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
246		fvco 6986	. . . 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 584	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
248	232, 239, 247	3eqtr4d 2779	. 2 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥))
249	8, 83, 248	eqfnfvd 7033	1 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 Vcvv 3463 ⊆ wss 3931 ifcif 4505 {cpr 4608 class class class wbr 5123 ↦ cmpt 5205 dom cdm 5665 ran crn 5666 ∘ ccom 5669 Fun wfun 6534 Fn wfn 6535 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7412 Fincfn 8966 ℂcc 11134 ℝcr 11135 1c1 11137 + caddc 11139 < clt 11276 ≤ cle 11277 − cmin 11473 ℕcn 12247 2c2 12302 ℤcz 12595 ℤ_≥cuz 12859 ...cfz 13528 pmTrspcpmtr 19426

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7736 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6493 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7869 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-2o 8488 df-er 8726 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11475 df-neg 11476 df-nn 12248 df-2 12310 df-n0 12509 df-z 12596 df-uz 12860 df-fz 13529 df-pmtr 19427

This theorem is referenced by: fzto1st 33053 psgnfzto1st 33055

W3C validator