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	⊢ ( 𝜑 → ¬ 𝑁 ∈ ℙ )