Step | Hyp | Ref
| Expression |
1 | | prmind.5 |
. 2
โข (๐ฅ = ๐ด โ (๐ โ ๐)) |
2 | | oveq2 5882 |
. . . 4
โข (๐ = 1 โ (1...๐) = (1...1)) |
3 | 2 | raleqdv 2678 |
. . 3
โข (๐ = 1 โ (โ๐ฅ โ (1...๐)๐ โ โ๐ฅ โ (1...1)๐)) |
4 | | oveq2 5882 |
. . . 4
โข (๐ = ๐ โ (1...๐) = (1...๐)) |
5 | 4 | raleqdv 2678 |
. . 3
โข (๐ = ๐ โ (โ๐ฅ โ (1...๐)๐ โ โ๐ฅ โ (1...๐)๐)) |
6 | | oveq2 5882 |
. . . 4
โข (๐ = (๐ + 1) โ (1...๐) = (1...(๐ + 1))) |
7 | 6 | raleqdv 2678 |
. . 3
โข (๐ = (๐ + 1) โ (โ๐ฅ โ (1...๐)๐ โ โ๐ฅ โ (1...(๐ + 1))๐)) |
8 | | oveq2 5882 |
. . . 4
โข (๐ = ๐ด โ (1...๐) = (1...๐ด)) |
9 | 8 | raleqdv 2678 |
. . 3
โข (๐ = ๐ด โ (โ๐ฅ โ (1...๐)๐ โ โ๐ฅ โ (1...๐ด)๐)) |
10 | | prmind.6 |
. . . . 5
โข ๐ |
11 | | elfz1eq 10034 |
. . . . . 6
โข (๐ฅ โ (1...1) โ ๐ฅ = 1) |
12 | | prmind.1 |
. . . . . 6
โข (๐ฅ = 1 โ (๐ โ ๐)) |
13 | 11, 12 | syl 14 |
. . . . 5
โข (๐ฅ โ (1...1) โ (๐ โ ๐)) |
14 | 10, 13 | mpbiri 168 |
. . . 4
โข (๐ฅ โ (1...1) โ ๐) |
15 | 14 | rgen 2530 |
. . 3
โข
โ๐ฅ โ
(1...1)๐ |
16 | | peano2nn 8930 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ + 1) โ
โ) |
17 | 16 | ad2antrr 488 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ + 1) โ โ) |
18 | 17 | nncnd 8932 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ + 1) โ โ) |
19 | | elfzuz 10020 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ (2...((๐ + 1) โ 1)) โ ๐ฆ โ
(โคโฅโ2)) |
20 | 19 | ad2antrl 490 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ
(โคโฅโ2)) |
21 | | eluz2nn 9565 |
. . . . . . . . . . . . 13
โข (๐ฆ โ
(โคโฅโ2) โ ๐ฆ โ โ) |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ โ) |
23 | 22 | nncnd 8932 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ โ) |
24 | 22 | nnap0d 8964 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ # 0) |
25 | 18, 23, 24 | divcanap2d 8748 |
. . . . . . . . . 10
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ฆ ยท ((๐ + 1) / ๐ฆ)) = (๐ + 1)) |
26 | | simprr 531 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โฅ (๐ + 1)) |
27 | 22 | nnzd 9373 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ โค) |
28 | 22 | nnne0d 8963 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ 0) |
29 | 17 | nnzd 9373 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ + 1) โ โค) |
30 | | dvdsval2 11796 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โค โง ๐ฆ โ 0 โง (๐ + 1) โ โค) โ
(๐ฆ โฅ (๐ + 1) โ ((๐ + 1) / ๐ฆ) โ โค)) |
31 | 27, 28, 29, 30 | syl3anc 1238 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ฆ โฅ (๐ + 1) โ ((๐ + 1) / ๐ฆ) โ โค)) |
32 | 26, 31 | mpbid 147 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) โ โค) |
33 | 23 | mulid2d 7975 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (1 ยท ๐ฆ) = ๐ฆ) |
34 | | elfzle2 10027 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ (2...((๐ + 1) โ 1)) โ ๐ฆ โค ((๐ + 1) โ 1)) |
35 | 34 | ad2antrl 490 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โค ((๐ + 1) โ 1)) |
36 | | nncn 8926 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ ๐ โ
โ) |
37 | 36 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ โ โ) |
38 | | ax-1cn 7903 |
. . . . . . . . . . . . . . . . 17
โข 1 โ
โ |
39 | | pncan 8162 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
40 | 37, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) โ 1) = ๐) |
41 | 35, 40 | breqtrd 4029 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โค ๐) |
42 | | nnz 9271 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ ๐ โ
โค) |
43 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ โ โค) |
44 | | zleltp1 9307 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โค โง ๐ โ โค) โ (๐ฆ โค ๐ โ ๐ฆ < (๐ + 1))) |
45 | 27, 43, 44 | syl2anc 411 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ฆ โค ๐ โ ๐ฆ < (๐ + 1))) |
46 | 41, 45 | mpbid 147 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ < (๐ + 1)) |
47 | 33, 46 | eqbrtrd 4025 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (1 ยท ๐ฆ) < (๐ + 1)) |
48 | | 1red 7971 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ 1 โ
โ) |
49 | 17 | nnred 8931 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ + 1) โ โ) |
50 | 22 | nnred 8931 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ โ) |
51 | 22 | nngt0d 8962 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ 0 < ๐ฆ) |
52 | | ltmuldiv 8830 |
. . . . . . . . . . . . . 14
โข ((1
โ โ โง (๐ +
1) โ โ โง (๐ฆ
โ โ โง 0 < ๐ฆ)) โ ((1 ยท ๐ฆ) < (๐ + 1) โ 1 < ((๐ + 1) / ๐ฆ))) |
53 | 48, 49, 50, 51, 52 | syl112anc 1242 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((1 ยท ๐ฆ) < (๐ + 1) โ 1 < ((๐ + 1) / ๐ฆ))) |
54 | 47, 53 | mpbid 147 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ 1 < ((๐ + 1) / ๐ฆ)) |
55 | | eluz2b1 9600 |
. . . . . . . . . . . 12
โข (((๐ + 1) / ๐ฆ) โ (โคโฅโ2)
โ (((๐ + 1) / ๐ฆ) โ โค โง 1 <
((๐ + 1) / ๐ฆ))) |
56 | 32, 54, 55 | sylanbrc 417 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) โ
(โคโฅโ2)) |
57 | | prmind.2 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) |
58 | | simplr 528 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ โ๐ฅ โ (1...๐)๐) |
59 | | fznn 10088 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (๐ฆ โ (1...๐) โ (๐ฆ โ โ โง ๐ฆ โค ๐))) |
60 | 43, 59 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ฆ โ (1...๐) โ (๐ฆ โ โ โง ๐ฆ โค ๐))) |
61 | 22, 41, 60 | mpbir2and 944 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ (1...๐)) |
62 | 57, 58, 61 | rspcdva 2846 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐) |
63 | | vex 2740 |
. . . . . . . . . . . . . . 15
โข ๐ง โ V |
64 | | prmind.3 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ง โ (๐ โ ๐)) |
65 | 63, 64 | sbcie 2997 |
. . . . . . . . . . . . . 14
โข
([๐ง / ๐ฅ]๐ โ ๐) |
66 | | dfsbcq 2964 |
. . . . . . . . . . . . . 14
โข (๐ง = ((๐ + 1) / ๐ฆ) โ ([๐ง / ๐ฅ]๐ โ [((๐ + 1) / ๐ฆ) / ๐ฅ]๐)) |
67 | 65, 66 | bitr3id 194 |
. . . . . . . . . . . . 13
โข (๐ง = ((๐ + 1) / ๐ฆ) โ (๐ โ [((๐ + 1) / ๐ฆ) / ๐ฅ]๐)) |
68 | 64 | cbvralv 2703 |
. . . . . . . . . . . . . 14
โข
(โ๐ฅ โ
(1...๐)๐ โ โ๐ง โ (1...๐)๐) |
69 | 58, 68 | sylib 122 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ โ๐ง โ (1...๐)๐) |
70 | 17 | nnrpd 9693 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ + 1) โ
โ+) |
71 | 22 | nnrpd 9693 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ๐ฆ โ โ+) |
72 | 70, 71 | rpdivcld 9713 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) โ
โ+) |
73 | 72 | rpgt0d 9698 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ 0 < ((๐ + 1) / ๐ฆ)) |
74 | | elnnz 9262 |
. . . . . . . . . . . . . . 15
โข (((๐ + 1) / ๐ฆ) โ โ โ (((๐ + 1) / ๐ฆ) โ โค โง 0 < ((๐ + 1) / ๐ฆ))) |
75 | 32, 73, 74 | sylanbrc 417 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) โ โ) |
76 | 17 | nnap0d 8964 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ + 1) # 0) |
77 | 18, 76 | dividapd 8742 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / (๐ + 1)) = 1) |
78 | | eluz2gt1 9601 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ
(โคโฅโ2) โ 1 < ๐ฆ) |
79 | 20, 78 | syl 14 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ 1 < ๐ฆ) |
80 | 77, 79 | eqbrtrd 4025 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / (๐ + 1)) < ๐ฆ) |
81 | 17 | nngt0d 8962 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ 0 < (๐ + 1)) |
82 | | ltdiv23 8848 |
. . . . . . . . . . . . . . . . 17
โข (((๐ + 1) โ โ โง
((๐ + 1) โ โ
โง 0 < (๐ + 1)) โง
(๐ฆ โ โ โง 0
< ๐ฆ)) โ (((๐ + 1) / (๐ + 1)) < ๐ฆ โ ((๐ + 1) / ๐ฆ) < (๐ + 1))) |
83 | 49, 49, 81, 50, 51, 82 | syl122anc 1247 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (((๐ + 1) / (๐ + 1)) < ๐ฆ โ ((๐ + 1) / ๐ฆ) < (๐ + 1))) |
84 | 80, 83 | mpbid 147 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) < (๐ + 1)) |
85 | | zleltp1 9307 |
. . . . . . . . . . . . . . . 16
โข ((((๐ + 1) / ๐ฆ) โ โค โง ๐ โ โค) โ (((๐ + 1) / ๐ฆ) โค ๐ โ ((๐ + 1) / ๐ฆ) < (๐ + 1))) |
86 | 32, 43, 85 | syl2anc 411 |
. . . . . . . . . . . . . . 15
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (((๐ + 1) / ๐ฆ) โค ๐ โ ((๐ + 1) / ๐ฆ) < (๐ + 1))) |
87 | 84, 86 | mpbird 167 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) โค ๐) |
88 | | fznn 10088 |
. . . . . . . . . . . . . . 15
โข (๐ โ โค โ (((๐ + 1) / ๐ฆ) โ (1...๐) โ (((๐ + 1) / ๐ฆ) โ โ โง ((๐ + 1) / ๐ฆ) โค ๐))) |
89 | 43, 88 | syl 14 |
. . . . . . . . . . . . . 14
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (((๐ + 1) / ๐ฆ) โ (1...๐) โ (((๐ + 1) / ๐ฆ) โ โ โง ((๐ + 1) / ๐ฆ) โค ๐))) |
90 | 75, 87, 89 | mpbir2and 944 |
. . . . . . . . . . . . 13
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ ((๐ + 1) / ๐ฆ) โ (1...๐)) |
91 | 67, 69, 90 | rspcdva 2846 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ [((๐ + 1) / ๐ฆ) / ๐ฅ]๐) |
92 | 62, 91 | jca 306 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ (๐ โง [((๐ + 1) / ๐ฆ) / ๐ฅ]๐)) |
93 | 67 | anbi2d 464 |
. . . . . . . . . . . . . 14
โข (๐ง = ((๐ + 1) / ๐ฆ) โ ((๐ โง ๐) โ (๐ โง [((๐ + 1) / ๐ฆ) / ๐ฅ]๐))) |
94 | | oveq2 5882 |
. . . . . . . . . . . . . . 15
โข (๐ง = ((๐ + 1) / ๐ฆ) โ (๐ฆ ยท ๐ง) = (๐ฆ ยท ((๐ + 1) / ๐ฆ))) |
95 | 94 | sbceq1d 2967 |
. . . . . . . . . . . . . 14
โข (๐ง = ((๐ + 1) / ๐ฆ) โ ([(๐ฆ ยท ๐ง) / ๐ฅ]๐ โ [(๐ฆ ยท ((๐ + 1) / ๐ฆ)) / ๐ฅ]๐)) |
96 | 93, 95 | imbi12d 234 |
. . . . . . . . . . . . 13
โข (๐ง = ((๐ + 1) / ๐ฆ) โ (((๐ โง ๐) โ [(๐ฆ ยท ๐ง) / ๐ฅ]๐) โ ((๐ โง [((๐ + 1) / ๐ฆ) / ๐ฅ]๐) โ [(๐ฆ ยท ((๐ + 1) / ๐ฆ)) / ๐ฅ]๐))) |
97 | 96 | imbi2d 230 |
. . . . . . . . . . . 12
โข (๐ง = ((๐ + 1) / ๐ฆ) โ ((๐ฆ โ (โคโฅโ2)
โ ((๐ โง ๐) โ [(๐ฆ ยท ๐ง) / ๐ฅ]๐)) โ (๐ฆ โ (โคโฅโ2)
โ ((๐ โง
[((๐ + 1) / ๐ฆ) / ๐ฅ]๐) โ [(๐ฆ ยท ((๐ + 1) / ๐ฆ)) / ๐ฅ]๐)))) |
98 | | prmind2.8 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ ((๐ โง ๐) โ ๐)) |
99 | 98 | ancoms 268 |
. . . . . . . . . . . . . 14
โข ((๐ง โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ ((๐ โง ๐) โ ๐)) |
100 | | eluzelz 9536 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ
(โคโฅโ2) โ ๐ฆ โ โค) |
101 | 100 | adantl 277 |
. . . . . . . . . . . . . . . 16
โข ((๐ง โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ ๐ฆ โ
โค) |
102 | | eluzelz 9536 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ
(โคโฅโ2) โ ๐ง โ โค) |
103 | 102 | adantr 276 |
. . . . . . . . . . . . . . . 16
โข ((๐ง โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ ๐ง โ
โค) |
104 | 101, 103 | zmulcld 9380 |
. . . . . . . . . . . . . . 15
โข ((๐ง โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ (๐ฆ ยท ๐ง) โ
โค) |
105 | | prmind.4 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (๐ โ ๐)) |
106 | 105 | sbcieg 2995 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ ยท ๐ง) โ โค โ ([(๐ฆ ยท ๐ง) / ๐ฅ]๐ โ ๐)) |
107 | 104, 106 | syl 14 |
. . . . . . . . . . . . . 14
โข ((๐ง โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ ([(๐ฆ ยท
๐ง) / ๐ฅ]๐ โ ๐)) |
108 | 99, 107 | sylibrd 169 |
. . . . . . . . . . . . 13
โข ((๐ง โ
(โคโฅโ2) โง ๐ฆ โ (โคโฅโ2))
โ ((๐ โง ๐) โ [(๐ฆ ยท ๐ง) / ๐ฅ]๐)) |
109 | 108 | ex 115 |
. . . . . . . . . . . 12
โข (๐ง โ
(โคโฅโ2) โ (๐ฆ โ (โคโฅโ2)
โ ((๐ โง ๐) โ [(๐ฆ ยท ๐ง) / ๐ฅ]๐))) |
110 | 97, 109 | vtoclga 2803 |
. . . . . . . . . . 11
โข (((๐ + 1) / ๐ฆ) โ (โคโฅโ2)
โ (๐ฆ โ
(โคโฅโ2) โ ((๐ โง [((๐ + 1) / ๐ฆ) / ๐ฅ]๐) โ [(๐ฆ ยท ((๐ + 1) / ๐ฆ)) / ๐ฅ]๐))) |
111 | 56, 20, 92, 110 | syl3c 63 |
. . . . . . . . . 10
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ [(๐ฆ ยท ((๐ + 1) / ๐ฆ)) / ๐ฅ]๐) |
112 | 25, 111 | sbceq1dd 2968 |
. . . . . . . . 9
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง (๐ฆ โ (2...((๐ + 1) โ 1)) โง ๐ฆ โฅ (๐ + 1))) โ [(๐ + 1) / ๐ฅ]๐) |
113 | 112 | rexlimdvaa 2595 |
. . . . . . . 8
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1) โ [(๐ + 1) / ๐ฅ]๐)) |
114 | | ralnex 2465 |
. . . . . . . . 9
โข
(โ๐ฆ โ
(2...((๐ + 1) โ 1))
ยฌ ๐ฆ โฅ (๐ + 1) โ ยฌ โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1)) |
115 | | simpl 109 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ๐ โ โ) |
116 | | elnnuz 9563 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
117 | 115, 116 | sylib 122 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ๐ โ
(โคโฅโ1)) |
118 | | eluzp1p1 9552 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ1) โ (๐ + 1) โ (โคโฅโ(1
+ 1))) |
119 | 117, 118 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (๐ + 1) โ (โคโฅโ(1
+ 1))) |
120 | | df-2 8977 |
. . . . . . . . . . . . 13
โข 2 = (1 +
1) |
121 | 120 | fveq2i 5518 |
. . . . . . . . . . . 12
โข
(โคโฅโ2) = (โคโฅโ(1 +
1)) |
122 | 119, 121 | eleqtrrdi 2271 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (๐ + 1) โ
(โคโฅโ2)) |
123 | | isprm3 12117 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ โ โ
((๐ + 1) โ
(โคโฅโ2) โง โ๐ฆ โ (2...((๐ + 1) โ 1)) ยฌ ๐ฆ โฅ (๐ + 1))) |
124 | 123 | baibr 920 |
. . . . . . . . . . 11
โข ((๐ + 1) โ
(โคโฅโ2) โ (โ๐ฆ โ (2...((๐ + 1) โ 1)) ยฌ ๐ฆ โฅ (๐ + 1) โ (๐ + 1) โ โ)) |
125 | 122, 124 | syl 14 |
. . . . . . . . . 10
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (โ๐ฆ โ (2...((๐ + 1) โ 1)) ยฌ ๐ฆ โฅ (๐ + 1) โ (๐ + 1) โ โ)) |
126 | | simpr 110 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ โ๐ฅ โ (1...๐)๐) |
127 | 57 | cbvralv 2703 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
(1...๐)๐ โ โ๐ฆ โ (1...๐)๐) |
128 | 126, 127 | sylib 122 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ โ๐ฆ โ (1...๐)๐) |
129 | 115 | nncnd 8932 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ๐ โ โ) |
130 | 129, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ((๐ + 1) โ 1) = ๐) |
131 | 130 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (1...((๐ + 1) โ 1)) = (1...๐)) |
132 | 131 | raleqdv 2678 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (โ๐ฆ โ (1...((๐ + 1) โ 1))๐ โ โ๐ฆ โ (1...๐)๐)) |
133 | 128, 132 | mpbird 167 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ โ๐ฆ โ (1...((๐ + 1) โ 1))๐) |
134 | | nfcv 2319 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ(๐ + 1) |
135 | | nfv 1528 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅโ๐ฆ โ (1...((๐ + 1) โ 1))๐ |
136 | | nfsbc1v 2981 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ[(๐ + 1) / ๐ฅ]๐ |
137 | 135, 136 | nfim 1572 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ(โ๐ฆ โ (1...((๐ + 1) โ 1))๐ โ [(๐ + 1) / ๐ฅ]๐) |
138 | | oveq1 5881 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ + 1) โ (๐ฅ โ 1) = ((๐ + 1) โ 1)) |
139 | 138 | oveq2d 5890 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐ + 1) โ (1...(๐ฅ โ 1)) = (1...((๐ + 1) โ 1))) |
140 | 139 | raleqdv 2678 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ + 1) โ (โ๐ฆ โ (1...(๐ฅ โ 1))๐ โ โ๐ฆ โ (1...((๐ + 1) โ 1))๐)) |
141 | | sbceq1a 2972 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ + 1) โ (๐ โ [(๐ + 1) / ๐ฅ]๐)) |
142 | 140, 141 | imbi12d 234 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ + 1) โ ((โ๐ฆ โ (1...(๐ฅ โ 1))๐ โ ๐) โ (โ๐ฆ โ (1...((๐ + 1) โ 1))๐ โ [(๐ + 1) / ๐ฅ]๐))) |
143 | | prmind2.7 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง
โ๐ฆ โ
(1...(๐ฅ โ 1))๐) โ ๐) |
144 | 143 | ex 115 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
(โ๐ฆ โ
(1...(๐ฅ โ 1))๐ โ ๐)) |
145 | 134, 137,
142, 144 | vtoclgaf 2802 |
. . . . . . . . . . 11
โข ((๐ + 1) โ โ โ
(โ๐ฆ โ
(1...((๐ + 1) โ
1))๐ โ [(๐ + 1) / ๐ฅ]๐)) |
146 | 133, 145 | syl5com 29 |
. . . . . . . . . 10
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ((๐ + 1) โ โ โ [(๐ + 1) / ๐ฅ]๐)) |
147 | 125, 146 | sylbid 150 |
. . . . . . . . 9
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (โ๐ฆ โ (2...((๐ + 1) โ 1)) ยฌ ๐ฆ โฅ (๐ + 1) โ [(๐ + 1) / ๐ฅ]๐)) |
148 | 114, 147 | biimtrrid 153 |
. . . . . . . 8
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (ยฌ โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1) โ [(๐ + 1) / ๐ฅ]๐)) |
149 | | 2z 9280 |
. . . . . . . . . . 11
โข 2 โ
โค |
150 | 149 | a1i 9 |
. . . . . . . . . 10
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ 2 โ โค) |
151 | 115 | nnzd 9373 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ๐ โ โค) |
152 | 151 | peano2zd 9377 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (๐ + 1) โ โค) |
153 | | 1zzd 9279 |
. . . . . . . . . . 11
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ 1 โ โค) |
154 | 152, 153 | zsubcld 9379 |
. . . . . . . . . 10
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ ((๐ + 1) โ 1) โ
โค) |
155 | 19, 21 | syl 14 |
. . . . . . . . . . 11
โข (๐ฆ โ (2...((๐ + 1) โ 1)) โ ๐ฆ โ
โ) |
156 | | dvdsdc 11804 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง (๐ + 1) โ โค) โ
DECID ๐ฆ
โฅ (๐ +
1)) |
157 | 155, 152,
156 | syl2anr 290 |
. . . . . . . . . 10
โข (((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โง ๐ฆ โ (2...((๐ + 1) โ 1))) โ
DECID ๐ฆ
โฅ (๐ +
1)) |
158 | 150, 154,
157 | exfzdc 10239 |
. . . . . . . . 9
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ DECID โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1)) |
159 | | exmiddc 836 |
. . . . . . . . 9
โข
(DECID โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1) โ (โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1) โจ ยฌ โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1))) |
160 | 158, 159 | syl 14 |
. . . . . . . 8
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ (โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1) โจ ยฌ โ๐ฆ โ (2...((๐ + 1) โ 1))๐ฆ โฅ (๐ + 1))) |
161 | 113, 148,
160 | mpjaod 718 |
. . . . . . 7
โข ((๐ โ โ โง
โ๐ฅ โ (1...๐)๐) โ [(๐ + 1) / ๐ฅ]๐) |
162 | 161 | ex 115 |
. . . . . 6
โข (๐ โ โ โ
(โ๐ฅ โ
(1...๐)๐ โ [(๐ + 1) / ๐ฅ]๐)) |
163 | | ralsnsg 3629 |
. . . . . . 7
โข ((๐ + 1) โ โ โ
(โ๐ฅ โ {(๐ + 1)}๐ โ [(๐ + 1) / ๐ฅ]๐)) |
164 | 16, 163 | syl 14 |
. . . . . 6
โข (๐ โ โ โ
(โ๐ฅ โ {(๐ + 1)}๐ โ [(๐ + 1) / ๐ฅ]๐)) |
165 | 162, 164 | sylibrd 169 |
. . . . 5
โข (๐ โ โ โ
(โ๐ฅ โ
(1...๐)๐ โ โ๐ฅ โ {(๐ + 1)}๐)) |
166 | 165 | ancld 325 |
. . . 4
โข (๐ โ โ โ
(โ๐ฅ โ
(1...๐)๐ โ (โ๐ฅ โ (1...๐)๐ โง โ๐ฅ โ {(๐ + 1)}๐))) |
167 | | fzsuc 10068 |
. . . . . . 7
โข (๐ โ
(โคโฅโ1) โ (1...(๐ + 1)) = ((1...๐) โช {(๐ + 1)})) |
168 | 116, 167 | sylbi 121 |
. . . . . 6
โข (๐ โ โ โ
(1...(๐ + 1)) = ((1...๐) โช {(๐ + 1)})) |
169 | 168 | raleqdv 2678 |
. . . . 5
โข (๐ โ โ โ
(โ๐ฅ โ
(1...(๐ + 1))๐ โ โ๐ฅ โ ((1...๐) โช {(๐ + 1)})๐)) |
170 | | ralunb 3316 |
. . . . 5
โข
(โ๐ฅ โ
((1...๐) โช {(๐ + 1)})๐ โ (โ๐ฅ โ (1...๐)๐ โง โ๐ฅ โ {(๐ + 1)}๐)) |
171 | 169, 170 | bitrdi 196 |
. . . 4
โข (๐ โ โ โ
(โ๐ฅ โ
(1...(๐ + 1))๐ โ (โ๐ฅ โ (1...๐)๐ โง โ๐ฅ โ {(๐ + 1)}๐))) |
172 | 166, 171 | sylibrd 169 |
. . 3
โข (๐ โ โ โ
(โ๐ฅ โ
(1...๐)๐ โ โ๐ฅ โ (1...(๐ + 1))๐)) |
173 | 3, 5, 7, 9, 15, 172 | nnind 8934 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ (1...๐ด)๐) |
174 | | elfz1end 10054 |
. . 3
โข (๐ด โ โ โ ๐ด โ (1...๐ด)) |
175 | 174 | biimpi 120 |
. 2
โข (๐ด โ โ โ ๐ด โ (1...๐ด)) |
176 | 1, 173, 175 | rspcdva 2846 |
1
โข (๐ด โ โ โ ๐) |