Theorem submateqlem2

Description: Lemma for submateq . (Contributed by Thierry Arnoux, 26-Aug-2020)

	Ref	Expression
Hypotheses	submateqlem2.n	|- ( ph -> N e. NN )
	submateqlem2.k	|- ( ph -> K e. ( 1 ... N ) )
	submateqlem2.m	|- ( ph -> M e. ( 1 ... ( N - 1 ) ) )
	submateqlem2.1	|- ( ph -> M < K )
Assertion	submateqlem2	|- ( ph -> ( M e. ( 1 ..^ K ) /\ M e. ( ( 1 ... N ) \ { K } ) ) )

Proof

Step	Hyp	Ref	Expression
1		submateqlem2.n	|- ( ph -> N e. NN )
2		submateqlem2.k	|- ( ph -> K e. ( 1 ... N ) )
3		submateqlem2.m	|- ( ph -> M e. ( 1 ... ( N - 1 ) ) )
4		submateqlem2.1	|- ( ph -> M < K )
5		fz1ssnn	|- ( 1 ... ( N - 1 ) ) C_ NN
6	5 3	sseldi	|- ( ph -> M e. NN )
7	6	nnge1d	|- ( ph -> 1 <_ M )
8	7 4	jca	|- ( ph -> ( 1 <_ M /\ M < K ) )
9	6	nnzd	|- ( ph -> M e. ZZ )
10		1zzd	|- ( ph -> 1 e. ZZ )
11		fz1ssnn	|- ( 1 ... N ) C_ NN
12	11 2	sseldi	|- ( ph -> K e. NN )
13	12	nnzd	|- ( ph -> K e. ZZ )
14		elfzo	|- ( ( M e. ZZ /\ 1 e. ZZ /\ K e. ZZ ) -> ( M e. ( 1 ..^ K ) <-> ( 1 <_ M /\ M < K ) ) )
15	9 10 13 14	syl3anc	|- ( ph -> ( M e. ( 1 ..^ K ) <-> ( 1 <_ M /\ M < K ) ) )
16	8 15	mpbird	|- ( ph -> M e. ( 1 ..^ K ) )
17	3	orcd	|- ( ph -> ( M e. ( 1 ... ( N - 1 ) ) \/ M = N ) )
18		nnuz	|- NN = ( ZZ>= ` 1 )
19	1 18	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 1 ) )
20		fzm1	|- ( N e. ( ZZ>= ` 1 ) -> ( M e. ( 1 ... N ) <-> ( M e. ( 1 ... ( N - 1 ) ) \/ M = N ) ) )
21	19 20	syl	|- ( ph -> ( M e. ( 1 ... N ) <-> ( M e. ( 1 ... ( N - 1 ) ) \/ M = N ) ) )
22	17 21	mpbird	|- ( ph -> M e. ( 1 ... N ) )
23	6	nnred	|- ( ph -> M e. RR )
24	23 4	ltned	|- ( ph -> M =/= K )
25		nelsn	|- ( M =/= K -> -. M e. { K } )
26	24 25	syl	|- ( ph -> -. M e. { K } )
27	22 26	eldifd	|- ( ph -> M e. ( ( 1 ... N ) \ { K } ) )
28	16 27	jca	|- ( ph -> ( M e. ( 1 ..^ K ) /\ M e. ( ( 1 ... N ) \ { K } ) ) )