Metamath Proof Explorer


Theorem freshmansdream

Description: For a prime number P , if X and Y are members of a commutative ring R of characteristic P , then ( ( X + Y ) ^ P ) = ( ( X ^ P ) + ( Y ^ P ) ) . This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023)

Ref Expression
Hypotheses freshmansdream.s B=BaseR
freshmansdream.a +˙=+R
freshmansdream.p ×˙=mulGrpR
freshmansdream.c P=chrR
freshmansdream.r φRCRing
freshmansdream.1 φP
freshmansdream.x φXB
freshmansdream.y φYB
Assertion freshmansdream φP×˙X+˙Y=P×˙X+˙P×˙Y

Proof

Step Hyp Ref Expression
1 freshmansdream.s B=BaseR
2 freshmansdream.a +˙=+R
3 freshmansdream.p ×˙=mulGrpR
4 freshmansdream.c P=chrR
5 freshmansdream.r φRCRing
6 freshmansdream.1 φP
7 freshmansdream.x φXB
8 freshmansdream.y φYB
9 crngring RCRingRRing
10 4 chrcl RRingP0
11 5 9 10 3syl φP0
12 eqid R=R
13 eqid R=R
14 eqid mulGrpR=mulGrpR
15 1 12 13 2 14 3 crngbinom RCRingP0XBYBP×˙X+˙Y=Ri=0P(Pi)RPi×˙XRi×˙Y
16 5 11 7 8 15 syl22anc φP×˙X+˙Y=Ri=0P(Pi)RPi×˙XRi×˙Y
17 11 nn0cnd φP
18 1cnd φ1
19 17 18 npcand φP-1+1=P
20 19 oveq2d φ0P-1+1=0P
21 20 eqcomd φ0P=0P-1+1
22 21 mpteq1d φi0P(Pi)RPi×˙XRi×˙Y=i0P-1+1(Pi)RPi×˙XRi×˙Y
23 22 oveq2d φRi=0P(Pi)RPi×˙XRi×˙Y=Ri=0P-1+1(Pi)RPi×˙XRi×˙Y
24 ringcmn RRingRCMnd
25 5 9 24 3syl φRCMnd
26 prmnn PP
27 nnm1nn0 PP10
28 6 26 27 3syl φP10
29 ringgrp RRingRGrp
30 5 9 29 3syl φRGrp
31 30 adantr φi0P-1+1RGrp
32 11 adantr φi0P-1+1P0
33 fzssz 0P-1+1
34 33 a1i φ0P-1+1
35 34 sselda φi0P-1+1i
36 bccl P0i(Pi)0
37 32 35 36 syl2anc φi0P-1+1(Pi)0
38 37 nn0zd φi0P-1+1(Pi)
39 5 9 syl φRRing
40 39 adantr φi0P-1+1RRing
41 14 ringmgp RRingmulGrpRMnd
42 39 41 syl φmulGrpRMnd
43 42 adantr φi0P-1+1mulGrpRMnd
44 simpr φi0P-1+1i0P-1+1
45 20 adantr φi0P-1+10P-1+1=0P
46 44 45 eleqtrd φi0P-1+1i0P
47 fznn0sub i0PPi0
48 46 47 syl φi0P-1+1Pi0
49 7 adantr φi0P-1+1XB
50 14 1 mgpbas B=BasemulGrpR
51 50 3 mulgnn0cl mulGrpRMndPi0XBPi×˙XB
52 43 48 49 51 syl3anc φi0P-1+1Pi×˙XB
53 elfznn0 i0P-1+1i0
54 53 adantl φi0P-1+1i0
55 8 adantr φi0P-1+1YB
56 50 3 mulgnn0cl mulGrpRMndi0YBi×˙YB
57 43 54 55 56 syl3anc φi0P-1+1i×˙YB
58 1 12 ringcl RRingPi×˙XBi×˙YBPi×˙XRi×˙YB
59 40 52 57 58 syl3anc φi0P-1+1Pi×˙XRi×˙YB
60 1 13 mulgcl RGrp(Pi)Pi×˙XRi×˙YB(Pi)RPi×˙XRi×˙YB
61 31 38 59 60 syl3anc φi0P-1+1(Pi)RPi×˙XRi×˙YB
62 1 2 25 28 61 gsummptfzsplit φRi=0P-1+1(Pi)RPi×˙XRi×˙Y=Ri=0P1(Pi)RPi×˙XRi×˙Y+˙RiP-1+1(Pi)RPi×˙XRi×˙Y
63 30 adantr φi0P1RGrp
64 elfzelz i0P1i
65 11 64 36 syl2an φi0P1(Pi)0
66 65 nn0zd φi0P1(Pi)
67 39 adantr φi0P1RRing
68 67 41 syl φi0P1mulGrpRMnd
69 fzssp1 0P10P-1+1
70 69 20 sseqtrid φ0P10P
71 70 sselda φi0P1i0P
72 71 47 syl φi0P1Pi0
73 7 adantr φi0P1XB
74 68 72 73 51 syl3anc φi0P1Pi×˙XB
75 elfznn0 i0P1i0
76 75 adantl φi0P1i0
77 8 adantr φi0P1YB
78 68 76 77 56 syl3anc φi0P1i×˙YB
79 67 74 78 58 syl3anc φi0P1Pi×˙XRi×˙YB
80 63 66 79 60 syl3anc φi0P1(Pi)RPi×˙XRi×˙YB
81 1 2 25 28 80 gsummptfzsplitl φRi=0P1(Pi)RPi×˙XRi×˙Y=Ri=1P1(Pi)RPi×˙XRi×˙Y+˙Ri0(Pi)RPi×˙XRi×˙Y
82 39 adantr φi1P1RRing
83 prmdvdsbc Pi1P1P(Pi)
84 6 83 sylan φi1P1P(Pi)
85 82 41 syl φi1P1mulGrpRMnd
86 11 nn0zd φP
87 1nn0 10
88 eluzmn P10PP1
89 86 87 88 sylancl φPP1
90 fzss2 PP11P11P
91 89 90 syl φ1P11P
92 91 sselda φi1P1i1P
93 fznn0sub i1PPi0
94 92 93 syl φi1P1Pi0
95 7 adantr φi1P1XB
96 85 94 95 51 syl3anc φi1P1Pi×˙XB
97 elfznn i1P1i
98 97 nnnn0d i1P1i0
99 98 adantl φi1P1i0
100 8 adantr φi1P1YB
101 85 99 100 56 syl3anc φi1P1i×˙YB
102 82 96 101 58 syl3anc φi1P1Pi×˙XRi×˙YB
103 eqid 0R=0R
104 4 1 13 103 dvdschrmulg RRingP(Pi)Pi×˙XRi×˙YB(Pi)RPi×˙XRi×˙Y=0R
105 82 84 102 104 syl3anc φi1P1(Pi)RPi×˙XRi×˙Y=0R
106 105 mpteq2dva φi1P1(Pi)RPi×˙XRi×˙Y=i1P10R
107 106 oveq2d φRi=1P1(Pi)RPi×˙XRi×˙Y=Ri=1P10R
108 ringmnd RRingRMnd
109 39 108 syl φRMnd
110 ovex 1P1V
111 103 gsumz RMnd1P1VRi=1P10R=0R
112 109 110 111 sylancl φRi=1P10R=0R
113 107 112 eqtrd φRi=1P1(Pi)RPi×˙XRi×˙Y=0R
114 0nn0 00
115 114 a1i φ00
116 50 3 mulgnn0cl mulGrpRMndP0XBP×˙XB
117 42 11 7 116 syl3anc φP×˙XB
118 simpr φi=0i=0
119 118 oveq2d φi=0(Pi)=(P0)
120 118 oveq2d φi=0Pi=P0
121 120 oveq1d φi=0Pi×˙X=P0×˙X
122 118 oveq1d φi=0i×˙Y=0×˙Y
123 121 122 oveq12d φi=0Pi×˙XRi×˙Y=P0×˙XR0×˙Y
124 119 123 oveq12d φi=0(Pi)RPi×˙XRi×˙Y=(P0)RP0×˙XR0×˙Y
125 bcn0 P0(P0)=1
126 11 125 syl φ(P0)=1
127 17 subid1d φP0=P
128 127 oveq1d φP0×˙X=P×˙X
129 eqid 1R=1R
130 14 129 ringidval 1R=0mulGrpR
131 50 130 3 mulg0 YB0×˙Y=1R
132 8 131 syl φ0×˙Y=1R
133 128 132 oveq12d φP0×˙XR0×˙Y=P×˙XR1R
134 1 12 129 ringridm RRingP×˙XBP×˙XR1R=P×˙X
135 39 117 134 syl2anc φP×˙XR1R=P×˙X
136 133 135 eqtrd φP0×˙XR0×˙Y=P×˙X
137 126 136 oveq12d φ(P0)RP0×˙XR0×˙Y=1RP×˙X
138 1 13 mulg1 P×˙XB1RP×˙X=P×˙X
139 117 138 syl φ1RP×˙X=P×˙X
140 137 139 eqtrd φ(P0)RP0×˙XR0×˙Y=P×˙X
141 140 adantr φi=0(P0)RP0×˙XR0×˙Y=P×˙X
142 124 141 eqtrd φi=0(Pi)RPi×˙XRi×˙Y=P×˙X
143 1 109 115 117 142 gsumsnd φRi0(Pi)RPi×˙XRi×˙Y=P×˙X
144 113 143 oveq12d φRi=1P1(Pi)RPi×˙XRi×˙Y+˙Ri0(Pi)RPi×˙XRi×˙Y=0R+˙P×˙X
145 1 2 103 grplid RGrpP×˙XB0R+˙P×˙X=P×˙X
146 30 117 145 syl2anc φ0R+˙P×˙X=P×˙X
147 81 144 146 3eqtrd φRi=0P1(Pi)RPi×˙XRi×˙Y=P×˙X
148 19 11 eqeltrd φP-1+10
149 50 3 mulgnn0cl mulGrpRMndP0YBP×˙YB
150 42 11 8 149 syl3anc φP×˙YB
151 simpr φi=P-1+1i=P-1+1
152 19 adantr φi=P-1+1P-1+1=P
153 151 152 eqtrd φi=P-1+1i=P
154 153 oveq2d φi=P-1+1(Pi)=(PP)
155 153 oveq2d φi=P-1+1Pi=PP
156 155 oveq1d φi=P-1+1Pi×˙X=PP×˙X
157 153 oveq1d φi=P-1+1i×˙Y=P×˙Y
158 156 157 oveq12d φi=P-1+1Pi×˙XRi×˙Y=PP×˙XRP×˙Y
159 154 158 oveq12d φi=P-1+1(Pi)RPi×˙XRi×˙Y=(PP)RPP×˙XRP×˙Y
160 bcnn P0(PP)=1
161 11 160 syl φ(PP)=1
162 17 subidd φPP=0
163 162 oveq1d φPP×˙X=0×˙X
164 50 130 3 mulg0 XB0×˙X=1R
165 7 164 syl φ0×˙X=1R
166 163 165 eqtrd φPP×˙X=1R
167 166 oveq1d φPP×˙XRP×˙Y=1RRP×˙Y
168 1 12 129 ringlidm RRingP×˙YB1RRP×˙Y=P×˙Y
169 39 150 168 syl2anc φ1RRP×˙Y=P×˙Y
170 167 169 eqtrd φPP×˙XRP×˙Y=P×˙Y
171 161 170 oveq12d φ(PP)RPP×˙XRP×˙Y=1RP×˙Y
172 1 13 mulg1 P×˙YB1RP×˙Y=P×˙Y
173 150 172 syl φ1RP×˙Y=P×˙Y
174 171 173 eqtrd φ(PP)RPP×˙XRP×˙Y=P×˙Y
175 174 adantr φi=P-1+1(PP)RPP×˙XRP×˙Y=P×˙Y
176 159 175 eqtrd φi=P-1+1(Pi)RPi×˙XRi×˙Y=P×˙Y
177 1 109 148 150 176 gsumsnd φRiP-1+1(Pi)RPi×˙XRi×˙Y=P×˙Y
178 147 177 oveq12d φRi=0P1(Pi)RPi×˙XRi×˙Y+˙RiP-1+1(Pi)RPi×˙XRi×˙Y=P×˙X+˙P×˙Y
179 62 178 eqtrd φRi=0P-1+1(Pi)RPi×˙XRi×˙Y=P×˙X+˙P×˙Y
180 16 23 179 3eqtrd φP×˙X+˙Y=P×˙X+˙P×˙Y