Metamath Proof Explorer


Theorem modprm0

Description: For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018)

Ref Expression
Assertion modprm0 ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 )

Proof

Step Hyp Ref Expression
1 reumodprminv โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ! ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 )
2 reurex โŠข ( โˆƒ! ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 โ†’ โˆƒ ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 )
3 prmz โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค )
4 3 3ad2ant1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„ค )
5 4 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ƒ โˆˆ โ„ค )
6 elfzelz โŠข ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ๐‘Ÿ โˆˆ โ„ค )
7 6 adantr โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โ†’ ๐‘Ÿ โˆˆ โ„ค )
8 elfzoelz โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ๐ผ โˆˆ โ„ค )
9 8 3ad2ant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐ผ โˆˆ โ„ค )
10 zmulcl โŠข ( ( ๐‘Ÿ โˆˆ โ„ค โˆง ๐ผ โˆˆ โ„ค ) โ†’ ( ๐‘Ÿ ยท ๐ผ ) โˆˆ โ„ค )
11 7 9 10 syl2an โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘Ÿ ยท ๐ผ ) โˆˆ โ„ค )
12 5 11 zsubcld โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) โˆˆ โ„ค )
13 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
14 13 3ad2ant1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
15 14 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
16 zmodfzo โŠข ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) โ†’ ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โˆˆ ( 0 ..^ ๐‘ƒ ) )
17 12 15 16 syl2anc โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โˆˆ ( 0 ..^ ๐‘ƒ ) )
18 8 zred โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ๐ผ โˆˆ โ„ )
19 18 3ad2ant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐ผ โˆˆ โ„ )
20 19 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐ผ โˆˆ โ„ )
21 13 nnred โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ )
22 21 3ad2ant1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„ )
23 22 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ƒ โˆˆ โ„ )
24 6 zred โŠข ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ๐‘Ÿ โˆˆ โ„ )
25 24 adantr โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โ†’ ๐‘Ÿ โˆˆ โ„ )
26 remulcl โŠข ( ( ๐‘Ÿ โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ ) โ†’ ( ๐‘Ÿ ยท ๐ผ ) โˆˆ โ„ )
27 25 19 26 syl2an โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘Ÿ ยท ๐ผ ) โˆˆ โ„ )
28 23 27 resubcld โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) โˆˆ โ„ )
29 elfzoelz โŠข ( ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ๐‘ โˆˆ โ„ค )
30 29 3ad2ant2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ โˆˆ โ„ค )
31 30 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ โˆˆ โ„ค )
32 13 nnrpd โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„+ )
33 32 3ad2ant1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„+ )
34 33 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ƒ โˆˆ โ„+ )
35 modaddmulmod โŠข ( ( ( ๐ผ โˆˆ โ„ โˆง ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ค ) โˆง ๐‘ƒ โˆˆ โ„+ ) โ†’ ( ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) ยท ๐‘ ) ) mod ๐‘ƒ ) )
36 20 28 31 34 35 syl31anc โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) ยท ๐‘ ) ) mod ๐‘ƒ ) )
37 13 nncnd โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„‚ )
38 37 3ad2ant1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
39 38 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
40 6 zcnd โŠข ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โ†’ ๐‘Ÿ โˆˆ โ„‚ )
41 40 adantr โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โ†’ ๐‘Ÿ โˆˆ โ„‚ )
42 8 zcnd โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ๐ผ โˆˆ โ„‚ )
43 42 3ad2ant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐ผ โˆˆ โ„‚ )
44 mulcl โŠข ( ( ๐‘Ÿ โˆˆ โ„‚ โˆง ๐ผ โˆˆ โ„‚ ) โ†’ ( ๐‘Ÿ ยท ๐ผ ) โˆˆ โ„‚ )
45 41 43 44 syl2an โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘Ÿ ยท ๐ผ ) โˆˆ โ„‚ )
46 29 zcnd โŠข ( ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ๐‘ โˆˆ โ„‚ )
47 46 3ad2ant2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ โˆˆ โ„‚ )
48 47 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ โˆˆ โ„‚ )
49 39 45 48 subdird โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) ยท ๐‘ ) = ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) )
50 49 oveq2d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐ผ + ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) ยท ๐‘ ) ) = ( ๐ผ + ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) ) )
51 50 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) ยท ๐‘ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) ) mod ๐‘ƒ ) )
52 mulcom โŠข ( ( ๐‘ƒ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ ) โ†’ ( ๐‘ƒ ยท ๐‘ ) = ( ๐‘ ยท ๐‘ƒ ) )
53 37 46 52 syl2an โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ๐‘ƒ ยท ๐‘ ) = ( ๐‘ ยท ๐‘ƒ ) )
54 53 oveq1d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) = ( ( ๐‘ ยท ๐‘ƒ ) mod ๐‘ƒ ) )
55 mulmod0 โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„+ ) โ†’ ( ( ๐‘ ยท ๐‘ƒ ) mod ๐‘ƒ ) = 0 )
56 29 32 55 syl2anr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘ ยท ๐‘ƒ ) mod ๐‘ƒ ) = 0 )
57 54 56 eqtrd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) = 0 )
58 57 3adant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) = 0 )
59 58 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) = 0 )
60 41 adantr โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘Ÿ โˆˆ โ„‚ )
61 43 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐ผ โˆˆ โ„‚ )
62 60 61 48 mul32d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) = ( ( ๐‘Ÿ ยท ๐‘ ) ยท ๐ผ ) )
63 62 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) mod ๐‘ƒ ) = ( ( ( ๐‘Ÿ ยท ๐‘ ) ยท ๐ผ ) mod ๐‘ƒ ) )
64 29 zred โŠข ( ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ๐‘ โˆˆ โ„ )
65 64 3ad2ant2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ โˆˆ โ„ )
66 remulcl โŠข ( ( ๐‘Ÿ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ ) โ†’ ( ๐‘Ÿ ยท ๐‘ ) โˆˆ โ„ )
67 25 65 66 syl2an โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘Ÿ ยท ๐‘ ) โˆˆ โ„ )
68 9 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐ผ โˆˆ โ„ค )
69 modmulmod โŠข ( ( ( ๐‘Ÿ ยท ๐‘ ) โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„+ ) โ†’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) = ( ( ( ๐‘Ÿ ยท ๐‘ ) ยท ๐ผ ) mod ๐‘ƒ ) )
70 67 68 34 69 syl3anc โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) = ( ( ( ๐‘Ÿ ยท ๐‘ ) ยท ๐ผ ) mod ๐‘ƒ ) )
71 63 70 eqtr4d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) mod ๐‘ƒ ) = ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) )
72 59 71 oveq12d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) โˆ’ ( ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) mod ๐‘ƒ ) ) = ( 0 โˆ’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) ) )
73 72 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) โˆ’ ( ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( 0 โˆ’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) )
74 remulcl โŠข ( ( ๐‘ƒ โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ ) โ†’ ( ๐‘ƒ ยท ๐‘ ) โˆˆ โ„ )
75 21 64 74 syl2an โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ๐‘ƒ ยท ๐‘ ) โˆˆ โ„ )
76 75 3adant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ๐‘ƒ ยท ๐‘ ) โˆˆ โ„ )
77 76 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘ƒ ยท ๐‘ ) โˆˆ โ„ )
78 65 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ๐‘ โˆˆ โ„ )
79 27 78 remulcld โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) โˆˆ โ„ )
80 modsubmodmod โŠข ( ( ( ๐‘ƒ ยท ๐‘ ) โˆˆ โ„ โˆง ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โ†’ ( ( ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) โˆ’ ( ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) )
81 77 79 34 80 syl3anc โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ( ๐‘ƒ ยท ๐‘ ) mod ๐‘ƒ ) โˆ’ ( ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) )
82 mulcom โŠข ( ( ๐‘ โˆˆ โ„‚ โˆง ๐‘Ÿ โˆˆ โ„‚ ) โ†’ ( ๐‘ ยท ๐‘Ÿ ) = ( ๐‘Ÿ ยท ๐‘ ) )
83 47 40 82 syl2anr โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐‘ ยท ๐‘Ÿ ) = ( ๐‘Ÿ ยท ๐‘ ) )
84 83 oveq1d โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) )
85 84 eqeq1d โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 โ†” ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) = 1 ) )
86 85 biimpd โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 โ†’ ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) = 1 ) )
87 86 impancom โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) = 1 ) )
88 87 imp โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) = 1 )
89 88 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) = ( 1 ยท ๐ผ ) )
90 89 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) = ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) )
91 90 oveq2d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( 0 โˆ’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) ) = ( 0 โˆ’ ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) ) )
92 91 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( 0 โˆ’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( 0 โˆ’ ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) )
93 61 mullidd โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( 1 ยท ๐ผ ) = ๐ผ )
94 93 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) = ( ๐ผ mod ๐‘ƒ ) )
95 32 18 anim12ci โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) )
96 elfzo2 โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†” ( ๐ผ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โˆง ๐‘ƒ โˆˆ โ„ค โˆง ๐ผ < ๐‘ƒ ) )
97 eluz2 โŠข ( ๐ผ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โ†” ( 1 โˆˆ โ„ค โˆง ๐ผ โˆˆ โ„ค โˆง 1 โ‰ค ๐ผ ) )
98 0red โŠข ( ๐ผ โˆˆ โ„ค โ†’ 0 โˆˆ โ„ )
99 1red โŠข ( ๐ผ โˆˆ โ„ค โ†’ 1 โˆˆ โ„ )
100 zre โŠข ( ๐ผ โˆˆ โ„ค โ†’ ๐ผ โˆˆ โ„ )
101 98 99 100 3jca โŠข ( ๐ผ โˆˆ โ„ค โ†’ ( 0 โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ ) )
102 101 adantr โŠข ( ( ๐ผ โˆˆ โ„ค โˆง 1 โ‰ค ๐ผ ) โ†’ ( 0 โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ ) )
103 0le1 โŠข 0 โ‰ค 1
104 103 a1i โŠข ( ๐ผ โˆˆ โ„ค โ†’ 0 โ‰ค 1 )
105 104 anim1i โŠข ( ( ๐ผ โˆˆ โ„ค โˆง 1 โ‰ค ๐ผ ) โ†’ ( 0 โ‰ค 1 โˆง 1 โ‰ค ๐ผ ) )
106 letr โŠข ( ( 0 โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ ) โ†’ ( ( 0 โ‰ค 1 โˆง 1 โ‰ค ๐ผ ) โ†’ 0 โ‰ค ๐ผ ) )
107 102 105 106 sylc โŠข ( ( ๐ผ โˆˆ โ„ค โˆง 1 โ‰ค ๐ผ ) โ†’ 0 โ‰ค ๐ผ )
108 107 3adant1 โŠข ( ( 1 โˆˆ โ„ค โˆง ๐ผ โˆˆ โ„ค โˆง 1 โ‰ค ๐ผ ) โ†’ 0 โ‰ค ๐ผ )
109 97 108 sylbi โŠข ( ๐ผ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โ†’ 0 โ‰ค ๐ผ )
110 109 3ad2ant1 โŠข ( ( ๐ผ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โˆง ๐‘ƒ โˆˆ โ„ค โˆง ๐ผ < ๐‘ƒ ) โ†’ 0 โ‰ค ๐ผ )
111 simp3 โŠข ( ( ๐ผ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โˆง ๐‘ƒ โˆˆ โ„ค โˆง ๐ผ < ๐‘ƒ ) โ†’ ๐ผ < ๐‘ƒ )
112 110 111 jca โŠข ( ( ๐ผ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โˆง ๐‘ƒ โˆˆ โ„ค โˆง ๐ผ < ๐‘ƒ ) โ†’ ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) )
113 96 112 sylbi โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) )
114 113 adantl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) )
115 95 114 jca โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) ) )
116 115 3adant2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) ) )
117 116 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) ) )
118 modid โŠข ( ( ( ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โˆง ( 0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ ) ) โ†’ ( ๐ผ mod ๐‘ƒ ) = ๐ผ )
119 117 118 syl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐ผ mod ๐‘ƒ ) = ๐ผ )
120 94 119 eqtrd โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) = ๐ผ )
121 120 oveq2d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( 0 โˆ’ ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) ) = ( 0 โˆ’ ๐ผ ) )
122 121 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( 0 โˆ’ ( ( 1 ยท ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) )
123 92 122 eqtrd โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( 0 โˆ’ ( ( ( ( ๐‘Ÿ ยท ๐‘ ) mod ๐‘ƒ ) ยท ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) )
124 73 81 123 3eqtr3d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) = ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) )
125 124 oveq2d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐ผ + ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) ) = ( ๐ผ + ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) ) )
126 125 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) )
127 77 79 resubcld โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) โˆˆ โ„ )
128 modadd2mod โŠข ( ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โ†’ ( ( ๐ผ + ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) ) mod ๐‘ƒ ) )
129 127 20 34 128 syl3anc โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) ) mod ๐‘ƒ ) )
130 0red โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ 0 โˆˆ โ„ )
131 130 18 resubcld โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ( 0 โˆ’ ๐ผ ) โˆˆ โ„ )
132 131 adantl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( 0 โˆ’ ๐ผ ) โˆˆ โ„ )
133 18 adantl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐ผ โˆˆ โ„ )
134 32 adantr โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„+ )
135 132 133 134 3jca โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( 0 โˆ’ ๐ผ ) โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) )
136 135 3adant2 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( 0 โˆ’ ๐ผ ) โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) )
137 136 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( 0 โˆ’ ๐ผ ) โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) )
138 modadd2mod โŠข ( ( ( 0 โˆ’ ๐ผ ) โˆˆ โ„ โˆง ๐ผ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+ ) โ†’ ( ( ๐ผ + ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( 0 โˆ’ ๐ผ ) ) mod ๐‘ƒ ) )
139 137 138 syl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( 0 โˆ’ ๐ผ ) ) mod ๐‘ƒ ) )
140 0cnd โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ 0 โˆˆ โ„‚ )
141 42 140 pncan3d โŠข ( ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) โ†’ ( ๐ผ + ( 0 โˆ’ ๐ผ ) ) = 0 )
142 141 3ad2ant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ๐ผ + ( 0 โˆ’ ๐ผ ) ) = 0 )
143 142 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ๐ผ + ( 0 โˆ’ ๐ผ ) ) = 0 )
144 143 oveq1d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( 0 โˆ’ ๐ผ ) ) mod ๐‘ƒ ) = ( 0 mod ๐‘ƒ ) )
145 0mod โŠข ( ๐‘ƒ โˆˆ โ„+ โ†’ ( 0 mod ๐‘ƒ ) = 0 )
146 32 145 syl โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ( 0 mod ๐‘ƒ ) = 0 )
147 146 3ad2ant1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( 0 mod ๐‘ƒ ) = 0 )
148 147 adantl โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( 0 mod ๐‘ƒ ) = 0 )
149 139 144 148 3eqtrd โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( 0 โˆ’ ๐ผ ) mod ๐‘ƒ ) ) mod ๐‘ƒ ) = 0 )
150 126 129 149 3eqtr3d โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( ๐‘ƒ ยท ๐‘ ) โˆ’ ( ( ๐‘Ÿ ยท ๐ผ ) ยท ๐‘ ) ) ) mod ๐‘ƒ ) = 0 )
151 36 51 150 3eqtrd โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ ( ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 )
152 oveq1 โŠข ( ๐‘— = ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โ†’ ( ๐‘— ยท ๐‘ ) = ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) )
153 152 oveq2d โŠข ( ๐‘— = ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โ†’ ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) = ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) )
154 153 oveq1d โŠข ( ๐‘— = ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โ†’ ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = ( ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) mod ๐‘ƒ ) )
155 154 eqeq1d โŠข ( ๐‘— = ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โ†’ ( ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 โ†” ( ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 ) )
156 155 rspcev โŠข ( ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) โˆˆ ( 0 ..^ ๐‘ƒ ) โˆง ( ( ๐ผ + ( ( ( ๐‘ƒ โˆ’ ( ๐‘Ÿ ยท ๐ผ ) ) mod ๐‘ƒ ) ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 )
157 17 151 156 syl2anc โŠข ( ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โˆง ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 )
158 157 ex โŠข ( ( ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) โˆง ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 ) โ†’ ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 ) )
159 158 rexlimiva โŠข ( โˆƒ ๐‘Ÿ โˆˆ ( 1 ... ( ๐‘ƒ โˆ’ 1 ) ) ( ( ๐‘ ยท ๐‘Ÿ ) mod ๐‘ƒ ) = 1 โ†’ ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 ) )
160 1 2 159 3syl โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 ) )
161 160 3adant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 ) )
162 161 pm2.43i โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ ( 1 ..^ ๐‘ƒ ) โˆง ๐ผ โˆˆ ( 1 ..^ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘— โˆˆ ( 0 ..^ ๐‘ƒ ) ( ( ๐ผ + ( ๐‘— ยท ๐‘ ) ) mod ๐‘ƒ ) = 0 )