MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem12 Structured version   Visualization version   GIF version

Theorem 4sqlem12 16924
Description: Lemma for 4sq 16932. For any odd prime ๐‘ƒ, there is a ๐‘˜ < ๐‘ƒ such that ๐‘˜๐‘ƒ โˆ’ 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)
Hypotheses
Ref Expression
4sq.1 ๐‘† = {๐‘› โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค โˆƒ๐‘ง โˆˆ โ„ค โˆƒ๐‘ค โˆˆ โ„ค ๐‘› = (((๐‘ฅโ†‘2) + (๐‘ฆโ†‘2)) + ((๐‘งโ†‘2) + (๐‘คโ†‘2)))}
4sq.2 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
4sq.3 (๐œ‘ โ†’ ๐‘ƒ = ((2 ยท ๐‘) + 1))
4sq.4 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
4sqlem11.5 ๐ด = {๐‘ข โˆฃ โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ)}
4sqlem11.6 ๐น = (๐‘ฃ โˆˆ ๐ด โ†ฆ ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ))
Assertion
Ref Expression
4sqlem12 (๐œ‘ โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ))
Distinct variable groups:   ๐‘ค,๐‘›,๐‘ฅ,๐‘ฆ,๐‘ง   ๐‘˜,๐‘›,๐‘ฃ,๐ด   ๐‘›,๐น   ๐‘ข,๐‘˜,๐‘›,๐‘š,๐‘,๐‘ฃ   ๐‘ƒ,๐‘˜,๐‘š,๐‘›,๐‘ข,๐‘ฃ   ๐œ‘,๐‘˜,๐‘š,๐‘›,๐‘ข,๐‘ฃ   ๐‘†,๐‘˜,๐‘š,๐‘›,๐‘ข,๐‘ฃ
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘ข,๐‘š)   ๐‘ƒ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘†(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐น(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘ฃ,๐‘ข,๐‘˜,๐‘š)   ๐‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)

