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