-theorem mod_times: ∀n,m,p:nat. O < p →
- n*m ≅_{p} (n \mod p)*(m \mod p).
-#n #m #p #posp @(eq_times_plus_to_congruent ?? p
- ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
-@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
- [@eq_f2 //
- |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
- (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
- >distributive_times_plus >distributive_times_plus_r
- >distributive_times_plus_r <associative_plus @eq_f2 //
+theorem mod_times: ∀n,m,p:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 p →
+ n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6m \ 5a title="congruent" href="cic:/fakeuri.def(1)"\ 6≅\ 5/a\ 6_{p} (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p).
+#n #m #p #posp @(\ 5a href="cic:/matita/arithmetics/congruence/eq_times_plus_to_congruent.def(14)"\ 6eq_times_plus_to_congruent\ 5/a\ 6 ?? p
+ ((n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p))) //
+@(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ?? (((n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))))
+ [@\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 //
+ |@(\ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6 ? ? (((n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n\ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6
+ (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6((m \ 5a title="natural divide" href="cic:/fakeuri.def(1)"\ 6/\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6p) \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 (n \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p)\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(m \ 5a title="natural remainder" href="cic:/fakeuri.def(1)"\ 6\mod\ 5/a\ 6 p))) //
+ >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"\ 6distributive_times_plus\ 5/a\ 6 >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6
+ >\ 5a href="cic:/matita/arithmetics/nat/distributive_times_plus_r.def(9)"\ 6distributive_times_plus_r\ 5/a\ 6 <\ 5a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"\ 6associative_plus\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"\ 6eq_f2\ 5/a\ 6 //