Metamath Proof Explorer


Theorem fmtnoprmfac2lem1

Description: Lemma for fmtnoprmfac2 . (Contributed by AV, 26-Jul-2021)

Ref Expression
Assertion fmtnoprmfac2lem1 N2P2PFermatNoN2P12modP=1

Proof

Step Hyp Ref Expression
1 eluz2nn N2N
2 eldifi P2P
3 id PFermatNoNPFermatNoN
4 fmtnoprmfac1 NPPFermatNoNnP=n2N+1+1
5 1 2 3 4 syl3an N2P2PFermatNoNnP=n2N+1+1
6 2z 2
7 simp2 N2P2PFermatNoNP2
8 lgsvalmod 2P22/LPmodP=2P12modP
9 8 eqcomd 2P22P12modP=2/LPmodP
10 6 7 9 sylancr N2P2PFermatNoN2P12modP=2/LPmodP
11 10 ad2antrr N2P2PFermatNoNnP=n2N+1+12P12modP=2/LPmodP
12 nncn nn
13 12 adantl N2nn
14 2nn 2
15 14 a1i N22
16 eluzge2nn0 N2N0
17 peano2nn0 N0N+10
18 16 17 syl N2N+10
19 15 18 nnexpcld N22N+1
20 19 nncnd N22N+1
21 20 adantr N2n2N+1
22 13 21 mulcomd N2nn2N+1=2N+1n
23 8cn 8
24 23 a1i N2n8
25 0re 0
26 8pos 0<8
27 25 26 gtneii 80
28 27 a1i N2n80
29 21 24 28 divcan2d N2n82N+18=2N+1
30 29 eqcomd N2n2N+1=82N+18
31 30 oveq1d N2n2N+1n=82N+18n
32 23 a1i N28
33 27 a1i N280
34 20 32 33 divcld N22N+18
35 34 adantr N2n2N+18
36 24 35 13 mulassd N2n82N+18n=82N+18n
37 22 31 36 3eqtrd N2nn2N+1=82N+18n
38 37 oveq1d N2nn2N+1+1=82N+18n+1
39 38 eqeq2d N2nP=n2N+1+1P=82N+18n+1
40 oveq1 P=82N+18n+1Pmod8=82N+18n+1mod8
41 40 adantl N2nP=82N+18n+1Pmod8=82N+18n+1mod8
42 3m1e2 31=2
43 eluzle N22N
44 42 43 eqbrtrid N231N
45 3re 3
46 45 a1i N23
47 1red N21
48 eluzelre N2N
49 46 47 48 lesubaddd N231N3N+1
50 44 49 mpbid N23N+1
51 3nn0 30
52 nn0sub 30N+103N+1N+1-30
53 51 18 52 sylancr N23N+1N+1-30
54 50 53 mpbid N2N+1-30
55 15 54 nnexpcld N22N+1-3
56 55 nnzd N22N+1-3
57 oveq2 k=2N+1-38k=82N+1-3
58 57 eqeq1d k=2N+1-38k=2N+182N+1-3=2N+1
59 58 adantl N2k=2N+1-38k=2N+182N+1-3=2N+1
60 cu2 23=8
61 60 eqcomi 8=23
62 61 a1i N28=23
63 2cnne0 220
64 63 a1i N2220
65 eluzelz N2N
66 65 peano2zd N2N+1
67 3z 3
68 67 a1i N23
69 expsub 220N+132N+1-3=2N+123
70 64 66 68 69 syl12anc N22N+1-3=2N+123
71 62 70 oveq12d N282N+1-3=232N+123
72 nnexpcl 23023
73 14 51 72 mp2an 23
74 73 nncni 23
75 74 a1i N223
76 2cn 2
77 2ne0 20
78 expne0i 2203230
79 76 77 67 78 mp3an 230
80 79 a1i N2230
81 20 75 80 divcan2d N2232N+123=2N+1
82 71 81 eqtrd N282N+1-3=2N+1
83 56 59 82 rspcedvd N2k8k=2N+1
84 8nn 8
85 2nn0 20
86 85 a1i N220
87 86 18 nn0expcld N22N+10
88 87 nn0zd N22N+1
89 zdiv 82N+1k8k=2N+12N+18
90 84 88 89 sylancr N2k8k=2N+12N+18
91 83 90 mpbid N22N+18
92 91 adantr N2n2N+18
93 nnz nn
94 93 adantl N2nn
95 92 94 zmulcld N2n2N+18n
96 84 nnzi 8
97 2re 2
98 8re 8
99 2lt8 2<8
100 97 98 99 ltleii 28
101 eluz2 822828
102 6 96 100 101 mpbir3an 82
103 mulp1mod1 2N+18n8282N+18n+1mod8=1
104 95 102 103 sylancl N2n82N+18n+1mod8=1
105 1nn 1
106 prid1g 1117
107 105 106 mp1i N2n117
108 104 107 eqeltrd N2n82N+18n+1mod817
109 108 adantr N2nP=82N+18n+182N+18n+1mod817
110 41 109 eqeltrd N2nP=82N+18n+1Pmod817
111 110 ex N2nP=82N+18n+1Pmod817
112 39 111 sylbid N2nP=n2N+1+1Pmod817
113 112 3ad2antl1 N2P2PFermatNoNnP=n2N+1+1Pmod817
114 113 imp N2P2PFermatNoNnP=n2N+1+1Pmod817
115 2lgs P2/LP=1Pmod817
116 2 115 syl P22/LP=1Pmod817
117 116 3ad2ant2 N2P2PFermatNoN2/LP=1Pmod817
118 117 ad2antrr N2P2PFermatNoNnP=n2N+1+12/LP=1Pmod817
119 114 118 mpbird N2P2PFermatNoNnP=n2N+1+12/LP=1
120 119 oveq1d N2P2PFermatNoNnP=n2N+1+12/LPmodP=1modP
121 prmuz2 PP2
122 eluzelre P2P
123 eluz2gt1 P21<P
124 122 123 jca P2P1<P
125 121 124 syl PP1<P
126 1mod P1<P1modP=1
127 2 125 126 3syl P21modP=1
128 127 3ad2ant2 N2P2PFermatNoN1modP=1
129 128 ad2antrr N2P2PFermatNoNnP=n2N+1+11modP=1
130 11 120 129 3eqtrd N2P2PFermatNoNnP=n2N+1+12P12modP=1
131 130 rexlimdva2 N2P2PFermatNoNnP=n2N+1+12P12modP=1
132 5 131 mpd N2P2PFermatNoN2P12modP=1