Metamath Proof Explorer

Theorem ncoprmlnprm

Description: If two positive integers are not coprime, the larger of them is not a prime number. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion ncoprmlnprm ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → ( 1 < ( 𝐴 gcd 𝐵 ) → 𝐵 ∉ ℙ ) )

Proof

Step Hyp Ref Expression
1 ncoprmgcdgt1b ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ 1 < ( 𝐴 gcd 𝐵 ) ) )
2 1 bicomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 1 < ( 𝐴 gcd 𝐵 ) ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → ( 1 < ( 𝐴 gcd 𝐵 ) ↔ ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) )
4 simp1 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℕ )
5 eluzelz ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → 𝑖 ∈ ℤ )
6 4 5 anim12ci ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ∈ ℤ ∧ 𝐴 ∈ ℕ ) )
7 dvdsle ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝐴 ∈ ℕ ) → ( 𝑖 ∥ 𝐴 → 𝑖 ≤ 𝐴 ) )
8 6 7 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ∥ 𝐴 → 𝑖 ≤ 𝐴 ) )
9 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
10 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
11 eluzelre ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → 𝑖 ∈ ℝ )
12 9 10 11 3anim123i ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑖 ∈ ℝ ) )
13 3anrot ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ↔ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑖 ∈ ℝ ) )
14 12 13 sylibr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
15 lelttr ⊢ ( ( 𝑖 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝑖 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → 𝑖 < 𝐵 ) )
16 14 15 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑖 ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → 𝑖 < 𝐵 ) )
17 16 expcomd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 < 𝐵 → ( 𝑖 ≤ 𝐴 → 𝑖 < 𝐵 ) ) )
18 17 3exp ⊢ ( 𝐴 ∈ ℕ → ( 𝐵 ∈ ℕ → ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 < 𝐵 → ( 𝑖 ≤ 𝐴 → 𝑖 < 𝐵 ) ) ) ) )
19 18 com34 ⊢ ( 𝐴 ∈ ℕ → ( 𝐵 ∈ ℕ → ( 𝐴 < 𝐵 → ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑖 ≤ 𝐴 → 𝑖 < 𝐵 ) ) ) ) )
20 19 3imp1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ≤ 𝐴 → 𝑖 < 𝐵 ) )
21 20 imp ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑖 ≤ 𝐴 ) → 𝑖 < 𝐵 )
22 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
23 22 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℤ )
24 23 5 anim12ci ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
25 24 adantr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑖 ≤ 𝐴 ) → ( 𝑖 ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
26 zltlem1 ⊢ ( ( 𝑖 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑖 < 𝐵 ↔ 𝑖 ≤ ( 𝐵 − 1 ) ) )
27 25 26 syl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑖 ≤ 𝐴 ) → ( 𝑖 < 𝐵 ↔ 𝑖 ≤ ( 𝐵 − 1 ) ) )
28 21 27 mpbid ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑖 ≤ 𝐴 ) → 𝑖 ≤ ( 𝐵 − 1 ) )
29 28 ex ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ≤ 𝐴 → 𝑖 ≤ ( 𝐵 − 1 ) ) )
30 8 29 syldc ⊢ ( 𝑖 ∥ 𝐴 → ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑖 ≤ ( 𝐵 − 1 ) ) )
31 30 adantr ⊢ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑖 ≤ ( 𝐵 − 1 ) ) )
32 31 impcom ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ≤ ( 𝐵 − 1 ) )
33 peano2zm ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 − 1 ) ∈ ℤ )
34 22 33 syl ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 − 1 ) ∈ ℤ )
35 34 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 1 ) ∈ ℤ )
36 35 anim1ci ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐵 − 1 ) ∈ ℤ ) )
37 36 adantr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐵 − 1 ) ∈ ℤ ) )
38 elfz5 ⊢ ( ( 𝑖 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐵 − 1 ) ∈ ℤ ) → ( 𝑖 ∈ ( 2 ... ( 𝐵 − 1 ) ) ↔ 𝑖 ≤ ( 𝐵 − 1 ) ) )
39 37 38 syl ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( 𝑖 ∈ ( 2 ... ( 𝐵 − 1 ) ) ↔ 𝑖 ≤ ( 𝐵 − 1 ) ) )
40 32 39 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∈ ( 2 ... ( 𝐵 − 1 ) ) )
41 breq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∥ 𝐵 ↔ 𝑖 ∥ 𝐵 ) )
42 41 adantl ⊢ ( ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) ∧ 𝑗 = 𝑖 ) → ( 𝑗 ∥ 𝐵 ↔ 𝑖 ∥ 𝐵 ) )
43 simprr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝑖 ∥ 𝐵 )
44 40 42 43 rspcedvd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ∃ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) 𝑗 ∥ 𝐵 )
45 rexnal ⊢ ( ∃ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ ¬ 𝑗 ∥ 𝐵 ↔ ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 )
46 notnotb ⊢ ( 𝑗 ∥ 𝐵 ↔ ¬ ¬ 𝑗 ∥ 𝐵 )
47 46 bicomi ⊢ ( ¬ ¬ 𝑗 ∥ 𝐵 ↔ 𝑗 ∥ 𝐵 )
48 47 rexbii ⊢ ( ∃ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ ¬ 𝑗 ∥ 𝐵 ↔ ∃ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) 𝑗 ∥ 𝐵 )
49 45 48 bitr3i ⊢ ( ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ↔ ∃ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) 𝑗 ∥ 𝐵 )
50 44 49 sylibr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 )
51 50 olcd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → ( ¬ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∨ ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ) )
52 df-nel ⊢ ( 𝐵 ∉ ℙ ↔ ¬ 𝐵 ∈ ℙ )
53 ianor ⊢ ( ¬ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ) ↔ ( ¬ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∨ ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ) )
54 isprm3 ⊢ ( 𝐵 ∈ ℙ ↔ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ) )
55 53 54 xchnxbir ⊢ ( ¬ 𝐵 ∈ ℙ ↔ ( ¬ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∨ ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ) )
56 52 55 bitri ⊢ ( 𝐵 ∉ ℙ ↔ ( ¬ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∨ ¬ ∀ 𝑗 ∈ ( 2 ... ( 𝐵 − 1 ) ) ¬ 𝑗 ∥ 𝐵 ) )
57 51 56 sylibr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) ∧ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ) → 𝐵 ∉ ℙ )
58 57 rexlimdva2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → ( ∃ 𝑖 ∈ ( ℤ≥ ‘ 2 ) ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝐵 ∉ ℙ ) )
59 3 58 sylbid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵 ) → ( 1 < ( 𝐴 gcd 𝐵 ) → 𝐵 ∉ ℙ ) )