Theorem prmlem0

Description: Lemma for prmlem1 and prmlem2 . (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	prmlem0.1	|- ( ( -. 2 || M /\ x e. ( ZZ>= ` M ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
	prmlem0.2	|- ( K e. Prime -> -. K || N )
	prmlem0.3	|- ( K + 2 ) = M
Assertion	prmlem0	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )

Proof

Step	Hyp	Ref	Expression
1		prmlem0.1	|- ( ( -. 2 || M /\ x e. ( ZZ>= ` M ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
2		prmlem0.2	|- ( K e. Prime -> -. K || N )
3		prmlem0.3	|- ( K + 2 ) = M
4		eldifi	|- ( x e. ( Prime \ { 2 } ) -> x e. Prime )
5		eleq1	|- ( x = K -> ( x e. Prime <-> K e. Prime ) )
6		breq1	|- ( x = K -> ( x || N <-> K || N ) )
7	6	notbid	|- ( x = K -> ( -. x || N <-> -. K || N ) )
8	5 7	imbi12d	|- ( x = K -> ( ( x e. Prime -> -. x || N ) <-> ( K e. Prime -> -. K || N ) ) )
9	2 8	mpbiri	|- ( x = K -> ( x e. Prime -> -. x || N ) )
10	4 9	syl5	|- ( x = K -> ( x e. ( Prime \ { 2 } ) -> -. x || N ) )
11	10	adantrd	|- ( x = K -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
12	11	a1i	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x = K -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
13		uzp1	|- ( x e. ( ZZ>= ` ( K + 1 ) ) -> ( x = ( K + 1 ) \/ x e. ( ZZ>= ` ( ( K + 1 ) + 1 ) ) ) )
14		eleq1	|- ( x = ( K + 1 ) -> ( x e. ( Prime \ { 2 } ) <-> ( K + 1 ) e. ( Prime \ { 2 } ) ) )
15	14	adantl	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ x = ( K + 1 ) ) -> ( x e. ( Prime \ { 2 } ) <-> ( K + 1 ) e. ( Prime \ { 2 } ) ) )
16		eldifsn	|- ( ( K + 1 ) e. ( Prime \ { 2 } ) <-> ( ( K + 1 ) e. Prime /\ ( K + 1 ) =/= 2 ) )
17		eluzel2	|- ( x e. ( ZZ>= ` K ) -> K e. ZZ )
18	17	adantl	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> K e. ZZ )
19		simpl	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> -. 2 || K )
20		1z	|- 1 e. ZZ
21		n2dvds1	|- -. 2 || 1
22		opoe	|- ( ( ( K e. ZZ /\ -. 2 || K ) /\ ( 1 e. ZZ /\ -. 2 || 1 ) ) -> 2 || ( K + 1 ) )
23	20 21 22	mpanr12	|- ( ( K e. ZZ /\ -. 2 || K ) -> 2 || ( K + 1 ) )
24	18 19 23	syl2anc	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> 2 || ( K + 1 ) )
25	24	adantr	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ ( K + 1 ) e. Prime ) -> 2 || ( K + 1 ) )
26		2z	|- 2 e. ZZ
27		uzid	|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
28	26 27	mp1i	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> 2 e. ( ZZ>= ` 2 ) )
29		dvdsprm	|- ( ( 2 e. ( ZZ>= ` 2 ) /\ ( K + 1 ) e. Prime ) -> ( 2 || ( K + 1 ) <-> 2 = ( K + 1 ) ) )
30	28 29	sylan	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ ( K + 1 ) e. Prime ) -> ( 2 || ( K + 1 ) <-> 2 = ( K + 1 ) ) )
31	25 30	mpbid	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ ( K + 1 ) e. Prime ) -> 2 = ( K + 1 ) )
32	31	eqcomd	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ ( K + 1 ) e. Prime ) -> ( K + 1 ) = 2 )
33	32	a1d	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ ( K + 1 ) e. Prime ) -> ( x || N -> ( K + 1 ) = 2 ) )
34	33	necon3ad	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ ( K + 1 ) e. Prime ) -> ( ( K + 1 ) =/= 2 -> -. x || N ) )
35	34	expimpd	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( ( K + 1 ) e. Prime /\ ( K + 1 ) =/= 2 ) -> -. x || N ) )
36	16 35	biimtrid	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) e. ( Prime \ { 2 } ) -> -. x || N ) )
37	36	adantr	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ x = ( K + 1 ) ) -> ( ( K + 1 ) e. ( Prime \ { 2 } ) -> -. x || N ) )
38	15 37	sylbid	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ x = ( K + 1 ) ) -> ( x e. ( Prime \ { 2 } ) -> -. x || N ) )
39	38	adantrd	|- ( ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) /\ x = ( K + 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
40	39	ex	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x = ( K + 1 ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
41	18	zcnd	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> K e. CC )
42		ax-1cn	|- 1 e. CC
43		addass	|- ( ( K e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( ( K + 1 ) + 1 ) = ( K + ( 1 + 1 ) ) )
44	42 42 43	mp3an23	|- ( K e. CC -> ( ( K + 1 ) + 1 ) = ( K + ( 1 + 1 ) ) )
45	41 44	syl	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) + 1 ) = ( K + ( 1 + 1 ) ) )
46		1p1e2	|- ( 1 + 1 ) = 2
47	46	oveq2i	|- ( K + ( 1 + 1 ) ) = ( K + 2 )
48	47 3	eqtri	|- ( K + ( 1 + 1 ) ) = M
49	45 48	eqtrdi	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( K + 1 ) + 1 ) = M )
50	49	fveq2d	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ZZ>= ` ( ( K + 1 ) + 1 ) ) = ( ZZ>= ` M ) )
51	50	eleq2d	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x e. ( ZZ>= ` ( ( K + 1 ) + 1 ) ) <-> x e. ( ZZ>= ` M ) ) )
52		dvdsaddr	|- ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 || K <-> 2 || ( K + 2 ) ) )
53	26 18 52	sylancr	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( 2 || K <-> 2 || ( K + 2 ) ) )
54	3	breq2i	|- ( 2 || ( K + 2 ) <-> 2 || M )
55	53 54	bitrdi	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( 2 || K <-> 2 || M ) )
56	19 55	mtbid	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> -. 2 || M )
57	1	ex	|- ( -. 2 || M -> ( x e. ( ZZ>= ` M ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
58	56 57	syl	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x e. ( ZZ>= ` M ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
59	51 58	sylbid	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x e. ( ZZ>= ` ( ( K + 1 ) + 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
60	40 59	jaod	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( x = ( K + 1 ) \/ x e. ( ZZ>= ` ( ( K + 1 ) + 1 ) ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
61	13 60	syl5	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x e. ( ZZ>= ` ( K + 1 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) )
62		uzp1	|- ( x e. ( ZZ>= ` K ) -> ( x = K \/ x e. ( ZZ>= ` ( K + 1 ) ) ) )
63	62	adantl	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( x = K \/ x e. ( ZZ>= ` ( K + 1 ) ) ) )
64	12 61 63	mpjaod	|- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )