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 33043

Description: Lemma for psgnfzto1st 33048. 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 7382	. . . . 5 ⊢ (𝐾 + 1) ∈ V
2		ovex 7382	. . . . . 6 ⊢ (𝑖 − 1) ∈ V
3		vex 3440	. . . . . 6 ⊢ 𝑖 ∈ V
4	2, 3	ifex 4527	. . . . 5 ⊢ if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) ∈ V
5	1, 4	ifex 4527	. . . 4 ⊢ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) ∈ V
6		eqid 2729	. . . 4 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))
7	5, 6	fnmpti 6625	. . 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 2729	. . . . 5 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
11	9, 10	pmtrto1cl 33042	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷))
12		eqid 2729	. . . . 5 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
13	10, 12	pmtrff1o 19342	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷)
14		f1ofn 6765	. . . 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 4484	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = 𝐾)
18		simpl 482	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℕ)
19	18	nnred 12143	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℝ)
20		fz1ssnn 13458	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
21	9	eleq2i 2820	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ 𝐷 ↔ (𝐾 + 1) ∈ (1...𝑁))
22	21	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ 𝐷 → (𝐾 + 1) ∈ (1...𝑁))
23	22	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ (1...𝑁))
24	20, 23	sselid 3933	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℕ)
25	24	nnred 12143	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℝ)
26		elfz1b 13496	. . . . . . . . . . . . . . 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 12143	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℝ)
31	19	lep1d 12056	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ (𝐾 + 1))
32		elfzle2 13431	. . . . . . . . . . . 12 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → (𝐾 + 1) ≤ 𝑁)
33	23, 32	syl 17	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ≤ 𝑁)
34	19, 25, 30, 31, 33	letrd 11273	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ 𝑁)
35	29	nnzd 12498	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℤ)
36		fznn 13495	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
38	18, 34, 37	mpbir2and 713	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ (1...𝑁))
39	38, 9	eleqtrrdi 2839	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ 𝐷)
40	39	ad2antrr 726	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝐾 ∈ 𝐷)
41	17, 40	eqeltrd 2828	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
42		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → ¬ 𝑖 = 1)
43	42	iffalsed 4487	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))
44		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝐾)
45	44	iftrued 4484	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = (𝑖 − 1))
46	42	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ¬ 𝑖 = 1)
47	9, 20	eqsstri 3982	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ⊆ ℕ
48		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
49	47, 48	sselid 3933	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℕ)
50		nn1m1nn 12149	. . . . . . . . . . . . . . 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 12143	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℝ)
55	49	nnred 12143	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℝ)
56	30	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑁 ∈ ℝ)
57	55	lem1d 12058	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑖)
58	48, 9	eleqtrdi 2838	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ (1...𝑁))
59		elfzle2 13431	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ≤ 𝑁)
60	58, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝑁)
61	54, 55, 56, 57, 60	letrd 11273	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑁)
62	53, 61	jca 511	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁))
63		fznn 13495	. . . . . . . . . . . . 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 2839	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ 𝐷)
68	45, 67	eqeltrd 2828	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
69		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → ¬ 𝑖 ≤ 𝐾)
70	69	iffalsed 4487	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = 𝑖)
71		simpllr 775	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
72	70, 71	eqeltrd 2828	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
73	68, 72	pm2.61dan 812	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
74	43, 73	eqeltrd 2828	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
75	41, 74	pm2.61dan 812	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
76	75	ralrimiva 3121	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
77		eqid 2729	. . . . 5 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
78	77	fnmpt 6622	. . . 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 7057	. . . 4 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
81	76, 80	syl 17	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
82		fnco 6600	. . 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 1373	. 2 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))) Fn 𝐷)
84		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → 𝑥 = 1)
85	84	iftrued 4484	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = 𝐾)
86	85	fveq2d 6826	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾))
87		fzfi 13879	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
88	9, 87	eqeltri 2824	. . . . . . . . 9 ⊢ 𝐷 ∈ Fin
89	88	a1i 11	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐷 ∈ Fin)
90	23, 21	sylibr 234	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ 𝐷)
91	19	ltp1d 12055	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 < (𝐾 + 1))
92	19, 91	ltned 11252	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≠ (𝐾 + 1))
93	10	pmtrprfv 19332	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
94	89, 39, 90, 92, 93	syl13anc 1374	. . . . . . 7 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
95	94	ad2antrr 726	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
96	86, 95	eqtr2d 2765	. . . . 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 33031	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
102	97, 98, 99, 100, 101	syl13anc 1374	. . . . . . . . 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 5120	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < 𝑥)
106	19	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
107		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
108	47, 107	sselid 3933	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℕ)
109	108	nnred 12143	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℝ)
110	109	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 ∈ ℝ)
111	106, 110	ltnled 11263	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐾))
112	105, 111	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
113	112	iffalsed 4487	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
114	113, 104	eqtrd 2764	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = (𝐾 + 1))
115	114	fveq2d 6826	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)))
116	104	oveq1d 7364	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = ((𝐾 + 1) − 1))
117	106	recnd 11143	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℂ)
118		1cnd 11110	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 1 ∈ ℂ)
119	117, 118	pncand 11476	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) − 1) = 𝐾)
120	116, 119	eqtrd 2764	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = 𝐾)
121	102, 115, 120	3eqtr4rd 2775	. . . . . . . 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 2980	. . . . . . . . . . . . 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 11261	. . . . . . . . . . . . 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 12531	. . . . . . . . . . . . 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 4484	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = (𝑥 − 1))
136	135	fveq2d 6826	. . . . . . . . 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 12826	. . . . . . . . . . . . . . . . . 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 12824	. . . . . . . . . . . . . . 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 12143	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℝ)
150	131, 139, 30	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℝ)
151	125	lem1d 12058	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑥)
152	107	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
153	152, 9	eleqtrdi 2838	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (1...𝑁))
154		elfzle2 13431	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
155	153, 154	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝑁)
156	149, 125, 150, 151, 155	letrd 11273	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑁)
157	147, 148, 156	3jca 1128	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
158		elfz1b 13496	. . . . . . . . . . . . 13 ⊢ ((𝑥 − 1) ∈ (1...𝑁) ↔ ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
159	157, 158	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ (1...𝑁))
160	159, 9	eleqtrrdi 2839	. . . . . . . . . . 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 7364	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → (𝐾 + 1) = ((𝑥 − 1) + 1))
165	109	recnd 11143	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
166	165	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 ∈ ℂ)
167		1cnd 11110	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 1 ∈ ℂ)
168	166, 167	npcand 11479	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → ((𝑥 − 1) + 1) = 𝑥)
169	164, 168	eqtr2d 2765	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 = (𝐾 + 1))
170	169	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝐾 = (𝑥 − 1) → 𝑥 = (𝐾 + 1)))
171	170	necon3d 2946	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 ≠ (𝐾 + 1) → 𝐾 ≠ (𝑥 − 1)))
172	171	imp 406	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝑥 − 1))
173	149, 125, 126, 151, 128	lelttrd 11274	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) < (𝐾 + 1))
174	149, 173	ltned 11252	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≠ (𝐾 + 1))
175	174	necomd 2980	. . . . . . . . . . 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 19333	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
178	137, 161, 176, 177	syl3anc 1373	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
179	136, 178	eqtr2d 2765	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
180	121, 179	pm2.61dane 3012	. . . . . . 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 11273	. . . . . . . . . . . . 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 4487	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
191	190	fveq2d 6826	. . . . . . . 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 11263	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ((𝐾 + 1) < 𝑥 ↔ ¬ 𝑥 ≤ (𝐾 + 1)))
204	202, 203	mpbird 257	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) < 𝑥)
205	198, 199, 200, 201, 204	lttrd 11277	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < 𝑥)
206	198, 205	ltned 11252	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ 𝑥)
207	199, 204	ltned 11252	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
208	197, 206, 207	3jca 1128	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥))
209	10	pmtrprfv3 19333	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
210	192, 196, 208, 209	syl3anc 1373	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
211	191, 210	eqtr2d 2765	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
212	180, 211	ifeqda 4513	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
213	140	iffalsed 4487	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
214	213	fveq2d 6826	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
215	212, 214	eqtr4d 2767	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
216	96, 215	ifeqda 4513	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
217		eqidd 2730	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
218		eqeq1 2733	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1))
219		breq1 5095	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐾 ↔ 𝑥 ≤ 𝐾))
220		oveq1 7356	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1))
221		id 22	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥)
222	219, 220, 221	ifbieq12d 4505	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
223	218, 222	ifbieq2d 4503	. . . . . . 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 7382	. . . . . . . . 9 ⊢ (𝑥 − 1) ∈ V
226		vex 3440	. . . . . . . . 9 ⊢ 𝑥 ∈ V
227	225, 226	ifcli 4524	. . . . . . . 8 ⊢ if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V
228	227	a1i 11	. . . . . . 7 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V)
229	130, 228	ifexd 4525	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) ∈ V)
230	217, 224, 107, 229	fvmptd 6937	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
231	230	fveq2d 6826	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
232	216, 231	eqtr4d 2767	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
233		breq1 5095	. . . . . . 7 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ (𝐾 + 1) ↔ 𝑥 ≤ (𝐾 + 1)))
234	233, 220, 221	ifbieq12d 4505	. . . . . 6 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) = if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥))
235	218, 234	ifbieq2d 4503	. . . . 5 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
236	225, 226	ifex 4527	. . . . . 6 ⊢ if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) ∈ V
237	1, 236	ifex 4527	. . . . 5 ⊢ if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) ∈ V
238	235, 6, 237	fvmpt 6930	. . . 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 6520	. . . . 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 6191	. . . . . 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 2831	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
246		fvco 6921	. . . 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 2774	. 2 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥))
249	8, 83, 248	eqfnfvd 6968	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 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 Vcvv 3436 ⊆ wss 3903 ifcif 4476 {cpr 4579 class class class wbr 5092 ↦ cmpt 5173 dom cdm 5619 ran crn 5620 ∘ ccom 5623 Fun wfun 6476 Fn wfn 6477 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 Fincfn 8872 ℂcc 11007 ℝcr 11008 1c1 11010 + caddc 11012 < clt 11149 ≤ cle 11150 − cmin 11347 ℕcn 12128 2c2 12183 ℤcz 12471 ℤ_≥cuz 12735 ...cfz 13410 pmTrspcpmtr 19320

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-2 12191 df-n0 12385 df-z 12472 df-uz 12736 df-fz 13411 df-pmtr 19321

This theorem is referenced by: fzto1st 33046 psgnfzto1st 33048

W3C validator