Metamath Proof Explorer

Theorem nprmdvdsfacm1lem3

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

Ref Expression
Assertion nprmdvdsfacm1lem3 ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) < ( 𝑁 − 1 ) )

Proof

Step Hyp Ref Expression
1 3z ⊢ 3 ∈ ℤ
2 1 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 3 ∈ ℤ )
3 elfzoelz ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
4 3 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝐴 ∈ ℤ )
5 nprmdvdsfacm1lem2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 3 ≤ 𝐴 )
6 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 3 ≤ 𝐴 ) )
7 2 4 5 6 syl3anbrc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 3 ) )
8 2timesltsqm1 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
9 7 8 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) )
10 oveq1 ⊢ ( 𝑁 = ( 𝐴 ↑ 2 ) → ( 𝑁 − 1 ) = ( ( 𝐴 ↑ 2 ) − 1 ) )
11 10 breq2d ⊢ ( 𝑁 = ( 𝐴 ↑ 2 ) → ( ( 2 · 𝐴 ) < ( 𝑁 − 1 ) ↔ ( 2 · 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( ( 2 · 𝐴 ) < ( 𝑁 − 1 ) ↔ ( 2 · 𝐴 ) < ( ( 𝐴 ↑ 2 ) − 1 ) ) )
13 9 12 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) < ( 𝑁 − 1 ) )