Metamath Proof Explorer

Theorem nprmdvdsfacm1lem4

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

Ref Expression
Assertion nprmdvdsfacm1lem4 
|- ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> N || ( ! ` ( N - 1 ) ) )

Proof

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