Step | Hyp | Ref
| Expression |
1 | | sbequ 1840 |
. . . . . . 7
โข (๐ค = ๐ง โ ([๐ค / ๐]๐ โ [๐ง / ๐]๐)) |
2 | 1 | anbi2d 464 |
. . . . . 6
โข (๐ค = ๐ง โ ((๐ โง [๐ค / ๐]๐) โ (๐ โง [๐ง / ๐]๐))) |
3 | | sbequ 1840 |
. . . . . . . . . 10
โข (๐ค = ๐ง โ ([๐ค / ๐ฅ]๐ โ [๐ง / ๐ฅ]๐)) |
4 | 3 | anbi1d 465 |
. . . . . . . . 9
โข (๐ค = ๐ง โ (([๐ค / ๐ฅ]๐ โง ๐) โ ([๐ง / ๐ฅ]๐ โง ๐))) |
5 | 4 | rexbidv 2478 |
. . . . . . . 8
โข (๐ค = ๐ง โ (โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐) โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
6 | 5 | imbi2d 230 |
. . . . . . 7
โข (๐ค = ๐ง โ (([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) โ ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
7 | 6 | ralbidv 2477 |
. . . . . 6
โข (๐ค = ๐ง โ (โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
8 | 2, 7 | imbi12d 234 |
. . . . 5
โข (๐ค = ๐ง โ (((๐ โง [๐ค / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) โ ((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))))) |
9 | | sbequ 1840 |
. . . . . . 7
โข (๐ค = ๐ฅ โ ([๐ค / ๐]๐ โ [๐ฅ / ๐]๐)) |
10 | 9 | anbi2d 464 |
. . . . . 6
โข (๐ค = ๐ฅ โ ((๐ โง [๐ค / ๐]๐) โ (๐ โง [๐ฅ / ๐]๐))) |
11 | | sbequ12r 1772 |
. . . . . . . . . 10
โข (๐ค = ๐ฅ โ ([๐ค / ๐ฅ]๐ โ ๐)) |
12 | 11 | anbi1d 465 |
. . . . . . . . 9
โข (๐ค = ๐ฅ โ (([๐ค / ๐ฅ]๐ โง ๐) โ (๐ โง ๐))) |
13 | 12 | rexbidv 2478 |
. . . . . . . 8
โข (๐ค = ๐ฅ โ (โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐) โ โ๐ โ โ0 (๐ โง ๐))) |
14 | 13 | imbi2d 230 |
. . . . . . 7
โข (๐ค = ๐ฅ โ (([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) โ ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐)))) |
15 | 14 | ralbidv 2477 |
. . . . . 6
โข (๐ค = ๐ฅ โ (โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐)))) |
16 | 10, 15 | imbi12d 234 |
. . . . 5
โข (๐ค = ๐ฅ โ (((๐ โง [๐ค / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) โ ((๐ โง [๐ฅ / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐))))) |
17 | | nfv 1528 |
. . . . . . . . . . 11
โข
โฒ๐ฆ ๐ค โ
โ0 |
18 | | nfcv 2319 |
. . . . . . . . . . . 12
โข
โฒ๐ฆ(0...(๐ค โ 1)) |
19 | | nfv 1528 |
. . . . . . . . . . . . 13
โข
โฒ๐ฆ(๐ โง [๐ง / ๐]๐) |
20 | | nfra1 2508 |
. . . . . . . . . . . . 13
โข
โฒ๐ฆโ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) |
21 | 19, 20 | nfim 1572 |
. . . . . . . . . . . 12
โข
โฒ๐ฆ((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
22 | 18, 21 | nfralxy 2515 |
. . . . . . . . . . 11
โข
โฒ๐ฆโ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
23 | 17, 22 | nfan 1565 |
. . . . . . . . . 10
โข
โฒ๐ฆ(๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
24 | | nfv 1528 |
. . . . . . . . . 10
โข
โฒ๐ฆ(๐ โง [๐ค / ๐]๐) |
25 | 23, 24 | nfan 1565 |
. . . . . . . . 9
โข
โฒ๐ฆ((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) |
26 | | nfv 1528 |
. . . . . . . . 9
โข
โฒ๐ฆ ๐ค = 0 |
27 | 25, 26 | nfan 1565 |
. . . . . . . 8
โข
โฒ๐ฆ(((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) |
28 | | simplr 528 |
. . . . . . . . . 10
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ ๐ฆ โ โ0) |
29 | | nfv 1528 |
. . . . . . . . . . . . . 14
โข
โฒ๐โ๐ง โ โ0 (๐ง โฅ ๐ฆ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)) |
30 | | breq2 4009 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ฆ โ (๐ง โฅ ๐ โ ๐ง โฅ ๐ฆ)) |
31 | 30 | imbi1d 231 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ฆ โ ((๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)) โ (๐ง โฅ ๐ฆ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)))) |
32 | 31 | ralbidv 2477 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ฆ โ (โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)) โ โ๐ง โ โ0 (๐ง โฅ ๐ฆ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)))) |
33 | 29, 32 | sbie 1791 |
. . . . . . . . . . . . 13
โข ([๐ฆ / ๐]โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)) โ โ๐ง โ โ0 (๐ง โฅ ๐ฆ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ))) |
34 | | nn0z 9275 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ โ0
โ ๐ง โ
โค) |
35 | | dvds0 11815 |
. . . . . . . . . . . . . . . 16
โข (๐ง โ โค โ ๐ง โฅ 0) |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . . . 15
โข (๐ง โ โ0
โ ๐ง โฅ
0) |
37 | 36 | biantrurd 305 |
. . . . . . . . . . . . . 14
โข (๐ง โ โ0
โ (๐ง โฅ ๐ฆ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ))) |
38 | 37 | biimpd 144 |
. . . . . . . . . . . . 13
โข (๐ง โ โ0
โ (๐ง โฅ ๐ฆ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ))) |
39 | 33, 38 | mprgbir 2535 |
. . . . . . . . . . . 12
โข [๐ฆ / ๐]โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)) |
40 | | nfv 1528 |
. . . . . . . . . . . . 13
โข
โฒ๐ ๐ค = 0 |
41 | | dfsbcq2 2967 |
. . . . . . . . . . . . . 14
โข (๐ค = 0 โ ([๐ค / ๐ฅ]๐ โ [0 / ๐ฅ]๐)) |
42 | | bezout.sub-gcd |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ))) |
43 | 42 | sbcbii 3024 |
. . . . . . . . . . . . . . 15
โข
([0 / ๐ฅ]๐ โ [0 / ๐ฅ]โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ))) |
44 | | c0ex 7953 |
. . . . . . . . . . . . . . . 16
โข 0 โ
V |
45 | | breq2 4009 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = 0 โ (๐ง โฅ ๐ฅ โ ๐ง โฅ 0)) |
46 | 45 | anbi1d 465 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = 0 โ ((๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ) โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ))) |
47 | 46 | imbi2d 230 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = 0 โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ)) โ (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)))) |
48 | 47 | ralbidv 2477 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = 0 โ (โ๐ง โ โ0
(๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ)) โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)))) |
49 | 44, 48 | sbcie 2999 |
. . . . . . . . . . . . . . 15
โข
([0 / ๐ฅ]โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ)) โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ))) |
50 | 43, 49 | bitri 184 |
. . . . . . . . . . . . . 14
โข
([0 / ๐ฅ]๐ โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ))) |
51 | 41, 50 | bitrdi 196 |
. . . . . . . . . . . . 13
โข (๐ค = 0 โ ([๐ค / ๐ฅ]๐ โ โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)))) |
52 | 40, 51 | sbbid 1846 |
. . . . . . . . . . . 12
โข (๐ค = 0 โ ([๐ฆ / ๐][๐ค / ๐ฅ]๐ โ [๐ฆ / ๐]โ๐ง โ โ0 (๐ง โฅ ๐ โ (๐ง โฅ 0 โง ๐ง โฅ ๐ฆ)))) |
53 | 39, 52 | mpbiri 168 |
. . . . . . . . . . 11
โข (๐ค = 0 โ [๐ฆ / ๐][๐ค / ๐ฅ]๐) |
54 | 53 | ad3antlr 493 |
. . . . . . . . . 10
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ [๐ฆ / ๐][๐ค / ๐ฅ]๐) |
55 | | simpr 110 |
. . . . . . . . . 10
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ [๐ฆ / ๐]๐) |
56 | | nfs1v 1939 |
. . . . . . . . . . . 12
โข
โฒ๐[๐ฆ / ๐][๐ค / ๐ฅ]๐ |
57 | | nfs1v 1939 |
. . . . . . . . . . . 12
โข
โฒ๐[๐ฆ / ๐]๐ |
58 | 56, 57 | nfan 1565 |
. . . . . . . . . . 11
โข
โฒ๐([๐ฆ / ๐][๐ค / ๐ฅ]๐ โง [๐ฆ / ๐]๐) |
59 | | sbequ12 1771 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ ([๐ค / ๐ฅ]๐ โ [๐ฆ / ๐][๐ค / ๐ฅ]๐)) |
60 | | sbequ12 1771 |
. . . . . . . . . . . 12
โข (๐ = ๐ฆ โ (๐ โ [๐ฆ / ๐]๐)) |
61 | 59, 60 | anbi12d 473 |
. . . . . . . . . . 11
โข (๐ = ๐ฆ โ (([๐ค / ๐ฅ]๐ โง ๐) โ ([๐ฆ / ๐][๐ค / ๐ฅ]๐ โง [๐ฆ / ๐]๐))) |
62 | 58, 61 | rspce 2838 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ([๐ฆ / ๐][๐ค / ๐ฅ]๐ โง [๐ฆ / ๐]๐)) โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) |
63 | 28, 54, 55, 62 | syl12anc 1236 |
. . . . . . . . 9
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) |
64 | 63 | exp31 364 |
. . . . . . . 8
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) โ (๐ฆ โ โ0 โ ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)))) |
65 | 27, 64 | ralrimi 2548 |
. . . . . . 7
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง ๐ค = 0) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) |
66 | | nfv 1528 |
. . . . . . . . . 10
โข
โฒ๐ฆ0 < ๐ค |
67 | 25, 66 | nfan 1565 |
. . . . . . . . 9
โข
โฒ๐ฆ(((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) |
68 | | bezout.is-bezout |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ โค โ๐ก โ โค ๐ = ((๐ด ยท ๐ ) + (๐ต ยท ๐ก))) |
69 | | simplrl 535 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ ๐) |
70 | | bezout.a |
. . . . . . . . . . . . 13
โข (๐ โ ๐ด โ
โ0) |
71 | 69, 70 | syl 14 |
. . . . . . . . . . . 12
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ ๐ด โ
โ0) |
72 | 71 | ad2antrr 488 |
. . . . . . . . . . 11
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ ๐ด โ
โ0) |
73 | | bezout.b |
. . . . . . . . . . . . 13
โข (๐ โ ๐ต โ
โ0) |
74 | 69, 73 | syl 14 |
. . . . . . . . . . . 12
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ ๐ต โ
โ0) |
75 | 74 | ad2antrr 488 |
. . . . . . . . . . 11
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ ๐ต โ
โ0) |
76 | | simplll 533 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ ๐ค โ โ0) |
77 | | simpr 110 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ 0 < ๐ค) |
78 | | elnnnn0b 9222 |
. . . . . . . . . . . . 13
โข (๐ค โ โ โ (๐ค โ โ0
โง 0 < ๐ค)) |
79 | 76, 77, 78 | sylanbrc 417 |
. . . . . . . . . . . 12
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ ๐ค โ โ) |
80 | 79 | ad2antrr 488 |
. . . . . . . . . . 11
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ ๐ค โ โ) |
81 | | simpr 110 |
. . . . . . . . . . 11
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ [๐ฆ / ๐]๐) |
82 | | simplr 528 |
. . . . . . . . . . 11
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ ๐ฆ โ โ0) |
83 | | simplrr 536 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ [๐ค / ๐]๐) |
84 | | sbsbc 2968 |
. . . . . . . . . . . . 13
โข ([๐ค / ๐]๐ โ [๐ค / ๐]๐) |
85 | 83, 84 | sylib 122 |
. . . . . . . . . . . 12
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ [๐ค / ๐]๐) |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . 11
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ [๐ค / ๐]๐) |
87 | | breq1 4008 |
. . . . . . . . . . . . . 14
โข (๐ง = ๐ โ (๐ง โฅ ๐ โ ๐ โฅ ๐)) |
88 | | breq1 4008 |
. . . . . . . . . . . . . . 15
โข (๐ง = ๐ โ (๐ง โฅ ๐ฅ โ ๐ โฅ ๐ฅ)) |
89 | | breq1 4008 |
. . . . . . . . . . . . . . 15
โข (๐ง = ๐ โ (๐ง โฅ ๐ฆ โ ๐ โฅ ๐ฆ)) |
90 | 88, 89 | anbi12d 473 |
. . . . . . . . . . . . . 14
โข (๐ง = ๐ โ ((๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ) โ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฆ))) |
91 | 87, 90 | imbi12d 234 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ ((๐ง โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ)) โ (๐ โฅ ๐ โ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฆ)))) |
92 | 91 | cbvralv 2705 |
. . . . . . . . . . . 12
โข
(โ๐ง โ
โ0 (๐ง
โฅ ๐ โ (๐ง โฅ ๐ฅ โง ๐ง โฅ ๐ฆ)) โ โ๐ โ โ0 (๐ โฅ ๐ โ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฆ))) |
93 | 42, 92 | bitri 184 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ โ0 (๐ โฅ ๐ โ (๐ โฅ ๐ฅ โง ๐ โฅ ๐ฆ))) |
94 | 69 | ad3antrrr 492 |
. . . . . . . . . . . . 13
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ ๐) |
95 | | simpr 110 |
. . . . . . . . . . . . 13
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ [(๐ฆ mod ๐ค) / ๐]๐) |
96 | 94, 95 | jca 306 |
. . . . . . . . . . . 12
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ (๐ โง [(๐ฆ mod ๐ค) / ๐]๐)) |
97 | 83 | ad3antrrr 492 |
. . . . . . . . . . . 12
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ [๐ค / ๐]๐) |
98 | | dfsbcq2 2967 |
. . . . . . . . . . . . . . 15
โข (๐ง = (๐ฆ mod ๐ค) โ ([๐ง / ๐]๐ โ [(๐ฆ mod ๐ค) / ๐]๐)) |
99 | 98 | anbi2d 464 |
. . . . . . . . . . . . . 14
โข (๐ง = (๐ฆ mod ๐ค) โ ((๐ โง [๐ง / ๐]๐) โ (๐ โง [(๐ฆ mod ๐ค) / ๐]๐))) |
100 | | sbsbc 2968 |
. . . . . . . . . . . . . . . . . . 19
โข ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โ [๐ง / ๐ฅ][๐ค / ๐ฆ]๐) |
101 | | sbsbc 2968 |
. . . . . . . . . . . . . . . . . . . 20
โข ([๐ค / ๐ฆ]๐ โ [๐ค / ๐ฆ]๐) |
102 | 101 | sbcbii 3024 |
. . . . . . . . . . . . . . . . . . 19
โข
([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โ [๐ง / ๐ฅ][๐ค / ๐ฆ]๐) |
103 | 100, 102 | bitri 184 |
. . . . . . . . . . . . . . . . . 18
โข ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โ [๐ง / ๐ฅ][๐ค / ๐ฆ]๐) |
104 | 103 | anbi1i 458 |
. . . . . . . . . . . . . . . . 17
โข (([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐) โ ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)) |
105 | | dfsbcq 2966 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = (๐ฆ mod ๐ค) โ ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โ [(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐)) |
106 | 105 | anbi1d 465 |
. . . . . . . . . . . . . . . . 17
โข (๐ง = (๐ฆ mod ๐ค) โ (([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐) โ ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))) |
107 | 104, 106 | bitrid 192 |
. . . . . . . . . . . . . . . 16
โข (๐ง = (๐ฆ mod ๐ค) โ (([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐) โ ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))) |
108 | 107 | rexbidv 2478 |
. . . . . . . . . . . . . . 15
โข (๐ง = (๐ฆ mod ๐ค) โ (โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐) โ โ๐ โ โ0 ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))) |
109 | 108 | imbi2d 230 |
. . . . . . . . . . . . . 14
โข (๐ง = (๐ฆ mod ๐ค) โ (([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)))) |
110 | 99, 109 | imbi12d 234 |
. . . . . . . . . . . . 13
โข (๐ง = (๐ฆ mod ๐ค) โ (((๐ โง [๐ง / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))) โ ((๐ โง [(๐ฆ mod ๐ค) / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))))) |
111 | | simpll 527 |
. . . . . . . . . . . . . 14
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ (((๐ค โ โ0 โง
โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค)) |
112 | | simpr 110 |
. . . . . . . . . . . . . . . 16
โข ((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โ โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
113 | 112 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
(((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง [(๐ฆ mod ๐ค) / ๐]๐) โ โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
114 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . 20
โข
โฒ๐ฆ[๐ค / ๐]๐ |
115 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . . . . 21
โข
โฒ๐ฆโ0 |
116 | | nfs1v 1939 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
โฒ๐ฆ[๐ค / ๐ฆ]๐ |
117 | 116 | nfsbxy 1942 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
โฒ๐ฆ[๐ง / ๐ฅ][๐ค / ๐ฆ]๐ |
118 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
โฒ๐ฆ๐ |
119 | 117, 118 | nfan 1565 |
. . . . . . . . . . . . . . . . . . . . 21
โข
โฒ๐ฆ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐) |
120 | 115, 119 | nfrexxy 2516 |
. . . . . . . . . . . . . . . . . . . 20
โข
โฒ๐ฆโ๐ โ โ0
([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐) |
121 | 114, 120 | nfim 1572 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐ฆ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)) |
122 | | sbequ 1840 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = ๐ค โ ([๐ฆ / ๐]๐ โ [๐ค / ๐]๐)) |
123 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
โฒ๐ฅ ๐ฆ = ๐ค |
124 | | sbequ12 1771 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ = ๐ค โ (๐ โ [๐ค / ๐ฆ]๐)) |
125 | 123, 124 | sbbid 1846 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ = ๐ค โ ([๐ง / ๐ฅ]๐ โ [๐ง / ๐ฅ][๐ค / ๐ฆ]๐)) |
126 | 125 | anbi1d 465 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = ๐ค โ (([๐ง / ๐ฅ]๐ โง ๐) โ ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))) |
127 | 126 | rexbidv 2478 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = ๐ค โ (โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐) โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))) |
128 | 122, 127 | imbi12d 234 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = ๐ค โ (([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)))) |
129 | 121, 128 | rspc 2837 |
. . . . . . . . . . . . . . . . . 18
โข (๐ค โ โ0
โ (โ๐ฆ โ
โ0 ([๐ฆ /
๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)))) |
130 | 129 | imim2d 54 |
. . . . . . . . . . . . . . . . 17
โข (๐ค โ โ0
โ (((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) โ ((๐ โง [๐ง / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))))) |
131 | 130 | ralimdv 2545 |
. . . . . . . . . . . . . . . 16
โข (๐ค โ โ0
โ (โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) โ โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))))) |
132 | 131 | ad4antr 494 |
. . . . . . . . . . . . . . 15
โข
(((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง [(๐ฆ mod ๐ค) / ๐]๐) โ (โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) โ โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐))))) |
133 | 113, 132 | mpd 13 |
. . . . . . . . . . . . . 14
โข
(((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง [(๐ฆ mod ๐ค) / ๐]๐) โ โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)))) |
134 | 111, 133 | sylan 283 |
. . . . . . . . . . . . 13
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)))) |
135 | | simpllr 534 |
. . . . . . . . . . . . . . 15
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ ๐ฆ โ โ0) |
136 | 135 | nn0zd 9375 |
. . . . . . . . . . . . . 14
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ ๐ฆ โ โค) |
137 | 79 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ ๐ค โ โ) |
138 | | zmodfz 10348 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โค โง ๐ค โ โ) โ (๐ฆ mod ๐ค) โ (0...(๐ค โ 1))) |
139 | 136, 137,
138 | syl2anc 411 |
. . . . . . . . . . . . 13
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ (๐ฆ mod ๐ค) โ (0...(๐ค โ 1))) |
140 | 110, 134,
139 | rspcdva 2848 |
. . . . . . . . . . . 12
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ ((๐ โง [(๐ฆ mod ๐ค) / ๐]๐) โ ([๐ค / ๐]๐ โ โ๐ โ โ0 ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)))) |
141 | 96, 97, 140 | mp2d 47 |
. . . . . . . . . . 11
โข
(((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โง [(๐ฆ mod ๐ค) / ๐]๐) โ โ๐ โ โ0 ([(๐ฆ mod ๐ค) / ๐ฅ][๐ค / ๐ฆ]๐ โง ๐)) |
142 | | nfv 1528 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐ฅ ๐ค โ
โ0 |
143 | | nfcv 2319 |
. . . . . . . . . . . . . . . . 17
โข
โฒ๐ฅ(0...(๐ค โ 1)) |
144 | | nfv 1528 |
. . . . . . . . . . . . . . . . . 18
โข
โฒ๐ฅ(๐ โง [๐ง / ๐]๐) |
145 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐ฅโ0 |
146 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . . . 21
โข
โฒ๐ฅ๐ |
147 | 146 | nfsbxy 1942 |
. . . . . . . . . . . . . . . . . . . 20
โข
โฒ๐ฅ[๐ฆ / ๐]๐ |
148 | | nfs1v 1939 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
โฒ๐ฅ[๐ง / ๐ฅ]๐ |
149 | 148, 146 | nfan 1565 |
. . . . . . . . . . . . . . . . . . . . 21
โข
โฒ๐ฅ([๐ง / ๐ฅ]๐ โง ๐) |
150 | 145, 149 | nfrexxy 2516 |
. . . . . . . . . . . . . . . . . . . 20
โข
โฒ๐ฅโ๐ โ โ0
([๐ง / ๐ฅ]๐ โง ๐) |
151 | 147, 150 | nfim 1572 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐ฅ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) |
152 | 145, 151 | nfralxy 2515 |
. . . . . . . . . . . . . . . . . 18
โข
โฒ๐ฅโ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) |
153 | 144, 152 | nfim 1572 |
. . . . . . . . . . . . . . . . 17
โข
โฒ๐ฅ((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
154 | 143, 153 | nfralxy 2515 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐ฅโ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
155 | 142, 154 | nfan 1565 |
. . . . . . . . . . . . . . 15
โข
โฒ๐ฅ(๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
156 | | nfv 1528 |
. . . . . . . . . . . . . . 15
โข
โฒ๐ฅ(๐ โง [๐ค / ๐]๐) |
157 | 155, 156 | nfan 1565 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) |
158 | | nfv 1528 |
. . . . . . . . . . . . . 14
โข
โฒ๐ฅ0 < ๐ค |
159 | 157, 158 | nfan 1565 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ(((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) |
160 | | nfv 1528 |
. . . . . . . . . . . . 13
โข
โฒ๐ฅ ๐ฆ โ
โ0 |
161 | 159, 160 | nfan 1565 |
. . . . . . . . . . . 12
โข
โฒ๐ฅ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) |
162 | 161, 147 | nfan 1565 |
. . . . . . . . . . 11
โข
โฒ๐ฅ(((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) |
163 | | nfv 1528 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐ ๐ค โ
โ0 |
164 | | nfcv 2319 |
. . . . . . . . . . . . . . . . 17
โข
โฒ๐(0...(๐ค โ 1)) |
165 | | nfv 1528 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐๐ |
166 | | nfs1v 1939 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐[๐ง / ๐]๐ |
167 | 165, 166 | nfan 1565 |
. . . . . . . . . . . . . . . . . 18
โข
โฒ๐(๐ โง [๐ง / ๐]๐) |
168 | | nfcv 2319 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐โ0 |
169 | | nfre1 2520 |
. . . . . . . . . . . . . . . . . . . 20
โข
โฒ๐โ๐ โ โ0
([๐ง / ๐ฅ]๐ โง ๐) |
170 | 57, 169 | nfim 1572 |
. . . . . . . . . . . . . . . . . . 19
โข
โฒ๐([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) |
171 | 168, 170 | nfralxy 2515 |
. . . . . . . . . . . . . . . . . 18
โข
โฒ๐โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)) |
172 | 167, 171 | nfim 1572 |
. . . . . . . . . . . . . . . . 17
โข
โฒ๐((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
173 | 164, 172 | nfralxy 2515 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) |
174 | 163, 173 | nfan 1565 |
. . . . . . . . . . . . . . 15
โข
โฒ๐(๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) |
175 | | nfs1v 1939 |
. . . . . . . . . . . . . . . 16
โข
โฒ๐[๐ค / ๐]๐ |
176 | 165, 175 | nfan 1565 |
. . . . . . . . . . . . . . 15
โข
โฒ๐(๐ โง [๐ค / ๐]๐) |
177 | 174, 176 | nfan 1565 |
. . . . . . . . . . . . . 14
โข
โฒ๐((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) |
178 | | nfv 1528 |
. . . . . . . . . . . . . 14
โข
โฒ๐0 < ๐ค |
179 | 177, 178 | nfan 1565 |
. . . . . . . . . . . . 13
โข
โฒ๐(((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) |
180 | | nfv 1528 |
. . . . . . . . . . . . 13
โข
โฒ๐ ๐ฆ โ
โ0 |
181 | 179, 180 | nfan 1565 |
. . . . . . . . . . . 12
โข
โฒ๐((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) |
182 | 181, 57 | nfan 1565 |
. . . . . . . . . . 11
โข
โฒ๐(((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) |
183 | 68, 72, 75, 80, 81, 82, 86, 93, 141, 162, 182 | bezoutlemstep 12000 |
. . . . . . . . . 10
โข
((((((๐ค โ
โ0 โง โ๐ง โ (0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โง ๐ฆ โ โ0) โง [๐ฆ / ๐]๐) โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) |
184 | 183 | exp31 364 |
. . . . . . . . 9
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ (๐ฆ โ โ0 โ ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)))) |
185 | 67, 184 | ralrimi 2548 |
. . . . . . . 8
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) |
186 | | sbsbc 2968 |
. . . . . . . . . . . 12
โข ([๐ค / ๐ฅ]๐ โ [๐ค / ๐ฅ]๐) |
187 | 186 | anbi1i 458 |
. . . . . . . . . . 11
โข (([๐ค / ๐ฅ]๐ โง ๐) โ ([๐ค / ๐ฅ]๐ โง ๐)) |
188 | 187 | rexbii 2484 |
. . . . . . . . . 10
โข
(โ๐ โ
โ0 ([๐ค /
๐ฅ]๐ โง ๐) โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) |
189 | 188 | imbi2i 226 |
. . . . . . . . 9
โข (([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) โ ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) |
190 | 189 | ralbii 2483 |
. . . . . . . 8
โข
(โ๐ฆ โ
โ0 ([๐ฆ /
๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐)) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) |
191 | 185, 190 | sylibr 134 |
. . . . . . 7
โข ((((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โง 0 < ๐ค) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) |
192 | | nn0nlt0 9204 |
. . . . . . . . 9
โข (๐ค โ โ0
โ ยฌ ๐ค <
0) |
193 | | nn0z 9275 |
. . . . . . . . . . . 12
โข (๐ค โ โ0
โ ๐ค โ
โค) |
194 | | ztri3or0 9297 |
. . . . . . . . . . . 12
โข (๐ค โ โค โ (๐ค < 0 โจ ๐ค = 0 โจ 0 < ๐ค)) |
195 | 193, 194 | syl 14 |
. . . . . . . . . . 11
โข (๐ค โ โ0
โ (๐ค < 0 โจ ๐ค = 0 โจ 0 < ๐ค)) |
196 | | 3orass 981 |
. . . . . . . . . . 11
โข ((๐ค < 0 โจ ๐ค = 0 โจ 0 < ๐ค) โ (๐ค < 0 โจ (๐ค = 0 โจ 0 < ๐ค))) |
197 | 195, 196 | sylib 122 |
. . . . . . . . . 10
โข (๐ค โ โ0
โ (๐ค < 0 โจ
(๐ค = 0 โจ 0 < ๐ค))) |
198 | 197 | orcomd 729 |
. . . . . . . . 9
โข (๐ค โ โ0
โ ((๐ค = 0 โจ 0 <
๐ค) โจ ๐ค < 0)) |
199 | 192, 198 | ecased 1349 |
. . . . . . . 8
โข (๐ค โ โ0
โ (๐ค = 0 โจ 0 <
๐ค)) |
200 | 199 | ad2antrr 488 |
. . . . . . 7
โข (((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โ (๐ค = 0 โจ 0 < ๐ค)) |
201 | 65, 191, 200 | mpjaodan 798 |
. . . . . 6
โข (((๐ค โ โ0
โง โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐)))) โง (๐ โง [๐ค / ๐]๐)) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))) |
202 | 201 | exp31 364 |
. . . . 5
โข (๐ค โ โ0
โ (โ๐ง โ
(0...(๐ค โ 1))((๐ โง [๐ง / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ง / ๐ฅ]๐ โง ๐))) โ ((๐ โง [๐ค / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 ([๐ค / ๐ฅ]๐ โง ๐))))) |
203 | 8, 16, 202 | nn0sinds 10446 |
. . . 4
โข (๐ฅ โ โ0
โ ((๐ โง [๐ฅ / ๐]๐) โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐)))) |
204 | 203 | expd 258 |
. . 3
โข (๐ฅ โ โ0
โ (๐ โ ([๐ฅ / ๐]๐ โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐))))) |
205 | 204 | impcom 125 |
. 2
โข ((๐ โง ๐ฅ โ โ0) โ ([๐ฅ / ๐]๐ โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐)))) |
206 | 205 | ralrimiva 2550 |
1
โข (๐ โ โ๐ฅ โ โ0 ([๐ฅ / ๐]๐ โ โ๐ฆ โ โ0 ([๐ฆ / ๐]๐ โ โ๐ โ โ0 (๐ โง ๐)))) |