Metamath Proof Explorer


Theorem 4sqlem18

Description: Lemma for 4sq . Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses 4sq.1 โŠข ๐‘† = { ๐‘› โˆฃ โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„ค โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„ค ๐‘› = ( ( ( ๐‘ฅ โ†‘ 2 ) + ( ๐‘ฆ โ†‘ 2 ) ) + ( ( ๐‘ง โ†‘ 2 ) + ( ๐‘ค โ†‘ 2 ) ) ) }
4sq.2 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
4sq.3 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( ( 2 ยท ๐‘ ) + 1 ) )
4sq.4 โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™ )
4sq.5 โŠข ( ๐œ‘ โ†’ ( 0 ... ( 2 ยท ๐‘ ) ) โІ ๐‘† )
4sq.6 โŠข ๐‘‡ = { ๐‘– โˆˆ โ„• โˆฃ ( ๐‘– ยท ๐‘ƒ ) โˆˆ ๐‘† }
4sq.7 โŠข ๐‘€ = inf ( ๐‘‡ , โ„ , < )
Assertion 4sqlem18 ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ๐‘† )

Proof

Step Hyp Ref Expression
1 4sq.1 โŠข ๐‘† = { ๐‘› โˆฃ โˆƒ ๐‘ฅ โˆˆ โ„ค โˆƒ ๐‘ฆ โˆˆ โ„ค โˆƒ ๐‘ง โˆˆ โ„ค โˆƒ ๐‘ค โˆˆ โ„ค ๐‘› = ( ( ( ๐‘ฅ โ†‘ 2 ) + ( ๐‘ฆ โ†‘ 2 ) ) + ( ( ๐‘ง โ†‘ 2 ) + ( ๐‘ค โ†‘ 2 ) ) ) }
2 4sq.2 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
3 4sq.3 โŠข ( ๐œ‘ โ†’ ๐‘ƒ = ( ( 2 ยท ๐‘ ) + 1 ) )
4 4sq.4 โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„™ )
5 4sq.5 โŠข ( ๐œ‘ โ†’ ( 0 ... ( 2 ยท ๐‘ ) ) โІ ๐‘† )
6 4sq.6 โŠข ๐‘‡ = { ๐‘– โˆˆ โ„• โˆฃ ( ๐‘– ยท ๐‘ƒ ) โˆˆ ๐‘† }
7 4sq.7 โŠข ๐‘€ = inf ( ๐‘‡ , โ„ , < )
8 prmnn โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„• )
9 4 8 syl โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„• )
10 9 nncnd โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚ )
11 10 mullidd โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘ƒ ) = ๐‘ƒ )
12 6 ssrab3 โŠข ๐‘‡ โІ โ„•
13 nnuz โŠข โ„• = ( โ„คโ‰ฅ โ€˜ 1 )
14 12 13 sseqtri โŠข ๐‘‡ โІ ( โ„คโ‰ฅ โ€˜ 1 )
15 1 2 3 4 5 6 7 4sqlem13 โŠข ( ๐œ‘ โ†’ ( ๐‘‡ โ‰  โˆ… โˆง ๐‘€ < ๐‘ƒ ) )
16 15 simpld โŠข ( ๐œ‘ โ†’ ๐‘‡ โ‰  โˆ… )
17 infssuzcl โŠข ( ( ๐‘‡ โІ ( โ„คโ‰ฅ โ€˜ 1 ) โˆง ๐‘‡ โ‰  โˆ… ) โ†’ inf ( ๐‘‡ , โ„ , < ) โˆˆ ๐‘‡ )
18 14 16 17 sylancr โŠข ( ๐œ‘ โ†’ inf ( ๐‘‡ , โ„ , < ) โˆˆ ๐‘‡ )
19 7 18 eqeltrid โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ ๐‘‡ )
20 oveq1 โŠข ( ๐‘– = ๐‘€ โ†’ ( ๐‘– ยท ๐‘ƒ ) = ( ๐‘€ ยท ๐‘ƒ ) )
21 20 eleq1d โŠข ( ๐‘– = ๐‘€ โ†’ ( ( ๐‘– ยท ๐‘ƒ ) โˆˆ ๐‘† โ†” ( ๐‘€ ยท ๐‘ƒ ) โˆˆ ๐‘† ) )
22 21 6 elrab2 โŠข ( ๐‘€ โˆˆ ๐‘‡ โ†” ( ๐‘€ โˆˆ โ„• โˆง ( ๐‘€ ยท ๐‘ƒ ) โˆˆ ๐‘† ) )
23 19 22 sylib โŠข ( ๐œ‘ โ†’ ( ๐‘€ โˆˆ โ„• โˆง ( ๐‘€ ยท ๐‘ƒ ) โˆˆ ๐‘† ) )
24 23 simprd โŠข ( ๐œ‘ โ†’ ( ๐‘€ ยท ๐‘ƒ ) โˆˆ ๐‘† )
25 1 4sqlem2 โŠข ( ( ๐‘€ ยท ๐‘ƒ ) โˆˆ ๐‘† โ†” โˆƒ ๐‘Ž โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘‘ โˆˆ โ„ค ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) )
26 24 25 sylib โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘Ž โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘‘ โˆˆ โ„ค ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) )
27 26 adantr โŠข ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ โˆƒ ๐‘Ž โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘‘ โˆˆ โ„ค ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) )
28 simp1l โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐œ‘ )
29 28 2 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘ โˆˆ โ„• )
30 28 3 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘ƒ = ( ( 2 ยท ๐‘ ) + 1 ) )
31 28 4 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘ƒ โˆˆ โ„™ )
32 28 5 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ( 0 ... ( 2 ยท ๐‘ ) ) โІ ๐‘† )
33 simp1r โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
34 simp2ll โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘Ž โˆˆ โ„ค )
35 simp2lr โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘ โˆˆ โ„ค )
36 simp2rl โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘ โˆˆ โ„ค )
37 simp2rr โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ๐‘‘ โˆˆ โ„ค )
38 eqid โŠข ( ( ( ๐‘Ž + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) = ( ( ( ๐‘Ž + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) )
39 eqid โŠข ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) = ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) )
40 eqid โŠข ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) = ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) )
41 eqid โŠข ( ( ( ๐‘‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) = ( ( ( ๐‘‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) )
42 eqid โŠข ( ( ( ( ( ( ( ๐‘Ž + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) + ( ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) ) + ( ( ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) + ( ( ( ( ๐‘‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) ) ) / ๐‘€ ) = ( ( ( ( ( ( ( ๐‘Ž + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) + ( ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) ) + ( ( ( ( ( ๐‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) + ( ( ( ( ๐‘‘ + ( ๐‘€ / 2 ) ) mod ๐‘€ ) โˆ’ ( ๐‘€ / 2 ) ) โ†‘ 2 ) ) ) / ๐‘€ )
43 simp3 โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) )
44 1 29 30 31 32 6 7 33 34 35 36 37 38 39 40 41 42 43 4sqlem17 โŠข ยฌ ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) )
45 44 pm2.21i โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โˆง ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) ) โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
46 45 3expia โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) ) โ†’ ( ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
47 46 anassrs โŠข ( ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) ) โˆง ( ๐‘ โˆˆ โ„ค โˆง ๐‘‘ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
48 47 rexlimdvva โŠข ( ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘Ž โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) ) โ†’ ( โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘‘ โˆˆ โ„ค ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
49 48 rexlimdvva โŠข ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( โˆƒ ๐‘Ž โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘ โˆˆ โ„ค โˆƒ ๐‘‘ โˆˆ โ„ค ( ๐‘€ ยท ๐‘ƒ ) = ( ( ( ๐‘Ž โ†‘ 2 ) + ( ๐‘ โ†‘ 2 ) ) + ( ( ๐‘ โ†‘ 2 ) + ( ๐‘‘ โ†‘ 2 ) ) ) โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
50 27 49 mpd โŠข ( ( ๐œ‘ โˆง ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
51 50 pm2.01da โŠข ( ๐œ‘ โ†’ ยฌ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
52 23 simpld โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
53 elnn1uz2 โŠข ( ๐‘€ โˆˆ โ„• โ†” ( ๐‘€ = 1 โˆจ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
54 52 53 sylib โŠข ( ๐œ‘ โ†’ ( ๐‘€ = 1 โˆจ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
55 54 ord โŠข ( ๐œ‘ โ†’ ( ยฌ ๐‘€ = 1 โ†’ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
56 51 55 mt3d โŠข ( ๐œ‘ โ†’ ๐‘€ = 1 )
57 56 19 eqeltrrd โŠข ( ๐œ‘ โ†’ 1 โˆˆ ๐‘‡ )
58 oveq1 โŠข ( ๐‘– = 1 โ†’ ( ๐‘– ยท ๐‘ƒ ) = ( 1 ยท ๐‘ƒ ) )
59 58 eleq1d โŠข ( ๐‘– = 1 โ†’ ( ( ๐‘– ยท ๐‘ƒ ) โˆˆ ๐‘† โ†” ( 1 ยท ๐‘ƒ ) โˆˆ ๐‘† ) )
60 59 6 elrab2 โŠข ( 1 โˆˆ ๐‘‡ โ†” ( 1 โˆˆ โ„• โˆง ( 1 ยท ๐‘ƒ ) โˆˆ ๐‘† ) )
61 60 simprbi โŠข ( 1 โˆˆ ๐‘‡ โ†’ ( 1 ยท ๐‘ƒ ) โˆˆ ๐‘† )
62 57 61 syl โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘ƒ ) โˆˆ ๐‘† )
63 11 62 eqeltrrd โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ ๐‘† )