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 33069

Description: Lemma for psgnfzto1st 33074. 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 7379	. . . . 5 ⊢ (𝐾 + 1) ∈ V
2		ovex 7379	. . . . . 6 ⊢ (𝑖 − 1) ∈ V
3		vex 3440	. . . . . 6 ⊢ 𝑖 ∈ V
4	2, 3	ifex 4523	. . . . 5 ⊢ if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) ∈ V
5	1, 4	ifex 4523	. . . 4 ⊢ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) ∈ V
6		eqid 2731	. . . 4 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))
7	5, 6	fnmpti 6624	. . 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 2731	. . . . 5 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
11	9, 10	pmtrto1cl 33068	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷))
12		eqid 2731	. . . . 5 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
13	10, 12	pmtrff1o 19375	. . . 4 ⊢ (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∈ ran (pmTrsp‘𝐷) → ((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}):𝐷–1-1-onto→𝐷)
14		f1ofn 6764	. . . 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 4480	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = 𝐾)
18		simpl 482	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℕ)
19	18	nnred 12140	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ ℝ)
20		fz1ssnn 13455	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℕ
21	9	eleq2i 2823	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 + 1) ∈ 𝐷 ↔ (𝐾 + 1) ∈ (1...𝑁))
22	21	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ((𝐾 + 1) ∈ 𝐷 → (𝐾 + 1) ∈ (1...𝑁))
23	22	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ (1...𝑁))
24	20, 23	sselid 3927	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℕ)
25	24	nnred 12140	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ ℝ)
26		elfz1b 13493	. . . . . . . . . . . . . . 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 12140	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℝ)
31	19	lep1d 12053	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ (𝐾 + 1))
32		elfzle2 13428	. . . . . . . . . . . 12 ⊢ ((𝐾 + 1) ∈ (1...𝑁) → (𝐾 + 1) ≤ 𝑁)
33	23, 32	syl 17	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ≤ 𝑁)
34	19, 25, 30, 31, 33	letrd 11270	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≤ 𝑁)
35	29	nnzd 12495	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝑁 ∈ ℤ)
36		fznn 13492	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
37	35, 36	syl 17	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 ∈ (1...𝑁) ↔ (𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁)))
38	18, 34, 37	mpbir2and 713	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ (1...𝑁))
39	38, 9	eleqtrrdi 2842	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ∈ 𝐷)
40	39	ad2antrr 726	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → 𝐾 ∈ 𝐷)
41	17, 40	eqeltrd 2831	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
42		simpr 484	. . . . . . . 8 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → ¬ 𝑖 = 1)
43	42	iffalsed 4483	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) = if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))
44		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝐾)
45	44	iftrued 4480	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = (𝑖 − 1))
46	42	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ¬ 𝑖 = 1)
47	9, 20	eqsstri 3976	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ⊆ ℕ
48		simpllr 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
49	47, 48	sselid 3927	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℕ)
50		nn1m1nn 12146	. . . . . . . . . . . . . . 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 12140	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ ℝ)
55	49	nnred 12140	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ ℝ)
56	30	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑁 ∈ ℝ)
57	55	lem1d 12055	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑖)
58	48, 9	eleqtrdi 2841	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ∈ (1...𝑁))
59		elfzle2 13428	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (1...𝑁) → 𝑖 ≤ 𝑁)
60	58, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → 𝑖 ≤ 𝑁)
61	54, 55, 56, 57, 60	letrd 11270	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ≤ 𝑁)
62	53, 61	jca 511	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → ((𝑖 − 1) ∈ ℕ ∧ (𝑖 − 1) ≤ 𝑁))
63		fznn 13492	. . . . . . . . . . . . 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 2842	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → (𝑖 − 1) ∈ 𝐷)
68	45, 67	eqeltrd 2831	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
69		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → ¬ 𝑖 ≤ 𝐾)
70	69	iffalsed 4483	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = 𝑖)
71		simpllr 775	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → 𝑖 ∈ 𝐷)
72	70, 71	eqeltrd 2831	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) ∧ ¬ 𝑖 ≤ 𝐾) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
73	68, 72	pm2.61dan 812	. . . . . . 7 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) ∈ 𝐷)
74	43, 73	eqeltrd 2831	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) ∧ ¬ 𝑖 = 1) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
75	41, 74	pm2.61dan 812	. . . . 5 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑖 ∈ 𝐷) → if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
76	75	ralrimiva 3124	. . . 4 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷)
77		eqid 2731	. . . . 5 ⊢ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))
78	77	fnmpt 6621	. . . 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 7056	. . . 4 ⊢ (∀𝑖 ∈ 𝐷 if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)) ∈ 𝐷 → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
81	76, 80	syl 17	. . 3 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → ran (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) ⊆ 𝐷)
82		fnco 6599	. . 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 4480	. . . . . . 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 2827	. . . . . . . . 9 ⊢ 𝐷 ∈ Fin
89	88	a1i 11	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐷 ∈ Fin)
90	23, 21	sylibr 234	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝐾 + 1) ∈ 𝐷)
91	19	ltp1d 12052	. . . . . . . . 9 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 < (𝐾 + 1))
92	19, 91	ltned 11249	. . . . . . . 8 ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → 𝐾 ≠ (𝐾 + 1))
93	10	pmtrprfv 19365	. . . . . . . 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 2767	. . . . 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 33057	. . . . . . . . . 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 5117	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 < 𝑥)
106	19	ad4antr 732	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℝ)
107		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷)
108	47, 107	sselid 3927	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℕ)
109	108	nnred 12140	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℝ)
110	109	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝑥 ∈ ℝ)
111	106, 110	ltnled 11260	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝐾 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐾))
112	105, 111	mpbid 232	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ¬ 𝑥 ≤ 𝐾)
113	112	iffalsed 4483	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) = 𝑥)
114	113, 104	eqtrd 2766	. . . . . . . . . 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 7361	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = ((𝐾 + 1) − 1))
117	106	recnd 11140	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 𝐾 ∈ ℂ)
118		1cnd 11107	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → 1 ∈ ℂ)
119	117, 118	pncand 11473	. . . . . . . . . 10 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) − 1) = 𝐾)
120	116, 119	eqtrd 2766	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 − 1) = 𝐾)
121	102, 115, 120	3eqtr4rd 2777	. . . . . . . 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 2983	. . . . . . . . . . . . 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 11258	. . . . . . . . . . . . 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 12528	. . . . . . . . . . . . 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 4480	. . . . . . . . . 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 12823	. . . . . . . . . . . . . . . . . 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 12821	. . . . . . . . . . . . . . 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 12140	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ ℝ)
150	131, 139, 30	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑁 ∈ ℝ)
151	125	lem1d 12055	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑥)
152	107	ad3antrrr 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ 𝐷)
153	152, 9	eleqtrdi 2841	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ∈ (1...𝑁))
154		elfzle2 13428	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
155	153, 154	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝑥 ≤ 𝑁)
156	149, 125, 150, 151, 155	letrd 11270	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≤ 𝑁)
157	147, 148, 156	3jca 1128	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
158		elfz1b 13493	. . . . . . . . . . . . 13 ⊢ ((𝑥 − 1) ∈ (1...𝑁) ↔ ((𝑥 − 1) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑥 − 1) ≤ 𝑁))
159	157, 158	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ∈ (1...𝑁))
160	159, 9	eleqtrrdi 2842	. . . . . . . . . . 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 7361	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → (𝐾 + 1) = ((𝑥 − 1) + 1))
165	109	recnd 11140	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
166	165	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 ∈ ℂ)
167		1cnd 11107	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 1 ∈ ℂ)
168	166, 167	npcand 11476	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → ((𝑥 − 1) + 1) = 𝑥)
169	164, 168	eqtr2d 2767	. . . . . . . . . . . . . 14 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝐾 = (𝑥 − 1)) → 𝑥 = (𝐾 + 1))
170	169	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝐾 = (𝑥 − 1) → 𝑥 = (𝐾 + 1)))
171	170	necon3d 2949	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) → (𝑥 ≠ (𝐾 + 1) → 𝐾 ≠ (𝑥 − 1)))
172	171	imp 406	. . . . . . . . . . 11 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → 𝐾 ≠ (𝑥 − 1))
173	149, 125, 126, 151, 128	lelttrd 11271	. . . . . . . . . . . . 13 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) < (𝐾 + 1))
174	149, 173	ltned 11249	. . . . . . . . . . . 12 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) ≠ (𝐾 + 1))
175	174	necomd 2983	. . . . . . . . . . 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 19366	. . . . . . . . . 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 2767	. . . . . . . 8 ⊢ ((((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ 𝑥 ≤ (𝐾 + 1)) ∧ 𝑥 ≠ (𝐾 + 1)) → (𝑥 − 1) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
180	121, 179	pm2.61dane 3015	. . . . . . 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 11270	. . . . . . . . . . . . 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 4483	. . . . . . . . 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 11260	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → ((𝐾 + 1) < 𝑥 ↔ ¬ 𝑥 ≤ (𝐾 + 1)))
204	202, 203	mpbird 257	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) < 𝑥)
205	198, 199, 200, 201, 204	lttrd 11274	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 < 𝑥)
206	198, 205	ltned 11249	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝐾 ≠ 𝑥)
207	199, 204	ltned 11249	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑥)
208	197, 206, 207	3jca 1128	. . . . . . . . 9 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥))
209	10	pmtrprfv3 19366	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ (𝐾 ∈ 𝐷 ∧ (𝐾 + 1) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷) ∧ (𝐾 ≠ (𝐾 + 1) ∧ 𝐾 ≠ 𝑥 ∧ (𝐾 + 1) ≠ 𝑥)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
210	192, 196, 208, 209	syl3anc 1373	. . . . . . . 8 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘𝑥) = 𝑥)
211	191, 210	eqtr2d 2767	. . . . . . 7 ⊢ (((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) ∧ ¬ 𝑥 ≤ (𝐾 + 1)) → 𝑥 = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
212	180, 211	ifeqda 4509	. . . . . 6 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)))
213	140	iffalsed 4483	. . . . . . 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 2769	. . . . 5 ⊢ ((((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) ∧ ¬ 𝑥 = 1) → if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
216	96, 215	ifeqda 4509	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))))
217		eqidd 2732	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))) = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
218		eqeq1 2735	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → (𝑖 = 1 ↔ 𝑥 = 1))
219		breq1 5092	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ 𝐾 ↔ 𝑥 ≤ 𝐾))
220		oveq1 7353	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → (𝑖 − 1) = (𝑥 − 1))
221		id 22	. . . . . . . . 9 ⊢ (𝑖 = 𝑥 → 𝑖 = 𝑥)
222	219, 220, 221	ifbieq12d 4501	. . . . . . . 8 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖) = if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥))
223	218, 222	ifbieq2d 4499	. . . . . . 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 7379	. . . . . . . . 9 ⊢ (𝑥 − 1) ∈ V
226		vex 3440	. . . . . . . . 9 ⊢ 𝑥 ∈ V
227	225, 226	ifcli 4520	. . . . . . . 8 ⊢ if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V
228	227	a1i 11	. . . . . . 7 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥) ∈ V)
229	130, 228	ifexd 4521	. . . . . 6 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, 𝐾, if(𝑥 ≤ 𝐾, (𝑥 − 1), 𝑥)) ∈ V)
230	217, 224, 107, 229	fvmptd 6936	. . . . 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 2769	. . 3 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)})‘((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖)))‘𝑥)))
233		breq1 5092	. . . . . . 7 ⊢ (𝑖 = 𝑥 → (𝑖 ≤ (𝐾 + 1) ↔ 𝑥 ≤ (𝐾 + 1)))
234	233, 220, 221	ifbieq12d 4501	. . . . . 6 ⊢ (𝑖 = 𝑥 → if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖) = if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥))
235	218, 234	ifbieq2d 4499	. . . . 5 ⊢ (𝑖 = 𝑥 → if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)) = if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)))
236	225, 226	ifex 4523	. . . . . 6 ⊢ if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥) ∈ V
237	1, 236	ifex 4523	. . . . 5 ⊢ if(𝑥 = 1, (𝐾 + 1), if(𝑥 ≤ (𝐾 + 1), (𝑥 − 1), 𝑥)) ∈ V
238	235, 6, 237	fvmpt 6929	. . . 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 6519	. . . . 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 6189	. . . . . 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 2834	. . . 4 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ dom (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))
246		fvco 6920	. . . 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 2776	. 2 ⊢ (((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) ∧ 𝑥 ∈ 𝐷) → ((𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖)))‘𝑥) = ((((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))‘𝑥))
249	8, 83, 248	eqfnfvd 6967	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 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 Vcvv 3436 ⊆ wss 3897 ifcif 4472 {cpr 4575 class class class wbr 5089 ↦ cmpt 5170 dom cdm 5614 ran crn 5615 ∘ ccom 5618 Fun wfun 6475 Fn wfn 6476 –1-1-onto→wf1o 6480 ‘cfv 6481 (class class class)co 7346 Fincfn 8869 ℂcc 11004 ℝcr 11005 1c1 11007 + caddc 11009 < clt 11146 ≤ cle 11147 − cmin 11344 ℕcn 12125 2c2 12180 ℤcz 12468 ℤ_≥cuz 12732 ...cfz 13407 pmTrspcpmtr 19353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-nn 12126 df-2 12188 df-n0 12382 df-z 12469 df-uz 12733 df-fz 13408 df-pmtr 19354

This theorem is referenced by: fzto1st 33072 psgnfzto1st 33074

W3C validator