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

Theorem 4sqlem17 16929
Description: Lemma for 4sq 16932. (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 16928 . . . . . 6 (๐œ‘ โ†’ (๐‘… โ‰ค ๐‘€ โˆง ((๐‘… = 0 โˆจ ๐‘… = ๐‘€) โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ))))
2019simpld 493 . . . . 5 (๐œ‘ โ†’ ๐‘… โ‰ค ๐‘€)
216ssrab3 4072 . . . . . . . 8 ๐‘‡ โІ โ„•
22 nnuz 12895 . . . . . . . 8 โ„• = (โ„คโ‰ฅโ€˜1)
2321, 22sseqtri 4009 . . . . . . 7 ๐‘‡ โІ (โ„คโ‰ฅโ€˜1)
241, 2, 3, 4, 5, 6, 74sqlem13 16925 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘‡ โ‰  โˆ… โˆง ๐‘€ < ๐‘ƒ))
2524simpld 493 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‡ โ‰  โˆ…)
26 infssuzcl 12946 . . . . . . . . . . . . . . 15 ((๐‘‡ โІ (โ„คโ‰ฅโ€˜1) โˆง ๐‘‡ โ‰  โˆ…) โ†’ inf(๐‘‡, โ„, < ) โˆˆ ๐‘‡)
2723, 25, 26sylancr 585 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ inf(๐‘‡, โ„, < ) โˆˆ ๐‘‡)
287, 27eqeltrid 2829 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘‡)
2921, 28sselid 3970 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
3029nnred 12257 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„)
3124simprd 494 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ < ๐‘ƒ)
3230, 31ltned 11380 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โ‰  ๐‘ƒ)
3329nncnd 12258 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
3433sqvald 14139 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘€โ†‘2) = (๐‘€ ยท ๐‘€))
3534breq1d 5153 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” (๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ)))
3629nnzd 12615 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
37 prmz 16645 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
384, 37syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„ค)
3929nnne0d 12292 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โ‰  0)
40 dvdscmulr 16261 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค โˆง (๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0)) โ†’ ((๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โˆฅ ๐‘ƒ))
4136, 38, 36, 39, 40syl112anc 1371 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โˆฅ ๐‘ƒ))
42 dvdsprm 16673 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘€ โˆฅ ๐‘ƒ โ†” ๐‘€ = ๐‘ƒ))
438, 4, 42syl2anc 582 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘€ โˆฅ ๐‘ƒ โ†” ๐‘€ = ๐‘ƒ))
4435, 41, 433bitrd 304 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ = ๐‘ƒ))
4544necon3bbid 2968 . . . . . . . . . 10 (๐œ‘ โ†’ (ยฌ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โ‰  ๐‘ƒ))
4632, 45mpbird 256 . . . . . . . . 9 (๐œ‘ โ†’ ยฌ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ))
471, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 184sqlem14 16926 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘… โˆˆ โ„•0)
48 elnn0 12504 . . . . . . . . . . . 12 (๐‘… โˆˆ โ„•0 โ†” (๐‘… โˆˆ โ„• โˆจ ๐‘… = 0))
4947, 48sylib 217 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘… โˆˆ โ„• โˆจ ๐‘… = 0))
5049ord 862 . . . . . . . . . 10 (๐œ‘ โ†’ (ยฌ ๐‘… โˆˆ โ„• โ†’ ๐‘… = 0))
51 orc 865 . . . . . . . . . . 11 (๐‘… = 0 โ†’ (๐‘… = 0 โˆจ ๐‘… = ๐‘€))
5219simprd 494 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘… = 0 โˆจ ๐‘… = ๐‘€) โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5351, 52syl5 34 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘… = 0 โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5450, 53syld 47 . . . . . . . . 9 (๐œ‘ โ†’ (ยฌ ๐‘… โˆˆ โ„• โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5546, 54mt3d 148 . . . . . . . 8 (๐œ‘ โ†’ ๐‘… โˆˆ โ„•)
56 gzreim 16907 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i])
579, 10, 56syl2anc 582 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i])
58 gzcn 16900 . . . . . . . . . . . . . . . . . 18 ((๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i] โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„‚)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„‚)
6059absvalsq2d 15422 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2)))
619zred 12696 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
6210zred 12696 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
6361, 62crred 15210 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„œโ€˜(๐ด + (i ยท ๐ต))) = ๐ด)
6463oveq1d 7431 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (๐ดโ†‘2))
6561, 62crimd 15211 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„‘โ€˜(๐ด + (i ยท ๐ต))) = ๐ต)
6665oveq1d 7431 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (๐ตโ†‘2))
6764, 66oveq12d 7434 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2)) = ((๐ดโ†‘2) + (๐ตโ†‘2)))
6860, 67eqtrd 2765 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = ((๐ดโ†‘2) + (๐ตโ†‘2)))
69 gzreim 16907 . . . . . . . . . . . . . . . . . . 19 ((๐ถ โˆˆ โ„ค โˆง ๐ท โˆˆ โ„ค) โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i])
7011, 12, 69syl2anc 582 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i])
71 gzcn 16900 . . . . . . . . . . . . . . . . . 18 ((๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i] โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„‚)
7270, 71syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„‚)
7372absvalsq2d 15422 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) + ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)))
7411zred 12696 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ถ โˆˆ โ„)
7512zred 12696 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ท โˆˆ โ„)
7674, 75crred 15210 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„œโ€˜(๐ถ + (i ยท ๐ท))) = ๐ถ)
7776oveq1d 7431 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (๐ถโ†‘2))
7874, 75crimd 15211 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„‘โ€˜(๐ถ + (i ยท ๐ท))) = ๐ท)
7978oveq1d 7431 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (๐ทโ†‘2))
8077, 79oveq12d 7434 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) + ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = ((๐ถโ†‘2) + (๐ทโ†‘2)))
8173, 80eqtrd 2765 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = ((๐ถโ†‘2) + (๐ทโ†‘2)))
8268, 81oveq12d 7434 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = (((๐ดโ†‘2) + (๐ตโ†‘2)) + ((๐ถโ†‘2) + (๐ทโ†‘2))))
8318, 82eqtr4d 2768 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘€ ยท ๐‘ƒ) = (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)))
8483oveq1d 7431 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘ƒ) / ๐‘€) = ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€))
85 prmnn 16644 . . . . . . . . . . . . . . 15 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
864, 85syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•)
8786nncnd 12258 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
8887, 33, 39divcan3d 12025 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘ƒ) / ๐‘€) = ๐‘ƒ)
8984, 88eqtr3d 2767 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) = ๐‘ƒ)
909, 29, 134sqlem5 16910 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ธ โˆˆ โ„ค โˆง ((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค))
9190simpld 493 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ธ โˆˆ โ„ค)
9210, 29, 144sqlem5 16910 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐น โˆˆ โ„ค โˆง ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค))
9392simpld 493 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐น โˆˆ โ„ค)
94 gzreim 16907 . . . . . . . . . . . . . . . . . 18 ((๐ธ โˆˆ โ„ค โˆง ๐น โˆˆ โ„ค) โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i])
9591, 93, 94syl2anc 582 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i])
96 gzcn 16900 . . . . . . . . . . . . . . . . 17 ((๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i] โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„‚)
9795, 96syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„‚)
9897absvalsq2d 15422 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2)))
9991zred 12696 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
10093zred 12696 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐น โˆˆ โ„)
10199, 100crred 15210 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„œโ€˜(๐ธ + (i ยท ๐น))) = ๐ธ)
102101oveq1d 7431 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (๐ธโ†‘2))
10399, 100crimd 15211 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„‘โ€˜(๐ธ + (i ยท ๐น))) = ๐น)
104103oveq1d 7431 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (๐นโ†‘2))
105102, 104oveq12d 7434 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2)) = ((๐ธโ†‘2) + (๐นโ†‘2)))
10698, 105eqtrd 2765 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = ((๐ธโ†‘2) + (๐นโ†‘2)))
10711, 29, 154sqlem5 16910 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ โˆˆ โ„ค โˆง ((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค))
108107simpld 493 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ โˆˆ โ„ค)
10912, 29, 164sqlem5 16910 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ป โˆˆ โ„ค โˆง ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค))
110109simpld 493 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ป โˆˆ โ„ค)
111 gzreim 16907 . . . . . . . . . . . . . . . . . 18 ((๐บ โˆˆ โ„ค โˆง ๐ป โˆˆ โ„ค) โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i])
112108, 110, 111syl2anc 582 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i])
113 gzcn 16900 . . . . . . . . . . . . . . . . 17 ((๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i] โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„‚)
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„‚)
115114absvalsq2d 15422 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) + ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2)))
116108zred 12696 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ โˆˆ โ„)
117110zred 12696 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ป โˆˆ โ„)
118116, 117crred 15210 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„œโ€˜(๐บ + (i ยท ๐ป))) = ๐บ)
119118oveq1d 7431 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (๐บโ†‘2))
120116, 117crimd 15211 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„‘โ€˜(๐บ + (i ยท ๐ป))) = ๐ป)
121120oveq1d 7431 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (๐ปโ†‘2))
122119, 121oveq12d 7434 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) + ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = ((๐บโ†‘2) + (๐ปโ†‘2)))
123115, 122eqtrd 2765 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = ((๐บโ†‘2) + (๐ปโ†‘2)))
124106, 123oveq12d 7434 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = (((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))))
125124oveq1d 7431 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€) = ((((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))) / ๐‘€))
126125, 17eqtr4di 2783 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€) = ๐‘…)
12789, 126oveq12d 7434 . . . . . . . . . 10 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) = (๐‘ƒ ยท ๐‘…))
12855nncnd 12258 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
12987, 128mulcomd 11265 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘…) = (๐‘… ยท ๐‘ƒ))
130127, 129eqtrd 2765 . . . . . . . . 9 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) = (๐‘… ยท ๐‘ƒ))
131 eqid 2725 . . . . . . . . . 10 (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2))
132 eqid 2725 . . . . . . . . . 10 (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2))
1339zcnd 12697 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
134 ax-icn 11197 . . . . . . . . . . . . . . . 16 i โˆˆ โ„‚
13510zcnd 12697 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
136 mulcl 11222 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (i ยท ๐ต) โˆˆ โ„‚)
137134, 135, 136sylancr 585 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ต) โˆˆ โ„‚)
13891zcnd 12697 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
13993zcnd 12697 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐น โˆˆ โ„‚)
140 mulcl 11222 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐น โˆˆ โ„‚) โ†’ (i ยท ๐น) โˆˆ โ„‚)
141134, 139, 140sylancr 585 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐น) โˆˆ โ„‚)
142133, 137, 138, 141addsub4d 11648 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) = ((๐ด โˆ’ ๐ธ) + ((i ยท ๐ต) โˆ’ (i ยท ๐น))))
143134a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ i โˆˆ โ„‚)
144143, 135, 139subdid 11700 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท (๐ต โˆ’ ๐น)) = ((i ยท ๐ต) โˆ’ (i ยท ๐น)))
145144oveq2d 7432 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) = ((๐ด โˆ’ ๐ธ) + ((i ยท ๐ต) โˆ’ (i ยท ๐น))))
146142, 145eqtr4d 2768 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) = ((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))))
147146oveq1d 7431 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) / ๐‘€))
148133, 138subcld 11601 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ด โˆ’ ๐ธ) โˆˆ โ„‚)
149135, 139subcld 11601 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต โˆ’ ๐น) โˆˆ โ„‚)
150 mulcl 11222 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง (๐ต โˆ’ ๐น) โˆˆ โ„‚) โ†’ (i ยท (๐ต โˆ’ ๐น)) โˆˆ โ„‚)
151134, 149, 150sylancr 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (i ยท (๐ต โˆ’ ๐น)) โˆˆ โ„‚)
152148, 151, 33, 39divdird 12058 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€)))
153143, 149, 33, 39divassd 12055 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€) = (i ยท ((๐ต โˆ’ ๐น) / ๐‘€)))
154153oveq2d 7432 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€)) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))))
155147, 152, 1543eqtrd 2769 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))))
15690simprd 494 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค)
15792simprd 494 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค)
158 gzreim 16907 . . . . . . . . . . . 12 ((((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค โˆง ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค) โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))) โˆˆ โ„ค[i])
159156, 157, 158syl2anc 582 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))) โˆˆ โ„ค[i])
160155, 159eqeltrd 2825 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) โˆˆ โ„ค[i])
16111zcnd 12697 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
16212zcnd 12697 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
163 mulcl 11222 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚) โ†’ (i ยท ๐ท) โˆˆ โ„‚)
164134, 162, 163sylancr 585 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ท) โˆˆ โ„‚)
165108zcnd 12697 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
166110zcnd 12697 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ป โˆˆ โ„‚)
167 mulcl 11222 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ป โˆˆ โ„‚) โ†’ (i ยท ๐ป) โˆˆ โ„‚)
168134, 166, 167sylancr 585 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ป) โˆˆ โ„‚)
169161, 164, 165, 168addsub4d 11648 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) = ((๐ถ โˆ’ ๐บ) + ((i ยท ๐ท) โˆ’ (i ยท ๐ป))))
170143, 162, 166subdid 11700 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท (๐ท โˆ’ ๐ป)) = ((i ยท ๐ท) โˆ’ (i ยท ๐ป)))
171170oveq2d 7432 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) = ((๐ถ โˆ’ ๐บ) + ((i ยท ๐ท) โˆ’ (i ยท ๐ป))))
172169, 171eqtr4d 2768 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) = ((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))))
173172oveq1d 7431 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) / ๐‘€))
174161, 165subcld 11601 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ถ โˆ’ ๐บ) โˆˆ โ„‚)
175162, 166subcld 11601 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท โˆ’ ๐ป) โˆˆ โ„‚)
176 mulcl 11222 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง (๐ท โˆ’ ๐ป) โˆˆ โ„‚) โ†’ (i ยท (๐ท โˆ’ ๐ป)) โˆˆ โ„‚)
177134, 175, 176sylancr 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (i ยท (๐ท โˆ’ ๐ป)) โˆˆ โ„‚)
178174, 177, 33, 39divdird 12058 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€)))
179143, 175, 33, 39divassd 12055 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€) = (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€)))
180179oveq2d 7432 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€)) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))))
181173, 178, 1803eqtrd 2769 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))))
182107simprd 494 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค)
183109simprd 494 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค)
184 gzreim 16907 . . . . . . . . . . . 12 ((((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค โˆง ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค) โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))) โˆˆ โ„ค[i])
185182, 183, 184syl2anc 582 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))) โˆˆ โ„ค[i])
186181, 185eqeltrd 2825 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) โˆˆ โ„ค[i])
18786nnnn0d 12562 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•0)
18889, 187eqeltrd 2825 . . . . . . . . . 10 (๐œ‘ โ†’ ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) โˆˆ โ„•0)
1891, 57, 70, 95, 112, 131, 132, 29, 160, 186, 188mul4sqlem 16921 . . . . . . . . 9 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) โˆˆ ๐‘†)
190130, 189eqeltrrd 2826 . . . . . . . 8 (๐œ‘ โ†’ (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†)
191 oveq1 7423 . . . . . . . . . 10 (๐‘– = ๐‘… โ†’ (๐‘– ยท ๐‘ƒ) = (๐‘… ยท ๐‘ƒ))
192191eleq1d 2810 . . . . . . . . 9 (๐‘– = ๐‘… โ†’ ((๐‘– ยท ๐‘ƒ) โˆˆ ๐‘† โ†” (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†))
193192, 6elrab2 3677 . . . . . . . 8 (๐‘… โˆˆ ๐‘‡ โ†” (๐‘… โˆˆ โ„• โˆง (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†))
19455, 190, 193sylanbrc 581 . . . . . . 7 (๐œ‘ โ†’ ๐‘… โˆˆ ๐‘‡)
195 infssuzle 12945 . . . . . . 7 ((๐‘‡ โІ (โ„คโ‰ฅโ€˜1) โˆง ๐‘… โˆˆ ๐‘‡) โ†’ inf(๐‘‡, โ„, < ) โ‰ค ๐‘…)
19623, 194, 195sylancr 585 . . . . . 6 (๐œ‘ โ†’ inf(๐‘‡, โ„, < ) โ‰ค ๐‘…)
1977, 196eqbrtrid 5178 . . . . 5 (๐œ‘ โ†’ ๐‘€ โ‰ค ๐‘…)
19855nnred 12257 . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ โ„)
199198, 30letri3d 11386 . . . . 5 (๐œ‘ โ†’ (๐‘… = ๐‘€ โ†” (๐‘… โ‰ค ๐‘€ โˆง ๐‘€ โ‰ค ๐‘…)))
20020, 197, 199mpbir2and 711 . . . 4 (๐œ‘ โ†’ ๐‘… = ๐‘€)
201200olcd 872 . . 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 845   = wceq 1533   โˆˆ wcel 2098  {cab 2702   โ‰  wne 2930  โˆƒwrex 3060  {crab 3419   โІ wss 3939  โˆ…c0 4318   class class class wbr 5143  โ€˜cfv 6543  (class class class)co 7416  infcinf 9464  โ„‚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  โ„•0cn0 12502  โ„คcz 12588  โ„คโ‰ฅcuz 12852  ...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:  4sqlem18  16930
  Copyright terms: Public domain W3C validator