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 ) โค ๐ โ ยฌ ๐ง โฅ ๐ ) ) ) |