Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulp1mod1 Unicode version

Theorem mulp1mod1 9499
 Description: The product of an integer and an integer greater than 1 increased by 1 is 1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021.)
Assertion
Ref Expression
mulp1mod1

Proof of Theorem mulp1mod1
StepHypRef Expression
1 eluzelcn 8763 . . . . . . . . 9
21adantl 271 . . . . . . . 8
3 simpl 107 . . . . . . . . 9
43zcnd 8603 . . . . . . . 8
52, 4mulcomd 7254 . . . . . . 7
65oveq1d 5578 . . . . . 6
7 eluzelz 8761 . . . . . . . . 9
8 zq 8844 . . . . . . . . 9
97, 8syl 14 . . . . . . . 8
109adantl 271 . . . . . . 7
11 0red 7234 . . . . . . . 8
12 2re 8228 . . . . . . . . 9
1312a1i 9 . . . . . . . 8
147adantl 271 . . . . . . . . 9
1514zred 8602 . . . . . . . 8
16 2pos 8249 . . . . . . . . 9
1716a1i 9 . . . . . . . 8
18 eluzle 8764 . . . . . . . . 9
1918adantl 271 . . . . . . . 8
2011, 13, 15, 17, 19ltletrd 7646 . . . . . . 7
21 mulqmod0 9464 . . . . . . 7
223, 10, 20, 21syl3anc 1170 . . . . . 6
236, 22eqtrd 2115 . . . . 5
2423oveq1d 5578 . . . 4
25 0p1e1 8272 . . . 4
2624, 25syl6eq 2131 . . 3
2726oveq1d 5578 . 2
28 zq 8844 . . . . 5
293, 28syl 14 . . . 4
30 qmulcl 8855 . . . 4
3110, 29, 30syl2anc 403 . . 3
32 1z 8510 . . . 4
33 zq 8844 . . . 4
3432, 33mp1i 10 . . 3
35 modqaddmod 9497 . . 3
3631, 34, 10, 20, 35syl22anc 1171 . 2
37 eluz2gt1 8822 . . . 4