Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
2 | 1 | oveq1d 7376 |
. . . . . . . 8
β’ (π₯ = 0 β ((πβπ₯) β 1) = ((πβ0) β 1)) |
3 | 2 | oveq2d 7377 |
. . . . . . 7
β’ (π₯ = 0 β (0...((πβπ₯) β 1)) = (0...((πβ0) β 1))) |
4 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = 0 β (π Β· π₯) = (π Β· 0)) |
5 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
6 | 4, 5 | oveq12d 7379 |
. . . . . . . 8
β’ (π₯ = 0 β ((π Β· π₯) Β· (πβπ₯)) = ((π Β· 0) Β· (πβ0))) |
7 | 6 | breq2d 5121 |
. . . . . . 7
β’ (π₯ = 0 β ((πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β (πΉβπ) β€ ((π Β· 0) Β· (πβ0)))) |
8 | 3, 7 | raleqbidv 3318 |
. . . . . 6
β’ (π₯ = 0 β (βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β βπ β (0...((πβ0) β 1))(πΉβπ) β€ ((π Β· 0) Β· (πβ0)))) |
9 | 8 | imbi2d 341 |
. . . . 5
β’ (π₯ = 0 β ((π β βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯))) β (π β βπ β (0...((πβ0) β 1))(πΉβπ) β€ ((π Β· 0) Β· (πβ0))))) |
10 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
11 | 10 | oveq1d 7376 |
. . . . . . . 8
β’ (π₯ = π β ((πβπ₯) β 1) = ((πβπ) β 1)) |
12 | 11 | oveq2d 7377 |
. . . . . . 7
β’ (π₯ = π β (0...((πβπ₯) β 1)) = (0...((πβπ) β 1))) |
13 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π β (π Β· π₯) = (π Β· π)) |
14 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
15 | 13, 14 | oveq12d 7379 |
. . . . . . . 8
β’ (π₯ = π β ((π Β· π₯) Β· (πβπ₯)) = ((π Β· π) Β· (πβπ))) |
16 | 15 | breq2d 5121 |
. . . . . . 7
β’ (π₯ = π β ((πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β (πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
17 | 12, 16 | raleqbidv 3318 |
. . . . . 6
β’ (π₯ = π β (βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
18 | 17 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β ((π β βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯))) β (π β βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ))))) |
19 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (πβπ₯) = (πβ(π + 1))) |
20 | 19 | oveq1d 7376 |
. . . . . . . 8
β’ (π₯ = (π + 1) β ((πβπ₯) β 1) = ((πβ(π + 1)) β 1)) |
21 | 20 | oveq2d 7377 |
. . . . . . 7
β’ (π₯ = (π + 1) β (0...((πβπ₯) β 1)) = (0...((πβ(π + 1)) β 1))) |
22 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (π Β· π₯) = (π Β· (π + 1))) |
23 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β (πβπ₯) = (πβ(π + 1))) |
24 | 22, 23 | oveq12d 7379 |
. . . . . . . 8
β’ (π₯ = (π + 1) β ((π Β· π₯) Β· (πβπ₯)) = ((π Β· (π + 1)) Β· (πβ(π + 1)))) |
25 | 24 | breq2d 5121 |
. . . . . . 7
β’ (π₯ = (π + 1) β ((πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β (πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
26 | 21, 25 | raleqbidv 3318 |
. . . . . 6
β’ (π₯ = (π + 1) β (βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β βπ β (0...((πβ(π + 1)) β 1))(πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
27 | 26 | imbi2d 341 |
. . . . 5
β’ (π₯ = (π + 1) β ((π β βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯))) β (π β βπ β (0...((πβ(π + 1)) β 1))(πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1)))))) |
28 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
29 | 28 | oveq1d 7376 |
. . . . . . . 8
β’ (π₯ = π β ((πβπ₯) β 1) = ((πβπ) β 1)) |
30 | 29 | oveq2d 7377 |
. . . . . . 7
β’ (π₯ = π β (0...((πβπ₯) β 1)) = (0...((πβπ) β 1))) |
31 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π β (π Β· π₯) = (π Β· π)) |
32 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
33 | 31, 32 | oveq12d 7379 |
. . . . . . . 8
β’ (π₯ = π β ((π Β· π₯) Β· (πβπ₯)) = ((π Β· π) Β· (πβπ))) |
34 | 33 | breq2d 5121 |
. . . . . . 7
β’ (π₯ = π β ((πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β (πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
35 | 30, 34 | raleqbidv 3318 |
. . . . . 6
β’ (π₯ = π β (βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯)) β βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
36 | 35 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β ((π β βπ β (0...((πβπ₯) β 1))(πΉβπ) β€ ((π Β· π₯) Β· (πβπ₯))) β (π β βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ))))) |
37 | | ostth2.5 |
. . . . . . . . . . . . . 14
β’ (π β π β
(β€β₯β2)) |
38 | | eluz2nn 12817 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β2) β π β β) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
40 | 39 | nncnd 12177 |
. . . . . . . . . . . 12
β’ (π β π β β) |
41 | 40 | exp0d 14054 |
. . . . . . . . . . 11
β’ (π β (πβ0) = 1) |
42 | 41 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π β ((πβ0) β 1) = (1 β
1)) |
43 | | 1m1e0 12233 |
. . . . . . . . . 10
β’ (1
β 1) = 0 |
44 | 42, 43 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π β ((πβ0) β 1) = 0) |
45 | 44 | oveq2d 7377 |
. . . . . . . 8
β’ (π β (0...((πβ0) β 1)) =
(0...0)) |
46 | 45 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π β (0...((πβ0) β 1)) β π β
(0...0))) |
47 | | 0le0 12262 |
. . . . . . . . . 10
β’ 0 β€
0 |
48 | 47 | a1i 11 |
. . . . . . . . 9
β’ (π β 0 β€ 0) |
49 | | ostth.1 |
. . . . . . . . . 10
β’ (π β πΉ β π΄) |
50 | | qabsabv.a |
. . . . . . . . . . 11
β’ π΄ = (AbsValβπ) |
51 | | qrng.q |
. . . . . . . . . . . 12
β’ π = (βfld
βΎs β) |
52 | 51 | qrng0 26992 |
. . . . . . . . . . 11
β’ 0 =
(0gβπ) |
53 | 50, 52 | abv0 20333 |
. . . . . . . . . 10
β’ (πΉ β π΄ β (πΉβ0) = 0) |
54 | 49, 53 | syl 17 |
. . . . . . . . 9
β’ (π β (πΉβ0) = 0) |
55 | 40 | mul01d 11362 |
. . . . . . . . . . 11
β’ (π β (π Β· 0) = 0) |
56 | 55 | oveq1d 7376 |
. . . . . . . . . 10
β’ (π β ((π Β· 0) Β· (πβ0)) = (0 Β· (πβ0))) |
57 | | ostth2.7 |
. . . . . . . . . . . . . 14
β’ π = if((πΉβπ) β€ 1, 1, (πΉβπ)) |
58 | | 1re 11163 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
59 | | nnq 12895 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
60 | 39, 59 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
61 | 51 | qrngbas 26990 |
. . . . . . . . . . . . . . . . 17
β’ β =
(Baseβπ) |
62 | 50, 61 | abvcl 20326 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
63 | 49, 60, 62 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉβπ) β β) |
64 | | ifcl 4535 |
. . . . . . . . . . . . . . 15
β’ ((1
β β β§ (πΉβπ) β β) β if((πΉβπ) β€ 1, 1, (πΉβπ)) β β) |
65 | 58, 63, 64 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β if((πΉβπ) β€ 1, 1, (πΉβπ)) β β) |
66 | 57, 65 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
67 | 66 | recnd 11191 |
. . . . . . . . . . . 12
β’ (π β π β β) |
68 | | 0nn0 12436 |
. . . . . . . . . . . 12
β’ 0 β
β0 |
69 | | expcl 13994 |
. . . . . . . . . . . 12
β’ ((π β β β§ 0 β
β0) β (πβ0) β β) |
70 | 67, 68, 69 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (πβ0) β β) |
71 | 70 | mul02d 11361 |
. . . . . . . . . 10
β’ (π β (0 Β· (πβ0)) = 0) |
72 | 56, 71 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ((π Β· 0) Β· (πβ0)) = 0) |
73 | 48, 54, 72 | 3brtr4d 5141 |
. . . . . . . 8
β’ (π β (πΉβ0) β€ ((π Β· 0) Β· (πβ0))) |
74 | | elfz1eq 13461 |
. . . . . . . . . 10
β’ (π β (0...0) β π = 0) |
75 | 74 | fveq2d 6850 |
. . . . . . . . 9
β’ (π β (0...0) β (πΉβπ) = (πΉβ0)) |
76 | 75 | breq1d 5119 |
. . . . . . . 8
β’ (π β (0...0) β ((πΉβπ) β€ ((π Β· 0) Β· (πβ0)) β (πΉβ0) β€ ((π Β· 0) Β· (πβ0)))) |
77 | 73, 76 | syl5ibrcom 247 |
. . . . . . 7
β’ (π β (π β (0...0) β (πΉβπ) β€ ((π Β· 0) Β· (πβ0)))) |
78 | 46, 77 | sylbid 239 |
. . . . . 6
β’ (π β (π β (0...((πβ0) β 1)) β (πΉβπ) β€ ((π Β· 0) Β· (πβ0)))) |
79 | 78 | ralrimiv 3139 |
. . . . 5
β’ (π β βπ β (0...((πβ0) β 1))(πΉβπ) β€ ((π Β· 0) Β· (πβ0))) |
80 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
81 | 80 | breq1d 5119 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) β€ ((π Β· π) Β· (πβπ)) β (πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
82 | 81 | cbvralvw 3224 |
. . . . . . . 8
β’
(βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)) β βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ))) |
83 | 49 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β πΉ β π΄) |
84 | | elfzelz 13450 |
. . . . . . . . . . . . . 14
β’ (π β (0...((πβ(π + 1)) β 1)) β π β β€) |
85 | 84 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β€) |
86 | | zq 12887 |
. . . . . . . . . . . . 13
β’ (π β β€ β π β
β) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
88 | 50, 61 | abvcl 20326 |
. . . . . . . . . . . 12
β’ ((πΉ β π΄ β§ π β β) β (πΉβπ) β β) |
89 | 83, 87, 88 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβπ) β β) |
90 | 39 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
91 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β0) |
92 | 90, 91 | nnexpcld 14157 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β β) |
93 | 85, 92 | zmodcld 13806 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π mod (πβπ)) β
β0) |
94 | 93 | nn0zd 12533 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π mod (πβπ)) β β€) |
95 | | zq 12887 |
. . . . . . . . . . . . . 14
β’ ((π mod (πβπ)) β β€ β (π mod (πβπ)) β β) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π mod (πβπ)) β β) |
97 | 50, 61 | abvcl 20326 |
. . . . . . . . . . . . 13
β’ ((πΉ β π΄ β§ (π mod (πβπ)) β β) β (πΉβ(π mod (πβπ))) β β) |
98 | 83, 96, 97 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(π mod (πβπ))) β β) |
99 | 90, 59 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
100 | 83, 99, 62 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβπ) β β) |
101 | 100, 91 | reexpcld 14077 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβπ)βπ) β β) |
102 | 85 | zred 12615 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
103 | 102, 92 | nndivred 12215 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π / (πβπ)) β β) |
104 | 103 | flcld 13712 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (ββ(π / (πβπ))) β β€) |
105 | | zq 12887 |
. . . . . . . . . . . . . . 15
β’
((ββ(π /
(πβπ))) β β€ β
(ββ(π / (πβπ))) β β) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (ββ(π / (πβπ))) β β) |
107 | 50, 61 | abvcl 20326 |
. . . . . . . . . . . . . 14
β’ ((πΉ β π΄ β§ (ββ(π / (πβπ))) β β) β (πΉβ(ββ(π / (πβπ)))) β β) |
108 | 83, 106, 107 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(ββ(π / (πβπ)))) β β) |
109 | 101, 108 | remulcld 11193 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ))))) β β) |
110 | 98, 109 | readdcld 11192 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(π mod (πβπ))) + (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ)))))) β β) |
111 | 90 | nnred 12176 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
112 | | nn0p1nn 12460 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β (π + 1) β
β) |
113 | 112 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π + 1) β β) |
114 | 113 | nnred 12176 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π + 1) β β) |
115 | 111, 114 | remulcld 11193 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· (π + 1)) β β) |
116 | 66 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
117 | | peano2nn0 12461 |
. . . . . . . . . . . . . 14
β’ (π β β0
β (π + 1) β
β0) |
118 | 117 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π + 1) β
β0) |
119 | 116, 118 | reexpcld 14077 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβ(π + 1)) β β) |
120 | 115, 119 | remulcld 11193 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· (π + 1)) Β· (πβ(π + 1))) β β) |
121 | | nnq 12895 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β β β (πβπ) β β) |
122 | 92, 121 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β β) |
123 | | qmulcl 12900 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β β β§ (ββ(π / (πβπ))) β β) β ((πβπ) Β· (ββ(π / (πβπ)))) β β) |
124 | 122, 106,
123 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πβπ) Β· (ββ(π / (πβπ)))) β β) |
125 | | qex 12894 |
. . . . . . . . . . . . . . 15
β’ β
β V |
126 | | cnfldadd 20824 |
. . . . . . . . . . . . . . . 16
β’ + =
(+gββfld) |
127 | 51, 126 | ressplusg 17179 |
. . . . . . . . . . . . . . 15
β’ (β
β V β + = (+gβπ)) |
128 | 125, 127 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ + =
(+gβπ) |
129 | 50, 61, 128 | abvtri 20332 |
. . . . . . . . . . . . 13
β’ ((πΉ β π΄ β§ (π mod (πβπ)) β β β§ ((πβπ) Β· (ββ(π / (πβπ)))) β β) β (πΉβ((π mod (πβπ)) + ((πβπ) Β· (ββ(π / (πβπ)))))) β€ ((πΉβ(π mod (πβπ))) + (πΉβ((πβπ) Β· (ββ(π / (πβπ))))))) |
130 | 83, 96, 124, 129 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ((π mod (πβπ)) + ((πβπ) Β· (ββ(π / (πβπ)))))) β€ ((πΉβ(π mod (πβπ))) + (πΉβ((πβπ) Β· (ββ(π / (πβπ))))))) |
131 | 92 | nnrpd 12963 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β
β+) |
132 | | modval 13785 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (πβπ) β β+) β (π mod (πβπ)) = (π β ((πβπ) Β· (ββ(π / (πβπ)))))) |
133 | 102, 131,
132 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π mod (πβπ)) = (π β ((πβπ) Β· (ββ(π / (πβπ)))))) |
134 | 133 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π mod (πβπ)) + ((πβπ) Β· (ββ(π / (πβπ))))) = ((π β ((πβπ) Β· (ββ(π / (πβπ))))) + ((πβπ) Β· (ββ(π / (πβπ)))))) |
135 | 102 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
136 | | qcn 12896 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ) Β· (ββ(π / (πβπ)))) β β β ((πβπ) Β· (ββ(π / (πβπ)))) β β) |
137 | 124, 136 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πβπ) Β· (ββ(π / (πβπ)))) β β) |
138 | 135, 137 | npcand 11524 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π β ((πβπ) Β· (ββ(π / (πβπ))))) + ((πβπ) Β· (ββ(π / (πβπ))))) = π) |
139 | 134, 138 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π mod (πβπ)) + ((πβπ) Β· (ββ(π / (πβπ))))) = π) |
140 | 139 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ((π mod (πβπ)) + ((πβπ) Β· (ββ(π / (πβπ)))))) = (πΉβπ)) |
141 | | cnfldmul 20825 |
. . . . . . . . . . . . . . . . . 18
β’ Β·
= (.rββfld) |
142 | 51, 141 | ressmulr 17196 |
. . . . . . . . . . . . . . . . 17
β’ (β
β V β Β· = (.rβπ)) |
143 | 125, 142 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ Β·
= (.rβπ) |
144 | 50, 61, 143 | abvmul 20331 |
. . . . . . . . . . . . . . 15
β’ ((πΉ β π΄ β§ (πβπ) β β β§ (ββ(π / (πβπ))) β β) β (πΉβ((πβπ) Β· (ββ(π / (πβπ))))) = ((πΉβ(πβπ)) Β· (πΉβ(ββ(π / (πβπ)))))) |
145 | 83, 122, 106, 144 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ((πβπ) Β· (ββ(π / (πβπ))))) = ((πΉβ(πβπ)) Β· (πΉβ(ββ(π / (πβπ)))))) |
146 | 51, 50 | qabvexp 26997 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β π΄ β§ π β β β§ π β β0) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
147 | 83, 99, 91, 146 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(πβπ)) = ((πΉβπ)βπ)) |
148 | 147 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(πβπ)) Β· (πΉβ(ββ(π / (πβπ))))) = (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ)))))) |
149 | 145, 148 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ((πβπ) Β· (ββ(π / (πβπ))))) = (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ)))))) |
150 | 149 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(π mod (πβπ))) + (πΉβ((πβπ) Β· (ββ(π / (πβπ)))))) = ((πΉβ(π mod (πβπ))) + (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ))))))) |
151 | 130, 140,
150 | 3brtr3d 5140 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβπ) β€ ((πΉβ(π mod (πβπ))) + (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ))))))) |
152 | 116, 91 | reexpcld 14077 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β β) |
153 | 115, 152 | remulcld 11193 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· (π + 1)) Β· (πβπ)) β β) |
154 | | nn0re 12430 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β) |
155 | 154 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
156 | 111, 155 | remulcld 11193 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· π) β β) |
157 | 156, 152 | remulcld 11193 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· π) Β· (πβπ)) β β) |
158 | 111, 152 | remulcld 11193 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· (πβπ)) β β) |
159 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = (π mod (πβπ)) β (πΉβπ) = (πΉβ(π mod (πβπ)))) |
160 | 159 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ (π = (π mod (πβπ)) β ((πΉβπ) β€ ((π Β· π) Β· (πβπ)) β (πΉβ(π mod (πβπ))) β€ ((π Β· π) Β· (πβπ)))) |
161 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ))) |
162 | | zmodfz 13807 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ (πβπ) β β) β (π mod (πβπ)) β (0...((πβπ) β 1))) |
163 | 85, 92, 162 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π mod (πβπ)) β (0...((πβπ) β 1))) |
164 | 160, 161,
163 | rspcdva 3584 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(π mod (πβπ))) β€ ((π Β· π) Β· (πβπ))) |
165 | 111, 101 | remulcld 11193 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· ((πΉβπ)βπ)) β β) |
166 | 101 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβπ)βπ) β β) |
167 | 108 | recnd 11191 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(ββ(π / (πβπ)))) β β) |
168 | 166, 167 | mulcomd 11184 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ))))) = ((πΉβ(ββ(π / (πβπ)))) Β· ((πΉβπ)βπ))) |
169 | 50, 61 | abvge0 20327 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ β π΄ β§ π β β) β 0 β€ (πΉβπ)) |
170 | 83, 99, 169 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 β€ (πΉβπ)) |
171 | 100, 91, 170 | expge0d 14078 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 β€ ((πΉβπ)βπ)) |
172 | 104 | zred 12615 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (ββ(π / (πβπ))) β β) |
173 | | elfzle1 13453 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (0...((πβ(π + 1)) β 1)) β 0 β€ π) |
174 | 173 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 β€ π) |
175 | 92 | nnred 12176 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β β) |
176 | 92 | nngt0d 12210 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 < (πβπ)) |
177 | | divge0 12032 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β β β§ 0 β€
π) β§ ((πβπ) β β β§ 0 < (πβπ))) β 0 β€ (π / (πβπ))) |
178 | 102, 174,
175, 176, 177 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 β€ (π / (πβπ))) |
179 | | flge0nn0 13734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π / (πβπ)) β β β§ 0 β€ (π / (πβπ))) β (ββ(π / (πβπ))) β
β0) |
180 | 103, 178,
179 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (ββ(π / (πβπ))) β
β0) |
181 | 51, 50 | qabvle 26996 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ β π΄ β§ (ββ(π / (πβπ))) β β0) β (πΉβ(ββ(π / (πβπ)))) β€ (ββ(π / (πβπ)))) |
182 | 83, 180, 181 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(ββ(π / (πβπ)))) β€ (ββ(π / (πβπ)))) |
183 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β (0...((πβ(π + 1)) β 1))) |
184 | | 0z 12518 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
β€ |
185 | 90, 118 | nnexpcld 14157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβ(π + 1)) β β) |
186 | 185 | nnzd 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβ(π + 1)) β β€) |
187 | | elfzm11 13521 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((0
β β€ β§ (πβ(π + 1)) β β€) β (π β (0...((πβ(π + 1)) β 1)) β (π β β€ β§ 0 β€ π β§ π < (πβ(π + 1))))) |
188 | 184, 186,
187 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π β (0...((πβ(π + 1)) β 1)) β (π β β€ β§ 0 β€ π β§ π < (πβ(π + 1))))) |
189 | 183, 188 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π β β€ β§ 0 β€ π β§ π < (πβ(π + 1)))) |
190 | 189 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π < (πβ(π + 1))) |
191 | 90 | nncnd 12177 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
192 | 191, 91 | expp1d 14061 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβ(π + 1)) = ((πβπ) Β· π)) |
193 | 190, 192 | breqtrd 5135 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π < ((πβπ) Β· π)) |
194 | | ltdivmul 12038 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π β β β§ ((πβπ) β β β§ 0 < (πβπ))) β ((π / (πβπ)) < π β π < ((πβπ) Β· π))) |
195 | 102, 111,
175, 176, 194 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π / (πβπ)) < π β π < ((πβπ) Β· π))) |
196 | 193, 195 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π / (πβπ)) < π) |
197 | 90 | nnzd 12534 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β€) |
198 | | fllt 13720 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π / (πβπ)) β β β§ π β β€) β ((π / (πβπ)) < π β (ββ(π / (πβπ))) < π)) |
199 | 103, 197,
198 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π / (πβπ)) < π β (ββ(π / (πβπ))) < π)) |
200 | 196, 199 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (ββ(π / (πβπ))) < π) |
201 | 172, 111,
200 | ltled 11311 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (ββ(π / (πβπ))) β€ π) |
202 | 108, 172,
111, 182, 201 | letrd 11320 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβ(ββ(π / (πβπ)))) β€ π) |
203 | 108, 111,
101, 171, 202 | lemul1ad 12102 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(ββ(π / (πβπ)))) Β· ((πΉβπ)βπ)) β€ (π Β· ((πΉβπ)βπ))) |
204 | 168, 203 | eqbrtrd 5131 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ))))) β€ (π Β· ((πΉβπ)βπ))) |
205 | 90 | nnnn0d 12481 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β
β0) |
206 | 205 | nn0ge0d 12484 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 β€ π) |
207 | | max1 13113 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉβπ) β β β§ 1 β β)
β (πΉβπ) β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
208 | 100, 58, 207 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβπ) β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
209 | 208, 57 | breqtrrdi 5151 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβπ) β€ π) |
210 | | leexp1a 14089 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉβπ) β β β§ π β β β§ π β β0) β§ (0 β€
(πΉβπ) β§ (πΉβπ) β€ π)) β ((πΉβπ)βπ) β€ (πβπ)) |
211 | 100, 116,
91, 170, 209, 210 | syl32anc 1379 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβπ)βπ) β€ (πβπ)) |
212 | 101, 152,
111, 206, 211 | lemul2ad 12103 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· ((πΉβπ)βπ)) β€ (π Β· (πβπ))) |
213 | 109, 165,
158, 204, 212 | letrd 11320 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ))))) β€ (π Β· (πβπ))) |
214 | 98, 109, 157, 158, 164, 213 | le2addd 11782 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(π mod (πβπ))) + (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ)))))) β€ (((π Β· π) Β· (πβπ)) + (π Β· (πβπ)))) |
215 | | nn0cn 12431 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β π β
β) |
216 | 215 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β) |
217 | | 1cnd 11158 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 1 β
β) |
218 | 191, 216,
217 | adddid 11187 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· (π + 1)) = ((π Β· π) + (π Β· 1))) |
219 | 191 | mulridd 11180 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· 1) = π) |
220 | 219 | oveq2d 7377 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· π) + (π Β· 1)) = ((π Β· π) + π)) |
221 | 218, 220 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· (π + 1)) = ((π Β· π) + π)) |
222 | 221 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· (π + 1)) Β· (πβπ)) = (((π Β· π) + π) Β· (πβπ))) |
223 | 191, 216 | mulcld 11183 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· π) β β) |
224 | 152 | recnd 11191 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β β) |
225 | 223, 191,
224 | adddird 11188 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (((π Β· π) + π) Β· (πβπ)) = (((π Β· π) Β· (πβπ)) + (π Β· (πβπ)))) |
226 | 222, 225 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· (π + 1)) Β· (πβπ)) = (((π Β· π) Β· (πβπ)) + (π Β· (πβπ)))) |
227 | 214, 226 | breqtrrd 5137 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(π mod (πβπ))) + (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ)))))) β€ ((π Β· (π + 1)) Β· (πβπ))) |
228 | | max2 13115 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β β β§ 1 β β)
β 1 β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
229 | 100, 58, 228 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 1 β€ if((πΉβπ) β€ 1, 1, (πΉβπ))) |
230 | 229, 57 | breqtrrdi 5151 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 1 β€ π) |
231 | | nn0z 12532 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β€) |
232 | 231 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β β€) |
233 | | uzid 12786 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β π β
(β€β₯βπ)) |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β π β (β€β₯βπ)) |
235 | | peano2uz 12834 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
236 | 234, 235 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π + 1) β
(β€β₯βπ)) |
237 | 116, 230,
236 | leexp2ad 14166 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πβπ) β€ (πβ(π + 1))) |
238 | 90, 113 | nnmulcld 12214 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (π Β· (π + 1)) β β) |
239 | 238 | nngt0d 12210 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β 0 < (π Β· (π + 1))) |
240 | | lemul2 12016 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β β β§ (πβ(π + 1)) β β β§ ((π Β· (π + 1)) β β β§ 0 < (π Β· (π + 1)))) β ((πβπ) β€ (πβ(π + 1)) β ((π Β· (π + 1)) Β· (πβπ)) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
241 | 152, 119,
115, 239, 240 | syl112anc 1375 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πβπ) β€ (πβ(π + 1)) β ((π Β· (π + 1)) Β· (πβπ)) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
242 | 237, 241 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((π Β· (π + 1)) Β· (πβπ)) β€ ((π Β· (π + 1)) Β· (πβ(π + 1)))) |
243 | 110, 153,
120, 227, 242 | letrd 11320 |
. . . . . . . . . . 11
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β ((πΉβ(π mod (πβπ))) + (((πΉβπ)βπ) Β· (πΉβ(ββ(π / (πβπ)))))) β€ ((π Β· (π + 1)) Β· (πβ(π + 1)))) |
244 | 89, 110, 120, 151, 243 | letrd 11320 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ (π β (0...((πβ(π + 1)) β 1)) β§ βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) β (πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1)))) |
245 | 244 | expr 458 |
. . . . . . . . 9
β’ (((π β§ π β β0) β§ π β (0...((πβ(π + 1)) β 1))) β (βπ β (0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)) β (πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
246 | 245 | ralrimdva 3148 |
. . . . . . . 8
β’ ((π β§ π β β0) β
(βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)) β βπ β (0...((πβ(π + 1)) β 1))(πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
247 | 82, 246 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π β β0) β
(βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)) β βπ β (0...((πβ(π + 1)) β 1))(πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1))))) |
248 | 247 | expcom 415 |
. . . . . 6
β’ (π β β0
β (π β
(βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)) β βπ β (0...((πβ(π + 1)) β 1))(πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1)))))) |
249 | 248 | a2d 29 |
. . . . 5
β’ (π β β0
β ((π β
βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ))) β (π β βπ β (0...((πβ(π + 1)) β 1))(πΉβπ) β€ ((π Β· (π + 1)) Β· (πβ(π + 1)))))) |
250 | 9, 18, 27, 36, 79, 249 | nn0ind 12606 |
. . . 4
β’ (π β β0
β (π β
βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
251 | 250 | impcom 409 |
. . 3
β’ ((π β§ π β β0) β
βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ))) |
252 | | fveq2 6846 |
. . . . 5
β’ (π = π β (πΉβπ) = (πΉβπ)) |
253 | 252 | breq1d 5119 |
. . . 4
β’ (π = π β ((πΉβπ) β€ ((π Β· π) Β· (πβπ)) β (πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
254 | 253 | rspccv 3580 |
. . 3
β’
(βπ β
(0...((πβπ) β 1))(πΉβπ) β€ ((π Β· π) Β· (πβπ)) β (π β (0...((πβπ) β 1)) β (πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
255 | 251, 254 | syl 17 |
. 2
β’ ((π β§ π β β0) β (π β (0...((πβπ) β 1)) β (πΉβπ) β€ ((π Β· π) Β· (πβπ)))) |
256 | 255 | 3impia 1118 |
1
β’ ((π β§ π β β0 β§ π β (0...((πβπ) β 1))) β (πΉβπ) β€ ((π Β· π) Β· (πβπ))) |