Metamath Proof Explorer


Theorem isprm5

Description: One need only check prime divisors of P up to sqrt P in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion isprm5 ( ๐‘ƒ โˆˆ โ„™ โ†” ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )

Proof

Step Hyp Ref Expression
1 isprm4 โŠข ( ๐‘ƒ โˆˆ โ„™ โ†” ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) ) )
2 prmuz2 โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
3 2 a1i โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ง โˆˆ โ„™ โ†’ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) )
4 eluz2gt1 โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 1 < ๐‘ƒ )
5 eluzelre โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ƒ โˆˆ โ„ )
6 eluz2nn โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ƒ โˆˆ โ„• )
7 6 nngt0d โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 0 < ๐‘ƒ )
8 ltmulgt11 โŠข ( ( ๐‘ƒ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„ โˆง 0 < ๐‘ƒ ) โ†’ ( 1 < ๐‘ƒ โ†” ๐‘ƒ < ( ๐‘ƒ ยท ๐‘ƒ ) ) )
9 5 5 7 8 syl3anc โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( 1 < ๐‘ƒ โ†” ๐‘ƒ < ( ๐‘ƒ ยท ๐‘ƒ ) ) )
10 4 9 mpbid โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ƒ < ( ๐‘ƒ ยท ๐‘ƒ ) )
11 5 5 remulcld โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ƒ ยท ๐‘ƒ ) โˆˆ โ„ )
12 5 11 ltnled โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ƒ < ( ๐‘ƒ ยท ๐‘ƒ ) โ†” ยฌ ( ๐‘ƒ ยท ๐‘ƒ ) โ‰ค ๐‘ƒ ) )
13 10 12 mpbid โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ยฌ ( ๐‘ƒ ยท ๐‘ƒ ) โ‰ค ๐‘ƒ )
14 oveq12 โŠข ( ( ๐‘ง = ๐‘ƒ โˆง ๐‘ง = ๐‘ƒ ) โ†’ ( ๐‘ง ยท ๐‘ง ) = ( ๐‘ƒ ยท ๐‘ƒ ) )
15 14 anidms โŠข ( ๐‘ง = ๐‘ƒ โ†’ ( ๐‘ง ยท ๐‘ง ) = ( ๐‘ƒ ยท ๐‘ƒ ) )
16 15 breq1d โŠข ( ๐‘ง = ๐‘ƒ โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†” ( ๐‘ƒ ยท ๐‘ƒ ) โ‰ค ๐‘ƒ ) )
17 16 notbid โŠข ( ๐‘ง = ๐‘ƒ โ†’ ( ยฌ ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†” ยฌ ( ๐‘ƒ ยท ๐‘ƒ ) โ‰ค ๐‘ƒ ) )
18 13 17 syl5ibrcom โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ง = ๐‘ƒ โ†’ ยฌ ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ ) )
19 18 imim2d โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ยฌ ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ ) ) )
20 con2 โŠข ( ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ยฌ ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ ) โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) )
21 19 20 syl6 โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
22 3 21 imim12d โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง โˆˆ โ„™ โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) ) )
23 22 ralimdv2 โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
24 annim โŠข ( ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) โ†” ยฌ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) )
25 oveq12 โŠข ( ( ๐‘ฅ = ๐‘ง โˆง ๐‘ฅ = ๐‘ง ) โ†’ ( ๐‘ฅ ยท ๐‘ฅ ) = ( ๐‘ง ยท ๐‘ง ) )
26 25 anidms โŠข ( ๐‘ฅ = ๐‘ง โ†’ ( ๐‘ฅ ยท ๐‘ฅ ) = ( ๐‘ง ยท ๐‘ง ) )
27 26 breq1d โŠข ( ๐‘ฅ = ๐‘ง โ†’ ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โ†” ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ ) )
28 breq1 โŠข ( ๐‘ฅ = ๐‘ง โ†’ ( ๐‘ฅ โˆฅ ๐‘ƒ โ†” ๐‘ง โˆฅ ๐‘ƒ ) )
29 27 28 anbi12d โŠข ( ๐‘ฅ = ๐‘ง โ†’ ( ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) โ†” ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โˆง ๐‘ง โˆฅ ๐‘ƒ ) ) )
30 29 rspcev โŠข ( ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โˆง ๐‘ง โˆฅ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) )
31 30 ancom2s โŠข ( ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) )
32 31 expr โŠข ( ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆฅ ๐‘ƒ ) โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) )
33 32 ad2ant2lr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) )
34 simprl โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โˆฅ ๐‘ƒ )
35 eluzelz โŠข ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ง โˆˆ โ„ค )
36 35 ad2antlr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โˆˆ โ„ค )
37 eluz2nn โŠข ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ง โˆˆ โ„• )
38 37 ad2antlr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โˆˆ โ„• )
39 38 nnne0d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โ‰  0 )
40 eluzelz โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ƒ โˆˆ โ„ค )
41 40 ad2antrr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„ค )
42 dvdsval2 โŠข ( ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ง โ‰  0 โˆง ๐‘ƒ โˆˆ โ„ค ) โ†’ ( ๐‘ง โˆฅ ๐‘ƒ โ†” ( ๐‘ƒ / ๐‘ง ) โˆˆ โ„ค ) )
43 36 39 41 42 syl3anc โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง โˆฅ ๐‘ƒ โ†” ( ๐‘ƒ / ๐‘ง ) โˆˆ โ„ค ) )
44 34 43 mpbid โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ / ๐‘ง ) โˆˆ โ„ค )
45 eluzelre โŠข ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ง โˆˆ โ„ )
46 45 ad2antlr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โˆˆ โ„ )
47 46 recnd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โˆˆ โ„‚ )
48 47 mullidd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( 1 ยท ๐‘ง ) = ๐‘ง )
49 5 ad2antrr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„ )
50 6 ad2antrr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
51 dvdsle โŠข ( ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) โ†’ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง โ‰ค ๐‘ƒ ) )
52 51 imp โŠข ( ( ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„• ) โˆง ๐‘ง โˆฅ ๐‘ƒ ) โ†’ ๐‘ง โ‰ค ๐‘ƒ )
53 36 50 34 52 syl21anc โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โ‰ค ๐‘ƒ )
54 simprr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ยฌ ๐‘ง = ๐‘ƒ )
55 54 neqned โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง โ‰  ๐‘ƒ )
56 55 necomd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ โ‰  ๐‘ง )
57 46 49 53 56 leneltd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ง < ๐‘ƒ )
58 48 57 eqbrtrd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( 1 ยท ๐‘ง ) < ๐‘ƒ )
59 1red โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ 1 โˆˆ โ„ )
60 41 zred โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„ )
61 nnre โŠข ( ๐‘ง โˆˆ โ„• โ†’ ๐‘ง โˆˆ โ„ )
62 nngt0 โŠข ( ๐‘ง โˆˆ โ„• โ†’ 0 < ๐‘ง )
63 61 62 jca โŠข ( ๐‘ง โˆˆ โ„• โ†’ ( ๐‘ง โˆˆ โ„ โˆง 0 < ๐‘ง ) )
64 38 63 syl โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง โˆˆ โ„ โˆง 0 < ๐‘ง ) )
65 ltmuldiv โŠข ( ( 1 โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„ โˆง ( ๐‘ง โˆˆ โ„ โˆง 0 < ๐‘ง ) ) โ†’ ( ( 1 ยท ๐‘ง ) < ๐‘ƒ โ†” 1 < ( ๐‘ƒ / ๐‘ง ) ) )
66 59 60 64 65 syl3anc โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( 1 ยท ๐‘ง ) < ๐‘ƒ โ†” 1 < ( ๐‘ƒ / ๐‘ง ) ) )
67 58 66 mpbid โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ 1 < ( ๐‘ƒ / ๐‘ง ) )
68 eluz2b1 โŠข ( ( ๐‘ƒ / ๐‘ง ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†” ( ( ๐‘ƒ / ๐‘ง ) โˆˆ โ„ค โˆง 1 < ( ๐‘ƒ / ๐‘ง ) ) )
69 44 67 68 sylanbrc โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ / ๐‘ง ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) )
70 46 46 remulcld โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„ )
71 38 38 nnmulcld โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„• )
72 nnrp โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„+ )
73 nnrp โŠข ( ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„• โ†’ ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„+ )
74 rpdivcl โŠข ( ( ๐‘ƒ โˆˆ โ„+ โˆง ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„+ ) โ†’ ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) โˆˆ โ„+ )
75 72 73 74 syl2an โŠข ( ( ๐‘ƒ โˆˆ โ„• โˆง ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„• ) โ†’ ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) โˆˆ โ„+ )
76 50 71 75 syl2anc โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) โˆˆ โ„+ )
77 49 70 76 lemul1d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ โ‰ค ( ๐‘ง ยท ๐‘ง ) โ†” ( ๐‘ƒ ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) โ‰ค ( ( ๐‘ง ยท ๐‘ง ) ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) ) )
78 49 recnd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ โˆˆ โ„‚ )
79 78 47 78 47 39 39 divmuldivd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) = ( ( ๐‘ƒ ยท ๐‘ƒ ) / ( ๐‘ง ยท ๐‘ง ) ) )
80 71 nncnd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„‚ )
81 71 nnne0d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โ‰  0 )
82 78 78 80 81 divassd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ ยท ๐‘ƒ ) / ( ๐‘ง ยท ๐‘ง ) ) = ( ๐‘ƒ ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) )
83 79 82 eqtrd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) = ( ๐‘ƒ ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) )
84 78 80 81 divcan2d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ๐‘ง ยท ๐‘ง ) ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) = ๐‘ƒ )
85 84 eqcomd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ๐‘ƒ = ( ( ๐‘ง ยท ๐‘ง ) ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) )
86 83 85 breq12d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ โ†” ( ๐‘ƒ ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) โ‰ค ( ( ๐‘ง ยท ๐‘ง ) ยท ( ๐‘ƒ / ( ๐‘ง ยท ๐‘ง ) ) ) ) )
87 77 86 bitr4d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ โ‰ค ( ๐‘ง ยท ๐‘ง ) โ†” ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ ) )
88 87 biimpd โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ โ‰ค ( ๐‘ง ยท ๐‘ง ) โ†’ ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ ) )
89 78 47 39 divcan2d โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ง ยท ( ๐‘ƒ / ๐‘ง ) ) = ๐‘ƒ )
90 dvds0lem โŠข ( ( ( ๐‘ง โˆˆ โ„ค โˆง ( ๐‘ƒ / ๐‘ง ) โˆˆ โ„ค โˆง ๐‘ƒ โˆˆ โ„ค ) โˆง ( ๐‘ง ยท ( ๐‘ƒ / ๐‘ง ) ) = ๐‘ƒ ) โ†’ ( ๐‘ƒ / ๐‘ง ) โˆฅ ๐‘ƒ )
91 36 44 41 89 90 syl31anc โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ / ๐‘ง ) โˆฅ ๐‘ƒ )
92 88 91 jctird โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ โ‰ค ( ๐‘ง ยท ๐‘ง ) โ†’ ( ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ โˆง ( ๐‘ƒ / ๐‘ง ) โˆฅ ๐‘ƒ ) ) )
93 oveq12 โŠข ( ( ๐‘ฅ = ( ๐‘ƒ / ๐‘ง ) โˆง ๐‘ฅ = ( ๐‘ƒ / ๐‘ง ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฅ ) = ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) )
94 93 anidms โŠข ( ๐‘ฅ = ( ๐‘ƒ / ๐‘ง ) โ†’ ( ๐‘ฅ ยท ๐‘ฅ ) = ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) )
95 94 breq1d โŠข ( ๐‘ฅ = ( ๐‘ƒ / ๐‘ง ) โ†’ ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โ†” ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ ) )
96 breq1 โŠข ( ๐‘ฅ = ( ๐‘ƒ / ๐‘ง ) โ†’ ( ๐‘ฅ โˆฅ ๐‘ƒ โ†” ( ๐‘ƒ / ๐‘ง ) โˆฅ ๐‘ƒ ) )
97 95 96 anbi12d โŠข ( ๐‘ฅ = ( ๐‘ƒ / ๐‘ง ) โ†’ ( ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) โ†” ( ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ โˆง ( ๐‘ƒ / ๐‘ง ) โˆฅ ๐‘ƒ ) ) )
98 97 rspcev โŠข ( ( ( ๐‘ƒ / ๐‘ง ) โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ( ( ( ๐‘ƒ / ๐‘ง ) ยท ( ๐‘ƒ / ๐‘ง ) ) โ‰ค ๐‘ƒ โˆง ( ๐‘ƒ / ๐‘ง ) โˆฅ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) )
99 69 92 98 syl6an โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ๐‘ƒ โ‰ค ( ๐‘ง ยท ๐‘ง ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) )
100 70 49 letrid โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โˆจ ๐‘ƒ โ‰ค ( ๐‘ง ยท ๐‘ง ) ) )
101 33 99 100 mpjaod โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) )
102 101 ex โŠข ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ๐‘ง โˆฅ ๐‘ƒ โˆง ยฌ ๐‘ง = ๐‘ƒ ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) )
103 24 102 biimtrrid โŠข ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ยฌ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) )
104 103 rexlimdva โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( โˆƒ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ยฌ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) )
105 prmz โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ๐‘ง โˆˆ โ„ค )
106 105 ad2antrl โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ง โˆˆ โ„ค )
107 106 zred โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ง โˆˆ โ„ )
108 107 107 remulcld โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โˆˆ โ„ )
109 eluzelz โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ฅ โˆˆ โ„ค )
110 109 ad3antlr โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„ค )
111 110 zred โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„ )
112 111 111 remulcld โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฅ ) โˆˆ โ„ )
113 40 ad3antrrr โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ƒ โˆˆ โ„ค )
114 113 zred โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ƒ โˆˆ โ„ )
115 eluz2nn โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ฅ โˆˆ โ„• )
116 115 ad3antlr โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆˆ โ„• )
117 simprr โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ง โˆฅ ๐‘ฅ )
118 dvdsle โŠข ( ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘ง โˆฅ ๐‘ฅ โ†’ ๐‘ง โ‰ค ๐‘ฅ ) )
119 118 imp โŠข ( ( ( ๐‘ง โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘ง โˆฅ ๐‘ฅ ) โ†’ ๐‘ง โ‰ค ๐‘ฅ )
120 106 116 117 119 syl21anc โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ง โ‰ค ๐‘ฅ )
121 eluzge2nn0 โŠข ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ๐‘ง โˆˆ โ„•0 )
122 121 nn0ge0d โŠข ( ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ 0 โ‰ค ๐‘ง )
123 2 122 syl โŠข ( ๐‘ง โˆˆ โ„™ โ†’ 0 โ‰ค ๐‘ง )
124 123 ad2antrl โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ 0 โ‰ค ๐‘ง )
125 nnnn0 โŠข ( ๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„•0 )
126 125 nn0ge0d โŠข ( ๐‘ฅ โˆˆ โ„• โ†’ 0 โ‰ค ๐‘ฅ )
127 116 126 syl โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ 0 โ‰ค ๐‘ฅ )
128 le2msq โŠข ( ( ( ๐‘ง โˆˆ โ„ โˆง 0 โ‰ค ๐‘ง ) โˆง ( ๐‘ฅ โˆˆ โ„ โˆง 0 โ‰ค ๐‘ฅ ) ) โ†’ ( ๐‘ง โ‰ค ๐‘ฅ โ†” ( ๐‘ง ยท ๐‘ง ) โ‰ค ( ๐‘ฅ ยท ๐‘ฅ ) ) )
129 107 124 111 127 128 syl22anc โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ( ๐‘ง โ‰ค ๐‘ฅ โ†” ( ๐‘ง ยท ๐‘ง ) โ‰ค ( ๐‘ฅ ยท ๐‘ฅ ) ) )
130 120 129 mpbid โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โ‰ค ( ๐‘ฅ ยท ๐‘ฅ ) )
131 simplrl โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ )
132 108 112 114 130 131 letrd โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ )
133 simplrr โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ฅ โˆฅ ๐‘ƒ )
134 106 110 113 117 133 dvdstrd โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ๐‘ง โˆฅ ๐‘ƒ )
135 132 134 jc โŠข ( ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โˆง ( ๐‘ง โˆˆ โ„™ โˆง ๐‘ง โˆฅ ๐‘ฅ ) ) โ†’ ยฌ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) )
136 exprmfct โŠข ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ โˆƒ ๐‘ง โˆˆ โ„™ ๐‘ง โˆฅ ๐‘ฅ )
137 136 ad2antlr โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘ง โˆˆ โ„™ ๐‘ง โˆฅ ๐‘ฅ )
138 135 137 reximddv โŠข ( ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โˆง ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) ) โ†’ โˆƒ ๐‘ง โˆˆ โ„™ ยฌ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) )
139 138 ex โŠข ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ) โ†’ ( ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) โ†’ โˆƒ ๐‘ง โˆˆ โ„™ ยฌ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
140 139 rexlimdva โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( โˆƒ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ( ๐‘ฅ ยท ๐‘ฅ ) โ‰ค ๐‘ƒ โˆง ๐‘ฅ โˆฅ ๐‘ƒ ) โ†’ โˆƒ ๐‘ง โˆˆ โ„™ ยฌ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
141 104 140 syld โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( โˆƒ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ยฌ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ โˆƒ ๐‘ง โˆˆ โ„™ ยฌ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
142 rexnal โŠข ( โˆƒ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ยฌ ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†” ยฌ โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) )
143 rexnal โŠข ( โˆƒ ๐‘ง โˆˆ โ„™ ยฌ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) โ†” ยฌ โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) )
144 141 142 143 3imtr3g โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( ยฌ โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†’ ยฌ โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
145 23 144 impcon4bid โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†” โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
146 prmnn โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ๐‘ง โˆˆ โ„• )
147 146 nncnd โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ๐‘ง โˆˆ โ„‚ )
148 147 sqvald โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ( ๐‘ง โ†‘ 2 ) = ( ๐‘ง ยท ๐‘ง ) )
149 148 breq1d โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†” ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ ) )
150 149 imbi1d โŠข ( ๐‘ง โˆˆ โ„™ โ†’ ( ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) โ†” ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
151 150 ralbiia โŠข ( โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) โ†” โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง ยท ๐‘ง ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) )
152 145 151 bitr4di โŠข ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โ†’ ( โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) โ†” โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
153 152 pm5.32i โŠข ( ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง โˆ€ ๐‘ง โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) ( ๐‘ง โˆฅ ๐‘ƒ โ†’ ๐‘ง = ๐‘ƒ ) ) โ†” ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )
154 1 153 bitri โŠข ( ๐‘ƒ โˆˆ โ„™ โ†” ( ๐‘ƒ โˆˆ ( โ„คโ‰ฅ โ€˜ 2 ) โˆง โˆ€ ๐‘ง โˆˆ โ„™ ( ( ๐‘ง โ†‘ 2 ) โ‰ค ๐‘ƒ โ†’ ยฌ ๐‘ง โˆฅ ๐‘ƒ ) ) )