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

Theorem modprm0 12256
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.)
Assertion
Ref Expression
modprm0 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0)
Distinct variable groups:   ๐‘—,๐ผ   ๐‘—,๐‘   ๐‘ƒ,๐‘—

Proof of Theorem modprm0
Dummy variable ๐‘Ÿ is distinct from all other variables.
StepHypRef Expression
1 reumodprminv 12255 . . . 4 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ!๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1))((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1)
2 reurex 2691 . . . 4 (โˆƒ!๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1))((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1 โ†’ โˆƒ๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1))((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1)
3 prmz 12113 . . . . . . . . . . 11 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
433ad2ant1 1018 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ƒ โˆˆ โ„ค)
54adantl 277 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„ค)
6 elfzelz 10027 . . . . . . . . . . 11 (๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†’ ๐‘Ÿ โˆˆ โ„ค)
76adantr 276 . . . . . . . . . 10 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โ†’ ๐‘Ÿ โˆˆ โ„ค)
8 elfzoelz 10149 . . . . . . . . . . 11 (๐ผ โˆˆ (1..^๐‘ƒ) โ†’ ๐ผ โˆˆ โ„ค)
983ad2ant3 1020 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐ผ โˆˆ โ„ค)
10 zmulcl 9308 . . . . . . . . . 10 ((๐‘Ÿ โˆˆ โ„ค โˆง ๐ผ โˆˆ โ„ค) โ†’ (๐‘Ÿ ยท ๐ผ) โˆˆ โ„ค)
117, 9, 10syl2an 289 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘Ÿ ยท ๐ผ) โˆˆ โ„ค)
125, 11zsubcld 9382 . . . . . . . 8 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) โˆˆ โ„ค)
13 prmnn 12112 . . . . . . . . . 10 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
14133ad2ant1 1018 . . . . . . . . 9 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ƒ โˆˆ โ„•)
1514adantl 277 . . . . . . . 8 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„•)
16 zmodfzo 10349 . . . . . . . 8 (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„•) โ†’ ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โˆˆ (0..^๐‘ƒ))
1712, 15, 16syl2anc 411 . . . . . . 7 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โˆˆ (0..^๐‘ƒ))
189adantl 277 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐ผ โˆˆ โ„ค)
19 zq 9628 . . . . . . . . . 10 (๐ผ โˆˆ โ„ค โ†’ ๐ผ โˆˆ โ„š)
2018, 19syl 14 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐ผ โˆˆ โ„š)
21 zq 9628 . . . . . . . . . 10 ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) โˆˆ โ„ค โ†’ (๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) โˆˆ โ„š)
2212, 21syl 14 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) โˆˆ โ„š)
23 elfzoelz 10149 . . . . . . . . . . 11 (๐‘ โˆˆ (1..^๐‘ƒ) โ†’ ๐‘ โˆˆ โ„ค)
24233ad2ant2 1019 . . . . . . . . . 10 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ โˆˆ โ„ค)
2524adantl 277 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ โˆˆ โ„ค)
26 zq 9628 . . . . . . . . . 10 (๐‘ƒ โˆˆ โ„ค โ†’ ๐‘ƒ โˆˆ โ„š)
275, 26syl 14 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„š)
2815nngt0d 8965 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ 0 < ๐‘ƒ)
29 modqaddmulmod 10393 . . . . . . . . 9 (((๐ผ โˆˆ โ„š โˆง (๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) โˆˆ โ„š โˆง ๐‘ โˆˆ โ„ค) โˆง (๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ)) โ†’ ((๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)) mod ๐‘ƒ) = ((๐ผ + ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) ยท ๐‘)) mod ๐‘ƒ))
3020, 22, 25, 27, 28, 29syl32anc 1246 . . . . . . . 8 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)) mod ๐‘ƒ) = ((๐ผ + ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) ยท ๐‘)) mod ๐‘ƒ))
3113nncnd 8935 . . . . . . . . . . . . 13 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„‚)
32313ad2ant1 1018 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ƒ โˆˆ โ„‚)
3332adantl 277 . . . . . . . . . . 11 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„‚)
346zcnd 9378 . . . . . . . . . . . . 13 (๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†’ ๐‘Ÿ โˆˆ โ„‚)
3534adantr 276 . . . . . . . . . . . 12 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โ†’ ๐‘Ÿ โˆˆ โ„‚)
368zcnd 9378 . . . . . . . . . . . . 13 (๐ผ โˆˆ (1..^๐‘ƒ) โ†’ ๐ผ โˆˆ โ„‚)
37363ad2ant3 1020 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐ผ โˆˆ โ„‚)
38 mulcl 7940 . . . . . . . . . . . 12 ((๐‘Ÿ โˆˆ โ„‚ โˆง ๐ผ โˆˆ โ„‚) โ†’ (๐‘Ÿ ยท ๐ผ) โˆˆ โ„‚)
3935, 37, 38syl2an 289 . . . . . . . . . . 11 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘Ÿ ยท ๐ผ) โˆˆ โ„‚)
4023zcnd 9378 . . . . . . . . . . . . 13 (๐‘ โˆˆ (1..^๐‘ƒ) โ†’ ๐‘ โˆˆ โ„‚)
41403ad2ant2 1019 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ โˆˆ โ„‚)
4241adantl 277 . . . . . . . . . . 11 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ โˆˆ โ„‚)
4333, 39, 42subdird 8374 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) ยท ๐‘) = ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)))
4443oveq2d 5893 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐ผ + ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) ยท ๐‘)) = (๐ผ + ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘))))
4544oveq1d 5892 . . . . . . . 8 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) ยท ๐‘)) mod ๐‘ƒ) = ((๐ผ + ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘))) mod ๐‘ƒ))
46 mulcom 7942 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (๐‘ƒ ยท ๐‘) = (๐‘ ยท ๐‘ƒ))
4731, 40, 46syl2an 289 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ (๐‘ƒ ยท ๐‘) = (๐‘ ยท ๐‘ƒ))
4847oveq1d 5892 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) = ((๐‘ ยท ๐‘ƒ) mod ๐‘ƒ))
4923adantl 277 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ โˆˆ โ„ค)
503adantr 276 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ƒ โˆˆ โ„ค)
5150, 26syl 14 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ƒ โˆˆ โ„š)
5213nngt0d 8965 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ โ„™ โ†’ 0 < ๐‘ƒ)
5352adantr 276 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ 0 < ๐‘ƒ)
54 mulqmod0 10332 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ) โ†’ ((๐‘ ยท ๐‘ƒ) mod ๐‘ƒ) = 0)
5549, 51, 53, 54syl3anc 1238 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘ ยท ๐‘ƒ) mod ๐‘ƒ) = 0)
5648, 55eqtrd 2210 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) = 0)
57563adant3 1017 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) = 0)
5857adantl 277 . . . . . . . . . . . . . 14 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) = 0)
5935adantr 276 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘Ÿ โˆˆ โ„‚)
6037adantl 277 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐ผ โˆˆ โ„‚)
6159, 60, 42mul32d 8112 . . . . . . . . . . . . . . . 16 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘) = ((๐‘Ÿ ยท ๐‘) ยท ๐ผ))
6261oveq1d 5892 . . . . . . . . . . . . . . 15 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) mod ๐‘ƒ) = (((๐‘Ÿ ยท ๐‘) ยท ๐ผ) mod ๐‘ƒ))
63 elfznn 10056 . . . . . . . . . . . . . . . . . . . 20 (๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†’ ๐‘Ÿ โˆˆ โ„•)
6463adantr 276 . . . . . . . . . . . . . . . . . . 19 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โ†’ ๐‘Ÿ โˆˆ โ„•)
6564adantr 276 . . . . . . . . . . . . . . . . . 18 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘Ÿ โˆˆ โ„•)
66 elfzo1 10192 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ โˆˆ (1..^๐‘ƒ) โ†” (๐‘ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„• โˆง ๐‘ < ๐‘ƒ))
6766simp1bi 1012 . . . . . . . . . . . . . . . . . . . 20 (๐‘ โˆˆ (1..^๐‘ƒ) โ†’ ๐‘ โˆˆ โ„•)
68673ad2ant2 1019 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐‘ โˆˆ โ„•)
6968adantl 277 . . . . . . . . . . . . . . . . . 18 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐‘ โˆˆ โ„•)
7065, 69nnmulcld 8970 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘Ÿ ยท ๐‘) โˆˆ โ„•)
71 nnq 9635 . . . . . . . . . . . . . . . . 17 ((๐‘Ÿ ยท ๐‘) โˆˆ โ„• โ†’ (๐‘Ÿ ยท ๐‘) โˆˆ โ„š)
7270, 71syl 14 . . . . . . . . . . . . . . . 16 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘Ÿ ยท ๐‘) โˆˆ โ„š)
73 modqmulmod 10391 . . . . . . . . . . . . . . . 16 ((((๐‘Ÿ ยท ๐‘) โˆˆ โ„š โˆง ๐ผ โˆˆ โ„ค) โˆง (๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ)) โ†’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ) = (((๐‘Ÿ ยท ๐‘) ยท ๐ผ) mod ๐‘ƒ))
7472, 18, 27, 28, 73syl22anc 1239 . . . . . . . . . . . . . . 15 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ) = (((๐‘Ÿ ยท ๐‘) ยท ๐ผ) mod ๐‘ƒ))
7562, 74eqtr4d 2213 . . . . . . . . . . . . . 14 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) mod ๐‘ƒ) = ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ))
7658, 75oveq12d 5895 . . . . . . . . . . . . 13 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) โˆ’ (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) mod ๐‘ƒ)) = (0 โˆ’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ)))
7776oveq1d 5892 . . . . . . . . . . . 12 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) โˆ’ (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) mod ๐‘ƒ)) mod ๐‘ƒ) = ((0 โˆ’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ))
7815, 69nnmulcld 8970 . . . . . . . . . . . . . 14 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘ƒ ยท ๐‘) โˆˆ โ„•)
79 nnq 9635 . . . . . . . . . . . . . 14 ((๐‘ƒ ยท ๐‘) โˆˆ โ„• โ†’ (๐‘ƒ ยท ๐‘) โˆˆ โ„š)
8078, 79syl 14 . . . . . . . . . . . . 13 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘ƒ ยท ๐‘) โˆˆ โ„š)
81 elfzo1 10192 . . . . . . . . . . . . . . . . . . 19 (๐ผ โˆˆ (1..^๐‘ƒ) โ†” (๐ผ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„• โˆง ๐ผ < ๐‘ƒ))
8281simp1bi 1012 . . . . . . . . . . . . . . . . . 18 (๐ผ โˆˆ (1..^๐‘ƒ) โ†’ ๐ผ โˆˆ โ„•)
83823ad2ant3 1020 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐ผ โˆˆ โ„•)
8483adantl 277 . . . . . . . . . . . . . . . 16 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐ผ โˆˆ โ„•)
8565, 84nnmulcld 8970 . . . . . . . . . . . . . . 15 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘Ÿ ยท ๐ผ) โˆˆ โ„•)
8685, 69nnmulcld 8970 . . . . . . . . . . . . . 14 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘) โˆˆ โ„•)
87 nnq 9635 . . . . . . . . . . . . . 14 (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) โˆˆ โ„• โ†’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘) โˆˆ โ„š)
8886, 87syl 14 . . . . . . . . . . . . 13 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘) โˆˆ โ„š)
89 modqsubmodmod 10385 . . . . . . . . . . . . 13 ((((๐‘ƒ ยท ๐‘) โˆˆ โ„š โˆง ((๐‘Ÿ ยท ๐ผ) ยท ๐‘) โˆˆ โ„š) โˆง (๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ)) โ†’ ((((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) โˆ’ (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) mod ๐‘ƒ)) mod ๐‘ƒ) = (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ))
9080, 88, 27, 28, 89syl22anc 1239 . . . . . . . . . . . 12 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((((๐‘ƒ ยท ๐‘) mod ๐‘ƒ) โˆ’ (((๐‘Ÿ ยท ๐ผ) ยท ๐‘) mod ๐‘ƒ)) mod ๐‘ƒ) = (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ))
91 mulcom 7942 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ โˆˆ โ„‚ โˆง ๐‘Ÿ โˆˆ โ„‚) โ†’ (๐‘ ยท ๐‘Ÿ) = (๐‘Ÿ ยท ๐‘))
9241, 34, 91syl2anr 290 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐‘ ยท ๐‘Ÿ) = (๐‘Ÿ ยท ๐‘))
9392oveq1d 5892 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = ((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ))
9493eqeq1d 2186 . . . . . . . . . . . . . . . . . . . 20 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1 โ†” ((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) = 1))
9594biimpd 144 . . . . . . . . . . . . . . . . . . 19 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1 โ†’ ((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) = 1))
9695impancom 260 . . . . . . . . . . . . . . . . . 18 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โ†’ ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) = 1))
9796imp 124 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) = 1)
9897oveq1d 5892 . . . . . . . . . . . . . . . 16 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) = (1 ยท ๐ผ))
9998oveq1d 5892 . . . . . . . . . . . . . . 15 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ) = ((1 ยท ๐ผ) mod ๐‘ƒ))
10099oveq2d 5893 . . . . . . . . . . . . . 14 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (0 โˆ’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ)) = (0 โˆ’ ((1 ยท ๐ผ) mod ๐‘ƒ)))
101100oveq1d 5892 . . . . . . . . . . . . 13 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((0 โˆ’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ) = ((0 โˆ’ ((1 ยท ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ))
10260mulid2d 7978 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (1 ยท ๐ผ) = ๐ผ)
103102oveq1d 5892 . . . . . . . . . . . . . . . 16 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((1 ยท ๐ผ) mod ๐‘ƒ) = (๐ผ mod ๐‘ƒ))
10484nnnn0d 9231 . . . . . . . . . . . . . . . . . 18 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐ผ โˆˆ โ„•0)
105104nn0ge0d 9234 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ 0 โ‰ค ๐ผ)
106 elfzolt2 10158 . . . . . . . . . . . . . . . . . . 19 (๐ผ โˆˆ (1..^๐‘ƒ) โ†’ ๐ผ < ๐‘ƒ)
1071063ad2ant3 1020 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ๐ผ < ๐‘ƒ)
108107adantl 277 . . . . . . . . . . . . . . . . 17 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ๐ผ < ๐‘ƒ)
109 modqid 10351 . . . . . . . . . . . . . . . . 17 (((๐ผ โˆˆ โ„š โˆง ๐‘ƒ โˆˆ โ„š) โˆง (0 โ‰ค ๐ผ โˆง ๐ผ < ๐‘ƒ)) โ†’ (๐ผ mod ๐‘ƒ) = ๐ผ)
11020, 27, 105, 108, 109syl22anc 1239 . . . . . . . . . . . . . . . 16 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐ผ mod ๐‘ƒ) = ๐ผ)
111103, 110eqtrd 2210 . . . . . . . . . . . . . . 15 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((1 ยท ๐ผ) mod ๐‘ƒ) = ๐ผ)
112111oveq2d 5893 . . . . . . . . . . . . . 14 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (0 โˆ’ ((1 ยท ๐ผ) mod ๐‘ƒ)) = (0 โˆ’ ๐ผ))
113112oveq1d 5892 . . . . . . . . . . . . 13 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((0 โˆ’ ((1 ยท ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ) = ((0 โˆ’ ๐ผ) mod ๐‘ƒ))
114101, 113eqtrd 2210 . . . . . . . . . . . 12 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((0 โˆ’ ((((๐‘Ÿ ยท ๐‘) mod ๐‘ƒ) ยท ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ) = ((0 โˆ’ ๐ผ) mod ๐‘ƒ))
11577, 90, 1143eqtr3d 2218 . . . . . . . . . . 11 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ) = ((0 โˆ’ ๐ผ) mod ๐‘ƒ))
116115oveq2d 5893 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐ผ + (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ)) = (๐ผ + ((0 โˆ’ ๐ผ) mod ๐‘ƒ)))
117116oveq1d 5892 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ)) mod ๐‘ƒ) = ((๐ผ + ((0 โˆ’ ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ))
118 qsubcl 9640 . . . . . . . . . . 11 (((๐‘ƒ ยท ๐‘) โˆˆ โ„š โˆง ((๐‘Ÿ ยท ๐ผ) ยท ๐‘) โˆˆ โ„š) โ†’ ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) โˆˆ โ„š)
11980, 88, 118syl2anc 411 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) โˆˆ โ„š)
120 modqadd2mod 10376 . . . . . . . . . 10 (((((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) โˆˆ โ„š โˆง ๐ผ โˆˆ โ„š) โˆง (๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ)) โ†’ ((๐ผ + (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ)) mod ๐‘ƒ) = ((๐ผ + ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘))) mod ๐‘ƒ))
121119, 20, 27, 28, 120syl22anc 1239 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + (((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘)) mod ๐‘ƒ)) mod ๐‘ƒ) = ((๐ผ + ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘))) mod ๐‘ƒ))
122 0zd 9267 . . . . . . . . . . . . 13 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ 0 โˆˆ โ„ค)
123122, 18zsubcld 9382 . . . . . . . . . . . 12 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (0 โˆ’ ๐ผ) โˆˆ โ„ค)
124 zq 9628 . . . . . . . . . . . 12 ((0 โˆ’ ๐ผ) โˆˆ โ„ค โ†’ (0 โˆ’ ๐ผ) โˆˆ โ„š)
125123, 124syl 14 . . . . . . . . . . 11 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (0 โˆ’ ๐ผ) โˆˆ โ„š)
126 modqadd2mod 10376 . . . . . . . . . . 11 ((((0 โˆ’ ๐ผ) โˆˆ โ„š โˆง ๐ผ โˆˆ โ„š) โˆง (๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ)) โ†’ ((๐ผ + ((0 โˆ’ ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ) = ((๐ผ + (0 โˆ’ ๐ผ)) mod ๐‘ƒ))
127125, 20, 27, 28, 126syl22anc 1239 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + ((0 โˆ’ ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ) = ((๐ผ + (0 โˆ’ ๐ผ)) mod ๐‘ƒ))
128 0cnd 7952 . . . . . . . . . . . . . 14 (๐ผ โˆˆ (1..^๐‘ƒ) โ†’ 0 โˆˆ โ„‚)
12936, 128pncan3d 8273 . . . . . . . . . . . . 13 (๐ผ โˆˆ (1..^๐‘ƒ) โ†’ (๐ผ + (0 โˆ’ ๐ผ)) = 0)
1301293ad2ant3 1020 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ (๐ผ + (0 โˆ’ ๐ผ)) = 0)
131130adantl 277 . . . . . . . . . . 11 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (๐ผ + (0 โˆ’ ๐ผ)) = 0)
132131oveq1d 5892 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + (0 โˆ’ ๐ผ)) mod ๐‘ƒ) = (0 mod ๐‘ƒ))
1333, 26syl 14 . . . . . . . . . . . . 13 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„š)
134 q0mod 10357 . . . . . . . . . . . . 13 ((๐‘ƒ โˆˆ โ„š โˆง 0 < ๐‘ƒ) โ†’ (0 mod ๐‘ƒ) = 0)
135133, 52, 134syl2anc 411 . . . . . . . . . . . 12 (๐‘ƒ โˆˆ โ„™ โ†’ (0 mod ๐‘ƒ) = 0)
1361353ad2ant1 1018 . . . . . . . . . . 11 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ (0 mod ๐‘ƒ) = 0)
137136adantl 277 . . . . . . . . . 10 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ (0 mod ๐‘ƒ) = 0)
138127, 132, 1373eqtrd 2214 . . . . . . . . 9 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + ((0 โˆ’ ๐ผ) mod ๐‘ƒ)) mod ๐‘ƒ) = 0)
139117, 121, 1383eqtr3d 2218 . . . . . . . 8 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + ((๐‘ƒ ยท ๐‘) โˆ’ ((๐‘Ÿ ยท ๐ผ) ยท ๐‘))) mod ๐‘ƒ) = 0)
14030, 45, 1393eqtrd 2214 . . . . . . 7 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ ((๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)) mod ๐‘ƒ) = 0)
141 oveq1 5884 . . . . . . . . . . 11 (๐‘— = ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โ†’ (๐‘— ยท ๐‘) = (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘))
142141oveq2d 5893 . . . . . . . . . 10 (๐‘— = ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โ†’ (๐ผ + (๐‘— ยท ๐‘)) = (๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)))
143142oveq1d 5892 . . . . . . . . 9 (๐‘— = ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โ†’ ((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = ((๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)) mod ๐‘ƒ))
144143eqeq1d 2186 . . . . . . . 8 (๐‘— = ((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โ†’ (((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0 โ†” ((๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)) mod ๐‘ƒ) = 0))
145144rspcev 2843 . . . . . . 7 ((((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) โˆˆ (0..^๐‘ƒ) โˆง ((๐ผ + (((๐‘ƒ โˆ’ (๐‘Ÿ ยท ๐ผ)) mod ๐‘ƒ) ยท ๐‘)) mod ๐‘ƒ) = 0) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0)
14617, 140, 145syl2anc 411 . . . . . 6 (((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ))) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0)
147146ex 115 . . . . 5 ((๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง ((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1) โ†’ ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0))
148147rexlimiva 2589 . . . 4 (โˆƒ๐‘Ÿ โˆˆ (1...(๐‘ƒ โˆ’ 1))((๐‘ ยท ๐‘Ÿ) mod ๐‘ƒ) = 1 โ†’ ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0))
1491, 2, 1483syl 17 . . 3 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0))
1501493adant3 1017 . 2 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0))
151150pm2.43i 49 1 ((๐‘ƒ โˆˆ โ„™ โˆง ๐‘ โˆˆ (1..^๐‘ƒ) โˆง ๐ผ โˆˆ (1..^๐‘ƒ)) โ†’ โˆƒ๐‘— โˆˆ (0..^๐‘ƒ)((๐ผ + (๐‘— ยท ๐‘)) mod ๐‘ƒ) = 0)
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โˆƒwrex 2456  โˆƒ!wreu 2457   class class class wbr 4005  (class class class)co 5877  โ„‚cc 7811  0cc0 7813  1c1 7814   + caddc 7816   ยท cmul 7818   < clt 7994   โ‰ค cle 7995   โˆ’ cmin 8130  โ„•cn 8921  โ„คcz 9255  โ„šcq 9621  ...cfz 10010  ..^cfzo 10144   mod cmo 10324  โ„™cprime 12109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-mulrcl 7912  ax-addcom 7913  ax-mulcom 7914  ax-addass 7915  ax-mulass 7916  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-1rid 7920  ax-0id 7921  ax-rnegex 7922  ax-precex 7923  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-apti 7928  ax-pre-ltadd 7929  ax-pre-mulgt0 7930  ax-pre-mulext 7931  ax-arch 7932  ax-caucvg 7933
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-irdg 6373  df-frec 6394  df-1o 6419  df-2o 6420  df-oadd 6423  df-er 6537  df-en 6743  df-dom 6744  df-fin 6745  df-sup 6985  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-reap 8534  df-ap 8541  df-div 8632  df-inn 8922  df-2 8980  df-3 8981  df-4 8982  df-n0 9179  df-z 9256  df-uz 9531  df-q 9622  df-rp 9656  df-fz 10011  df-fzo 10145  df-fl 10272  df-mod 10325  df-seqfrec 10448  df-exp 10522  df-ihash 10758  df-cj 10853  df-re 10854  df-im 10855  df-rsqrt 11009  df-abs 11010  df-clim 11289  df-proddc 11561  df-dvds 11797  df-gcd 11946  df-prm 12110  df-phi 12213
This theorem is referenced by:  nnnn0modprm0  12257
  Copyright terms: Public domain W3C validator