This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )