Metamath Proof Explorer

Theorem nprmdvdsfacm1lem2

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

Ref Expression
Assertion nprmdvdsfacm1lem2 ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 3 ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ↔ ( 6 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) )
2 breq2 ⊢ ( 𝑁 = ( 𝐴 ↑ 2 ) → ( 6 ≤ 𝑁 ↔ 6 ≤ ( 𝐴 ↑ 2 ) ) )
3 2 adantr ⊢ ( ( 𝑁 = ( 𝐴 ↑ 2 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( 6 ≤ 𝑁 ↔ 6 ≤ ( 𝐴 ↑ 2 ) ) )
4 elfzo2 ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) )
5 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) )
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℝ )
8 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
9 7 8 leloed ⊢ ( 𝐴 ∈ ℤ → ( 2 ≤ 𝐴 ↔ ( 2 < 𝐴 ∨ 2 = 𝐴 ) ) )
10 df-3 ⊢ 3 = ( 2 + 1 )
11 2z ⊢ 2 ∈ ℤ
12 11 a1i ⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℤ )
13 id ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℤ )
14 12 13 zltp1led ⊢ ( 𝐴 ∈ ℤ → ( 2 < 𝐴 ↔ ( 2 + 1 ) ≤ 𝐴 ) )
15 14 biimpa ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → ( 2 + 1 ) ≤ 𝐴 )
16 10 15 eqbrtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → 3 ≤ 𝐴 )
17 16 a1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 < 𝐴 ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
18 17 ex ⊢ ( 𝐴 ∈ ℤ → ( 2 < 𝐴 → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
19 oveq1 ⊢ ( 2 = 𝐴 → ( 2 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
20 19 breq2d ⊢ ( 2 = 𝐴 → ( 6 ≤ ( 2 ↑ 2 ) ↔ 6 ≤ ( 𝐴 ↑ 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 ≤ 𝐴 )
29 22 28 sylbi ⊢ ( 6 ≤ ( 2 ↑ 2 ) → 3 ≤ 𝐴 )
30 20 29 biimtrrdi ⊢ ( 2 = 𝐴 → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
31 30 a1i ⊢ ( 𝐴 ∈ ℤ → ( 2 = 𝐴 → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
32 18 31 jaod ⊢ ( 𝐴 ∈ ℤ → ( ( 2 < 𝐴 ∨ 2 = 𝐴 ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
33 9 32 sylbid ⊢ ( 𝐴 ∈ ℤ → ( 2 ≤ 𝐴 → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
34 33 a1i ⊢ ( 2 ∈ ℤ → ( 𝐴 ∈ ℤ → ( 2 ≤ 𝐴 → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) ) )
35 34 3imp ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
36 5 35 sylbi ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
37 36 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
38 4 37 sylbi ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
39 38 adantl ⊢ ( ( 𝑁 = ( 𝐴 ↑ 2 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( 6 ≤ ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) )
40 3 39 sylbid ⊢ ( ( 𝑁 = ( 𝐴 ↑ 2 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( 6 ≤ 𝑁 → 3 ≤ 𝐴 ) )
41 40 ex ⊢ ( 𝑁 = ( 𝐴 ↑ 2 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 6 ≤ 𝑁 → 3 ≤ 𝐴 ) ) )
42 41 com13 ⊢ ( 6 ≤ 𝑁 → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝑁 = ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
43 42 3ad2ant3 ⊢ ( ( 6 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝑁 = ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
44 1 43 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝑁 = ( 𝐴 ↑ 2 ) → 3 ≤ 𝐴 ) ) )
45 44 3imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 3 ≤ 𝐴 )