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 31269

Description: Lemma for psgnfzto1st 31274. 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 7288	. . . . 5 ⊢ (𝐾 + 1) ∈ V
2		ovex 7288	. . . . . 6 ⊢ (𝑖 − 1) ∈ V
3		vex 3426	. . . . . 6 ⊢ 𝑖 ∈ V
4	2, 3	ifex 4506	. . . . 5 ⊢ if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) ∈ V
5	1, 4	ifex 4506	. . . 4 ⊢ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) ∈ V
6		eqid 2738	. . . 4 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))
7	5, 6	fnmpti 6560	. . 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 2738	. . . . 5 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
11	9, 10	pmtrto1cl 31268	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷))
12		eqid 2738	. . . . 5 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
13	10, 12	pmtrff1o 18986	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷)
14		f1ofn 6701	. . . 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 4464	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = 𝐾)
18		simpl 482	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℕ)
19	18	nnred 11918	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℝ)
20		fz1ssnn 13216	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
21	9	eleq2i 2830	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ 𝐷 ↔ (𝐾 + 1) ∈ (1...𝑁))
22	21	biimpi 215	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ 𝐷 → (𝐾 + 1) ∈ (1...𝑁))
23	22	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ (1...𝑁))
24	20, 23	sselid 3915	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℕ)
25	24	nnred 11918	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℝ)
26		elfz1b 13254	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ (1...𝑁) ↔ ((𝐾 + 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝐾 + 1) ≤ 𝑁))
27	26	simp2bi 1144	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → 𝑁 ∈ ℕ)
28	22, 27	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 + 1) ∈ 𝐷 → 𝑁 ∈ ℕ)
29	28	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℕ)
30	29	nnred 11918	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℝ)
31	19	lep1d 11836	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ (𝐾 + 1))
32		elfzle2 13189	. . . . . . . . . . . 12 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → (𝐾 + 1) ≤ 𝑁)
33	23, 32	syl 17	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ≤ 𝑁)
34	19, 25, 30, 31, 33	letrd 11062	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ 𝑁)
35	29	nnzd 12354	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℤ)
36		fznn 13253	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
38	18, 34, 37	mpbir2and 709	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ (1...𝑁))
39	38, 9	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ 𝐷)
40	39	ad2antrr 722	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝐾 ∈ 𝐷)
41	17, 40	eqeltrd 2839	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
42		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → ¬ 𝑖 = 1)
43	42	iffalsed 4467	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))
44		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝐾)
45	44	iftrued 4464	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = (𝑖 − 1))
46	42	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ¬ 𝑖 = 1)
47	9, 20	eqsstri 3951	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ⊆ ℕ
48		simpllr 772	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
49	47, 48	sselid 3915	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℕ)
50		nn1m1nn 11924	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ℕ → (𝑖 = 1 ∨ (𝑖 − 1) ∈ ℕ))
51	49, 50	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 = 1 ∨ (𝑖 − 1) ∈ ℕ))
52	51	ord 860	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (¬ 𝑖 = 1 → (𝑖 − 1) ∈ ℕ))
53	46, 52	mpd 15	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℕ)
54	53	nnred 11918	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℝ)
55	49	nnred 11918	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℝ)
56	30	ad3antrrr 726	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑁 ∈ ℝ)
57	55	lem1d 11838	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑖)
58	48, 9	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ (1...𝑁))
59		elfzle2 13189	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ≤ 𝑁)
60	58, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝑁)
61	54, 55, 56, 57, 60	letrd 11062	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑁)
62	53, 61	jca 511	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁))
63		fznn 13253	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℤ → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
64	35, 63	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
65	64	ad3antrrr 726	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ (1...𝑁) ↔ ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁)))
66	62, 65	mpbird 256	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ (1...𝑁))
67	66, 9	eleqtrrdi 2850	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ 𝐷)
68	45, 67	eqeltrd 2839	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
69		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → ¬ 𝑖 ≤ 𝐾)
70	69	iffalsed 4467	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = 𝑖)
71		simpllr 772	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
72	70, 71	eqeltrd 2839	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
73	68, 72	pm2.61dan 809	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
74	43, 73	eqeltrd 2839	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
75	41, 74	pm2.61dan 809	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
76	75	ralrimiva 3107	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
77		eqid 2738	. . . . 5 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
78	77	fnmpt 6557	. . . 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 6978	. . . 4 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
81	76, 80	syl 17	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
82		fnco 6533	. . 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 1369	. 2 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))) Fn 𝐷)
84		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → 𝑥 = 1)
85	84	iftrued 4464	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = 𝐾)
86	85	fveq2d 6760	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾))
87		fzfi 13620	. . . . . . . . . 10 ⊢ (1...𝑁) ∈ Fin
88	9, 87	eqeltri 2835	. . . . . . . . 9 ⊢ 𝐷 ∈ Fin
89	88	a1i 11	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐷 ∈ Fin)
90	23, 21	sylibr 233	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ 𝐷)
91	19	ltp1d 11835	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 < (𝐾 + 1))
92	19, 91	ltned 11041	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≠ (𝐾 + 1))
93	10	pmtrprfv 18976	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
94	89, 39, 90, 92, 93	syl13anc 1370	. . . . . . 7 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
95	94	ad2antrr 722	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝐾) = (𝐾 + 1))
96	86, 95	eqtr2d 2779	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 = 1) → (𝐾 + 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
97	88	a1i 11	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐷 ∈ Fin)
98	39	ad4antr 728	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ 𝐷)
99	90	ad4antr 728	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
100	92	ad4antr 728	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
101	10	pmtrprfv2 31259	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝐾 ≠ (𝐾 + 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
102	97, 98, 99, 100, 101	syl13anc 1370	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)) = 𝐾)
103	91	ad4antr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < (𝐾 + 1))
104		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 = (𝐾 + 1))
105	103, 104	breqtrrd 5098	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < 𝑥)
106	19	ad4antr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
107		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
108	47, 107	sselid 3915	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℕ)
109	108	nnred 11918	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℝ)
110	109	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 ∈ ℝ)
111	106, 110	ltnled 11052	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐾))
112	105, 111	mpbid 231	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
113	112	iffalsed 4467	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
114	113, 104	eqtrd 2778	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = (𝐾 + 1))
115	114	fveq2d 6760	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝐾 + 1)))
116	104	oveq1d 7270	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = ((𝐾 + 1) − 1))
117	106	recnd 10934	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℂ)
118		1cnd 10901	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 1 ∈ ℂ)
119	117, 118	pncand 11263	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) − 1) = 𝐾)
120	116, 119	eqtrd 2778	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = 𝐾)
121	102, 115, 120	3eqtr4rd 2789	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
122		simplr 765	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ (𝐾 + 1))
123		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≠ (𝐾 + 1))
124	123	necomd 2998	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
125	109	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ ℝ)
126	25	ad4antr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
127	125, 126	ltlend 11050	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 < (𝐾 + 1) ↔ (𝑥 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑥)))
128	122, 124, 127	mpbir2and 709	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 < (𝐾 + 1))
129	108	ad3antrrr 726	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ ℕ)
130		simpll 763	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝐾 ∈ ℕ)
131	130	ad3antrrr 726	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ∈ ℕ)
132		nnleltp1 12305	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑥 ≤ 𝐾 ↔ 𝑥 < (𝐾 + 1)))
133	129, 131, 132	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 ≤ 𝐾 ↔ 𝑥 < (𝐾 + 1)))
134	128, 133	mpbird 256	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝐾)
135	134	iftrued 4464	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = (𝑥 − 1))
136	135	fveq2d 6760	. . . . . . . . 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 728	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ∈ 𝐷)
139		simp-5r 782	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
140		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → ¬ 𝑥 = 1)
141	140	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ¬ 𝑥 = 1)
142		elnn1uz2 12594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ ↔ (𝑥 = 1 ∨ 𝑥 ∈ (ℤ_≥‘2)))
143	129, 142	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 = 1 ∨ 𝑥 ∈ (ℤ_≥‘2)))
144	143	ord 860	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (¬ 𝑥 = 1 → 𝑥 ∈ (ℤ_≥‘2)))
145	141, 144	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (ℤ_≥‘2))
146		uz2m1nn 12592	. . . . . . . . . . . . . . 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 11918	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℝ)
150	131, 139, 30	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℝ)
151	125	lem1d 11838	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑥)
152	107	ad3antrrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
153	152, 9	eleqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (1...𝑁))
154		elfzle2 13189	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
155	153, 154	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝑁)
156	149, 125, 150, 151, 155	letrd 11062	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑁)
157	147, 148, 156	3jca 1126	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
158		elfz1b 13254	. . . . . . . . . . . . 13 ⊢ ((𝑥 − 1) ∈ (1...𝑁) ↔ ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
159	157, 158	sylibr 233	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ (1...𝑁))
160	159, 9	eleqtrrdi 2850	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ 𝐷)
161	138, 139, 160	3jca 1126	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷))
162	131, 139, 92	syl2anc 583	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
163		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝐾 = (𝑥 − 1))
164	163	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → (𝐾 + 1) = ((𝑥 − 1) + 1))
165	109	recnd 10934	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
166	165	ad3antrrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 ∈ ℂ)
167		1cnd 10901	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 1 ∈ ℂ)
168	166, 167	npcand 11266	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → ((𝑥 − 1) + 1) = 𝑥)
169	164, 168	eqtr2d 2779	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 = (𝐾 + 1))
170	169	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝐾 = (𝑥 − 1) → 𝑥 = (𝐾 + 1)))
171	170	necon3d 2963	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 ≠ (𝐾 + 1) → 𝐾 ≠ (𝑥 − 1)))
172	171	imp 406	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝑥 − 1))
173	149, 125, 126, 151, 128	lelttrd 11063	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) < (𝐾 + 1))
174	149, 173	ltned 11041	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≠ (𝐾 + 1))
175	174	necomd 2998	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 + 1) ≠ (𝑥 − 1))
176	162, 172, 175	3jca 1126	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1)))
177	10	pmtrprfv3 18977	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ (𝑥 − 1) ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ (𝑥 − 1) ∧ (𝐾 + 1) ≠ (𝑥 − 1))) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
178	137, 161, 176, 177	syl3anc 1369	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘(𝑥 − 1)) = (𝑥 − 1))
179	136, 178	eqtr2d 2779	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
180	121, 179	pm2.61dane 3031	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
181	109	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ∈ ℝ)
182	19	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝐾 ∈ ℝ)
183	25	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → (𝐾 + 1) ∈ ℝ)
184		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝑥 ≤ 𝐾)
185	31	ad3antrrr 726	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ 𝐾) → 𝐾 ≤ (𝐾 + 1))
186	181, 182, 183, 184, 185	letrd 11062	. . . . . . . . . . . . 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 4467	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
191	190	fveq2d 6760	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥))
192	88	a1i 11	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐷 ∈ Fin)
193	39	ad3antrrr 726	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ∈ 𝐷)
194	90	ad3antrrr 726	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ∈ 𝐷)
195	107	ad2antrr 722	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
196	193, 194, 195	3jca 1126	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷))
197	92	ad3antrrr 726	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ (𝐾 + 1))
198	19	ad3antrrr 726	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ∈ ℝ)
199	25	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ)
200	109	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 ∈ ℝ)
201	91	ad3antrrr 726	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < (𝐾 + 1))
202		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ¬ 𝑥 ≤ (𝐾 + 1))
203	199, 200	ltnled 11052	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ((𝐾 + 1) < 𝑥 ↔ ¬ 𝑥 ≤ (𝐾 + 1)))
204	202, 203	mpbird 256	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) < 𝑥)
205	198, 199, 200, 201, 204	lttrd 11066	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < 𝑥)
206	198, 205	ltned 11041	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ 𝑥)
207	199, 204	ltned 11041	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
208	197, 206, 207	3jca 1126	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥))
209	10	pmtrprfv3 18977	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
210	192, 196, 208, 209	syl3anc 1369	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
211	191, 210	eqtr2d 2779	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
212	180, 211	ifeqda 4492	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
213	140	iffalsed 4467	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
214	213	fveq2d 6760	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
215	212, 214	eqtr4d 2781	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
216	96, 215	ifeqda 4492	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
217		eqidd 2739	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
218		eqeq1 2742	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1))
219		breq1 5073	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐾 ↔ 𝑥 ≤ 𝐾))
220		oveq1 7262	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1))
221		id 22	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥)
222	219, 220, 221	ifbieq12d 4484	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
223	218, 222	ifbieq2d 4482	. . . . . . 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 7288	. . . . . . . . 9 ⊢ (𝑥 − 1) ∈ V
226		vex 3426	. . . . . . . . 9 ⊢ 𝑥 ∈ V
227	225, 226	ifcli 4503	. . . . . . . 8 ⊢ if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V
228	227	a1i 11	. . . . . . 7 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V)
229	130, 228	ifexd 4504	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) ∈ V)
230	217, 224, 107, 229	fvmptd 6864	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥) = if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
231	230	fveq2d 6760	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
232	216, 231	eqtr4d 2781	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
233		breq1 5073	. . . . . . 7 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ (𝐾 + 1) ↔ 𝑥 ≤ (𝐾 + 1)))
234	233, 220, 221	ifbieq12d 4484	. . . . . 6 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) = if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥))
235	218, 234	ifbieq2d 4482	. . . . 5 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
236	225, 226	ifex 4506	. . . . . 6 ⊢ if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) ∈ V
237	1, 236	ifex 4506	. . . . 5 ⊢ if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) ∈ V
238	235, 6, 237	fvmpt 6857	. . . 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 6456	. . . . 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 6134	. . . . . 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 2842	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
246		fvco 6848	. . . 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 583	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
248	232, 239, 247	3eqtr4d 2788	. 2 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥))
249	8, 83, 248	eqfnfvd 6894	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 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 Vcvv 3422 ⊆ wss 3883 ifcif 4456 {cpr 4560 class class class wbr 5070 ↦ cmpt 5153 dom cdm 5580 ran crn 5581 ∘ ccom 5584 Fun wfun 6412 Fn wfn 6413 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 Fincfn 8691 ℂcc 10800 ℝcr 10801 1c1 10803 + caddc 10805 < clt 10940 ≤ cle 10941 − cmin 11135 ℕcn 11903 2c2 11958 ℤcz 12249 ℤ_≥cuz 12511 ...cfz 13168 pmTrspcpmtr 18964

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-pmtr 18965

This theorem is referenced by: fzto1st 31272 psgnfzto1st 31274

W3C validator