Step | Hyp | Ref
| Expression |
1 | | isprm5lem.x |
. . 3
โข (๐ โ ๐ โ (2...(๐ โ 1))) |
2 | | elfzuz 10021 |
. . 3
โข (๐ โ (2...(๐ โ 1)) โ ๐ โ
(โคโฅโ2)) |
3 | | exprmfct 12138 |
. . 3
โข (๐ โ
(โคโฅโ2) โ โ๐ฆ โ โ ๐ฆ โฅ ๐) |
4 | 1, 2, 3 | 3syl 17 |
. 2
โข (๐ โ โ๐ฆ โ โ ๐ฆ โฅ ๐) |
5 | | simpr 110 |
. . . . 5
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โ (๐ฆโ2) โค ๐) |
6 | | oveq1 5882 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ (๐งโ2) = (๐ฆโ2)) |
7 | 6 | breq1d 4014 |
. . . . . . 7
โข (๐ง = ๐ฆ โ ((๐งโ2) โค ๐ โ (๐ฆโ2) โค ๐)) |
8 | | breq1 4007 |
. . . . . . . 8
โข (๐ง = ๐ฆ โ (๐ง โฅ ๐ โ ๐ฆ โฅ ๐)) |
9 | 8 | notbid 667 |
. . . . . . 7
โข (๐ง = ๐ฆ โ (ยฌ ๐ง โฅ ๐ โ ยฌ ๐ฆ โฅ ๐)) |
10 | 7, 9 | imbi12d 234 |
. . . . . 6
โข (๐ง = ๐ฆ โ (((๐งโ2) โค ๐ โ ยฌ ๐ง โฅ ๐) โ ((๐ฆโ2) โค ๐ โ ยฌ ๐ฆ โฅ ๐))) |
11 | | isprm5lem.z |
. . . . . . 7
โข (๐ โ โ๐ง โ โ ((๐งโ2) โค ๐ โ ยฌ ๐ง โฅ ๐)) |
12 | 11 | ad2antrr 488 |
. . . . . 6
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โ โ๐ง โ โ ((๐งโ2) โค ๐ โ ยฌ ๐ง โฅ ๐)) |
13 | | simplrl 535 |
. . . . . 6
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โ ๐ฆ โ โ) |
14 | 10, 12, 13 | rspcdva 2847 |
. . . . 5
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โ ((๐ฆโ2) โค ๐ โ ยฌ ๐ฆ โฅ ๐)) |
15 | 5, 14 | mpd 13 |
. . . 4
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โ ยฌ ๐ฆ โฅ ๐) |
16 | | prmz 12111 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
17 | 16 | ad2antrl 490 |
. . . . . 6
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ๐ฆ โ โค) |
18 | 17 | ad2antrr 488 |
. . . . 5
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โง ๐ โฅ ๐) โ ๐ฆ โ โค) |
19 | | elfzelz 10025 |
. . . . . . . 8
โข (๐ โ (2...(๐ โ 1)) โ ๐ โ โค) |
20 | 1, 19 | syl 14 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
21 | 20 | ad2antrr 488 |
. . . . . 6
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ โฅ ๐) โ ๐ โ โค) |
22 | 21 | adantlr 477 |
. . . . 5
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โง ๐ โฅ ๐) โ ๐ โ โค) |
23 | | isprm5lem.p |
. . . . . . . 8
โข (๐ โ ๐ โ
(โคโฅโ2)) |
24 | | eluzelz 9537 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ2) โ ๐ โ โค) |
25 | 23, 24 | syl 14 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
26 | 25 | ad2antrr 488 |
. . . . . 6
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ โฅ ๐) โ ๐ โ โค) |
27 | 26 | adantlr 477 |
. . . . 5
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โง ๐ โฅ ๐) โ ๐ โ โค) |
28 | | simplrr 536 |
. . . . . 6
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ โฅ ๐) โ ๐ฆ โฅ ๐) |
29 | 28 | adantlr 477 |
. . . . 5
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โง ๐ โฅ ๐) โ ๐ฆ โฅ ๐) |
30 | | simpr 110 |
. . . . 5
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โง ๐ โฅ ๐) โ ๐ โฅ ๐) |
31 | 18, 22, 27, 29, 30 | dvdstrd 11837 |
. . . 4
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โง ๐ โฅ ๐) โ ๐ฆ โฅ ๐) |
32 | 15, 31 | mtand 665 |
. . 3
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง (๐ฆโ2) โค ๐) โ ยฌ ๐ โฅ ๐) |
33 | 17 | ad2antrr 488 |
. . . . . . . . 9
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ ๐ฆ โ โค) |
34 | 21 | adantlr 477 |
. . . . . . . . 9
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ ๐ โ โค) |
35 | 25 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ๐ โ โค) |
36 | 35 | ad2antrr 488 |
. . . . . . . . 9
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ ๐ โ โค) |
37 | 28 | adantlr 477 |
. . . . . . . . 9
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ ๐ฆ โฅ ๐) |
38 | | simpr 110 |
. . . . . . . . 9
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ ๐ โฅ ๐) |
39 | 33, 34, 36, 37, 38 | dvdstrd 11837 |
. . . . . . . 8
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ ๐ฆ โฅ ๐) |
40 | 17 | adantr 276 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โ โค) |
41 | | prmnn 12110 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
42 | 41 | nnne0d 8964 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ๐ฆ โ 0) |
43 | 42 | ad2antrl 490 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ๐ฆ โ 0) |
44 | 43 | adantr 276 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โ 0) |
45 | 25 | ad2antrr 488 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ โ โค) |
46 | | dvdsval2 11797 |
. . . . . . . . . 10
โข ((๐ฆ โ โค โง ๐ฆ โ 0 โง ๐ โ โค) โ (๐ฆ โฅ ๐ โ (๐ / ๐ฆ) โ โค)) |
47 | 40, 44, 45, 46 | syl3anc 1238 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐ฆ โฅ ๐ โ (๐ / ๐ฆ) โ โค)) |
48 | 47 | adantr 276 |
. . . . . . . 8
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ (๐ฆ โฅ ๐ โ (๐ / ๐ฆ) โ โค)) |
49 | 39, 48 | mpbid 147 |
. . . . . . 7
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ (๐ / ๐ฆ) โ โค) |
50 | 40 | zred 9375 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โ โ) |
51 | 50 | recnd 7986 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โ โ) |
52 | 51 | mulid2d 7976 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (1 ยท ๐ฆ) = ๐ฆ) |
53 | | 2nn 9080 |
. . . . . . . . . . . . . . 15
โข 2 โ
โ |
54 | | fzssnn 10068 |
. . . . . . . . . . . . . . 15
โข (2 โ
โ โ (2...(๐
โ 1)) โ โ) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . 14
โข
(2...(๐ โ 1))
โ โ |
56 | 55, 1 | sselid 3154 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
57 | 56 | ad2antrr 488 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ โ โ) |
58 | 57 | nnred 8932 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ โ โ) |
59 | 25 | zred 9375 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โ) |
60 | 59 | ad2antrr 488 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ โ โ) |
61 | | simplrr 536 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โฅ ๐) |
62 | | dvdsle 11850 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โค โง ๐ โ โ) โ (๐ฆ โฅ ๐ โ ๐ฆ โค ๐)) |
63 | 40, 57, 62 | syl2anc 411 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐ฆ โฅ ๐ โ ๐ฆ โค ๐)) |
64 | 61, 63 | mpd 13 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โค ๐) |
65 | | elfzle2 10028 |
. . . . . . . . . . . . . 14
โข (๐ โ (2...(๐ โ 1)) โ ๐ โค (๐ โ 1)) |
66 | 1, 65 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โค (๐ โ 1)) |
67 | | zltlem1 9310 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง ๐ โ โค) โ (๐ < ๐ โ ๐ โค (๐ โ 1))) |
68 | 20, 25, 67 | syl2anc 411 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ < ๐ โ ๐ โค (๐ โ 1))) |
69 | 66, 68 | mpbird 167 |
. . . . . . . . . . . 12
โข (๐ โ ๐ < ๐) |
70 | 69 | ad2antrr 488 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ < ๐) |
71 | 50, 58, 60, 64, 70 | lelttrd 8082 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ < ๐) |
72 | 52, 71 | eqbrtrd 4026 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (1 ยท ๐ฆ) < ๐) |
73 | | 1red 7972 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ 1 โ
โ) |
74 | 41 | nnrpd 9694 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ๐ฆ โ
โ+) |
75 | 74 | ad2antrl 490 |
. . . . . . . . . . 11
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ๐ฆ โ โ+) |
76 | 75 | adantr 276 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โ โ+) |
77 | 73, 60, 76 | ltmuldivd 9744 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ((1 ยท ๐ฆ) < ๐ โ 1 < (๐ / ๐ฆ))) |
78 | 72, 77 | mpbid 147 |
. . . . . . . 8
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ 1 < (๐ / ๐ฆ)) |
79 | 78 | adantr 276 |
. . . . . . 7
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ 1 < (๐ / ๐ฆ)) |
80 | | eluz2b1 9601 |
. . . . . . 7
โข ((๐ / ๐ฆ) โ (โคโฅโ2)
โ ((๐ / ๐ฆ) โ โค โง 1 <
(๐ / ๐ฆ))) |
81 | 49, 79, 80 | sylanbrc 417 |
. . . . . 6
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ (๐ / ๐ฆ) โ
(โคโฅโ2)) |
82 | | exprmfct 12138 |
. . . . . 6
โข ((๐ / ๐ฆ) โ (โคโฅโ2)
โ โ๐ค โ
โ ๐ค โฅ (๐ / ๐ฆ)) |
83 | 81, 82 | syl 14 |
. . . . 5
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ โ๐ค โ โ ๐ค โฅ (๐ / ๐ฆ)) |
84 | | prmz 12111 |
. . . . . . . 8
โข (๐ค โ โ โ ๐ค โ
โค) |
85 | 84 | ad2antrl 490 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ค โ โค) |
86 | 49 | adantr 276 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ / ๐ฆ) โ โค) |
87 | 45 | ad2antrr 488 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ โ โค) |
88 | | simprr 531 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ค โฅ (๐ / ๐ฆ)) |
89 | 39 | adantr 276 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ฆ โฅ ๐) |
90 | 44 | ad2antrr 488 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ฆ โ 0) |
91 | | divconjdvds 11855 |
. . . . . . . 8
โข ((๐ฆ โฅ ๐ โง ๐ฆ โ 0) โ (๐ / ๐ฆ) โฅ ๐) |
92 | 89, 90, 91 | syl2anc 411 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ / ๐ฆ) โฅ ๐) |
93 | 85, 86, 87, 88, 92 | dvdstrd 11837 |
. . . . . 6
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ค โฅ ๐) |
94 | 85 | zred 9375 |
. . . . . . . . 9
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ค โ โ) |
95 | 94 | resqcld 10680 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐คโ2) โ โ) |
96 | 60 | ad2antrr 488 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ โ โ) |
97 | 81 | adantr 276 |
. . . . . . . . . . . 12
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ / ๐ฆ) โ
(โคโฅโ2)) |
98 | | eluz2nn 9566 |
. . . . . . . . . . . 12
โข ((๐ / ๐ฆ) โ (โคโฅโ2)
โ (๐ / ๐ฆ) โ
โ) |
99 | 97, 98 | syl 14 |
. . . . . . . . . . 11
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ / ๐ฆ) โ โ) |
100 | 99 | nnred 8932 |
. . . . . . . . . 10
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ / ๐ฆ) โ โ) |
101 | 100 | resqcld 10680 |
. . . . . . . . 9
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ((๐ / ๐ฆ)โ2) โ โ) |
102 | | dvdsle 11850 |
. . . . . . . . . . . 12
โข ((๐ค โ โค โง (๐ / ๐ฆ) โ โ) โ (๐ค โฅ (๐ / ๐ฆ) โ ๐ค โค (๐ / ๐ฆ))) |
103 | 85, 99, 102 | syl2anc 411 |
. . . . . . . . . . 11
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ค โฅ (๐ / ๐ฆ) โ ๐ค โค (๐ / ๐ฆ))) |
104 | 88, 103 | mpd 13 |
. . . . . . . . . 10
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ค โค (๐ / ๐ฆ)) |
105 | | prmnn 12110 |
. . . . . . . . . . . . . 14
โข (๐ค โ โ โ ๐ค โ
โ) |
106 | 105 | nnnn0d 9229 |
. . . . . . . . . . . . 13
โข (๐ค โ โ โ ๐ค โ
โ0) |
107 | 106 | nn0ge0d 9232 |
. . . . . . . . . . . 12
โข (๐ค โ โ โ 0 โค
๐ค) |
108 | 107 | ad2antrl 490 |
. . . . . . . . . . 11
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ 0 โค ๐ค) |
109 | | 0red 7958 |
. . . . . . . . . . . 12
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ 0 โ โ) |
110 | | 1red 7972 |
. . . . . . . . . . . 12
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ 1 โ โ) |
111 | | 0le1 8438 |
. . . . . . . . . . . . 13
โข 0 โค
1 |
112 | 111 | a1i 9 |
. . . . . . . . . . . 12
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ 0 โค 1) |
113 | 99 | nnge1d 8962 |
. . . . . . . . . . . 12
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ 1 โค (๐ / ๐ฆ)) |
114 | 109, 110,
100, 112, 113 | letrd 8081 |
. . . . . . . . . . 11
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ 0 โค (๐ / ๐ฆ)) |
115 | 94, 100, 108, 114 | le2sqd 10686 |
. . . . . . . . . 10
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐ค โค (๐ / ๐ฆ) โ (๐คโ2) โค ((๐ / ๐ฆ)โ2))) |
116 | 104, 115 | mpbid 147 |
. . . . . . . . 9
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐คโ2) โค ((๐ / ๐ฆ)โ2)) |
117 | 60 | recnd 7986 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ โ โ) |
118 | 41 | ad2antrl 490 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ๐ฆ โ โ) |
119 | 118 | adantr 276 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ โ โ) |
120 | 119 | nnap0d 8965 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ฆ # 0) |
121 | 117, 51, 120 | sqdivapd 10667 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ((๐ / ๐ฆ)โ2) = ((๐โ2) / (๐ฆโ2))) |
122 | 117 | sqvald 10651 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐โ2) = (๐ ยท ๐)) |
123 | 50 | resqcld 10680 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐ฆโ2) โ โ) |
124 | | eluz2nn 9566 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
125 | 23, 124 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โ) |
126 | 125 | nnrpd 9694 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ
โ+) |
127 | 126 | ad2antrr 488 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ โ
โ+) |
128 | | simpr 110 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ๐ < (๐ฆโ2)) |
129 | 60, 123, 127, 128 | ltmul2dd 9753 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐ ยท ๐) < (๐ ยท (๐ฆโ2))) |
130 | 122, 129 | eqbrtrd 4026 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐โ2) < (๐ ยท (๐ฆโ2))) |
131 | 60 | resqcld 10680 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐โ2) โ โ) |
132 | 119 | nnsqcld 10675 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐ฆโ2) โ โ) |
133 | 132 | nnrpd 9694 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (๐ฆโ2) โ
โ+) |
134 | 131, 60, 133 | ltdivmul2d 9749 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ (((๐โ2) / (๐ฆโ2)) < ๐ โ (๐โ2) < (๐ ยท (๐ฆโ2)))) |
135 | 130, 134 | mpbird 167 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ((๐โ2) / (๐ฆโ2)) < ๐) |
136 | 121, 135 | eqbrtrd 4026 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ((๐ / ๐ฆ)โ2) < ๐) |
137 | 136 | ad2antrr 488 |
. . . . . . . . 9
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ((๐ / ๐ฆ)โ2) < ๐) |
138 | 95, 101, 96, 116, 137 | lelttrd 8082 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐คโ2) < ๐) |
139 | 95, 96, 138 | ltled 8076 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ (๐คโ2) โค ๐) |
140 | | oveq1 5882 |
. . . . . . . . . 10
โข (๐ง = ๐ค โ (๐งโ2) = (๐คโ2)) |
141 | 140 | breq1d 4014 |
. . . . . . . . 9
โข (๐ง = ๐ค โ ((๐งโ2) โค ๐ โ (๐คโ2) โค ๐)) |
142 | | breq1 4007 |
. . . . . . . . . 10
โข (๐ง = ๐ค โ (๐ง โฅ ๐ โ ๐ค โฅ ๐)) |
143 | 142 | notbid 667 |
. . . . . . . . 9
โข (๐ง = ๐ค โ (ยฌ ๐ง โฅ ๐ โ ยฌ ๐ค โฅ ๐)) |
144 | 141, 143 | imbi12d 234 |
. . . . . . . 8
โข (๐ง = ๐ค โ (((๐งโ2) โค ๐ โ ยฌ ๐ง โฅ ๐) โ ((๐คโ2) โค ๐ โ ยฌ ๐ค โฅ ๐))) |
145 | 11 | ad4antr 494 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ โ๐ง โ โ ((๐งโ2) โค ๐ โ ยฌ ๐ง โฅ ๐)) |
146 | | simprl 529 |
. . . . . . . 8
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ๐ค โ โ) |
147 | 144, 145,
146 | rspcdva 2847 |
. . . . . . 7
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ((๐คโ2) โค ๐ โ ยฌ ๐ค โฅ ๐)) |
148 | 139, 147 | mpd 13 |
. . . . . 6
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ ยฌ ๐ค โฅ ๐) |
149 | 93, 148 | pm2.21fal 1373 |
. . . . 5
โข
(((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โง (๐ค โ โ โง ๐ค โฅ (๐ / ๐ฆ))) โ โฅ) |
150 | 83, 149 | rexlimddv 2599 |
. . . 4
โข ((((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โง ๐ โฅ ๐) โ โฅ) |
151 | 150 | inegd 1372 |
. . 3
โข (((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โง ๐ < (๐ฆโ2)) โ ยฌ ๐ โฅ ๐) |
152 | | zsqcl 10591 |
. . . . 5
โข (๐ฆ โ โค โ (๐ฆโ2) โ
โค) |
153 | 17, 152 | syl 14 |
. . . 4
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ (๐ฆโ2) โ โค) |
154 | | zlelttric 9298 |
. . . 4
โข (((๐ฆโ2) โ โค โง
๐ โ โค) โ
((๐ฆโ2) โค ๐ โจ ๐ < (๐ฆโ2))) |
155 | 153, 35, 154 | syl2anc 411 |
. . 3
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ((๐ฆโ2) โค ๐ โจ ๐ < (๐ฆโ2))) |
156 | 32, 151, 155 | mpjaodan 798 |
. 2
โข ((๐ โง (๐ฆ โ โ โง ๐ฆ โฅ ๐)) โ ยฌ ๐ โฅ ๐) |
157 | 4, 156 | rexlimddv 2599 |
1
โข (๐ โ ยฌ ๐ โฅ ๐) |