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

Metamath Proof Explorer

Theorem dvdsnprmd

Description: If a number is divisible by an integer greater than 1 and less than the number, the number is not prime. (Contributed by AV, 24-Jul-2021)

Ref Expression
Hypotheses dvdsnprmd.g ⊢ ( 𝜑 → 1 < 𝐴 )
dvdsnprmd.l ⊢ ( 𝜑 → 𝐴 < 𝑁 )
dvdsnprmd.d ⊢ ( 𝜑 → 𝐴 ∥ 𝑁 )
Assertion dvdsnprmd ( 𝜑 → ¬ 𝑁 ∈ ℙ )

Proof

Step Hyp Ref Expression
1 dvdsnprmd.g ⊢ ( 𝜑 → 1 < 𝐴 )
2 dvdsnprmd.l ⊢ ( 𝜑 → 𝐴 < 𝑁 )
3 dvdsnprmd.d ⊢ ( 𝜑 → 𝐴 ∥ 𝑁 )
4 dvdszrcl ⊢ ( 𝐴 ∥ 𝑁 → ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
5 divides ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝑁 ) )
6 3 4 5 3syl ⊢ ( 𝜑 → ( 𝐴 ∥ 𝑁 ↔ ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝑁 ) )
7 2z ⊢ 2 ∈ ℤ
8 7 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 2 ∈ ℤ )
9 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 𝑘 ∈ ℤ )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐴 < 𝑁 )
11 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 𝐴 < 𝑁 )
12 breq2 ⊢ ( ( 𝑘 · 𝐴 ) = 𝑁 → ( 𝐴 < ( 𝑘 · 𝐴 ) ↔ 𝐴 < 𝑁 ) )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ( 𝐴 < ( 𝑘 · 𝐴 ) ↔ 𝐴 < 𝑁 ) )
14 11 13 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 𝐴 < ( 𝑘 · 𝐴 ) )
15 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
16 15 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ∧ 𝑘 ∈ ℤ ) → 𝐴 ∈ ℝ )
17 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
18 17 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
19 0lt1 ⊢ 0 < 1
20 0red ⊢ ( 𝐴 ∈ ℤ → 0 ∈ ℝ )
21 1red ⊢ ( 𝐴 ∈ ℤ → 1 ∈ ℝ )
22 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝐴 ) → 0 < 𝐴 ) )
23 20 21 15 22 syl3anc ⊢ ( 𝐴 ∈ ℤ → ( ( 0 < 1 ∧ 1 < 𝐴 ) → 0 < 𝐴 ) )
24 19 23 mpani ⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → 0 < 𝐴 ) )
25 24 imp ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
26 25 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ∧ 𝑘 ∈ ℤ ) → 0 < 𝐴 )
27 16 18 26 3jca ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) )
28 27 3exp ⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → ( 𝑘 ∈ ℤ → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) ) ) )
29 28 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 < 𝐴 → ( 𝑘 ∈ ℤ → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) ) ) )
30 3 4 29 3syl ⊢ ( 𝜑 → ( 1 < 𝐴 → ( 𝑘 ∈ ℤ → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) ) ) )
31 1 30 mpd ⊢ ( 𝜑 → ( 𝑘 ∈ ℤ → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) ) )
32 31 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) )
34 ltmulgt12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝑘 ↔ 𝐴 < ( 𝑘 · 𝐴 ) ) )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ( 1 < 𝑘 ↔ 𝐴 < ( 𝑘 · 𝐴 ) ) )
36 14 35 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 1 < 𝑘 )
37 df-2 ⊢ 2 = ( 1 + 1 )
38 37 breq1i ⊢ ( 2 ≤ 𝑘 ↔ ( 1 + 1 ) ≤ 𝑘 )
39 1zzd ⊢ ( 𝑘 ∈ ℤ → 1 ∈ ℤ )
40 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 1 < 𝑘 ↔ ( 1 + 1 ) ≤ 𝑘 ) )
41 39 40 mpancom ⊢ ( 𝑘 ∈ ℤ → ( 1 < 𝑘 ↔ ( 1 + 1 ) ≤ 𝑘 ) )
42 41 bicomd ⊢ ( 𝑘 ∈ ℤ → ( ( 1 + 1 ) ≤ 𝑘 ↔ 1 < 𝑘 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 1 + 1 ) ≤ 𝑘 ↔ 1 < 𝑘 ) )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ( ( 1 + 1 ) ≤ 𝑘 ↔ 1 < 𝑘 ) )
45 38 44 bitrid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ( 2 ≤ 𝑘 ↔ 1 < 𝑘 ) )
46 36 45 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 2 ≤ 𝑘 )
47 eluz2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ) )
48 8 9 46 47 syl3anbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
49 7 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ) → 2 ∈ ℤ )
50 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℤ )
51 1zzd ⊢ ( 𝐴 ∈ ℤ → 1 ∈ ℤ )
52 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 1 < 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) )
53 51 52 mpancom ⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 ) )
54 53 biimpa ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ) → ( 1 + 1 ) ≤ 𝐴 )
55 37 breq1i ⊢ ( 2 ≤ 𝐴 ↔ ( 1 + 1 ) ≤ 𝐴 )
56 54 55 sylibr ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ) → 2 ≤ 𝐴 )
57 49 50 56 3jca ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 < 𝐴 ) → ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) )
58 57 ex ⊢ ( 𝐴 ∈ ℤ → ( 1 < 𝐴 → ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) ) )
59 58 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 < 𝐴 → ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) ) )
60 3 4 59 3syl ⊢ ( 𝜑 → ( 1 < 𝐴 → ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) ) )
61 1 60 mpd ⊢ ( 𝜑 → ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) )
62 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) )
63 61 62 sylibr ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
66 nprm ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝑘 · 𝐴 ) ∈ ℙ )
67 48 65 66 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ¬ ( 𝑘 · 𝐴 ) ∈ ℙ )
68 eleq1 ⊢ ( ( 𝑘 · 𝐴 ) = 𝑁 → ( ( 𝑘 · 𝐴 ) ∈ ℙ ↔ 𝑁 ∈ ℙ ) )
69 68 notbid ⊢ ( ( 𝑘 · 𝐴 ) = 𝑁 → ( ¬ ( 𝑘 · 𝐴 ) ∈ ℙ ↔ ¬ 𝑁 ∈ ℙ ) )
70 69 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ( ¬ ( 𝑘 · 𝐴 ) ∈ ℙ ↔ ¬ 𝑁 ∈ ℙ ) )
71 67 70 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑘 · 𝐴 ) = 𝑁 ) → ¬ 𝑁 ∈ ℙ )
72 71 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) = 𝑁 → ¬ 𝑁 ∈ ℙ ) )
73 6 72 sylbid ⊢ ( 𝜑 → ( 𝐴 ∥ 𝑁 → ¬ 𝑁 ∈ ℙ ) )
74 3 73 mpd ⊢ ( 𝜑 → ¬ 𝑁 ∈ ℙ )