Proof of Theorem 4sqlem12
Dummy variable ๐‘— is distinct from all other variables.
StepHypRef Expression
1 4sq.1 . . . 4 ๐‘† = {๐‘› โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค โˆƒ๐‘ง โˆˆ โ„ค โˆƒ๐‘ค โˆˆ โ„ค ๐‘› = (((๐‘ฅโ†‘2) + (๐‘ฆโ†‘2)) + ((๐‘งโ†‘2) + (๐‘คโ†‘2)))}
2 4sq.2 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
3 4sq.3 . . . 4 (๐œ‘ โ†’ ๐‘ƒ = ((2 ยท ๐‘) + 1))
4 4sq.4 . . . 4 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
5 4sqlem11.5 . . . 4 ๐ด = {๐‘ข โˆฃ โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ)}
6 4sqlem11.6 . . . 4 ๐น = (๐‘ฃ โˆˆ ๐ด โ†ฆ ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ))
71, 2, 3, 4, 5, 64sqlem11 16923 . . 3 (๐œ‘ โ†’ (๐ด โˆฉ ran ๐น) โ‰  โˆ…)
8 n0 4342 . . 3 ((๐ด โˆฉ ran ๐น) โ‰  โˆ… โ†” โˆƒ๐‘— ๐‘— โˆˆ (๐ด โˆฉ ran ๐น))
97, 8sylib 217 . 2 (๐œ‘ โ†’ โˆƒ๐‘— ๐‘— โˆˆ (๐ด โˆฉ ran ๐น))
10 vex 3467 . . . . . . 7 ๐‘— โˆˆ V
11 eqeq1 2729 . . . . . . . 8 (๐‘ข = ๐‘— โ†’ (๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ) โ†” ๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ)))
1211rexbidv 3169 . . . . . . 7 (๐‘ข = ๐‘— โ†’ (โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ) โ†” โˆƒ๐‘š โˆˆ (0...๐‘)๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ)))
1310, 12, 5elab2 3663 . . . . . 6 (๐‘— โˆˆ ๐ด โ†” โˆƒ๐‘š โˆˆ (0...๐‘)๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ))
14 abid 2706 . . . . . . . . 9 (๐‘— โˆˆ {๐‘— โˆฃ โˆƒ๐‘ฃ โˆˆ ๐ด ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)} โ†” โˆƒ๐‘ฃ โˆˆ ๐ด ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ))
155rexeqi 3314 . . . . . . . . 9 (โˆƒ๐‘ฃ โˆˆ ๐ด ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ) โ†” โˆƒ๐‘ฃ โˆˆ {๐‘ข โˆฃ โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ)}๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ))
16 oveq1 7423 . . . . . . . . . . . . . 14 (๐‘š = ๐‘› โ†’ (๐‘šโ†‘2) = (๐‘›โ†‘2))
1716oveq1d 7431 . . . . . . . . . . . . 13 (๐‘š = ๐‘› โ†’ ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘›โ†‘2) mod ๐‘ƒ))
1817eqeq2d 2736 . . . . . . . . . . . 12 (๐‘š = ๐‘› โ†’ (๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ) โ†” ๐‘ข = ((๐‘›โ†‘2) mod ๐‘ƒ)))
1918cbvrexvw 3226 . . . . . . . . . . 11 (โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ) โ†” โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ข = ((๐‘›โ†‘2) mod ๐‘ƒ))
20 eqeq1 2729 . . . . . . . . . . . 12 (๐‘ข = ๐‘ฃ โ†’ (๐‘ข = ((๐‘›โ†‘2) mod ๐‘ƒ) โ†” ๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ)))
2120rexbidv 3169 . . . . . . . . . . 11 (๐‘ข = ๐‘ฃ โ†’ (โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ข = ((๐‘›โ†‘2) mod ๐‘ƒ) โ†” โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ)))
2219, 21bitrid 282 . . . . . . . . . 10 (๐‘ข = ๐‘ฃ โ†’ (โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ) โ†” โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ)))
2322rexab 3681 . . . . . . . . 9 (โˆƒ๐‘ฃ โˆˆ {๐‘ข โˆฃ โˆƒ๐‘š โˆˆ (0...๐‘)๐‘ข = ((๐‘šโ†‘2) mod ๐‘ƒ)}๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ) โ†” โˆƒ๐‘ฃ(โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
2414, 15, 233bitri 296 . . . . . . . 8 (๐‘— โˆˆ {๐‘— โˆฃ โˆƒ๐‘ฃ โˆˆ ๐ด ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)} โ†” โˆƒ๐‘ฃ(โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
256rnmpt 5951 . . . . . . . . 9 ran ๐น = {๐‘— โˆฃ โˆƒ๐‘ฃ โˆˆ ๐ด ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)}
2625eleq2i 2817 . . . . . . . 8 (๐‘— โˆˆ ran ๐น โ†” ๐‘— โˆˆ {๐‘— โˆฃ โˆƒ๐‘ฃ โˆˆ ๐ด ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)})
27 rexcom4 3276 . . . . . . . . 9 (โˆƒ๐‘› โˆˆ (0...๐‘)โˆƒ๐‘ฃ(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)) โ†” โˆƒ๐‘ฃโˆƒ๐‘› โˆˆ (0...๐‘)(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
28 r19.41v 3179 . . . . . . . . . 10 (โˆƒ๐‘› โˆˆ (0...๐‘)(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)) โ†” (โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
2928exbii 1842 . . . . . . . . 9 (โˆƒ๐‘ฃโˆƒ๐‘› โˆˆ (0...๐‘)(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)) โ†” โˆƒ๐‘ฃ(โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
3027, 29bitri 274 . . . . . . . 8 (โˆƒ๐‘› โˆˆ (0...๐‘)โˆƒ๐‘ฃ(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)) โ†” โˆƒ๐‘ฃ(โˆƒ๐‘› โˆˆ (0...๐‘)๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
3124, 26, 303bitr4i 302 . . . . . . 7 (๐‘— โˆˆ ran ๐น โ†” โˆƒ๐‘› โˆˆ (0...๐‘)โˆƒ๐‘ฃ(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)))
32 ovex 7449 . . . . . . . . 9 ((๐‘›โ†‘2) mod ๐‘ƒ) โˆˆ V
33 oveq2 7424 . . . . . . . . . 10 (๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โ†’ ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
3433eqeq2d 2736 . . . . . . . . 9 (๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โ†’ (๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ) โ†” ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))))
3532, 34ceqsexv 3515 . . . . . . . 8 (โˆƒ๐‘ฃ(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)) โ†” ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
3635rexbii 3084 . . . . . . 7 (โˆƒ๐‘› โˆˆ (0...๐‘)โˆƒ๐‘ฃ(๐‘ฃ = ((๐‘›โ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ๐‘ฃ)) โ†” โˆƒ๐‘› โˆˆ (0...๐‘)๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
3731, 36bitri 274 . . . . . 6 (๐‘— โˆˆ ran ๐น โ†” โˆƒ๐‘› โˆˆ (0...๐‘)๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
3813, 37anbi12i 626 . . . . 5 ((๐‘— โˆˆ ๐ด โˆง ๐‘— โˆˆ ran ๐น) โ†” (โˆƒ๐‘š โˆˆ (0...๐‘)๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง โˆƒ๐‘› โˆˆ (0...๐‘)๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))))
39 elin 3955 . . . . 5 (๐‘— โˆˆ (๐ด โˆฉ ran ๐น) โ†” (๐‘— โˆˆ ๐ด โˆง ๐‘— โˆˆ ran ๐น))
40 reeanv 3217 . . . . 5 (โˆƒ๐‘š โˆˆ (0...๐‘)โˆƒ๐‘› โˆˆ (0...๐‘)(๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†” (โˆƒ๐‘š โˆˆ (0...๐‘)๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง โˆƒ๐‘› โˆˆ (0...๐‘)๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))))
4138, 39, 403bitr4i 302 . . . 4 (๐‘— โˆˆ (๐ด โˆฉ ran ๐น) โ†” โˆƒ๐‘š โˆˆ (0...๐‘)โˆƒ๐‘› โˆˆ (0...๐‘)(๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))))
42 eqtr2 2749 . . . . . 6 ((๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
4343ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„™)
44 prmnn 16644 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„•)
46 nnm1nn0 12543 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ โ„• โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„•0)
4745, 46syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„•0)
4847nn0red 12563 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
4945nnrpd 13046 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„+)
5047nn0ge0d 12565 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 0 โ‰ค (๐‘ƒ โˆ’ 1))
5145nnred 12257 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„)
5251ltm1d 12176 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ 1) < ๐‘ƒ)
53 modid 13893 . . . . . . . . . . . . . . . 16 ((((๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โˆง (0 โ‰ค (๐‘ƒ โˆ’ 1) โˆง (๐‘ƒ โˆ’ 1) < ๐‘ƒ)) โ†’ ((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) = (๐‘ƒ โˆ’ 1))
5448, 49, 50, 52, 53syl22anc 837 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) = (๐‘ƒ โˆ’ 1))
5554oveq1d 7431 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
56 simp2r 1197 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘› โˆˆ (0...๐‘))
5756elfzelzd 13534 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘› โˆˆ โ„ค)
58 zsqcl2 14134 . . . . . . . . . . . . . . . . . . . 20 (๐‘› โˆˆ โ„ค โ†’ (๐‘›โ†‘2) โˆˆ โ„•0)
5957, 58syl 17 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘›โ†‘2) โˆˆ โ„•0)
6059nn0red 12563 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘›โ†‘2) โˆˆ โ„)
61 modlt 13877 . . . . . . . . . . . . . . . . . 18 (((๐‘›โ†‘2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ ((๐‘›โ†‘2) mod ๐‘ƒ) < ๐‘ƒ)
6260, 49, 61syl2anc 582 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘›โ†‘2) mod ๐‘ƒ) < ๐‘ƒ)
63 zsqcl 14125 . . . . . . . . . . . . . . . . . . . . 21 (๐‘› โˆˆ โ„ค โ†’ (๐‘›โ†‘2) โˆˆ โ„ค)
6457, 63syl 17 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘›โ†‘2) โˆˆ โ„ค)
6564, 45zmodcld 13889 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘›โ†‘2) mod ๐‘ƒ) โˆˆ โ„•0)
6665nn0zd 12614 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘›โ†‘2) mod ๐‘ƒ) โˆˆ โ„ค)
67 prmz 16645 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
6843, 67syl 17 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„ค)
69 zltlem1 12645 . . . . . . . . . . . . . . . . . 18 ((((๐‘›โ†‘2) mod ๐‘ƒ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ (((๐‘›โ†‘2) mod ๐‘ƒ) < ๐‘ƒ โ†” ((๐‘›โ†‘2) mod ๐‘ƒ) โ‰ค (๐‘ƒ โˆ’ 1)))
7066, 68, 69syl2anc 582 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘›โ†‘2) mod ๐‘ƒ) < ๐‘ƒ โ†” ((๐‘›โ†‘2) mod ๐‘ƒ) โ‰ค (๐‘ƒ โˆ’ 1)))
7162, 70mpbid 231 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘›โ†‘2) mod ๐‘ƒ) โ‰ค (๐‘ƒ โˆ’ 1))
7271, 54breqtrrd 5171 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘›โ†‘2) mod ๐‘ƒ) โ‰ค ((๐‘ƒ โˆ’ 1) mod ๐‘ƒ))
73 modsubdir 13937 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (๐‘›โ†‘2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ (((๐‘›โ†‘2) mod ๐‘ƒ) โ‰ค ((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) โ†” (((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) mod ๐‘ƒ) = (((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))))
7448, 60, 49, 73syl3anc 1368 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘›โ†‘2) mod ๐‘ƒ) โ‰ค ((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) โ†” (((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) mod ๐‘ƒ) = (((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))))
7572, 74mpbid 231 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) mod ๐‘ƒ) = (((๐‘ƒ โˆ’ 1) mod ๐‘ƒ) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
76 simp3 1135 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)))
7755, 75, 763eqtr4rd 2776 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) mod ๐‘ƒ) = (((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) mod ๐‘ƒ))
78 simp2l 1196 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘š โˆˆ (0...๐‘))
7978elfzelzd 13534 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘š โˆˆ โ„ค)
80 zsqcl 14125 . . . . . . . . . . . . . . 15 (๐‘š โˆˆ โ„ค โ†’ (๐‘šโ†‘2) โˆˆ โ„ค)
8179, 80syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘šโ†‘2) โˆˆ โ„ค)
8247nn0zd 12614 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„ค)
8382, 64zsubcld 12701 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) โˆˆ โ„ค)
84 moddvds 16241 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ โ„• โˆง (๐‘šโ†‘2) โˆˆ โ„ค โˆง ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) โˆˆ โ„ค) โ†’ (((๐‘šโ†‘2) mod ๐‘ƒ) = (((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ ((๐‘šโ†‘2) โˆ’ ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)))))
8545, 81, 83, 84syl3anc 1368 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) mod ๐‘ƒ) = (((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)) mod ๐‘ƒ) โ†” ๐‘ƒ โˆฅ ((๐‘šโ†‘2) โˆ’ ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2)))))
8677, 85mpbid 231 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆฅ ((๐‘šโ†‘2) โˆ’ ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2))))
87 zsqcl2 14134 . . . . . . . . . . . . . . . 16 (๐‘š โˆˆ โ„ค โ†’ (๐‘šโ†‘2) โˆˆ โ„•0)
8879, 87syl 17 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘šโ†‘2) โˆˆ โ„•0)
8988nn0cnd 12564 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘šโ†‘2) โˆˆ โ„‚)
9047nn0cnd 12564 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„‚)
9159nn0cnd 12564 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘›โ†‘2) โˆˆ โ„‚)
9289, 90, 91subsub3d 11631 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) โˆ’ ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2))) = (((๐‘šโ†‘2) + (๐‘›โ†‘2)) โˆ’ (๐‘ƒ โˆ’ 1)))
9388, 59nn0addcld 12566 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) โˆˆ โ„•0)
9493nn0cnd 12564 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) โˆˆ โ„‚)
9545nncnd 12258 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆˆ โ„‚)
96 1cnd 11239 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 1 โˆˆ โ„‚)
9794, 95, 96subsub3d 11631 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) โˆ’ (๐‘ƒ โˆ’ 1)) = ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆ’ ๐‘ƒ))
9892, 97eqtrd 2765 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) โˆ’ ((๐‘ƒ โˆ’ 1) โˆ’ (๐‘›โ†‘2))) = ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆ’ ๐‘ƒ))
9986, 98breqtrd 5169 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆฅ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆ’ ๐‘ƒ))
100 nn0p1nn 12541 . . . . . . . . . . . . . 14 (((๐‘šโ†‘2) + (๐‘›โ†‘2)) โˆˆ โ„•0 โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„•)
10193, 100syl 17 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„•)
102101nnzd 12615 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„ค)
103 dvdssubr 16281 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„ค โˆง (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„ค) โ†’ (๐‘ƒ โˆฅ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โ†” ๐‘ƒ โˆฅ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆ’ ๐‘ƒ)))
10468, 102, 103syl2anc 582 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆฅ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โ†” ๐‘ƒ โˆฅ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆ’ ๐‘ƒ)))
10599, 104mpbird 256 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โˆฅ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1))
10645nnne0d 12292 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ โ‰  0)
107 dvdsval2 16233 . . . . . . . . . . 11 ((๐‘ƒ โˆˆ โ„ค โˆง ๐‘ƒ โ‰  0 โˆง (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„ค) โ†’ (๐‘ƒ โˆฅ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โ†” ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„ค))
10868, 106, 102, 107syl3anc 1368 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ โˆฅ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โ†” ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„ค))
109105, 108mpbid 231 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„ค)
110 nnrp 13017 . . . . . . . . . . . . . 14 ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„• โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„+)
111 nnrp 13017 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„+)
112 rpdivcl 13031 . . . . . . . . . . . . . 14 (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„+ โˆง ๐‘ƒ โˆˆ โ„+) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„+)
113110, 111, 112syl2an 594 . . . . . . . . . . . . 13 (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„•) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„+)
114101, 45, 113syl2anc 582 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„+)
115114rpgt0d 13051 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 0 < ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ))
116 elnnz 12598 . . . . . . . . . . 11 (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„• โ†” (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„ค โˆง 0 < ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ)))
117109, 115, 116sylanbrc 581 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„•)
118117nnge1d 12290 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 1 โ‰ค ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ))
11993nn0red 12563 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) โˆˆ โ„)
120 2nn 12315 . . . . . . . . . . . . . . . 16 2 โˆˆ โ„•
12123ad2ant1 1130 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ โˆˆ โ„•)
122 nnmulcl 12266 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (2 ยท ๐‘) โˆˆ โ„•)
123120, 121, 122sylancr 585 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท ๐‘) โˆˆ โ„•)
124123nnred 12257 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท ๐‘) โˆˆ โ„)
125124resqcld 14121 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((2 ยท ๐‘)โ†‘2) โˆˆ โ„)
126 nnmulcl 12266 . . . . . . . . . . . . . . 15 ((2 โˆˆ โ„• โˆง (2 ยท ๐‘) โˆˆ โ„•) โ†’ (2 ยท (2 ยท ๐‘)) โˆˆ โ„•)
127120, 123, 126sylancr 585 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (2 ยท ๐‘)) โˆˆ โ„•)
128127nnred 12257 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (2 ยท ๐‘)) โˆˆ โ„)
129125, 128readdcld 11273 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))) โˆˆ โ„)
130 1red 11245 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 1 โˆˆ โ„)
131121nnsqcld 14238 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘โ†‘2) โˆˆ โ„•)
132 nnmulcl 12266 . . . . . . . . . . . . . . . 16 ((2 โˆˆ โ„• โˆง (๐‘โ†‘2) โˆˆ โ„•) โ†’ (2 ยท (๐‘โ†‘2)) โˆˆ โ„•)
133120, 131, 132sylancr 585 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (๐‘โ†‘2)) โˆˆ โ„•)
134133nnred 12257 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (๐‘โ†‘2)) โˆˆ โ„)
13588nn0red 12563 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘šโ†‘2) โˆˆ โ„)
136131nnred 12257 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘โ†‘2) โˆˆ โ„)
13779zred 12696 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘š โˆˆ โ„)
138 elfzle1 13536 . . . . . . . . . . . . . . . . . 18 (๐‘š โˆˆ (0...๐‘) โ†’ 0 โ‰ค ๐‘š)
13978, 138syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 0 โ‰ค ๐‘š)
140121nnred 12257 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ โˆˆ โ„)
141 elfzle2 13537 . . . . . . . . . . . . . . . . . 18 (๐‘š โˆˆ (0...๐‘) โ†’ ๐‘š โ‰ค ๐‘)
14278, 141syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘š โ‰ค ๐‘)
143 le2sq2 14131 . . . . . . . . . . . . . . . . 17 (((๐‘š โˆˆ โ„ โˆง 0 โ‰ค ๐‘š) โˆง (๐‘ โˆˆ โ„ โˆง ๐‘š โ‰ค ๐‘)) โ†’ (๐‘šโ†‘2) โ‰ค (๐‘โ†‘2))
144137, 139, 140, 142, 143syl22anc 837 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘šโ†‘2) โ‰ค (๐‘โ†‘2))
14557zred 12696 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘› โˆˆ โ„)
146 elfzle1 13536 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ (0...๐‘) โ†’ 0 โ‰ค ๐‘›)
14756, 146syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 0 โ‰ค ๐‘›)
148 elfzle2 13537 . . . . . . . . . . . . . . . . . 18 (๐‘› โˆˆ (0...๐‘) โ†’ ๐‘› โ‰ค ๐‘)
14956, 148syl 17 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘› โ‰ค ๐‘)
150 le2sq2 14131 . . . . . . . . . . . . . . . . 17 (((๐‘› โˆˆ โ„ โˆง 0 โ‰ค ๐‘›) โˆง (๐‘ โˆˆ โ„ โˆง ๐‘› โ‰ค ๐‘)) โ†’ (๐‘›โ†‘2) โ‰ค (๐‘โ†‘2))
151145, 147, 140, 149, 150syl22anc 837 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘›โ†‘2) โ‰ค (๐‘โ†‘2))
152135, 60, 136, 136, 144, 151le2addd 11863 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) โ‰ค ((๐‘โ†‘2) + (๐‘โ†‘2)))
153131nncnd 12258 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘โ†‘2) โˆˆ โ„‚)
1541532timesd 12485 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (๐‘โ†‘2)) = ((๐‘โ†‘2) + (๐‘โ†‘2)))
155152, 154breqtrrd 5171 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) โ‰ค (2 ยท (๐‘โ†‘2)))
156 2lt4 12417 . . . . . . . . . . . . . . . 16 2 < 4
157 2re 12316 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„
158157a1i 11 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 2 โˆˆ โ„)
159 4re 12326 . . . . . . . . . . . . . . . . . 18 4 โˆˆ โ„
160159a1i 11 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 4 โˆˆ โ„)
161131nngt0d 12291 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 0 < (๐‘โ†‘2))
162 ltmul1 12094 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„ โˆง 4 โˆˆ โ„ โˆง ((๐‘โ†‘2) โˆˆ โ„ โˆง 0 < (๐‘โ†‘2))) โ†’ (2 < 4 โ†” (2 ยท (๐‘โ†‘2)) < (4 ยท (๐‘โ†‘2))))
163158, 160, 136, 161, 162syl112anc 1371 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 < 4 โ†” (2 ยท (๐‘โ†‘2)) < (4 ยท (๐‘โ†‘2))))
164156, 163mpbii 232 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (๐‘โ†‘2)) < (4 ยท (๐‘โ†‘2)))
165 2cn 12317 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„‚
166121nncnd 12258 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ โˆˆ โ„‚)
167 sqmul 14115 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ ((2 ยท ๐‘)โ†‘2) = ((2โ†‘2) ยท (๐‘โ†‘2)))
168165, 166, 167sylancr 585 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((2 ยท ๐‘)โ†‘2) = ((2โ†‘2) ยท (๐‘โ†‘2)))
169 sq2 14192 . . . . . . . . . . . . . . . . 17 (2โ†‘2) = 4
170169oveq1i 7426 . . . . . . . . . . . . . . . 16 ((2โ†‘2) ยท (๐‘โ†‘2)) = (4 ยท (๐‘โ†‘2))
171168, 170eqtrdi 2781 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((2 ยท ๐‘)โ†‘2) = (4 ยท (๐‘โ†‘2)))
172164, 171breqtrrd 5171 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (๐‘โ†‘2)) < ((2 ยท ๐‘)โ†‘2))
173119, 134, 125, 155, 172lelttrd 11402 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) < ((2 ยท ๐‘)โ†‘2))
174127nnrpd 13046 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท (2 ยท ๐‘)) โˆˆ โ„+)
175125, 174ltaddrpd 13081 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((2 ยท ๐‘)โ†‘2) < (((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))))
176119, 125, 129, 173, 175lttrd 11405 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((๐‘šโ†‘2) + (๐‘›โ†‘2)) < (((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))))
177119, 129, 130, 176ltadd1dd 11855 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) < ((((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))) + 1))
17833ad2ant1 1130 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ๐‘ƒ = ((2 ยท ๐‘) + 1))
179178oveq1d 7431 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒโ†‘2) = (((2 ยท ๐‘) + 1)โ†‘2))
18095sqvald 14139 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒโ†‘2) = (๐‘ƒ ยท ๐‘ƒ))
181123nncnd 12258 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
182 binom21 14213 . . . . . . . . . . . . 13 ((2 ยท ๐‘) โˆˆ โ„‚ โ†’ (((2 ยท ๐‘) + 1)โ†‘2) = ((((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))) + 1))
183181, 182syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((2 ยท ๐‘) + 1)โ†‘2) = ((((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))) + 1))
184179, 180, 1833eqtr3d 2773 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘ƒ ยท ๐‘ƒ) = ((((2 ยท ๐‘)โ†‘2) + (2 ยท (2 ยท ๐‘))) + 1))
185177, 184breqtrrd 5171 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) < (๐‘ƒ ยท ๐‘ƒ))
186101nnred 12257 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„)
18745nngt0d 12291 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ 0 < ๐‘ƒ)
188 ltdivmul 12119 . . . . . . . . . . 11 (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„ โˆง (๐‘ƒ โˆˆ โ„ โˆง 0 < ๐‘ƒ)) โ†’ (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) < ๐‘ƒ โ†” (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) < (๐‘ƒ ยท ๐‘ƒ)))
189186, 51, 51, 187, 188syl112anc 1371 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) < ๐‘ƒ โ†” (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) < (๐‘ƒ ยท ๐‘ƒ)))
190185, 189mpbird 256 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) < ๐‘ƒ)
191 1z 12622 . . . . . . . . . 10 1 โˆˆ โ„ค
192 elfzm11 13604 . . . . . . . . . 10 ((1 โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค) โ†’ (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†” (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„ค โˆง 1 โ‰ค ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆง ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) < ๐‘ƒ)))
193191, 68, 192sylancr 585 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โ†” (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ โ„ค โˆง 1 โ‰ค ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆง ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) < ๐‘ƒ)))
194109, 118, 190, 193mpbir3and 1339 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ (1...(๐‘ƒ โˆ’ 1)))
195 gzreim 16907 . . . . . . . . 9 ((๐‘š โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„ค) โ†’ (๐‘š + (i ยท ๐‘›)) โˆˆ โ„ค[i])
19679, 57, 195syl2anc 582 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘š + (i ยท ๐‘›)) โˆˆ โ„ค[i])
197 gzcn 16900 . . . . . . . . . . . . 13 ((๐‘š + (i ยท ๐‘›)) โˆˆ โ„ค[i] โ†’ (๐‘š + (i ยท ๐‘›)) โˆˆ โ„‚)
198196, 197syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (๐‘š + (i ยท ๐‘›)) โˆˆ โ„‚)
199198absvalsq2d 15422 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) = (((โ„œโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + ((โ„‘โ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2)))
200137, 145crred 15210 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (โ„œโ€˜(๐‘š + (i ยท ๐‘›))) = ๐‘š)
201200oveq1d 7431 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((โ„œโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) = (๐‘šโ†‘2))
202137, 145crimd 15211 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (โ„‘โ€˜(๐‘š + (i ยท ๐‘›))) = ๐‘›)
203202oveq1d 7431 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((โ„‘โ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) = (๐‘›โ†‘2))
204201, 203oveq12d 7434 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((โ„œโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + ((โ„‘โ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2)) = ((๐‘šโ†‘2) + (๐‘›โ†‘2)))
205199, 204eqtrd 2765 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ ((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) = ((๐‘šโ†‘2) + (๐‘›โ†‘2)))
206205oveq1d 7431 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + 1) = (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1))
207101nncnd 12258 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) โˆˆ โ„‚)
208207, 95, 106divcan1d 12021 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ) = (((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1))
209206, 208eqtr4d 2768 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ (((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + 1) = (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ))
210 oveq1 7423 . . . . . . . . . 10 (๐‘˜ = ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โ†’ (๐‘˜ ยท ๐‘ƒ) = (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ))
211210eqeq2d 2736 . . . . . . . . 9 (๐‘˜ = ((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โ†’ ((((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ) โ†” (((absโ€˜๐‘ข)โ†‘2) + 1) = (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ)))
212 fveq2 6892 . . . . . . . . . . . 12 (๐‘ข = (๐‘š + (i ยท ๐‘›)) โ†’ (absโ€˜๐‘ข) = (absโ€˜(๐‘š + (i ยท ๐‘›))))
213212oveq1d 7431 . . . . . . . . . . 11 (๐‘ข = (๐‘š + (i ยท ๐‘›)) โ†’ ((absโ€˜๐‘ข)โ†‘2) = ((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2))
214213oveq1d 7431 . . . . . . . . . 10 (๐‘ข = (๐‘š + (i ยท ๐‘›)) โ†’ (((absโ€˜๐‘ข)โ†‘2) + 1) = (((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + 1))
215214eqeq1d 2727 . . . . . . . . 9 (๐‘ข = (๐‘š + (i ยท ๐‘›)) โ†’ ((((absโ€˜๐‘ข)โ†‘2) + 1) = (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ) โ†” (((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + 1) = (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ)))
216211, 215rspc2ev 3614 . . . . . . . 8 ((((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) โˆˆ (1...(๐‘ƒ โˆ’ 1)) โˆง (๐‘š + (i ยท ๐‘›)) โˆˆ โ„ค[i] โˆง (((absโ€˜(๐‘š + (i ยท ๐‘›)))โ†‘2) + 1) = (((((๐‘šโ†‘2) + (๐‘›โ†‘2)) + 1) / ๐‘ƒ) ยท ๐‘ƒ)) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ))
217194, 196, 209, 216syl3anc 1368 . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘)) โˆง ((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ))
2182173expia 1118 . . . . . 6 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘))) โ†’ (((๐‘šโ†‘2) mod ๐‘ƒ) = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ)) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ)))
21942, 218syl5 34 . . . . 5 ((๐œ‘ โˆง (๐‘š โˆˆ (0...๐‘) โˆง ๐‘› โˆˆ (0...๐‘))) โ†’ ((๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ)))
220219rexlimdvva 3202 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘š โˆˆ (0...๐‘)โˆƒ๐‘› โˆˆ (0...๐‘)(๐‘— = ((๐‘šโ†‘2) mod ๐‘ƒ) โˆง ๐‘— = ((๐‘ƒ โˆ’ 1) โˆ’ ((๐‘›โ†‘2) mod ๐‘ƒ))) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ)))
22141, 220biimtrid 241 . . 3 (๐œ‘ โ†’ (๐‘— โˆˆ (๐ด โˆฉ ran ๐น) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ)))
222221exlimdv 1928 . 2 (๐œ‘ โ†’ (โˆƒ๐‘— ๐‘— โˆˆ (๐ด โˆฉ ran ๐น) โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ)))
2239, 222mpd 15 1 (๐œ‘ โ†’ โˆƒ๐‘˜ โˆˆ (1...(๐‘ƒ โˆ’ 1))โˆƒ๐‘ข โˆˆ โ„ค[i] (((absโ€˜๐‘ข)โ†‘2) + 1) = (๐‘˜ ยท ๐‘ƒ))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1084   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098  {cab 2702   โ‰  wne 2930  โˆƒwrex 3060   โˆฉ cin 3938  โˆ…c0 4318   class class class wbr 5143   โ†ฆ cmpt 5226  ran crn 5673  โ€˜cfv 6543  (class class class)co 7416  โ„‚cc 11136  โ„cr 11137  0cc0 11138  1c1 11139  ici 11140   + caddc 11141   ยท cmul 11143   < clt 11278   โ‰ค cle 11279   โˆ’ cmin 11474   / cdiv 11901  โ„•cn 12242  2c2 12297  4c4 12299  โ„•0cn0 12502  โ„คcz 12588  โ„+crp 13006  ...cfz 13516   mod cmo 13866  โ†‘cexp 14058  โ„œcre 15076  โ„‘cim 15077  abscabs 15213   โˆฅ cdvds 16230  โ„™cprime 16641  โ„ค[i]cgz 16897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7991  df-2nd 7992  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-oadd 8489  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-sup 9465  df-inf 9466  df-dju 9924  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-n0 12503  df-xnn0 12575  df-z 12589  df-uz 12853  df-rp 13007  df-fz 13517  df-fl 13789  df-mod 13867  df-seq 13999  df-exp 14059  df-hash 14322  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-dvds 16231  df-gcd 16469  df-prm 16642  df-gz 16898
This theorem is referenced by:  4sqlem13  16925
  Copyright terms: Public domain W3C validator