Metamath Proof Explorer

Theorem nprmdvdsfacm1lem4

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

Ref Expression
Assertion nprmdvdsfacm1lem4 ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ℤ )
2 1 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∈ ℤ )
3 elfzoelz ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
4 id ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℤ )
5 2z ⊢ 2 ∈ ℤ
6 5 a1i ⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℤ )
7 6 4 zmulcld ⊢ ( 𝐴 ∈ ℤ → ( 2 · 𝐴 ) ∈ ℤ )
8 4 7 zmulcld ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 · ( 2 · 𝐴 ) ) ∈ ℤ )
9 3 8 syl ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 · ( 2 · 𝐴 ) ) ∈ ℤ )
10 9 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 · ( 2 · 𝐴 ) ) ∈ ℤ )
11 1z ⊢ 1 ∈ ℤ
12 6nn ⊢ 6 ∈ ℕ
13 12 nnzi ⊢ 6 ∈ ℤ
14 1re ⊢ 1 ∈ ℝ
15 6re ⊢ 6 ∈ ℝ
16 1lt6 ⊢ 1 < 6
17 14 15 16 ltleii ⊢ 1 ≤ 6
18 eluz2 ⊢ ( 6 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 6 ∈ ℤ ∧ 1 ≤ 6 ) )
19 11 13 17 18 mpbir3an ⊢ 6 ∈ ( ℤ≥ ‘ 1 )
20 uzss ⊢ ( 6 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 1 ) )
21 19 20 ax-mp ⊢ ( ℤ≥ ‘ 6 ) ⊆ ( ℤ≥ ‘ 1 )
22 21 sseli ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
23 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
24 22 23 sylibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → 𝑁 ∈ ℕ )
25 24 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∈ ℕ )
26 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
27 25 26 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝑁 − 1 ) ∈ ℕ0 )
28 27 faccld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℕ )
29 28 nnzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( ! ‘ ( 𝑁 − 1 ) ) ∈ ℤ )
30 nprmdvdsfacm1lem1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∥ ( 𝐴 · ( 2 · 𝐴 ) ) )
31 elfzo2 ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) )
32 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
33 uzss ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 1 ) )
34 32 33 ax-mp ⊢ ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 1 )
35 34 sseli ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
36 35 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
37 5 a1i ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℤ )
38 eluzelz ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℤ )
39 37 38 zmulcld ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 2 · 𝐴 ) ∈ ℤ )
40 39 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 2 · 𝐴 ) ∈ ℤ )
41 1lt2 ⊢ 1 < 2
42 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) )
43 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
44 43 3ad2ant2 ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
45 2re ⊢ 2 ∈ ℝ
46 45 a1i ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → 2 ∈ ℝ )
47 2pos ⊢ 0 < 2
48 0red ⊢ ( 𝐴 ∈ ℤ → 0 ∈ ℝ )
49 45 a1i ⊢ ( 𝐴 ∈ ℤ → 2 ∈ ℝ )
50 48 49 43 3jca ⊢ ( 𝐴 ∈ ℤ → ( 0 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
51 ltletr ⊢ ( ( 0 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 < 2 ∧ 2 ≤ 𝐴 ) → 0 < 𝐴 ) )
52 50 51 syl ⊢ ( 𝐴 ∈ ℤ → ( ( 0 < 2 ∧ 2 ≤ 𝐴 ) → 0 < 𝐴 ) )
53 47 52 mpani ⊢ ( 𝐴 ∈ ℤ → ( 2 ≤ 𝐴 → 0 < 𝐴 ) )
54 53 imp ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → 0 < 𝐴 )
55 54 3adant1 ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → 0 < 𝐴 )
56 44 46 55 3jca ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 𝐴 ) )
57 42 56 sylbi ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 𝐴 ) )
58 57 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 𝐴 ) )
59 ltmulgt12 ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 < 2 ↔ 𝐴 < ( 2 · 𝐴 ) ) )
60 58 59 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 1 < 2 ↔ 𝐴 < ( 2 · 𝐴 ) ) )
61 41 60 mpbii ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → 𝐴 < ( 2 · 𝐴 ) )
62 36 40 61 3jca ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 𝐴 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 2 · 𝐴 ) ∈ ℤ ∧ 𝐴 < ( 2 · 𝐴 ) ) )
63 31 62 sylbi ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 2 · 𝐴 ) ∈ ℤ ∧ 𝐴 < ( 2 · 𝐴 ) ) )
64 elfzo2 ⊢ ( 𝐴 ∈ ( 1 ..^ ( 2 · 𝐴 ) ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 2 · 𝐴 ) ∈ ℤ ∧ 𝐴 < ( 2 · 𝐴 ) ) )
65 63 64 sylibr ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ( 1 ..^ ( 2 · 𝐴 ) ) )
66 65 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝐴 ∈ ( 1 ..^ ( 2 · 𝐴 ) ) )
67 11 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 1 ∈ ℤ )
68 5 a1i ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 2 ∈ ℤ )
69 68 3 zmulcld ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 2 · 𝐴 ) ∈ ℤ )
70 69 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) ∈ ℤ )
71 47 a1i ⊢ ( 𝐴 ∈ ℤ → 0 < 2 )
72 lemul2 ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 2 ≤ 𝐴 ↔ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) )
73 49 43 49 71 72 syl112anc ⊢ ( 𝐴 ∈ ℤ → ( 2 ≤ 𝐴 ↔ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) )
74 1red ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) → 1 ∈ ℝ )
75 2t2e4 ⊢ ( 2 · 2 ) = 4
76 4re ⊢ 4 ∈ ℝ
77 75 76 eqeltri ⊢ ( 2 · 2 ) ∈ ℝ
78 77 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) → ( 2 · 2 ) ∈ ℝ )
79 7 zred ⊢ ( 𝐴 ∈ ℤ → ( 2 · 𝐴 ) ∈ ℝ )
80 79 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) → ( 2 · 𝐴 ) ∈ ℝ )
81 1lt4 ⊢ 1 < 4
82 14 76 81 ltleii ⊢ 1 ≤ 4
83 82 75 breqtrri ⊢ 1 ≤ ( 2 · 2 )
84 83 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) → 1 ≤ ( 2 · 2 ) )
85 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) → ( 2 · 2 ) ≤ ( 2 · 𝐴 ) )
86 74 78 80 84 85 letrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 · 2 ) ≤ ( 2 · 𝐴 ) ) → 1 ≤ ( 2 · 𝐴 ) )
87 73 86 sylbida ⊢ ( ( 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → 1 ≤ ( 2 · 𝐴 ) )
88 87 3adant1 ⊢ ( ( 2 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 2 ≤ 𝐴 ) → 1 ≤ ( 2 · 𝐴 ) )
89 42 88 sylbi ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( 2 · 𝐴 ) )
90 89 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → 1 ≤ ( 2 · 𝐴 ) )
91 31 90 sylbi ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 1 ≤ ( 2 · 𝐴 ) )
92 91 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 1 ≤ ( 2 · 𝐴 ) )
93 eluz2 ⊢ ( ( 2 · 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ ( 2 · 𝐴 ) ∈ ℤ ∧ 1 ≤ ( 2 · 𝐴 ) ) )
94 67 70 92 93 syl3anbrc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
95 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
96 3 95 syl ⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
97 96 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 ↑ 2 ) ∈ ℤ )
98 3z ⊢ 3 ∈ ℤ
99 98 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 3 ∈ ℤ )
100 3 3ad2ant2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝐴 ∈ ℤ )
101 nprmdvdsfacm1lem2 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 3 ≤ 𝐴 )
102 eluz2 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 3 ≤ 𝐴 ) )
103 99 100 101 102 syl3anbrc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝐴 ∈ ( ℤ≥ ‘ 3 ) )
104 2timesltsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 3 ) → ( 2 · 𝐴 ) < ( 𝐴 ↑ 2 ) )
105 103 104 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) < ( 𝐴 ↑ 2 ) )
106 94 97 105 elfzod ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) ∈ ( 1 ..^ ( 𝐴 ↑ 2 ) ) )
107 oveq2 ⊢ ( 𝑁 = ( 𝐴 ↑ 2 ) → ( 1 ..^ 𝑁 ) = ( 1 ..^ ( 𝐴 ↑ 2 ) ) )
108 107 eleq2d ⊢ ( 𝑁 = ( 𝐴 ↑ 2 ) → ( ( 2 · 𝐴 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( 2 · 𝐴 ) ∈ ( 1 ..^ ( 𝐴 ↑ 2 ) ) ) )
109 108 3ad2ant3 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( ( 2 · 𝐴 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( 2 · 𝐴 ) ∈ ( 1 ..^ ( 𝐴 ↑ 2 ) ) ) )
110 106 109 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 2 · 𝐴 ) ∈ ( 1 ..^ 𝑁 ) )
111 muldvdsfacm1 ⊢ ( ( 𝐴 ∈ ( 1 ..^ ( 2 · 𝐴 ) ) ∧ ( 2 · 𝐴 ) ∈ ( 1 ..^ 𝑁 ) ) → ( 𝐴 · ( 2 · 𝐴 ) ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
112 66 110 111 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → ( 𝐴 · ( 2 · 𝐴 ) ) ∥ ( ! ‘ ( 𝑁 − 1 ) ) )
113 2 10 29 30 112 dvdstrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 = ( 𝐴 ↑ 2 ) ) → 𝑁 ∥ ( ! ‘ ( 𝑁 − 1 ) ) )