Metamath Proof Explorer

Theorem prmlem0

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

Ref Expression
Hypotheses prmlem0.1 ⊢ ( ( ¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
prmlem0.2 ⊢ ( 𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁 )
prmlem0.3 ⊢ ( 𝐾 + 2 ) = 𝑀
Assertion prmlem0 ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 prmlem0.1 ⊢ ( ( ¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
2 prmlem0.2 ⊢ ( 𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁 )
3 prmlem0.3 ⊢ ( 𝐾 + 2 ) = 𝑀
4 eldifi ⊢ ( 𝑥 ∈ ( ℙ ∖ { 2 } ) → 𝑥 ∈ ℙ )
5 eleq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∈ ℙ ↔ 𝐾 ∈ ℙ ) )
6 breq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁 ) )
7 6 notbid ⊢ ( 𝑥 = 𝐾 → ( ¬ 𝑥 ∥ 𝑁 ↔ ¬ 𝐾 ∥ 𝑁 ) )
8 5 7 imbi12d ⊢ ( 𝑥 = 𝐾 → ( ( 𝑥 ∈ ℙ → ¬ 𝑥 ∥ 𝑁 ) ↔ ( 𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁 ) ) )
9 2 8 mpbiri ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∈ ℙ → ¬ 𝑥 ∥ 𝑁 ) )
10 4 9 syl5 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑥 ∥ 𝑁 ) )
11 10 adantrd ⊢ ( 𝑥 = 𝐾 → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
12 11 a1i ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 = 𝐾 → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
13 uzp1 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) → ( 𝑥 = ( 𝐾 + 1 ) ∨ 𝑥 ∈ ( ℤ≥ ‘ ( ( 𝐾 + 1 ) + 1 ) ) ) )
14 eleq1 ⊢ ( 𝑥 = ( 𝐾 + 1 ) → ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝐾 + 1 ) ∈ ( ℙ ∖ { 2 } ) ) )
15 14 adantl ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝐾 + 1 ) ∈ ( ℙ ∖ { 2 } ) ) )
16 eldifsn ⊢ ( ( 𝐾 + 1 ) ∈ ( ℙ ∖ { 2 } ) ↔ ( ( 𝐾 + 1 ) ∈ ℙ ∧ ( 𝐾 + 1 ) ≠ 2 ) )
17 eluzel2 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) → 𝐾 ∈ ℤ )
18 17 adantl ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℤ )
19 simpl ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ 2 ∥ 𝐾 )
20 1z ⊢ 1 ∈ ℤ
21 n2dvds1 ⊢ ¬ 2 ∥ 1
22 opoe ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) ∧ ( 1 ∈ ℤ ∧ ¬ 2 ∥ 1 ) ) → 2 ∥ ( 𝐾 + 1 ) )
23 20 21 22 mpanr12 ⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 2 ∥ 𝐾 ) → 2 ∥ ( 𝐾 + 1 ) )
24 18 19 23 syl2anc ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 2 ∥ ( 𝐾 + 1 ) )
25 24 adantr ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → 2 ∥ ( 𝐾 + 1 ) )
26 2z ⊢ 2 ∈ ℤ
27 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
28 26 27 mp1i ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 2 ∈ ( ℤ≥ ‘ 2 ) )
29 dvdsprm ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → ( 2 ∥ ( 𝐾 + 1 ) ↔ 2 = ( 𝐾 + 1 ) ) )
30 28 29 sylan ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → ( 2 ∥ ( 𝐾 + 1 ) ↔ 2 = ( 𝐾 + 1 ) ) )
31 25 30 mpbid ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → 2 = ( 𝐾 + 1 ) )
32 31 eqcomd ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → ( 𝐾 + 1 ) = 2 )
33 32 a1d ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → ( 𝑥 ∥ 𝑁 → ( 𝐾 + 1 ) = 2 ) )
34 33 necon3ad ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ ( 𝐾 + 1 ) ∈ ℙ ) → ( ( 𝐾 + 1 ) ≠ 2 → ¬ 𝑥 ∥ 𝑁 ) )
35 34 expimpd ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( ( 𝐾 + 1 ) ∈ ℙ ∧ ( 𝐾 + 1 ) ≠ 2 ) → ¬ 𝑥 ∥ 𝑁 ) )
36 16 35 biimtrid ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑥 ∥ 𝑁 ) )
37 36 adantr ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( ( 𝐾 + 1 ) ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑥 ∥ 𝑁 ) )
38 15 37 sylbid ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝑥 ∈ ( ℙ ∖ { 2 } ) → ¬ 𝑥 ∥ 𝑁 ) )
39 38 adantrd ⊢ ( ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
40 39 ex ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 = ( 𝐾 + 1 ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
41 18 zcnd ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝐾 ∈ ℂ )
42 ax-1cn ⊢ 1 ∈ ℂ
43 addass ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) + 1 ) = ( 𝐾 + ( 1 + 1 ) ) )
44 42 42 43 mp3an23 ⊢ ( 𝐾 ∈ ℂ → ( ( 𝐾 + 1 ) + 1 ) = ( 𝐾 + ( 1 + 1 ) ) )
45 41 44 syl ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) + 1 ) = ( 𝐾 + ( 1 + 1 ) ) )
46 1p1e2 ⊢ ( 1 + 1 ) = 2
47 46 oveq2i ⊢ ( 𝐾 + ( 1 + 1 ) ) = ( 𝐾 + 2 )
48 47 3 eqtri ⊢ ( 𝐾 + ( 1 + 1 ) ) = 𝑀
49 45 48 eqtrdi ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝐾 + 1 ) + 1 ) = 𝑀 )
50 49 fveq2d ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ℤ≥ ‘ ( ( 𝐾 + 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝑀 ) )
51 50 eleq2d ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( ( 𝐾 + 1 ) + 1 ) ) ↔ 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
52 dvdsaddr ⊢ ( ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 2 ∥ 𝐾 ↔ 2 ∥ ( 𝐾 + 2 ) ) )
53 26 18 52 sylancr ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 2 ∥ 𝐾 ↔ 2 ∥ ( 𝐾 + 2 ) ) )
54 3 breq2i ⊢ ( 2 ∥ ( 𝐾 + 2 ) ↔ 2 ∥ 𝑀 )
55 53 54 bitrdi ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 2 ∥ 𝐾 ↔ 2 ∥ 𝑀 ) )
56 19 55 mtbid ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ¬ 2 ∥ 𝑀 )
57 1 ex ⊢ ( ¬ 2 ∥ 𝑀 → ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
58 56 57 syl ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
59 51 58 sylbid ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( ( 𝐾 + 1 ) + 1 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
60 40 59 jaod ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑥 = ( 𝐾 + 1 ) ∨ 𝑥 ∈ ( ℤ≥ ‘ ( ( 𝐾 + 1 ) + 1 ) ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
61 13 60 syl5 ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) ) )
62 uzp1 ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑥 = 𝐾 ∨ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) )
63 62 adantl ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 𝑥 = 𝐾 ∨ 𝑥 ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) )
64 12 61 63 mpjaod ⊢ ( ( ¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )