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

Theorem 4sqlem17 16840
Description: Lemma for 4sq 16843. (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 16839 . . . . . 6 (๐œ‘ โ†’ (๐‘… โ‰ค ๐‘€ โˆง ((๐‘… = 0 โˆจ ๐‘… = ๐‘€) โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ))))
2019simpld 496 . . . . 5 (๐œ‘ โ†’ ๐‘… โ‰ค ๐‘€)
216ssrab3 4045 . . . . . . . 8 ๐‘‡ โŠ† โ„•
22 nnuz 12813 . . . . . . . 8 โ„• = (โ„คโ‰ฅโ€˜1)
2321, 22sseqtri 3985 . . . . . . 7 ๐‘‡ โŠ† (โ„คโ‰ฅโ€˜1)
241, 2, 3, 4, 5, 6, 74sqlem13 16836 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐‘‡ โ‰  โˆ… โˆง ๐‘€ < ๐‘ƒ))
2524simpld 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐‘‡ โ‰  โˆ…)
26 infssuzcl 12864 . . . . . . . . . . . . . . 15 ((๐‘‡ โŠ† (โ„คโ‰ฅโ€˜1) โˆง ๐‘‡ โ‰  โˆ…) โ†’ inf(๐‘‡, โ„, < ) โˆˆ ๐‘‡)
2723, 25, 26sylancr 588 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ inf(๐‘‡, โ„, < ) โˆˆ ๐‘‡)
287, 27eqeltrid 2842 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘‡)
2921, 28sselid 3947 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
3029nnred 12175 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„)
3124simprd 497 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ < ๐‘ƒ)
3230, 31ltned 11298 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘€ โ‰  ๐‘ƒ)
3329nncnd 12176 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„‚)
3433sqvald 14055 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘€โ†‘2) = (๐‘€ ยท ๐‘€))
3534breq1d 5120 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” (๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ)))
3629nnzd 12533 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
37 prmz 16558 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
384, 37syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„ค)
3929nnne0d 12210 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘€ โ‰  0)
40 dvdscmulr 16174 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค โˆง (๐‘€ โˆˆ โ„ค โˆง ๐‘€ โ‰  0)) โ†’ ((๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โˆฅ ๐‘ƒ))
4136, 38, 36, 39, 40syl112anc 1375 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘€) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ โˆฅ ๐‘ƒ))
42 dvdsprm 16586 . . . . . . . . . . . . 13 ((๐‘€ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ƒ โˆˆ โ„™) โ†’ (๐‘€ โˆฅ ๐‘ƒ โ†” ๐‘€ = ๐‘ƒ))
438, 4, 42syl2anc 585 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘€ โˆฅ ๐‘ƒ โ†” ๐‘€ = ๐‘ƒ))
4435, 41, 433bitrd 305 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ) โ†” ๐‘€ = ๐‘ƒ))
4544necon3bbid 2982 . . . . . . . . . 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 16837 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘… โˆˆ โ„•0)
48 elnn0 12422 . . . . . . . . . . . 12 (๐‘… โˆˆ โ„•0 โ†” (๐‘… โˆˆ โ„• โˆจ ๐‘… = 0))
4947, 48sylib 217 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘… โˆˆ โ„• โˆจ ๐‘… = 0))
5049ord 863 . . . . . . . . . 10 (๐œ‘ โ†’ (ยฌ ๐‘… โˆˆ โ„• โ†’ ๐‘… = 0))
51 orc 866 . . . . . . . . . . 11 (๐‘… = 0 โ†’ (๐‘… = 0 โˆจ ๐‘… = ๐‘€))
5219simprd 497 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐‘… = 0 โˆจ ๐‘… = ๐‘€) โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5351, 52syl5 34 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘… = 0 โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5450, 53syld 47 . . . . . . . . 9 (๐œ‘ โ†’ (ยฌ ๐‘… โˆˆ โ„• โ†’ (๐‘€โ†‘2) โˆฅ (๐‘€ ยท ๐‘ƒ)))
5546, 54mt3d 148 . . . . . . . 8 (๐œ‘ โ†’ ๐‘… โˆˆ โ„•)
56 gzreim 16818 . . . . . . . . . . . . . . . . . . 19 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i])
579, 10, 56syl2anc 585 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i])
58 gzcn 16811 . . . . . . . . . . . . . . . . . 18 ((๐ด + (i ยท ๐ต)) โˆˆ โ„ค[i] โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„‚)
5957, 58syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ด + (i ยท ๐ต)) โˆˆ โ„‚)
6059absvalsq2d 15335 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2)))
619zred 12614 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
6210zred 12614 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
6361, 62crred 15123 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„œโ€˜(๐ด + (i ยท ๐ต))) = ๐ด)
6463oveq1d 7377 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (๐ดโ†‘2))
6561, 62crimd 15124 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„‘โ€˜(๐ด + (i ยท ๐ต))) = ๐ต)
6665oveq1d 7377 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = (๐ตโ†‘2))
6764, 66oveq12d 7380 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โ„œโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((โ„‘โ€˜(๐ด + (i ยท ๐ต)))โ†‘2)) = ((๐ดโ†‘2) + (๐ตโ†‘2)))
6860, 67eqtrd 2777 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) = ((๐ดโ†‘2) + (๐ตโ†‘2)))
69 gzreim 16818 . . . . . . . . . . . . . . . . . . 19 ((๐ถ โˆˆ โ„ค โˆง ๐ท โˆˆ โ„ค) โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i])
7011, 12, 69syl2anc 585 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i])
71 gzcn 16811 . . . . . . . . . . . . . . . . . 18 ((๐ถ + (i ยท ๐ท)) โˆˆ โ„ค[i] โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„‚)
7270, 71syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ถ + (i ยท ๐ท)) โˆˆ โ„‚)
7372absvalsq2d 15335 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) + ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)))
7411zred 12614 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ถ โˆˆ โ„)
7512zred 12614 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ๐ท โˆˆ โ„)
7674, 75crred 15123 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„œโ€˜(๐ถ + (i ยท ๐ท))) = ๐ถ)
7776oveq1d 7377 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (๐ถโ†‘2))
7874, 75crimd 15124 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โ„‘โ€˜(๐ถ + (i ยท ๐ท))) = ๐ท)
7978oveq1d 7377 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = (๐ทโ†‘2))
8077, 79oveq12d 7380 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โ„œโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) + ((โ„‘โ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = ((๐ถโ†‘2) + (๐ทโ†‘2)))
8173, 80eqtrd 2777 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2) = ((๐ถโ†‘2) + (๐ทโ†‘2)))
8268, 81oveq12d 7380 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = (((๐ดโ†‘2) + (๐ตโ†‘2)) + ((๐ถโ†‘2) + (๐ทโ†‘2))))
8318, 82eqtr4d 2780 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐‘€ ยท ๐‘ƒ) = (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)))
8483oveq1d 7377 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘ƒ) / ๐‘€) = ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€))
85 prmnn 16557 . . . . . . . . . . . . . . 15 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
864, 85syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•)
8786nncnd 12176 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
8887, 33, 39divcan3d 11943 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐‘€ ยท ๐‘ƒ) / ๐‘€) = ๐‘ƒ)
8984, 88eqtr3d 2779 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) = ๐‘ƒ)
909, 29, 134sqlem5 16821 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ธ โˆˆ โ„ค โˆง ((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค))
9190simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ธ โˆˆ โ„ค)
9210, 29, 144sqlem5 16821 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐น โˆˆ โ„ค โˆง ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค))
9392simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐น โˆˆ โ„ค)
94 gzreim 16818 . . . . . . . . . . . . . . . . . 18 ((๐ธ โˆˆ โ„ค โˆง ๐น โˆˆ โ„ค) โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i])
9591, 93, 94syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i])
96 gzcn 16811 . . . . . . . . . . . . . . . . 17 ((๐ธ + (i ยท ๐น)) โˆˆ โ„ค[i] โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„‚)
9795, 96syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ธ + (i ยท ๐น)) โˆˆ โ„‚)
9897absvalsq2d 15335 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2)))
9991zred 12614 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
10093zred 12614 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐น โˆˆ โ„)
10199, 100crred 15123 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„œโ€˜(๐ธ + (i ยท ๐น))) = ๐ธ)
102101oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (๐ธโ†‘2))
10399, 100crimd 15124 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„‘โ€˜(๐ธ + (i ยท ๐น))) = ๐น)
104103oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = (๐นโ†‘2))
105102, 104oveq12d 7380 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โ„œโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((โ„‘โ€˜(๐ธ + (i ยท ๐น)))โ†‘2)) = ((๐ธโ†‘2) + (๐นโ†‘2)))
10698, 105eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) = ((๐ธโ†‘2) + (๐นโ†‘2)))
10711, 29, 154sqlem5 16821 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐บ โˆˆ โ„ค โˆง ((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค))
108107simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ โˆˆ โ„ค)
10912, 29, 164sqlem5 16821 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ป โˆˆ โ„ค โˆง ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค))
110109simpld 496 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ป โˆˆ โ„ค)
111 gzreim 16818 . . . . . . . . . . . . . . . . . 18 ((๐บ โˆˆ โ„ค โˆง ๐ป โˆˆ โ„ค) โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i])
112108, 110, 111syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i])
113 gzcn 16811 . . . . . . . . . . . . . . . . 17 ((๐บ + (i ยท ๐ป)) โˆˆ โ„ค[i] โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„‚)
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐บ + (i ยท ๐ป)) โˆˆ โ„‚)
115114absvalsq2d 15335 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) + ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2)))
116108zred 12614 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐บ โˆˆ โ„)
117110zred 12614 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ป โˆˆ โ„)
118116, 117crred 15123 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„œโ€˜(๐บ + (i ยท ๐ป))) = ๐บ)
119118oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (๐บโ†‘2))
120116, 117crimd 15124 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โ„‘โ€˜(๐บ + (i ยท ๐ป))) = ๐ป)
121120oveq1d 7377 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = (๐ปโ†‘2))
122119, 121oveq12d 7380 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((โ„œโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) + ((โ„‘โ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = ((๐บโ†‘2) + (๐ปโ†‘2)))
123115, 122eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2) = ((๐บโ†‘2) + (๐ปโ†‘2)))
124106, 123oveq12d 7380 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = (((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))))
125124oveq1d 7377 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€) = ((((๐ธโ†‘2) + (๐นโ†‘2)) + ((๐บโ†‘2) + (๐ปโ†‘2))) / ๐‘€))
126125, 17eqtr4di 2795 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€) = ๐‘…)
12789, 126oveq12d 7380 . . . . . . . . . 10 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) = (๐‘ƒ ยท ๐‘…))
12855nncnd 12176 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
12987, 128mulcomd 11183 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ƒ ยท ๐‘…) = (๐‘… ยท ๐‘ƒ))
130127, 129eqtrd 2777 . . . . . . . . 9 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) = (๐‘… ยท ๐‘ƒ))
131 eqid 2737 . . . . . . . . . 10 (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) = (((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2))
132 eqid 2737 . . . . . . . . . 10 (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) = (((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2))
1339zcnd 12615 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
134 ax-icn 11117 . . . . . . . . . . . . . . . 16 i โˆˆ โ„‚
13510zcnd 12615 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
136 mulcl 11142 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚) โ†’ (i ยท ๐ต) โˆˆ โ„‚)
137134, 135, 136sylancr 588 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ต) โˆˆ โ„‚)
13891zcnd 12615 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
13993zcnd 12615 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐น โˆˆ โ„‚)
140 mulcl 11142 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐น โˆˆ โ„‚) โ†’ (i ยท ๐น) โˆˆ โ„‚)
141134, 139, 140sylancr 588 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐น) โˆˆ โ„‚)
142133, 137, 138, 141addsub4d 11566 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) = ((๐ด โˆ’ ๐ธ) + ((i ยท ๐ต) โˆ’ (i ยท ๐น))))
143134a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ i โˆˆ โ„‚)
144143, 135, 139subdid 11618 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท (๐ต โˆ’ ๐น)) = ((i ยท ๐ต) โˆ’ (i ยท ๐น)))
145144oveq2d 7378 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) = ((๐ด โˆ’ ๐ธ) + ((i ยท ๐ต) โˆ’ (i ยท ๐น))))
146142, 145eqtr4d 2780 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) = ((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))))
147146oveq1d 7377 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) / ๐‘€))
148133, 138subcld 11519 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ด โˆ’ ๐ธ) โˆˆ โ„‚)
149135, 139subcld 11519 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต โˆ’ ๐น) โˆˆ โ„‚)
150 mulcl 11142 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง (๐ต โˆ’ ๐น) โˆˆ โ„‚) โ†’ (i ยท (๐ต โˆ’ ๐น)) โˆˆ โ„‚)
151134, 149, 150sylancr 588 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (i ยท (๐ต โˆ’ ๐น)) โˆˆ โ„‚)
152148, 151, 33, 39divdird 11976 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) + (i ยท (๐ต โˆ’ ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€)))
153143, 149, 33, 39divassd 11973 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€) = (i ยท ((๐ต โˆ’ ๐น) / ๐‘€)))
154153oveq2d 7378 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + ((i ยท (๐ต โˆ’ ๐น)) / ๐‘€)) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))))
155147, 152, 1543eqtrd 2781 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) = (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))))
15690simprd 497 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค)
15792simprd 497 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค)
158 gzreim 16818 . . . . . . . . . . . 12 ((((๐ด โˆ’ ๐ธ) / ๐‘€) โˆˆ โ„ค โˆง ((๐ต โˆ’ ๐น) / ๐‘€) โˆˆ โ„ค) โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))) โˆˆ โ„ค[i])
159156, 157, 158syl2anc 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ด โˆ’ ๐ธ) / ๐‘€) + (i ยท ((๐ต โˆ’ ๐น) / ๐‘€))) โˆˆ โ„ค[i])
160155, 159eqeltrd 2838 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ด + (i ยท ๐ต)) โˆ’ (๐ธ + (i ยท ๐น))) / ๐‘€) โˆˆ โ„ค[i])
16111zcnd 12615 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
16212zcnd 12615 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
163 mulcl 11142 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚) โ†’ (i ยท ๐ท) โˆˆ โ„‚)
164134, 162, 163sylancr 588 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ท) โˆˆ โ„‚)
165108zcnd 12615 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ๐บ โˆˆ โ„‚)
166110zcnd 12615 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ป โˆˆ โ„‚)
167 mulcl 11142 . . . . . . . . . . . . . . . 16 ((i โˆˆ โ„‚ โˆง ๐ป โˆˆ โ„‚) โ†’ (i ยท ๐ป) โˆˆ โ„‚)
168134, 166, 167sylancr 588 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท ๐ป) โˆˆ โ„‚)
169161, 164, 165, 168addsub4d 11566 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) = ((๐ถ โˆ’ ๐บ) + ((i ยท ๐ท) โˆ’ (i ยท ๐ป))))
170143, 162, 166subdid 11618 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (i ยท (๐ท โˆ’ ๐ป)) = ((i ยท ๐ท) โˆ’ (i ยท ๐ป)))
171170oveq2d 7378 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) = ((๐ถ โˆ’ ๐บ) + ((i ยท ๐ท) โˆ’ (i ยท ๐ป))))
172169, 171eqtr4d 2780 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) = ((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))))
173172oveq1d 7377 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) / ๐‘€))
174161, 165subcld 11519 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ถ โˆ’ ๐บ) โˆˆ โ„‚)
175162, 166subcld 11519 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท โˆ’ ๐ป) โˆˆ โ„‚)
176 mulcl 11142 . . . . . . . . . . . . . 14 ((i โˆˆ โ„‚ โˆง (๐ท โˆ’ ๐ป) โˆˆ โ„‚) โ†’ (i ยท (๐ท โˆ’ ๐ป)) โˆˆ โ„‚)
177134, 175, 176sylancr 588 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (i ยท (๐ท โˆ’ ๐ป)) โˆˆ โ„‚)
178174, 177, 33, 39divdird 11976 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) + (i ยท (๐ท โˆ’ ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€)))
179143, 175, 33, 39divassd 11973 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€) = (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€)))
180179oveq2d 7378 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + ((i ยท (๐ท โˆ’ ๐ป)) / ๐‘€)) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))))
181173, 178, 1803eqtrd 2781 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) = (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))))
182107simprd 497 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค)
183109simprd 497 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค)
184 gzreim 16818 . . . . . . . . . . . 12 ((((๐ถ โˆ’ ๐บ) / ๐‘€) โˆˆ โ„ค โˆง ((๐ท โˆ’ ๐ป) / ๐‘€) โˆˆ โ„ค) โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))) โˆˆ โ„ค[i])
185182, 183, 184syl2anc 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ถ โˆ’ ๐บ) / ๐‘€) + (i ยท ((๐ท โˆ’ ๐ป) / ๐‘€))) โˆˆ โ„ค[i])
186181, 185eqeltrd 2838 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ถ + (i ยท ๐ท)) โˆ’ (๐บ + (i ยท ๐ป))) / ๐‘€) โˆˆ โ„ค[i])
18786nnnn0d 12480 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•0)
18889, 187eqeltrd 2838 . . . . . . . . . 10 (๐œ‘ โ†’ ((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) โˆˆ โ„•0)
1891, 57, 70, 95, 112, 131, 132, 29, 160, 186, 188mul4sqlem 16832 . . . . . . . . 9 (๐œ‘ โ†’ (((((absโ€˜(๐ด + (i ยท ๐ต)))โ†‘2) + ((absโ€˜(๐ถ + (i ยท ๐ท)))โ†‘2)) / ๐‘€) ยท ((((absโ€˜(๐ธ + (i ยท ๐น)))โ†‘2) + ((absโ€˜(๐บ + (i ยท ๐ป)))โ†‘2)) / ๐‘€)) โˆˆ ๐‘†)
190130, 189eqeltrrd 2839 . . . . . . . 8 (๐œ‘ โ†’ (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†)
191 oveq1 7369 . . . . . . . . . 10 (๐‘– = ๐‘… โ†’ (๐‘– ยท ๐‘ƒ) = (๐‘… ยท ๐‘ƒ))
192191eleq1d 2823 . . . . . . . . 9 (๐‘– = ๐‘… โ†’ ((๐‘– ยท ๐‘ƒ) โˆˆ ๐‘† โ†” (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†))
193192, 6elrab2 3653 . . . . . . . 8 (๐‘… โˆˆ ๐‘‡ โ†” (๐‘… โˆˆ โ„• โˆง (๐‘… ยท ๐‘ƒ) โˆˆ ๐‘†))
19455, 190, 193sylanbrc 584 . . . . . . 7 (๐œ‘ โ†’ ๐‘… โˆˆ ๐‘‡)
195 infssuzle 12863 . . . . . . 7 ((๐‘‡ โŠ† (โ„คโ‰ฅโ€˜1) โˆง ๐‘… โˆˆ ๐‘‡) โ†’ inf(๐‘‡, โ„, < ) โ‰ค ๐‘…)
19623, 194, 195sylancr 588 . . . . . 6 (๐œ‘ โ†’ inf(๐‘‡, โ„, < ) โ‰ค ๐‘…)
1977, 196eqbrtrid 5145 . . . . 5 (๐œ‘ โ†’ ๐‘€ โ‰ค ๐‘…)
19855nnred 12175 . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ โ„)
199198, 30letri3d 11304 . . . . 5 (๐œ‘ โ†’ (๐‘… = ๐‘€ โ†” (๐‘… โ‰ค ๐‘€ โˆง ๐‘€ โ‰ค ๐‘…)))
20020, 197, 199mpbir2and 712 . . . 4 (๐œ‘ โ†’ ๐‘… = ๐‘€)
201200olcd 873 . . 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 846   = wceq 1542   โˆˆ wcel 2107  {cab 2714   โ‰  wne 2944  โˆƒwrex 3074  {crab 3410   โŠ† wss 3915  โˆ…c0 4287   class class class wbr 5110  โ€˜cfv 6501  (class class class)co 7362  infcinf 9384  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059  ici 11060   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392   / cdiv 11819  โ„•cn 12160  2c2 12215  โ„•0cn0 12420  โ„คcz 12506  โ„คโ‰ฅcuz 12770  ...cfz 13431   mod cmo 13781  โ†‘cexp 13974  โ„œcre 14989  โ„‘cim 14990  abscabs 15126   โˆฅ cdvds 16143  โ„™cprime 16554  โ„ค[i]cgz 16808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-dvds 16144  df-gcd 16382  df-prm 16555  df-gz 16809
This theorem is referenced by:  4sqlem18  16841
  Copyright terms: Public domain W3C validator