Metamath Proof Explorer

Theorem nprm

Description: A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion nprm ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝐴 · 𝐵 ) ∈ ℙ )

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
2 1 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℤ )
3 2 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ )
4 eluz2gt1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 )
5 4 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝐵 )
6 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℤ )
7 6 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℤ )
8 7 zred ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐵 ∈ ℝ )
9 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
10 9 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℕ )
11 10 nngt0d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 0 < 𝐴 )
12 ltmulgt11 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) )
13 3 8 11 12 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) )
14 5 13 mpbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 < ( 𝐴 · 𝐵 ) )
15 3 14 ltned ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ≠ ( 𝐴 · 𝐵 ) )
16 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
17 1 6 16 syl2an ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∥ ( 𝐴 · 𝐵 ) )
18 isprm4 ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℙ ↔ ( ( 𝐴 · 𝐵 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( 𝑥 ∥ ( 𝐴 · 𝐵 ) → 𝑥 = ( 𝐴 · 𝐵 ) ) ) )
19 18 simprbi ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℙ → ∀ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( 𝑥 ∥ ( 𝐴 · 𝐵 ) → 𝑥 = ( 𝐴 · 𝐵 ) ) )
20 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∥ ( 𝐴 · 𝐵 ) ↔ 𝐴 ∥ ( 𝐴 · 𝐵 ) ) )
21 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( 𝐴 · 𝐵 ) ↔ 𝐴 = ( 𝐴 · 𝐵 ) ) )
22 20 21 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∥ ( 𝐴 · 𝐵 ) → 𝑥 = ( 𝐴 · 𝐵 ) ) ↔ ( 𝐴 ∥ ( 𝐴 · 𝐵 ) → 𝐴 = ( 𝐴 · 𝐵 ) ) ) )
23 22 rspcv ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ( 𝑥 ∥ ( 𝐴 · 𝐵 ) → 𝑥 = ( 𝐴 · 𝐵 ) ) → ( 𝐴 ∥ ( 𝐴 · 𝐵 ) → 𝐴 = ( 𝐴 · 𝐵 ) ) ) )
24 19 23 syl5 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 · 𝐵 ) ∈ ℙ → ( 𝐴 ∥ ( 𝐴 · 𝐵 ) → 𝐴 = ( 𝐴 · 𝐵 ) ) ) )
25 24 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 · 𝐵 ) ∈ ℙ → ( 𝐴 ∥ ( 𝐴 · 𝐵 ) → 𝐴 = ( 𝐴 · 𝐵 ) ) ) )
26 17 25 mpid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 · 𝐵 ) ∈ ℙ → 𝐴 = ( 𝐴 · 𝐵 ) ) )
27 26 necon3ad ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 ≠ ( 𝐴 · 𝐵 ) → ¬ ( 𝐴 · 𝐵 ) ∈ ℙ ) )
28 15 27 mpd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝐴 · 𝐵 ) ∈ ℙ )