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

Theorem 4sqlem17 16903
Description: Lemma for 4sq 16906. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
Hypotheses
Ref Expression
4sq.1 ๐‘† = {๐‘› โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค โˆƒ๐‘ง โˆˆ โ„ค โˆƒ๐‘ค โˆˆ โ„ค ๐‘› = (((๐‘ฅโ†‘2) + (๐‘ฆโ†‘2)) + ((๐‘งโ†‘2) + (๐‘คโ†‘2)))}
4sq.2 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
4sq.3 (๐œ‘ โ†’ ๐‘ƒ = ((2 ยท ๐‘) + 1))
4sq.4 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
4sq.5 (๐œ‘ โ†’ (0...(2 ยท ๐‘)) โІ ๐‘†)
4sq.6 ๐‘‡ = {๐‘– โˆˆ โ„• โˆฃ (๐‘– ยท ๐‘ƒ) โˆˆ ๐‘†}
4sq.7 ๐‘€ = inf(๐‘‡, โ„, < )
4sq.m (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜2))
4sq.a (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
4sq.b (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
4sq.c (๐œ‘ โ†’ ๐ถ โˆˆ โ„ค)
4sq.d (๐œ‘ โ†’ ๐ท โˆˆ โ„ค)
4sq.e ๐ธ = (((๐ด + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
4sq.f ๐น = (((๐ต + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
4sq.g ๐บ = (((๐ถ + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
4sq.h ๐ป = (((๐ท + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
4sq.r ๐‘… = ((((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))) / ๐‘€)
4sq.p (๐œ‘ โ†’ (๐‘€ ยท ๐‘ƒ) = (((๐ดโ†‘2) + (๐ตโ†‘2)) + ((๐ถโ†‘2) + (๐ทโ†‘2))))
Assertion
Ref Expression
4sqlem17 ยฌ ๐œ‘
Distinct variable groups:   ๐‘ค,๐‘›,๐‘ฅ,๐‘ฆ,๐‘ง   ๐ต,๐‘›   ๐‘›,๐ธ   ๐‘›,๐บ   ๐‘›,๐ป   ๐ด,๐‘›   ๐ถ,๐‘›   ๐ท,๐‘›   ๐‘›,๐น   ๐‘–,๐‘›,๐‘€   ๐‘›,๐‘   ๐‘ƒ,๐‘–,๐‘›   ๐œ‘,๐‘›   ๐‘†,๐‘–,๐‘›   ๐‘…,๐‘–
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐ด(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐ต(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐ถ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐ท(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐‘ƒ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘…(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘›)   ๐‘†(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘‡(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–,๐‘›)   ๐ธ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐น(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐บ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐ป(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)   ๐‘€(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค)   ๐‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค,๐‘–)

Proof of Theorem 4sqlem17
StepHypRef Expression
1 4sq.1 . . . . . . 7 ๐‘† = {๐‘› โˆฃ โˆƒ๐‘ฅ โˆˆ โ„ค โˆƒ๐‘ฆ โˆˆ โ„ค โˆƒ๐‘ง โˆˆ โ„ค โˆƒ๐‘ค โˆˆ โ„ค ๐‘› = (((๐‘ฅโ†‘2) + (๐‘ฆโ†‘2)) + ((๐‘งโ†‘2) + (๐‘คโ†‘2)))}
2 4sq.2 . . . . . . 7 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
3 4sq.3 . . . . . . 7 (๐œ‘ โ†’ ๐‘ƒ = ((2 ยท ๐‘) + 1))
4 4sq.4 . . . . . . 7 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™)
5 4sq.5 . . . . . . 7 (๐œ‘ โ†’ (0...(2 ยท ๐‘)) โІ ๐‘†)
6 4sq.6 . . . . . . 7 ๐‘‡ = {๐‘– โˆˆ โ„• โˆฃ (๐‘– ยท ๐‘ƒ) โˆˆ ๐‘†}
7 4sq.7 . . . . . . 7 ๐‘€ = inf(๐‘‡, โ„, < )
8 4sq.m . . . . . . 7 (๐œ‘ โ†’ ๐‘€ โˆˆ (โ„คโ‰ฅโ€˜2))
9 4sq.a . . . . . . 7 (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
10 4sq.b . . . . . . 7 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
11 4sq.c . . . . . . 7 (๐œ‘ โ†’ ๐ถ โˆˆ โ„ค)
12 4sq.d . . . . . . 7 (๐œ‘ โ†’ ๐ท โˆˆ โ„ค)
13 4sq.e . . . . . . 7 ๐ธ = (((๐ด + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
14 4sq.f . . . . . . 7 ๐น = (((๐ต + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
15 4sq.g . . . . . . 7 ๐บ = (((๐ถ + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
16 4sq.h . . . . . . 7 ๐ป = (((๐ท + (๐‘€ / 2)) mod ๐‘€) โˆ’ (๐‘€ / 2))
17 4sq.r . . . . . . 7 ๐‘… = ((((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))) / ๐‘€)
18 4sq.p . . . . . . 7 (๐œ‘ โ†’ (๐‘€ ยท ๐‘ƒ) = (((๐ดโ†‘2) + (๐ตโ†‘2)) + ((๐ถโ†‘2) + (๐ทโ†‘2))))
191, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem16 16902 . . . . . 6 (๐œ‘ โ†’ (๐‘… โ‰ค ๐‘€ โˆง ((๐‘… = 0 โˆจ ๐‘… = ๐‘€) โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ))))
2019simpld 494 . . . . 5 (๐œ‘ โ†’ ๐‘… โ‰ค ๐‘€)
216ssrab3 4075 . . . . . . . 8 ๐‘‡ โІ โ„•
22 nnuz 12869 . . . . . . . 8 โ„• = (โ„คโ‰ฅโ€˜1)
2321, 22sseqtri 4013 . . . . . . 7 ๐‘‡ โІ (โ„คโ‰ฅโ€˜1)
241, 2, 3, 4, 5, 6, 74sqlem13 16899 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘‡ โ‰  โˆ… โˆง ๐‘€ < ๐‘ƒ))
2524simpld 494 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‡ โ‰  โˆ…)
26 infssuzcl 12920 . . . . . . . . . . . . . . 15 ((๐‘‡ โІ (โ„คโ‰ฅโ€˜1) โˆง ๐‘‡ โ‰  โˆ…) โ†’ inf(๐‘‡, โ„, < ) โˆˆ ๐‘‡)
2723, 25, 26sylancr 586 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ inf(๐‘‡, โ„, < ) โˆˆ ๐‘‡)
287, 27eqeltrid 2831 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘‡)
2921, 28sselid 3975 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
3029nnred 12231 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„)
3124simprd 495 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ < ๐‘ƒ)
3230, 31ltned 11354 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โ‰  ๐‘ƒ)
3329nncnd 12232 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
3433sqvald 14113 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘€โ†‘2) = (๐‘€ ยท ๐‘€))
3534breq1d 5151 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” (๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ)))
3629nnzd 12589 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
37 prmz 16619 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
384, 37syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„ค)
3929nnne0d 12266 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โ‰  0)
40 dvdscmulr 16235 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค โˆง (๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0)) โ†’ ((๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โˆฅ ๐‘ƒ))
4136, 38, 36, 39, 40syl112anc 1371 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โˆฅ ๐‘ƒ))
42 dvdsprm 16647 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘€ โˆฅ ๐‘ƒ โ†” ๐‘€ = ๐‘ƒ))
438, 4, 42syl2anc 583 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘€ โˆฅ ๐‘ƒ โ†” ๐‘€ = ๐‘ƒ))
4435, 41, 433bitrd 305 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ = ๐‘ƒ))
4544necon3bbid 2972 . . . . . . . . . 10 (๐œ‘ โ†’ (ยฌ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โ‰  ๐‘ƒ))
4632, 45mpbird 257 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ))
471, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem14 16900 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘… โˆˆ โ„•0)
48 elnn0 12478 . . . . . . . . . . . 12 (๐‘… โˆˆ โ„•0 โ†” (๐‘… โˆˆ โ„• โˆจ ๐‘… = 0))
4947, 48sylib 217 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘… โˆˆ โ„• โˆจ ๐‘… = 0))
5049ord 861 . . . . . . . . . 10 (๐œ‘ โ†’ (ยฌ ๐‘… โˆˆ โ„• โ†’ ๐‘… = 0))
51 orc 864 . . . . . . . . . . 11 (๐‘… = 0 โ†’ (๐‘… = 0 โˆจ ๐‘… = ๐‘€))
5219simprd 495 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘… = 0 โˆจ ๐‘… = ๐‘€) โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5351, 52syl5 34 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘… = 0 โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5450, 53syld 47 . . . . . . . . 9 (๐œ‘ โ†’ (ยฌ ๐‘… โˆˆ โ„• โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5546, 54mt3d 148 . . . . . . . 8 (๐œ‘ โ†’ ๐‘… โˆˆ โ„•)
56 gzreim 16881 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i])
579, 10, 56syl2anc 583 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i])
58 gzcn 16874 . . . . . . . . . . . . . . . . . 18 ((๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i] โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„‚)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„‚)
6059absvalsq2d 15396 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2)))
619zred 12670 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
6210zred 12670 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
6361, 62crred 15184 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„œโ€˜(๐ด + (i ยท ๐ต))) = ๐ด)
6463oveq1d 7420 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (๐ดโ†‘2))
6561, 62crimd 15185 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„‘โ€˜(๐ด + (i ยท ๐ต))) = ๐ต)
6665oveq1d 7420 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (๐ตโ†‘2))
6764, 66oveq12d 7423 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2)) = ((๐ดโ†‘2) + (๐ตโ†‘2)))
6860, 67eqtrd 2766 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = ((๐ดโ†‘2) + (๐ตโ†‘2)))
69 gzreim 16881 . . . . . . . . . . . . . . . . . . 19 ((๐ถ โˆˆ โ„ค โˆง ๐ท โˆˆ โ„ค) โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i])
7011, 12, 69syl2anc 583 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i])
71 gzcn 16874 . . . . . . . . . . . . . . . . . 18 ((๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i] โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„‚)
7270, 71syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„‚)
7372absvalsq2d 15396 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) + ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)))
7411zred 12670 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ถ โˆˆ โ„)
7512zred 12670 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ท โˆˆ โ„)
7674, 75crred 15184 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„œโ€˜(๐ถ + (i ยท ๐ท))) = ๐ถ)
7776oveq1d 7420 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (๐ถโ†‘2))
7874, 75crimd 15185 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„‘โ€˜(๐ถ + (i ยท ๐ท))) = ๐ท)
7978oveq1d 7420 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (๐ทโ†‘2))
8077, 79oveq12d 7423 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) + ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = ((๐ถโ†‘2) + (๐ทโ†‘2)))
8173, 80eqtrd 2766 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = ((๐ถโ†‘2) + (๐ทโ†‘2)))
8268, 81oveq12d 7423 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = (((๐ดโ†‘2) + (๐ตโ†‘2)) + ((๐ถโ†‘2) + (๐ทโ†‘2))))
8318, 82eqtr4d 2769 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘€ ยท ๐‘ƒ) = (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)))
8483oveq1d 7420 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘ƒ) / ๐‘€) = ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€))
85 prmnn 16618 . . . . . . . . . . . . . . 15 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
864, 85syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•)
8786nncnd 12232 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
8887, 33, 39divcan3d 11999 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘ƒ) / ๐‘€) = ๐‘ƒ)
8984, 88eqtr3d 2768 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) = ๐‘ƒ)
909, 29, 134sqlem5 16884 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ธ โˆˆ โ„ค โˆง ((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค))
9190simpld 494 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ธ โˆˆ โ„ค)
9210, 29, 144sqlem5 16884 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐น โˆˆ โ„ค โˆง ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค))
9392simpld 494 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐น โˆˆ โ„ค)
94 gzreim 16881 . . . . . . . . . . . . . . . . . 18 ((๐ธ โˆˆ โ„ค โˆง ๐น โˆˆ โ„ค) โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i])
9591, 93, 94syl2anc 583 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i])
96 gzcn 16874 . . . . . . . . . . . . . . . . 17 ((๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i] โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„‚)
9795, 96syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„‚)
9897absvalsq2d 15396 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2)))
9991zred 12670 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
10093zred 12670 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐น โˆˆ โ„)
10199, 100crred 15184 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„œโ€˜(๐ธ + (i ยท ๐น))) = ๐ธ)
102101oveq1d 7420 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (๐ธโ†‘2))
10399, 100crimd 15185 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„‘โ€˜(๐ธ + (i ยท ๐น))) = ๐น)
104103oveq1d 7420 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (๐นโ†‘2))
105102, 104oveq12d 7423 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2)) = ((๐ธโ†‘2) + (๐นโ†‘2)))
10698, 105eqtrd 2766 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = ((๐ธโ†‘2) + (๐นโ†‘2)))
10711, 29, 154sqlem5 16884 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ โˆˆ โ„ค โˆง ((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค))
108107simpld 494 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ โˆˆ โ„ค)
10912, 29, 164sqlem5 16884 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ป โˆˆ โ„ค โˆง ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค))
110109simpld 494 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ป โˆˆ โ„ค)
111 gzreim 16881 . . . . . . . . . . . . . . . . . 18 ((๐บ โˆˆ โ„ค โˆง ๐ป โˆˆ โ„ค) โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i])
112108, 110, 111syl2anc 583 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i])
113 gzcn 16874 . . . . . . . . . . . . . . . . 17 ((๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i] โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„‚)
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„‚)
115114absvalsq2d 15396 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) + ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2)))
116108zred 12670 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ โˆˆ โ„)
117110zred 12670 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ป โˆˆ โ„)
118116, 117crred 15184 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„œโ€˜(๐บ + (i ยท ๐ป))) = ๐บ)
119118oveq1d 7420 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (๐บโ†‘2))
120116, 117crimd 15185 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„‘โ€˜(๐บ + (i ยท ๐ป))) = ๐ป)
121120oveq1d 7420 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (๐ปโ†‘2))
122119, 121oveq12d 7423 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) + ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = ((๐บโ†‘2) + (๐ปโ†‘2)))
123115, 122eqtrd 2766 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = ((๐บโ†‘2) + (๐ปโ†‘2)))
124106, 123oveq12d 7423 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = (((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))))
125124oveq1d 7420 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€) = ((((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))) / ๐‘€))
126125, 17eqtr4di 2784 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€) = ๐‘…)
12789, 126oveq12d 7423 . . . . . . . . . 10 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) = (๐‘ƒ ยท ๐‘…))
12855nncnd 12232 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
12987, 128mulcomd 11239 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘…) = (๐‘… ยท ๐‘ƒ))
130127, 129eqtrd 2766 . . . . . . . . 9 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) = (๐‘… ยท ๐‘ƒ))
131 eqid 2726 . . . . . . . . . 10 (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2))
132 eqid 2726 . . . . . . . . . 10 (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2))
1339zcnd 12671 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
134 ax-icn 11171 . . . . . . . . . . . . . . . 16 i โˆˆ โ„‚
13510zcnd 12671 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
136 mulcl 11196 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (i ยท ๐ต) โˆˆ โ„‚)
137134, 135, 136sylancr 586 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ต) โˆˆ โ„‚)
13891zcnd 12671 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
13993zcnd 12671 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐น โˆˆ โ„‚)
140 mulcl 11196 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐น โˆˆ โ„‚) โ†’ (i ยท ๐น) โˆˆ โ„‚)
141134, 139, 140sylancr 586 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐น) โˆˆ โ„‚)
142133, 137, 138, 141addsub4d 11622 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) = ((๐ด โˆ’ ๐ธ) + ((i ยท ๐ต) โˆ’ (i ยท ๐น))))
143134a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ i โˆˆ โ„‚)
144143, 135, 139subdid 11674 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท (๐ต โˆ’ ๐น)) = ((i ยท ๐ต) โˆ’ (i ยท ๐น)))
145144oveq2d 7421 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) = ((๐ด โˆ’ ๐ธ) + ((i ยท ๐ต) โˆ’ (i ยท ๐น))))
146142, 145eqtr4d 2769 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) = ((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))))
147146oveq1d 7420 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) / ๐‘€))
148133, 138subcld 11575 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ด โˆ’ ๐ธ) โˆˆ โ„‚)
149135, 139subcld 11575 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต โˆ’ ๐น) โˆˆ โ„‚)
150 mulcl 11196 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง (๐ต โˆ’ ๐น) โˆˆ โ„‚) โ†’ (i ยท (๐ต โˆ’ ๐น)) โˆˆ โ„‚)
151134, 149, 150sylancr 586 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (i ยท (๐ต โˆ’ ๐น)) โˆˆ โ„‚)
152148, 151, 33, 39divdird 12032 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€)))
153143, 149, 33, 39divassd 12029 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€) = (i ยท ((๐ต โˆ’ ๐น) / ๐‘€)))
154153oveq2d 7421 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€)) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))))
155147, 152, 1543eqtrd 2770 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))))
15690simprd 495 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค)
15792simprd 495 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค)
158 gzreim 16881 . . . . . . . . . . . 12 ((((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค โˆง ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค) โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))) โˆˆ โ„ค[i])
159156, 157, 158syl2anc 583 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))) โˆˆ โ„ค[i])
160155, 159eqeltrd 2827 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) โˆˆ โ„ค[i])
16111zcnd 12671 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
16212zcnd 12671 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
163 mulcl 11196 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚) โ†’ (i ยท ๐ท) โˆˆ โ„‚)
164134, 162, 163sylancr 586 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ท) โˆˆ โ„‚)
165108zcnd 12671 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
166110zcnd 12671 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ป โˆˆ โ„‚)
167 mulcl 11196 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ป โˆˆ โ„‚) โ†’ (i ยท ๐ป) โˆˆ โ„‚)
168134, 166, 167sylancr 586 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ป) โˆˆ โ„‚)
169161, 164, 165, 168addsub4d 11622 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) = ((๐ถ โˆ’ ๐บ) + ((i ยท ๐ท) โˆ’ (i ยท ๐ป))))
170143, 162, 166subdid 11674 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท (๐ท โˆ’ ๐ป)) = ((i ยท ๐ท) โˆ’ (i ยท ๐ป)))
171170oveq2d 7421 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) = ((๐ถ โˆ’ ๐บ) + ((i ยท ๐ท) โˆ’ (i ยท ๐ป))))
172169, 171eqtr4d 2769 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) = ((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))))
173172oveq1d 7420 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) / ๐‘€))
174161, 165subcld 11575 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ถ โˆ’ ๐บ) โˆˆ โ„‚)
175162, 166subcld 11575 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท โˆ’ ๐ป) โˆˆ โ„‚)
176 mulcl 11196 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง (๐ท โˆ’ ๐ป) โˆˆ โ„‚) โ†’ (i ยท (๐ท โˆ’ ๐ป)) โˆˆ โ„‚)
177134, 175, 176sylancr 586 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (i ยท (๐ท โˆ’ ๐ป)) โˆˆ โ„‚)
178174, 177, 33, 39divdird 12032 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€)))
179143, 175, 33, 39divassd 12029 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€) = (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€)))
180179oveq2d 7421 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€)) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))))
181173, 178, 1803eqtrd 2770 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))))
182107simprd 495 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค)
183109simprd 495 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค)
184 gzreim 16881 . . . . . . . . . . . 12 ((((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค โˆง ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค) โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))) โˆˆ โ„ค[i])
185182, 183, 184syl2anc 583 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))) โˆˆ โ„ค[i])
186181, 185eqeltrd 2827 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) โˆˆ โ„ค[i])
18786nnnn0d 12536 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•0)
18889, 187eqeltrd 2827 . . . . . . . . . 10 (๐œ‘ โ†’ ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) โˆˆ โ„•0)
1891, 57, 70, 95, 112, 131, 132, 29, 160, 186, 188mul4sqlem 16895 . . . . . . . . 9 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) โˆˆ ๐‘†)
190130, 189eqeltrrd 2828 . . . . . . . 8 (๐œ‘ โ†’ (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†)
191 oveq1 7412 . . . . . . . . . 10 (๐‘– = ๐‘… โ†’ (๐‘– ยท ๐‘ƒ) = (๐‘… ยท ๐‘ƒ))
192191eleq1d 2812 . . . . . . . . 9 (๐‘– = ๐‘… โ†’ ((๐‘– ยท ๐‘ƒ) โˆˆ ๐‘† โ†” (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†))
193192, 6elrab2 3681 . . . . . . . 8 (๐‘… โˆˆ ๐‘‡ โ†” (๐‘… โˆˆ โ„• โˆง (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†))
19455, 190, 193sylanbrc 582 . . . . . . 7 (๐œ‘ โ†’ ๐‘… โˆˆ ๐‘‡)
195 infssuzle 12919 . . . . . . 7 ((๐‘‡ โІ (โ„คโ‰ฅโ€˜1) โˆง ๐‘… โˆˆ ๐‘‡) โ†’ inf(๐‘‡, โ„, < ) โ‰ค ๐‘…)
19623, 194, 195sylancr 586 . . . . . 6 (๐œ‘ โ†’ inf(๐‘‡, โ„, < ) โ‰ค ๐‘…)
1977, 196eqbrtrid 5176 . . . . 5 (๐œ‘ โ†’ ๐‘€ โ‰ค ๐‘…)
19855nnred 12231 . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ โ„)
199198, 30letri3d 11360 . . . . 5 (๐œ‘ โ†’ (๐‘… = ๐‘€ โ†” (๐‘… โ‰ค ๐‘€ โˆง ๐‘€ โ‰ค ๐‘…)))
20020, 197, 199mpbir2and 710 . . . 4 (๐œ‘ โ†’ ๐‘… = ๐‘€)
201200olcd 871 . . 3 (๐œ‘ โ†’ (๐‘… = 0 โˆจ ๐‘… = ๐‘€))
202201, 52mpd 15 . 2 (๐œ‘ โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ))
203202, 46pm2.65i 193 1 ยฌ ๐œ‘
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆจ wo 844   = wceq 1533   โˆˆ wcel 2098  {cab 2703   โ‰  wne 2934  โˆƒwrex 3064  {crab 3426   โІ wss 3943  โˆ…c0 4317   class class class wbr 5141  โ€˜cfv 6537  (class class class)co 7405  infcinf 9438  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113  ici 11114   + caddc 11115   ยท cmul 11117   < clt 11252   โ‰ค cle 11253   โˆ’ cmin 11448   / cdiv 11875  โ„•cn 12216  2c2 12271  โ„•0cn0 12476  โ„คcz 12562  โ„คโ‰ฅcuz 12826  ...cfz 13490   mod cmo 13840  โ†‘cexp 14032  โ„œcre 15050  โ„‘cim 15051  abscabs 15187   โˆฅ cdvds 16204  โ„™cprime 16615  โ„ค[i]cgz 16871
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-oadd 8471  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-rp 12981  df-fz 13491  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-hash 14296  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16205  df-gcd 16443  df-prm 16616  df-gz 16872
This theorem is referenced by:  4sqlem18  16904
  Copyright terms: Public domain W3C validator