psgnfzto1stlem

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

		Ref	Expression
	Hypothesis	psgnfzto1st.d	$⊢ D = (1 \dots N)$
	Assertion	psgnfzto1stlem	$⊢ (K \in ℕ \land K + 1 \in D) \to (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) = pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$

Proof

Step	Hyp	Ref	Expression
1		psgnfzto1st.d	$⊢ D = (1 \dots N)$
2		ovex	$⊢ K + 1 \in V$
3		ovex	$⊢ i - 1 \in V$
4		vex	$⊢ i \in V$
5	3 4	ifex	$⊢ if (i \leq K + 1, i - 1, i) \in V$
6	2 5	ifex	$⊢ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i)) \in V$
7		eqid	$⊢ (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) = (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i)))$
8	6 7	fnmpti	$⊢ (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) Fn D$
9	8	a1i	$⊢ (K \in ℕ \land K + 1 \in D) \to (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) Fn D$
10		eqid	$⊢ pmTrsp (D) = pmTrsp (D)$
11	1 10	pmtrto1cl	$⊢ (K \in ℕ \land K + 1 \in D) \to pmTrsp (D) (\{K, K + 1\}) \in ran pmTrsp (D)$
12		eqid	$⊢ ran pmTrsp (D) = ran pmTrsp (D)$
13	10 12	pmtrff1o	$⊢ pmTrsp (D) (\{K, K + 1\}) \in ran pmTrsp (D) \to pmTrsp (D) (\{K, K + 1\}) : D \underset{1-1 onto}{⟶} D$
14		f1ofn	$⊢ pmTrsp (D) (\{K, K + 1\}) : D \underset{1-1 onto}{⟶} D \to pmTrsp (D) (\{K, K + 1\}) Fn D$
15	11 13 14	3syl	$⊢ (K \in ℕ \land K + 1 \in D) \to pmTrsp (D) (\{K, K + 1\}) Fn D$
16		simpr	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land i = 1) \to i = 1$
17	16	iftrued	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land i = 1) \to if (i = 1, K, if (i \leq K, i - 1, i)) = K$
18		simpl	$⊢ (K \in ℕ \land K + 1 \in D) \to K \in ℕ$
19	18	nnred	$⊢ (K \in ℕ \land K + 1 \in D) \to K \in ℝ$
20		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
21	1	eleq2i	$⊢ K + 1 \in D \leftrightarrow K + 1 \in (1 \dots N)$
22	21	biimpi	$⊢ K + 1 \in D \to K + 1 \in (1 \dots N)$
23	22	adantl	$⊢ (K \in ℕ \land K + 1 \in D) \to K + 1 \in (1 \dots N)$
24	20 23	sselid	$⊢ (K \in ℕ \land K + 1 \in D) \to K + 1 \in ℕ$
25	24	nnred	$⊢ (K \in ℕ \land K + 1 \in D) \to K + 1 \in ℝ$
26		elfz1b	$⊢ K + 1 \in (1 \dots N) \leftrightarrow (K + 1 \in ℕ \land N \in ℕ \land K + 1 \leq N)$
27	26	simp2bi	$⊢ K + 1 \in (1 \dots N) \to N \in ℕ$
28	22 27	syl	$⊢ K + 1 \in D \to N \in ℕ$
29	28	adantl	$⊢ (K \in ℕ \land K + 1 \in D) \to N \in ℕ$
30	29	nnred	$⊢ (K \in ℕ \land K + 1 \in D) \to N \in ℝ$
31	19	lep1d	$⊢ (K \in ℕ \land K + 1 \in D) \to K \leq K + 1$
32		elfzle2	$⊢ K + 1 \in (1 \dots N) \to K + 1 \leq N$
33	23 32	syl	$⊢ (K \in ℕ \land K + 1 \in D) \to K + 1 \leq N$
34	19 25 30 31 33	letrd	$⊢ (K \in ℕ \land K + 1 \in D) \to K \leq N$
35	29	nnzd	$⊢ (K \in ℕ \land K + 1 \in D) \to N \in ℤ$
36		fznn	$⊢ N \in ℤ \to (K \in (1 \dots N) \leftrightarrow (K \in ℕ \land K \leq N))$
37	35 36	syl	$⊢ (K \in ℕ \land K + 1 \in D) \to (K \in (1 \dots N) \leftrightarrow (K \in ℕ \land K \leq N))$
38	18 34 37	mpbir2and	$⊢ (K \in ℕ \land K + 1 \in D) \to K \in (1 \dots N)$
39	38 1	eleqtrrdi	$⊢ (K \in ℕ \land K + 1 \in D) \to K \in D$
40	39	ad2antrr	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land i = 1) \to K \in D$
41	17 40	eqeltrd	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land i = 1) \to if (i = 1, K, if (i \leq K, i - 1, i)) \in D$
42		simpr	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \to \neg i = 1$
43	42	iffalsed	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \to if (i = 1, K, if (i \leq K, i - 1, i)) = if (i \leq K, i - 1, i)$
44		simpr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i \leq K$
45	44	iftrued	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to if (i \leq K, i - 1, i) = i - 1$
46	42	adantr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to \neg i = 1$
47	1 20	eqsstri	$⊢ D \subseteq ℕ$
48		simpllr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i \in D$
49	47 48	sselid	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i \in ℕ$
50		nn1m1nn	$⊢ i \in ℕ \to (i = 1 \lor i - 1 \in ℕ)$
51	49 50	syl	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to (i = 1 \lor i - 1 \in ℕ)$
52	51	ord	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to (\neg i = 1 \to i - 1 \in ℕ)$
53	46 52	mpd	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i - 1 \in ℕ$
54	53	nnred	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i - 1 \in ℝ$
55	49	nnred	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i \in ℝ$
56	30	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to N \in ℝ$
57	55	lem1d	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i - 1 \leq i$
58	48 1	eleqtrdi	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i \in (1 \dots N)$
59		elfzle2	$⊢ i \in (1 \dots N) \to i \leq N$
60	58 59	syl	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i \leq N$
61	54 55 56 57 60	letrd	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i - 1 \leq N$
62	53 61	jca	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to (i - 1 \in ℕ \land i - 1 \leq N)$
63		fznn	$⊢ N \in ℤ \to (i - 1 \in (1 \dots N) \leftrightarrow (i - 1 \in ℕ \land i - 1 \leq N))$
64	35 63	syl	$⊢ (K \in ℕ \land K + 1 \in D) \to (i - 1 \in (1 \dots N) \leftrightarrow (i - 1 \in ℕ \land i - 1 \leq N))$
65	64	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to (i - 1 \in (1 \dots N) \leftrightarrow (i - 1 \in ℕ \land i - 1 \leq N))$
66	62 65	mpbird	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i - 1 \in (1 \dots N)$
67	66 1	eleqtrrdi	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to i - 1 \in D$
68	45 67	eqeltrd	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land i \leq K) \to if (i \leq K, i - 1, i) \in D$
69		simpr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land \neg i \leq K) \to \neg i \leq K$
70	69	iffalsed	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land \neg i \leq K) \to if (i \leq K, i - 1, i) = i$
71		simpllr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land \neg i \leq K) \to i \in D$
72	70 71	eqeltrd	$⊢ ((((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \land \neg i \leq K) \to if (i \leq K, i - 1, i) \in D$
73	68 72	pm2.61dan	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \to if (i \leq K, i - 1, i) \in D$
74	43 73	eqeltrd	$⊢ (((K \in ℕ \land K + 1 \in D) \land i \in D) \land \neg i = 1) \to if (i = 1, K, if (i \leq K, i - 1, i)) \in D$
75	41 74	pm2.61dan	$⊢ ((K \in ℕ \land K + 1 \in D) \land i \in D) \to if (i = 1, K, if (i \leq K, i - 1, i)) \in D$
76	75	ralrimiva	$⊢ (K \in ℕ \land K + 1 \in D) \to \forall i \in D if (i = 1, K, if (i \leq K, i - 1, i)) \in D$
77		eqid	$⊢ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) = (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$
78	77	fnmpt	$⊢ \forall i \in D if (i = 1, K, if (i \leq K, i - 1, i)) \in D \to (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) Fn D$
79	76 78	syl	$⊢ (K \in ℕ \land K + 1 \in D) \to (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) Fn D$
80	77	rnmptss	$⊢ \forall i \in D if (i = 1, K, if (i \leq K, i - 1, i)) \in D \to ran (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) \subseteq D$
81	76 80	syl	$⊢ (K \in ℕ \land K + 1 \in D) \to ran (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) \subseteq D$
82		fnco	$⊢ (pmTrsp (D) (\{K, K + 1\}) Fn D \land (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) Fn D \land ran (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) \subseteq D) \to (pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))) Fn D$
83	15 79 81 82	syl3anc	$⊢ (K \in ℕ \land K + 1 \in D) \to (pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))) Fn D$
84		simpr	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land x = 1) \to x = 1$
85	84	iftrued	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land x = 1) \to if (x = 1, K, if (x \leq K, x - 1, x)) = K$
86	85	fveq2d	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land x = 1) \to pmTrsp (D) (\{K, K + 1\}) (if (x = 1, K, if (x \leq K, x - 1, x))) = pmTrsp (D) (\{K, K + 1\}) (K)$
87		fzfi	$⊢ (1 \dots N) \in Fin$
88	1 87	eqeltri	$⊢ D \in Fin$
89	88	a1i	$⊢ (K \in ℕ \land K + 1 \in D) \to D \in Fin$
90	23 21	sylibr	$⊢ (K \in ℕ \land K + 1 \in D) \to K + 1 \in D$
91	19	ltp1d	$⊢ (K \in ℕ \land K + 1 \in D) \to K < K + 1$
92	19 91	ltned	$⊢ (K \in ℕ \land K + 1 \in D) \to K \neq K + 1$
93	10	pmtrprfv	$⊢ (D \in Fin \land (K \in D \land K + 1 \in D \land K \neq K + 1)) \to pmTrsp (D) (\{K, K + 1\}) (K) = K + 1$
94	89 39 90 92 93	syl13anc	$⊢ (K \in ℕ \land K + 1 \in D) \to pmTrsp (D) (\{K, K + 1\}) (K) = K + 1$
95	94	ad2antrr	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land x = 1) \to pmTrsp (D) (\{K, K + 1\}) (K) = K + 1$
96	86 95	eqtr2d	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land x = 1) \to K + 1 = pmTrsp (D) (\{K, K + 1\}) (if (x = 1, K, if (x \leq K, x - 1, x)))$
97	88	a1i	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to D \in Fin$
98	39	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K \in D$
99	90	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K + 1 \in D$
100	92	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K \neq K + 1$
101	10	pmtrprfv2	$⊢ (D \in Fin \land (K \in D \land K + 1 \in D \land K \neq K + 1)) \to pmTrsp (D) (\{K, K + 1\}) (K + 1) = K$
102	97 98 99 100 101	syl13anc	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to pmTrsp (D) (\{K, K + 1\}) (K + 1) = K$
103	91	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K < K + 1$
104		simpr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to x = K + 1$
105	103 104	breqtrrd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K < x$
106	19	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K \in ℝ$
107		simpr	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to x \in D$
108	47 107	sselid	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to x \in ℕ$
109	108	nnred	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to x \in ℝ$
110	109	ad3antrrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to x \in ℝ$
111	106 110	ltnled	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to (K < x \leftrightarrow \neg x \leq K)$
112	105 111	mpbid	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to \neg x \leq K$
113	112	iffalsed	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to if (x \leq K, x - 1, x) = x$
114	113 104	eqtrd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to if (x \leq K, x - 1, x) = K + 1$
115	114	fveq2d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x)) = pmTrsp (D) (\{K, K + 1\}) (K + 1)$
116	104	oveq1d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to x - 1 = K + 1 - 1$
117	106	recnd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K \in ℂ$
118		1cnd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to 1 \in ℂ$
119	117 118	pncand	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to K + 1 - 1 = K$
120	116 119	eqtrd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to x - 1 = K$
121	102 115 120	3eqtr4rd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x = K + 1) \to x - 1 = pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x))$
122		simplr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \leq K + 1$
123		simpr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \neq K + 1$
124	123	necomd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K + 1 \neq x$
125	109	ad3antrrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \in ℝ$
126	25	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K + 1 \in ℝ$
127	125 126	ltlend	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (x < K + 1 \leftrightarrow (x \leq K + 1 \land K + 1 \neq x))$
128	122 124 127	mpbir2and	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x < K + 1$
129	108	ad3antrrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \in ℕ$
130		simpll	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to K \in ℕ$
131	130	ad3antrrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K \in ℕ$
132		nnleltp1	$⊢ (x \in ℕ \land K \in ℕ) \to (x \leq K \leftrightarrow x < K + 1)$
133	129 131 132	syl2anc	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (x \leq K \leftrightarrow x < K + 1)$
134	128 133	mpbird	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \leq K$
135	134	iftrued	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to if (x \leq K, x - 1, x) = x - 1$
136	135	fveq2d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x)) = pmTrsp (D) (\{K, K + 1\}) (x - 1)$
137	88	a1i	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to D \in Fin$
138	39	ad4antr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K \in D$
139		simp-5r	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K + 1 \in D$
140		simpr	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to \neg x = 1$
141	140	ad2antrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to \neg x = 1$
142		elnn1uz2	$⊢ x \in ℕ \leftrightarrow (x = 1 \lor x \in ℤ_{\geq 2})$
143	129 142	sylib	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (x = 1 \lor x \in ℤ_{\geq 2})$
144	143	ord	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (\neg x = 1 \to x \in ℤ_{\geq 2})$
145	141 144	mpd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \in ℤ_{\geq 2}$
146		uz2m1nn	$⊢ x \in ℤ_{\geq 2} \to x - 1 \in ℕ$
147	145 146	syl	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \in ℕ$
148	139 28	syl	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to N \in ℕ$
149	147	nnred	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \in ℝ$
150	131 139 30	syl2anc	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to N \in ℝ$
151	125	lem1d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \leq x$
152	107	ad3antrrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \in D$
153	152 1	eleqtrdi	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \in (1 \dots N)$
154		elfzle2	$⊢ x \in (1 \dots N) \to x \leq N$
155	153 154	syl	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x \leq N$
156	149 125 150 151 155	letrd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \leq N$
157	147 148 156	3jca	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (x - 1 \in ℕ \land N \in ℕ \land x - 1 \leq N)$
158		elfz1b	$⊢ x - 1 \in (1 \dots N) \leftrightarrow (x - 1 \in ℕ \land N \in ℕ \land x - 1 \leq N)$
159	157 158	sylibr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \in (1 \dots N)$
160	159 1	eleqtrrdi	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \in D$
161	138 139 160	3jca	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (K \in D \land K + 1 \in D \land x - 1 \in D)$
162	131 139 92	syl2anc	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K \neq K + 1$
163		simpr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land K = x - 1) \to K = x - 1$
164	163	oveq1d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land K = x - 1) \to K + 1 = x - 1 + 1$
165	109	recnd	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to x \in ℂ$
166	165	ad3antrrr	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land K = x - 1) \to x \in ℂ$
167		1cnd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land K = x - 1) \to 1 \in ℂ$
168	166 167	npcand	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land K = x - 1) \to x - 1 + 1 = x$
169	164 168	eqtr2d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land K = x - 1) \to x = K + 1$
170	169	ex	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \to (K = x - 1 \to x = K + 1)$
171	170	necon3d	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \to (x \neq K + 1 \to K \neq x - 1)$
172	171	imp	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K \neq x - 1$
173	149 125 126 151 128	lelttrd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 < K + 1$
174	149 173	ltned	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 \neq K + 1$
175	174	necomd	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to K + 1 \neq x - 1$
176	162 172 175	3jca	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to (K \neq K + 1 \land K \neq x - 1 \land K + 1 \neq x - 1)$
177	10	pmtrprfv3	$⊢ (D \in Fin \land (K \in D \land K + 1 \in D \land x - 1 \in D) \land (K \neq K + 1 \land K \neq x - 1 \land K + 1 \neq x - 1)) \to pmTrsp (D) (\{K, K + 1\}) (x - 1) = x - 1$
178	137 161 176 177	syl3anc	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to pmTrsp (D) (\{K, K + 1\}) (x - 1) = x - 1$
179	136 178	eqtr2d	$⊢ (((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \land x \neq K + 1) \to x - 1 = pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x))$
180	121 179	pm2.61dane	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K + 1) \to x - 1 = pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x))$
181	109	ad2antrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K) \to x \in ℝ$
182	19	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K) \to K \in ℝ$
183	25	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K) \to K + 1 \in ℝ$
184		simpr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K) \to x \leq K$
185	31	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K) \to K \leq K + 1$
186	181 182 183 184 185	letrd	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land x \leq K) \to x \leq K + 1$
187	186	ex	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to (x \leq K \to x \leq K + 1)$
188	187	con3d	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to (\neg x \leq K + 1 \to \neg x \leq K)$
189	188	imp	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to \neg x \leq K$
190	189	iffalsed	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to if (x \leq K, x - 1, x) = x$
191	190	fveq2d	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x)) = pmTrsp (D) (\{K, K + 1\}) (x)$
192	88	a1i	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to D \in Fin$
193	39	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K \in D$
194	90	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K + 1 \in D$
195	107	ad2antrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to x \in D$
196	193 194 195	3jca	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to (K \in D \land K + 1 \in D \land x \in D)$
197	92	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K \neq K + 1$
198	19	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K \in ℝ$
199	25	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K + 1 \in ℝ$
200	109	ad2antrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to x \in ℝ$
201	91	ad3antrrr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K < K + 1$
202		simpr	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to \neg x \leq K + 1$
203	199 200	ltnled	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to (K + 1 < x \leftrightarrow \neg x \leq K + 1)$
204	202 203	mpbird	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K + 1 < x$
205	198 199 200 201 204	lttrd	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K < x$
206	198 205	ltned	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K \neq x$
207	199 204	ltned	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to K + 1 \neq x$
208	197 206 207	3jca	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to (K \neq K + 1 \land K \neq x \land K + 1 \neq x)$
209	10	pmtrprfv3	$⊢ (D \in Fin \land (K \in D \land K + 1 \in D \land x \in D) \land (K \neq K + 1 \land K \neq x \land K + 1 \neq x)) \to pmTrsp (D) (\{K, K + 1\}) (x) = x$
210	192 196 208 209	syl3anc	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to pmTrsp (D) (\{K, K + 1\}) (x) = x$
211	191 210	eqtr2d	$⊢ ((((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \land \neg x \leq K + 1) \to x = pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x))$
212	180 211	ifeqda	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to if (x \leq K + 1, x - 1, x) = pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x))$
213	140	iffalsed	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to if (x = 1, K, if (x \leq K, x - 1, x)) = if (x \leq K, x - 1, x)$
214	213	fveq2d	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to pmTrsp (D) (\{K, K + 1\}) (if (x = 1, K, if (x \leq K, x - 1, x))) = pmTrsp (D) (\{K, K + 1\}) (if (x \leq K, x - 1, x))$
215	212 214	eqtr4d	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land \neg x = 1) \to if (x \leq K + 1, x - 1, x) = pmTrsp (D) (\{K, K + 1\}) (if (x = 1, K, if (x \leq K, x - 1, x)))$
216	96 215	ifeqda	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to if (x = 1, K + 1, if (x \leq K + 1, x - 1, x)) = pmTrsp (D) (\{K, K + 1\}) (if (x = 1, K, if (x \leq K, x - 1, x)))$
217		eqidd	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) = (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$
218		eqeq1	$⊢ i = x \to (i = 1 \leftrightarrow x = 1)$
219		breq1	$⊢ i = x \to (i \leq K \leftrightarrow x \leq K)$
220		oveq1	$⊢ i = x \to i - 1 = x - 1$
221		id	$⊢ i = x \to i = x$
222	219 220 221	ifbieq12d	$⊢ i = x \to if (i \leq K, i - 1, i) = if (x \leq K, x - 1, x)$
223	218 222	ifbieq2d	$⊢ i = x \to if (i = 1, K, if (i \leq K, i - 1, i)) = if (x = 1, K, if (x \leq K, x - 1, x))$
224	223	adantl	$⊢ (((K \in ℕ \land K + 1 \in D) \land x \in D) \land i = x) \to if (i = 1, K, if (i \leq K, i - 1, i)) = if (x = 1, K, if (x \leq K, x - 1, x))$
225		ovex	$⊢ x - 1 \in V$
226		vex	$⊢ x \in V$
227	225 226	ifcli	$⊢ if (x \leq K, x - 1, x) \in V$
228	227	a1i	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to if (x \leq K, x - 1, x) \in V$
229	130 228	ifexd	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to if (x = 1, K, if (x \leq K, x - 1, x)) \in V$
230	217 224 107 229	fvmptd	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) (x) = if (x = 1, K, if (x \leq K, x - 1, x))$
231	230	fveq2d	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to pmTrsp (D) (\{K, K + 1\}) ((i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) (x)) = pmTrsp (D) (\{K, K + 1\}) (if (x = 1, K, if (x \leq K, x - 1, x)))$
232	216 231	eqtr4d	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to if (x = 1, K + 1, if (x \leq K + 1, x - 1, x)) = pmTrsp (D) (\{K, K + 1\}) ((i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) (x))$
233		breq1	$⊢ i = x \to (i \leq K + 1 \leftrightarrow x \leq K + 1)$
234	233 220 221	ifbieq12d	$⊢ i = x \to if (i \leq K + 1, i - 1, i) = if (x \leq K + 1, x - 1, x)$
235	218 234	ifbieq2d	$⊢ i = x \to if (i = 1, K + 1, if (i \leq K + 1, i - 1, i)) = if (x = 1, K + 1, if (x \leq K + 1, x - 1, x))$
236	225 226	ifex	$⊢ if (x \leq K + 1, x - 1, x) \in V$
237	2 236	ifex	$⊢ if (x = 1, K + 1, if (x \leq K + 1, x - 1, x)) \in V$
238	235 7 237	fvmpt	$⊢ x \in D \to (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) (x) = if (x = 1, K + 1, if (x \leq K + 1, x - 1, x))$
239	238	adantl	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) (x) = if (x = 1, K + 1, if (x \leq K + 1, x - 1, x))$
240		funmpt	$⊢ Fun (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$
241	240	a1i	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to Fun (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$
242	76	adantr	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to \forall i \in D if (i = 1, K, if (i \leq K, i - 1, i)) \in D$
243		dmmptg	$⊢ \forall i \in D if (i = 1, K, if (i \leq K, i - 1, i)) \in D \to dom (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) = D$
244	242 243	syl	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to dom (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) = D$
245	107 244	eleqtrrd	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to x \in dom (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$
246		fvco	$⊢ (Fun (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) \land x \in dom (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))) \to (pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))) (x) = pmTrsp (D) (\{K, K + 1\}) ((i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) (x))$
247	241 245 246	syl2anc	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to (pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))) (x) = pmTrsp (D) (\{K, K + 1\}) ((i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i))) (x))$
248	232 239 247	3eqtr4d	$⊢ ((K \in ℕ \land K + 1 \in D) \land x \in D) \to (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) (x) = (pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))) (x)$
249	9 83 248	eqfnfvd	$⊢ (K \in ℕ \land K + 1 \in D) \to (i \in D ⟼ if (i = 1, K + 1, if (i \leq K + 1, i - 1, i))) = pmTrsp (D) (\{K, K + 1\}) \circ (i \in D ⟼ if (i = 1, K, if (i \leq K, i - 1, i)))$

Metamath Proof Explorer

Theorem psgnfzto1stlem

Proof