Metamath Proof Explorer

Theorem nprmdvdsfacm1lem2

Description: Lemma 2 for nprmdvdsfacm1 . (Contributed by AV, 7-Apr-2026)

Ref Expression
Assertion nprmdvdsfacm1lem2 ⊢ N ∈ ℤ ≥ 6 ∧ A ∈ 2 ..^ N ∧ N = A 2 → 3 ≤ A

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ N ∈ ℤ ≥ 6 ↔ 6 ∈ ℤ ∧ N ∈ ℤ ∧ 6 ≤ N
2 breq2 ⊢ N = A 2 → 6 ≤ N ↔ 6 ≤ A 2
3 2 adantr ⊢ N = A 2 ∧ A ∈ 2 ..^ N → 6 ≤ N ↔ 6 ≤ A 2
4 elfzo2 ⊢ A ∈ 2 ..^ N ↔ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ A < N
5 eluz2 ⊢ A ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ A ∈ ℤ ∧ 2 ≤ A
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ A ∈ ℤ → 2 ∈ ℝ
8 zre ⊢ A ∈ ℤ → A ∈ ℝ
9 7 8 leloed ⊢ A ∈ ℤ → 2 ≤ A ↔ 2 < A ∨ 2 = A
10 df-3 ⊢ 3 = 2 + 1
11 2z ⊢ 2 ∈ ℤ
12 11 a1i ⊢ A ∈ ℤ → 2 ∈ ℤ
13 id ⊢ A ∈ ℤ → A ∈ ℤ
14 12 13 zltp1led ⊢ A ∈ ℤ → 2 < A ↔ 2 + 1 ≤ A
15 14 biimpa ⊢ A ∈ ℤ ∧ 2 < A → 2 + 1 ≤ A
16 10 15 eqbrtrid ⊢ A ∈ ℤ ∧ 2 < A → 3 ≤ A
17 16 a1d ⊢ A ∈ ℤ ∧ 2 < A → 6 ≤ A 2 → 3 ≤ A
18 17 ex ⊢ A ∈ ℤ → 2 < A → 6 ≤ A 2 → 3 ≤ A
19 oveq1 ⊢ 2 = A → 2 2 = A 2
20 19 breq2d ⊢ 2 = A → 6 ≤ 2 2 ↔ 6 ≤ A 2
21 sq2 ⊢ 2 2 = 4
22 21 breq2i ⊢ 6 ≤ 2 2 ↔ 6 ≤ 4
23 4lt6 ⊢ 4 < 6
24 4re ⊢ 4 ∈ ℝ
25 6re ⊢ 6 ∈ ℝ
26 24 25 ltnlei ⊢ 4 < 6 ↔ ¬ 6 ≤ 4
27 23 26 mpbi ⊢ ¬ 6 ≤ 4
28 27 pm2.21i ⊢ 6 ≤ 4 → 3 ≤ A
29 22 28 sylbi ⊢ 6 ≤ 2 2 → 3 ≤ A
30 20 29 biimtrrdi ⊢ 2 = A → 6 ≤ A 2 → 3 ≤ A
31 30 a1i ⊢ A ∈ ℤ → 2 = A → 6 ≤ A 2 → 3 ≤ A
32 18 31 jaod ⊢ A ∈ ℤ → 2 < A ∨ 2 = A → 6 ≤ A 2 → 3 ≤ A
33 9 32 sylbid ⊢ A ∈ ℤ → 2 ≤ A → 6 ≤ A 2 → 3 ≤ A
34 33 a1i ⊢ 2 ∈ ℤ → A ∈ ℤ → 2 ≤ A → 6 ≤ A 2 → 3 ≤ A
35 34 3imp ⊢ 2 ∈ ℤ ∧ A ∈ ℤ ∧ 2 ≤ A → 6 ≤ A 2 → 3 ≤ A
36 5 35 sylbi ⊢ A ∈ ℤ ≥ 2 → 6 ≤ A 2 → 3 ≤ A
37 36 3ad2ant1 ⊢ A ∈ ℤ ≥ 2 ∧ N ∈ ℤ ∧ A < N → 6 ≤ A 2 → 3 ≤ A
38 4 37 sylbi ⊢ A ∈ 2 ..^ N → 6 ≤ A 2 → 3 ≤ A
39 38 adantl ⊢ N = A 2 ∧ A ∈ 2 ..^ N → 6 ≤ A 2 → 3 ≤ A
40 3 39 sylbid ⊢ N = A 2 ∧ A ∈ 2 ..^ N → 6 ≤ N → 3 ≤ A
41 40 ex ⊢ N = A 2 → A ∈ 2 ..^ N → 6 ≤ N → 3 ≤ A
42 41 com13 ⊢ 6 ≤ N → A ∈ 2 ..^ N → N = A 2 → 3 ≤ A
43 42 3ad2ant3 ⊢ 6 ∈ ℤ ∧ N ∈ ℤ ∧ 6 ≤ N → A ∈ 2 ..^ N → N = A 2 → 3 ≤ A
44 1 43 sylbi ⊢ N ∈ ℤ ≥ 6 → A ∈ 2 ..^ N → N = A 2 → 3 ≤ A
45 44 3imp ⊢ N ∈ ℤ ≥ 6 ∧ A ∈ 2 ..^ N ∧ N = A 2 → 3 ≤ A