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

Metamath Proof Explorer

Theorem nnmul2

Description: If one factor of a product of integers is at least 2 and less then the product, so is the second factor. (Contributed by AV, 5-Apr-2026)

Ref Expression
Assertion nnmul2 ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 ⊢ ( 𝐵 ∈ ℕ ↔ ( 𝐵 = 1 ∨ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) )
2 oveq2 ⊢ ( 𝐵 = 1 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 1 ) )
3 2 eqeq1d ⊢ ( 𝐵 = 1 → ( ( 𝐴 · 𝐵 ) = 𝑁 ↔ ( 𝐴 · 1 ) = 𝑁 ) )
4 3 adantr ⊢ ( ( 𝐵 = 1 ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝐴 · 𝐵 ) = 𝑁 ↔ ( 𝐴 · 1 ) = 𝑁 ) )
5 elfzoelz ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
6 5 zred ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℝ )
7 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
8 6 7 syl ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 · 1 ) = 𝐴 )
9 8 eqeq1d ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 1 ) = 𝑁 ↔ 𝐴 = 𝑁 ) )
10 elfzo2 ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) )
11 breq2 ⊢ ( 𝑁 = 𝐴 → ( 𝐴 < 𝑁 ↔ 𝐴 < 𝐴 ) )
12 11 eqcoms ⊢ ( 𝐴 = 𝑁 → ( 𝐴 < 𝑁 ↔ 𝐴 < 𝐴 ) )
13 12 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 = 𝑁 ) → ( 𝐴 < 𝑁 ↔ 𝐴 < 𝐴 ) )
14 eluzelre ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
15 14 ltnrd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ¬ 𝐴 < 𝐴 )
16 15 pm2.21d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 < 𝐴 → 2 ≤ 𝐵 ) )
17 16 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 = 𝑁 ) → ( 𝐴 < 𝐴 → 2 ≤ 𝐵 ) )
18 13 17 sylbid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 = 𝑁 ) → ( 𝐴 < 𝑁 → 2 ≤ 𝐵 ) )
19 18 impancom ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 < 𝑁 ) → ( 𝐴 = 𝑁 → 2 ≤ 𝐵 ) )
20 19 3adant2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 𝐴 = 𝑁 → 2 ≤ 𝐵 ) )
21 10 20 sylbi ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 = 𝑁 → 2 ≤ 𝐵 ) )
22 9 21 sylbid ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 1 ) = 𝑁 → 2 ≤ 𝐵 ) )
23 22 adantl ⊢ ( ( 𝐵 = 1 ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝐴 · 1 ) = 𝑁 → 2 ≤ 𝐵 ) )
24 4 23 sylbid ⊢ ( ( 𝐵 = 1 ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) )
25 24 ex ⊢ ( 𝐵 = 1 → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
26 eluzle ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝐵 )
27 26 2a1d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
28 25 27 jaoi ⊢ ( ( 𝐵 = 1 ∨ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
29 1 28 sylbi ⊢ ( 𝐵 ∈ ℕ → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
30 29 3imp21 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 2 ≤ 𝐵 )
31 eluz2gt1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐴 )
32 31 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → 1 < 𝐴 )
33 10 32 sylbi ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 1 < 𝐴 )
34 33 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 1 < 𝐴 )
35 6 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐴 ∈ ℝ )
36 nnrp ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
37 36 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ℝ+ )
38 35 37 ltmulgt12d ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 1 < 𝐴 ↔ 𝐵 < ( 𝐴 · 𝐵 ) ) )
39 34 38 mpbid ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 < ( 𝐴 · 𝐵 ) )
40 breq2 ⊢ ( ( 𝐴 · 𝐵 ) = 𝑁 → ( 𝐵 < ( 𝐴 · 𝐵 ) ↔ 𝐵 < 𝑁 ) )
41 40 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 < ( 𝐴 · 𝐵 ) ↔ 𝐵 < 𝑁 ) )
42 39 41 mpbid ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 < 𝑁 )
43 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
44 43 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ℤ )
45 2z ⊢ 2 ∈ ℤ
46 45 a1i ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 2 ∈ ℤ )
47 elfzoel2 ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
48 47 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝑁 ∈ ℤ )
49 elfzo ⊢ ( ( 𝐵 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 ∈ ( 2 ..^ 𝑁 ) ↔ ( 2 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) ) )
50 44 46 48 49 syl3anc ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 ∈ ( 2 ..^ 𝑁 ) ↔ ( 2 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) ) )
51 30 42 50 mpbir2and ⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) )