Step | Hyp | Ref
| Expression |
1 | | nnz 9272 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โค) |
2 | | nnne0 8947 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ 0) |
3 | | peano2z 9289 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ + 1) โ
โค) |
4 | 3 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (๐ + 1) โ
โค) |
5 | | dvdsval2 11797 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ 0 โง (๐ + 1) โ โค) โ (๐ โฅ (๐ + 1) โ ((๐ + 1) / ๐) โ โค)) |
6 | 1, 2, 4, 5 | syl2an23an 1299 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ (๐ + 1) โ ((๐ + 1) / ๐) โ โค)) |
7 | 6 | biimpa 296 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((๐ + 1) / ๐) โ โค) |
8 | | flid 10284 |
. . . . . . 7
โข (((๐ + 1) / ๐) โ โค โ
(โโ((๐ + 1) /
๐)) = ((๐ + 1) / ๐)) |
9 | 7, 8 | syl 14 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ (โโ((๐ + 1) / ๐)) = ((๐ + 1) / ๐)) |
10 | | nnm1nn0 9217 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
11 | 10 | nn0red 9230 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
12 | 10 | nn0ge0d 9232 |
. . . . . . . . 9
โข (๐ โ โ โ 0 โค
(๐ โ
1)) |
13 | | nnre 8926 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
14 | | nngt0 8944 |
. . . . . . . . 9
โข (๐ โ โ โ 0 <
๐) |
15 | | divge0 8830 |
. . . . . . . . 9
โข ((((๐ โ 1) โ โ โง
0 โค (๐ โ 1)) โง
(๐ โ โ โง 0
< ๐)) โ 0 โค
((๐ โ 1) / ๐)) |
16 | 11, 12, 13, 14, 15 | syl22anc 1239 |
. . . . . . . 8
โข (๐ โ โ โ 0 โค
((๐ โ 1) / ๐)) |
17 | 16 | ad2antlr 489 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ 0 โค ((๐ โ 1) / ๐)) |
18 | 13 | ltm1d 8889 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ 1) < ๐) |
19 | | nncn 8927 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ) |
20 | 19 | mulridd 7974 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
21 | 18, 20 | breqtrrd 4032 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ 1) < (๐ ยท 1)) |
22 | | 1red 7972 |
. . . . . . . . . 10
โข (๐ โ โ โ 1 โ
โ) |
23 | | ltdivmul 8833 |
. . . . . . . . . 10
โข (((๐ โ 1) โ โ โง
1 โ โ โง (๐
โ โ โง 0 < ๐)) โ (((๐ โ 1) / ๐) < 1 โ (๐ โ 1) < (๐ ยท 1))) |
24 | 11, 22, 13, 14, 23 | syl112anc 1242 |
. . . . . . . . 9
โข (๐ โ โ โ (((๐ โ 1) / ๐) < 1 โ (๐ โ 1) < (๐ ยท 1))) |
25 | 21, 24 | mpbird 167 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ 1) / ๐) < 1) |
26 | 25 | ad2antlr 489 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((๐ โ 1) / ๐) < 1) |
27 | 10 | nn0zd 9373 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ โ 1) โ
โค) |
28 | | znq 9624 |
. . . . . . . . . 10
โข (((๐ โ 1) โ โค โง
๐ โ โ) โ
((๐ โ 1) / ๐) โ
โ) |
29 | 27, 28 | mpancom 422 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ 1) / ๐) โ โ) |
30 | 29 | ad2antlr 489 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((๐ โ 1) / ๐) โ โ) |
31 | | flqbi2 10291 |
. . . . . . . 8
โข ((((๐ + 1) / ๐) โ โค โง ((๐ โ 1) / ๐) โ โ) โ
((โโ(((๐ + 1) /
๐) + ((๐ โ 1) / ๐))) = ((๐ + 1) / ๐) โ (0 โค ((๐ โ 1) / ๐) โง ((๐ โ 1) / ๐) < 1))) |
32 | 7, 30, 31 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((โโ(((๐ + 1) / ๐) + ((๐ โ 1) / ๐))) = ((๐ + 1) / ๐) โ (0 โค ((๐ โ 1) / ๐) โง ((๐ โ 1) / ๐) < 1))) |
33 | 17, 26, 32 | mpbir2and 944 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ (โโ(((๐ + 1) / ๐) + ((๐ โ 1) / ๐))) = ((๐ + 1) / ๐)) |
34 | 9, 33 | eqtr4d 2213 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ (โโ((๐ + 1) / ๐)) = (โโ(((๐ + 1) / ๐) + ((๐ โ 1) / ๐)))) |
35 | | zcn 9258 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
36 | 35 | adantr 276 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
37 | 19 | adantl 277 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
38 | | nnap0 8948 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ # 0) |
39 | 38 | adantl 277 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ๐ # 0) |
40 | 36, 37, 37, 39 | divdirapd 8786 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + ๐) / ๐) = ((๐ / ๐) + (๐ / ๐))) |
41 | | ax-1cn 7904 |
. . . . . . . . . . . 12
โข 1 โ
โ |
42 | 41 | a1i 9 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ 1 โ
โ) |
43 | 36, 42, 37 | ppncand 8308 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) + (๐ โ 1)) = (๐ + ๐)) |
44 | 43 | oveq1d 5890 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) + (๐ โ 1)) / ๐) = ((๐ + ๐) / ๐)) |
45 | 4 | zcnd 9376 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (๐ + 1) โ
โ) |
46 | | subcl 8156 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
47 | 19, 41, 46 | sylancl 413 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ โ 1) โ
โ) |
48 | 47 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โ 1) โ
โ) |
49 | 45, 48, 37, 39 | divdirapd 8786 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) + (๐ โ 1)) / ๐) = (((๐ + 1) / ๐) + ((๐ โ 1) / ๐))) |
50 | 44, 49 | eqtr3d 2212 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + ๐) / ๐) = (((๐ + 1) / ๐) + ((๐ โ 1) / ๐))) |
51 | 37, 39 | dividapd 8743 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) = 1) |
52 | 51 | oveq2d 5891 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) + (๐ / ๐)) = ((๐ / ๐) + 1)) |
53 | 40, 50, 52 | 3eqtr3d 2218 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) / ๐) + ((๐ โ 1) / ๐)) = ((๐ / ๐) + 1)) |
54 | 53 | fveq2d 5520 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ(((๐ + 1) /
๐) + ((๐ โ 1) / ๐))) = (โโ((๐ / ๐) + 1))) |
55 | 54 | adantr 276 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ (โโ(((๐ + 1) / ๐) + ((๐ โ 1) / ๐))) = (โโ((๐ / ๐) + 1))) |
56 | | znq 9624 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
57 | | 1z 9279 |
. . . . . . 7
โข 1 โ
โค |
58 | | flqaddz 10297 |
. . . . . . 7
โข (((๐ / ๐) โ โ โง 1 โ โค)
โ (โโ((๐ /
๐) + 1)) =
((โโ(๐ / ๐)) + 1)) |
59 | 56, 57, 58 | sylancl 413 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ((๐ / ๐) + 1)) = ((โโ(๐ / ๐)) + 1)) |
60 | 59 | adantr 276 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ (โโ((๐ / ๐) + 1)) = ((โโ(๐ / ๐)) + 1)) |
61 | 34, 55, 60 | 3eqtrrd 2215 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((โโ(๐ / ๐)) + 1) = (โโ((๐ + 1) / ๐))) |
62 | | znq 9624 |
. . . . . . . . 9
โข (((๐ + 1) โ โค โง ๐ โ โ) โ ((๐ + 1) / ๐) โ โ) |
63 | 3, 62 | sylan 283 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) / ๐) โ โ) |
64 | 63 | flqcld 10277 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ((๐ + 1) /
๐)) โ
โค) |
65 | 64 | zcnd 9376 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ((๐ + 1) /
๐)) โ
โ) |
66 | 56 | flqcld 10277 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ(๐ / ๐)) โ
โค) |
67 | 66 | zcnd 9376 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โ) โ
(โโ(๐ / ๐)) โ
โ) |
68 | 65, 67, 42 | subaddd 8286 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ
(((โโ((๐ + 1) /
๐)) โ
(โโ(๐ / ๐))) = 1 โ
((โโ(๐ / ๐)) + 1) = (โโ((๐ + 1) / ๐)))) |
69 | 68 | adantr 276 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ (((โโ((๐ + 1) / ๐)) โ (โโ(๐ / ๐))) = 1 โ ((โโ(๐ / ๐)) + 1) = (โโ((๐ + 1) / ๐)))) |
70 | 61, 69 | mpbird 167 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((โโ((๐ + 1) / ๐)) โ (โโ(๐ / ๐))) = 1) |
71 | | iftrue 3540 |
. . . 4
โข (๐ โฅ (๐ + 1) โ if(๐ โฅ (๐ + 1), 1, 0) = 1) |
72 | 71 | adantl 277 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ if(๐ โฅ (๐ + 1), 1, 0) = 1) |
73 | 70, 72 | eqtr4d 2213 |
. 2
โข (((๐ โ โค โง ๐ โ โ) โง ๐ โฅ (๐ + 1)) โ ((โโ((๐ + 1) / ๐)) โ (โโ(๐ / ๐))) = if(๐ โฅ (๐ + 1), 1, 0)) |
74 | | zmodcl 10344 |
. . . . . . . . . . 11
โข (((๐ + 1) โ โค โง ๐ โ โ) โ ((๐ + 1) mod ๐) โ
โ0) |
75 | 3, 74 | sylan 283 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) mod ๐) โ
โ0) |
76 | 75 | nn0red 9230 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) mod ๐) โ โ) |
77 | | 1re 7956 |
. . . . . . . . 9
โข 1 โ
โ |
78 | | resubcl 8221 |
. . . . . . . . 9
โข ((((๐ + 1) mod ๐) โ โ โง 1 โ โ)
โ (((๐ + 1) mod ๐) โ 1) โ
โ) |
79 | 76, 77, 78 | sylancl 413 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) โ
โ) |
80 | 79 | adantr 276 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ (((๐ + 1) mod ๐) โ 1) โ
โ) |
81 | 75 | nn0zd 9373 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) mod ๐) โ โค) |
82 | | elnndc 9612 |
. . . . . . . . . . . 12
โข (((๐ + 1) mod ๐) โ โค โ DECID
((๐ + 1) mod ๐) โ
โ) |
83 | 81, 82 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ
DECID ((๐ +
1) mod ๐) โ
โ) |
84 | | elnn0 9178 |
. . . . . . . . . . . . . 14
โข (((๐ + 1) mod ๐) โ โ0 โ (((๐ + 1) mod ๐) โ โ โจ ((๐ + 1) mod ๐) = 0)) |
85 | 75, 84 | sylib 122 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ โ โจ ((๐ + 1) mod ๐) = 0)) |
86 | 85 | ord 724 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ (ยฌ
((๐ + 1) mod ๐) โ โ โ ((๐ + 1) mod ๐) = 0)) |
87 | | id 19 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
88 | | dvdsval3 11798 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ + 1) โ โค) โ
(๐ โฅ (๐ + 1) โ ((๐ + 1) mod ๐) = 0)) |
89 | 87, 3, 88 | syl2anr 290 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ (๐ + 1) โ ((๐ + 1) mod ๐) = 0)) |
90 | 86, 89 | sylibrd 169 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ (ยฌ
((๐ + 1) mod ๐) โ โ โ ๐ โฅ (๐ + 1))) |
91 | | con1dc 856 |
. . . . . . . . . . 11
โข
(DECID ((๐ + 1) mod ๐) โ โ โ ((ยฌ ((๐ + 1) mod ๐) โ โ โ ๐ โฅ (๐ + 1)) โ (ยฌ ๐ โฅ (๐ + 1) โ ((๐ + 1) mod ๐) โ โ))) |
92 | 83, 90, 91 | sylc 62 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (ยฌ
๐ โฅ (๐ + 1) โ ((๐ + 1) mod ๐) โ โ)) |
93 | 92 | imp 124 |
. . . . . . . . 9
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ ((๐ + 1) mod ๐) โ โ) |
94 | | nnm1nn0 9217 |
. . . . . . . . 9
โข (((๐ + 1) mod ๐) โ โ โ (((๐ + 1) mod ๐) โ 1) โ
โ0) |
95 | 93, 94 | syl 14 |
. . . . . . . 8
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ (((๐ + 1) mod ๐) โ 1) โ
โ0) |
96 | 95 | nn0ge0d 9232 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ 0 โค (((๐ + 1) mod ๐) โ 1)) |
97 | 13, 14 | jca 306 |
. . . . . . . 8
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
98 | 97 | ad2antlr 489 |
. . . . . . 7
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ (๐ โ โ โง 0 < ๐)) |
99 | | divge0 8830 |
. . . . . . 7
โข
((((((๐ + 1) mod
๐) โ 1) โ
โ โง 0 โค (((๐ +
1) mod ๐) โ 1)) โง
(๐ โ โ โง 0
< ๐)) โ 0 โค
((((๐ + 1) mod ๐) โ 1) / ๐)) |
100 | 80, 96, 98, 99 | syl21anc 1237 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ 0 โค ((((๐ + 1) mod ๐) โ 1) / ๐)) |
101 | 13 | adantl 277 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
102 | 76 | ltm1d 8889 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) < ((๐ + 1) mod ๐)) |
103 | | zq 9626 |
. . . . . . . . . . . . 13
โข ((๐ + 1) โ โค โ
(๐ + 1) โ
โ) |
104 | 3, 103 | syl 14 |
. . . . . . . . . . . 12
โข (๐ โ โค โ (๐ + 1) โ
โ) |
105 | 104 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ (๐ + 1) โ
โ) |
106 | | nnq 9633 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
107 | 106 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
108 | 14 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ 0 <
๐) |
109 | | modqlt 10333 |
. . . . . . . . . . 11
โข (((๐ + 1) โ โ โง ๐ โ โ โง 0 <
๐) โ ((๐ + 1) mod ๐) < ๐) |
110 | 105, 107,
108, 109 | syl3anc 1238 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) mod ๐) < ๐) |
111 | 79, 76, 101, 102, 110 | lttrd 8083 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) < ๐) |
112 | 37 | mulridd 7974 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท 1) = ๐) |
113 | 111, 112 | breqtrrd 4032 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) < (๐ ยท 1)) |
114 | | 1red 7972 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ 1 โ
โ) |
115 | | ltdivmul 8833 |
. . . . . . . . 9
โข
(((((๐ + 1) mod
๐) โ 1) โ
โ โง 1 โ โ โง (๐ โ โ โง 0 < ๐)) โ (((((๐ + 1) mod ๐) โ 1) / ๐) < 1 โ (((๐ + 1) mod ๐) โ 1) < (๐ ยท 1))) |
116 | 79, 114, 101, 108, 115 | syl112anc 1242 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ
(((((๐ + 1) mod ๐) โ 1) / ๐) < 1 โ (((๐ + 1) mod ๐) โ 1) < (๐ ยท 1))) |
117 | 113, 116 | mpbird 167 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ
((((๐ + 1) mod ๐) โ 1) / ๐) < 1) |
118 | 117 | adantr 276 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ ((((๐ + 1) mod ๐) โ 1) / ๐) < 1) |
119 | | peano2zm 9291 |
. . . . . . . . . 10
โข (((๐ + 1) mod ๐) โ โค โ (((๐ + 1) mod ๐) โ 1) โ
โค) |
120 | 81, 119 | syl 14 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) โ
โค) |
121 | | znq 9624 |
. . . . . . . . 9
โข
(((((๐ + 1) mod
๐) โ 1) โ
โค โง ๐ โ
โ) โ ((((๐ + 1)
mod ๐) โ 1) / ๐) โ
โ) |
122 | 120, 121 | sylancom 420 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ
((((๐ + 1) mod ๐) โ 1) / ๐) โ โ) |
123 | | flqbi2 10291 |
. . . . . . . 8
โข
(((โโ((๐
+ 1) / ๐)) โ โค
โง ((((๐ + 1) mod ๐) โ 1) / ๐) โ โ) โ
((โโ((โโ((๐ + 1) / ๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐))) = (โโ((๐ + 1) / ๐)) โ (0 โค ((((๐ + 1) mod ๐) โ 1) / ๐) โง ((((๐ + 1) mod ๐) โ 1) / ๐) < 1))) |
124 | 64, 122, 123 | syl2anc 411 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ((โโ((๐ + 1) / ๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐))) = (โโ((๐ + 1) / ๐)) โ (0 โค ((((๐ + 1) mod ๐) โ 1) / ๐) โง ((((๐ + 1) mod ๐) โ 1) / ๐) < 1))) |
125 | 124 | adantr 276 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
((โโ((โโ((๐ + 1) / ๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐))) = (โโ((๐ + 1) / ๐)) โ (0 โค ((((๐ + 1) mod ๐) โ 1) / ๐) โง ((((๐ + 1) mod ๐) โ 1) / ๐) < 1))) |
126 | 100, 118,
125 | mpbir2and 944 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
(โโ((โโ((๐ + 1) / ๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐))) = (โโ((๐ + 1) / ๐))) |
127 | | modqval 10324 |
. . . . . . . . . . . . 13
โข (((๐ + 1) โ โ โง ๐ โ โ โง 0 <
๐) โ ((๐ + 1) mod ๐) = ((๐ + 1) โ (๐ ยท (โโ((๐ + 1) / ๐))))) |
128 | 105, 107,
108, 127 | syl3anc 1238 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) mod ๐) = ((๐ + 1) โ (๐ ยท (โโ((๐ + 1) / ๐))))) |
129 | 128 | oveq1d 5890 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) = (((๐ + 1) โ (๐ ยท (โโ((๐ + 1) / ๐)))) โ 1)) |
130 | 37, 65 | mulcld 7978 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ (๐ ยท (โโ((๐ + 1) / ๐))) โ โ) |
131 | 45, 42, 130 | sub32d 8300 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) โ 1) โ (๐ ยท (โโ((๐ + 1) / ๐)))) = (((๐ + 1) โ (๐ ยท (โโ((๐ + 1) / ๐)))) โ 1)) |
132 | | pncan 8163 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
133 | 36, 41, 132 | sylancl 413 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ + 1) โ 1) = ๐) |
134 | 133 | oveq1d 5890 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) โ 1) โ (๐ ยท (โโ((๐ + 1) / ๐)))) = (๐ โ (๐ ยท (โโ((๐ + 1) / ๐))))) |
135 | 129, 131,
134 | 3eqtr2d 2216 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ + 1) mod ๐) โ 1) = (๐ โ (๐ ยท (โโ((๐ + 1) / ๐))))) |
136 | 135 | oveq1d 5890 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ
((((๐ + 1) mod ๐) โ 1) / ๐) = ((๐ โ (๐ ยท (โโ((๐ + 1) / ๐)))) / ๐)) |
137 | 36, 130, 37, 39 | divsubdirapd 8787 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ โ (๐ ยท (โโ((๐ + 1) / ๐)))) / ๐) = ((๐ / ๐) โ ((๐ ยท (โโ((๐ + 1) / ๐))) / ๐))) |
138 | 65, 37, 39 | divcanap3d 8752 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ ยท (โโ((๐ + 1) / ๐))) / ๐) = (โโ((๐ + 1) / ๐))) |
139 | 138 | oveq2d 5891 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) โ ((๐ ยท (โโ((๐ + 1) / ๐))) / ๐)) = ((๐ / ๐) โ (โโ((๐ + 1) / ๐)))) |
140 | 136, 137,
139 | 3eqtrrd 2215 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ ((๐ / ๐) โ (โโ((๐ + 1) / ๐))) = ((((๐ + 1) mod ๐) โ 1) / ๐)) |
141 | | zre 9257 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ
โ) |
142 | | nndivre 8955 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ โ) โ (๐ / ๐) โ โ) |
143 | 141, 142 | sylan 283 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
144 | 143 | recnd 7986 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ (๐ / ๐) โ โ) |
145 | | nndivre 8955 |
. . . . . . . . . . 11
โข
(((((๐ + 1) mod
๐) โ 1) โ
โ โง ๐ โ
โ) โ ((((๐ + 1)
mod ๐) โ 1) / ๐) โ
โ) |
146 | 79, 145 | sylancom 420 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ โ โ) โ
((((๐ + 1) mod ๐) โ 1) / ๐) โ โ) |
147 | 146 | recnd 7986 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ โ โ) โ
((((๐ + 1) mod ๐) โ 1) / ๐) โ โ) |
148 | 144, 65, 147 | subaddd 8286 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ โ โ) โ (((๐ / ๐) โ (โโ((๐ + 1) / ๐))) = ((((๐ + 1) mod ๐) โ 1) / ๐) โ ((โโ((๐ + 1) / ๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐)) = (๐ / ๐))) |
149 | 140, 148 | mpbid 147 |
. . . . . . 7
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ((๐ + 1) /
๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐)) = (๐ / ๐)) |
150 | 149 | adantr 276 |
. . . . . 6
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
((โโ((๐ + 1) /
๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐)) = (๐ / ๐)) |
151 | 150 | fveq2d 5520 |
. . . . 5
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
(โโ((โโ((๐ + 1) / ๐)) + ((((๐ + 1) mod ๐) โ 1) / ๐))) = (โโ(๐ / ๐))) |
152 | 126, 151 | eqtr3d 2212 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
(โโ((๐ + 1) /
๐)) = (โโ(๐ / ๐))) |
153 | 65, 67 | subeq0ad 8278 |
. . . . 5
โข ((๐ โ โค โง ๐ โ โ) โ
(((โโ((๐ + 1) /
๐)) โ
(โโ(๐ / ๐))) = 0 โ
(โโ((๐ + 1) /
๐)) = (โโ(๐ / ๐)))) |
154 | 153 | adantr 276 |
. . . 4
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
(((โโ((๐ + 1) /
๐)) โ
(โโ(๐ / ๐))) = 0 โ
(โโ((๐ + 1) /
๐)) = (โโ(๐ / ๐)))) |
155 | 152, 154 | mpbird 167 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
((โโ((๐ + 1) /
๐)) โ
(โโ(๐ / ๐))) = 0) |
156 | | iffalse 3543 |
. . . 4
โข (ยฌ
๐ โฅ (๐ + 1) โ if(๐ โฅ (๐ + 1), 1, 0) = 0) |
157 | 156 | adantl 277 |
. . 3
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ if(๐ โฅ (๐ + 1), 1, 0) = 0) |
158 | 155, 157 | eqtr4d 2213 |
. 2
โข (((๐ โ โค โง ๐ โ โ) โง ยฌ
๐ โฅ (๐ + 1)) โ
((โโ((๐ + 1) /
๐)) โ
(โโ(๐ / ๐))) = if(๐ โฅ (๐ + 1), 1, 0)) |
159 | | simpr 110 |
. . . 4
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โ
โ) |
160 | | dvdsdc 11805 |
. . . 4
โข ((๐ โ โ โง (๐ + 1) โ โค) โ
DECID ๐
โฅ (๐ +
1)) |
161 | 159, 4, 160 | syl2anc 411 |
. . 3
โข ((๐ โ โค โง ๐ โ โ) โ
DECID ๐
โฅ (๐ +
1)) |
162 | | exmiddc 836 |
. . 3
โข
(DECID ๐ โฅ (๐ + 1) โ (๐ โฅ (๐ + 1) โจ ยฌ ๐ โฅ (๐ + 1))) |
163 | 161, 162 | syl 14 |
. 2
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ (๐ + 1) โจ ยฌ ๐ โฅ (๐ + 1))) |
164 | 73, 158, 163 | mpjaodan 798 |
1
โข ((๐ โ โค โง ๐ โ โ) โ
((โโ((๐ + 1) /
๐)) โ
(โโ(๐ / ๐))) = if(๐ โฅ (๐ + 1), 1, 0)) |