Theorem ppiqub 16254

Description: An upper bound on the prime-counting function π, which counts the number of primes less than N. (Contributed by Mario Carneiro, 13-Mar-2014.)

Assertion

Ref	Expression
ppiqub	|- ( ( N e. QQ /\ 0 <_ N ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )

Proof of Theorem ppiqub

Dummy variables x k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ppiqcl 16212	. . . . . . . 8 |- ( N e. QQ -> (π ` N ) e. NN0 )
2	1	nn0red 9626	. . . . . . 7 |- ( N e. QQ -> (π ` N ) e. RR )
3	2	adantr 276	. . . . . 6 |- ( ( N e. QQ /\ 3 <_ N ) -> (π ` N ) e. RR )
4		2re 9377	. . . . . 6 |- 2 e. RR
5		resubcl 8592	. . . . . 6 |- ( ( (π ` N ) e. RR /\ 2 e. RR ) -> ( (π ` N ) - 2 ) e. RR )
6	3, 4, 5	sylancl 417	. . . . 5 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` N ) - 2 ) e. RR )
7		4z 9679	. . . . . . . . . . 11 |- 4 e. ZZ
8	7	a1i 9	. . . . . . . . . 10 |- ( N e. QQ -> 4 e. ZZ )
9		flqcl 10719	. . . . . . . . . 10 |- ( N e. QQ -> ( |_ ` N ) e. ZZ )
10	8, 9	fzfigd 10883	. . . . . . . . 9 |- ( N e. QQ -> ( 4 ... ( |_ ` N ) ) e. Fin )
11		ssrab2 3333	. . . . . . . . . 10 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } C_ ( 4 ... ( |_ ` N ) )
12	11	a1i 9	. . . . . . . . 9 |- ( N e. QQ -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } C_ ( 4 ... ( |_ ` N ) ) )
13		animorrl 838	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> ( x e. ( 4 ... ( |_ ` N ) ) \/ -. x e. ( 4 ... ( |_ ` N ) ) ) )
14		df-dc 847	. . . . . . . . . . . . 13 |- (DECID x e. ( 4 ... ( |_ ` N ) ) <-> ( x e. ( 4 ... ( |_ ` N ) ) \/ -. x e. ( 4 ... ( |_ ` N ) ) ) )
15	13, 14	sylibr 134	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID x e. ( 4 ... ( |_ ` N ) ) )
16		elfzelz 10439	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( 4 ... ( |_ ` N ) ) -> x e. ZZ )
17	16	adantl 277	. . . . . . . . . . . . . . . . 17 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> x e. ZZ )
18		6nn 9475	. . . . . . . . . . . . . . . . 17 |- 6 e. NN
19		zmodcl 10796	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ZZ /\ 6 e. NN ) -> ( x mod 6 ) e. NN0 )
20	17, 18, 19	sylancl 417	. . . . . . . . . . . . . . . 16 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> ( x mod 6 ) e. NN0 )
21	20	nn0zd 9771	. . . . . . . . . . . . . . 15 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> ( x mod 6 ) e. ZZ )
22		1z 9675	. . . . . . . . . . . . . . 15 |- 1 e. ZZ
23		zdceq 9725	. . . . . . . . . . . . . . 15 |- ( ( ( x mod 6 ) e. ZZ /\ 1 e. ZZ ) -> DECID ( x mod 6 ) = 1 )
24	21, 22, 23	sylancl 417	. . . . . . . . . . . . . 14 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x mod 6 ) = 1 )
25		5nn 9474	. . . . . . . . . . . . . . . 16 |- 5 e. NN
26	25	nnzi 9670	. . . . . . . . . . . . . . 15 |- 5 e. ZZ
27		zdceq 9725	. . . . . . . . . . . . . . 15 |- ( ( ( x mod 6 ) e. ZZ /\ 5 e. ZZ ) -> DECID ( x mod 6 ) = 5 )
28	21, 26, 27	sylancl 417	. . . . . . . . . . . . . 14 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x mod 6 ) = 5 )
29		dcor 948	. . . . . . . . . . . . . 14 |- (DECID ( x mod 6 ) = 1 -> (DECID ( x mod 6 ) = 5 -> DECID ( ( x mod 6 ) = 1 \/ ( x mod 6 ) = 5 ) ) )
30	24, 28, 29	sylc 62	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( ( x mod 6 ) = 1 \/ ( x mod 6 ) = 5 ) )
31		elprg 3729	. . . . . . . . . . . . . . 15 |- ( ( x mod 6 ) e. NN0 -> ( ( x mod 6 ) e. { 1 , 5 } <-> ( ( x mod 6 ) = 1 \/ ( x mod 6 ) = 5 ) ) )
32	20, 31	syl 14	. . . . . . . . . . . . . 14 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> ( ( x mod 6 ) e. { 1 , 5 } <-> ( ( x mod 6 ) = 1 \/ ( x mod 6 ) = 5 ) ) )
33	32	dcbid 850	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> (DECID ( x mod 6 ) e. { 1 , 5 } <-> DECID ( ( x mod 6 ) = 1 \/ ( x mod 6 ) = 5 ) ) )
34	30, 33	mpbird 167	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x mod 6 ) e. { 1 , 5 } )
35	15, 34	dcand 945	. . . . . . . . . . 11 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) e. { 1 , 5 } ) )
36		oveq1 6092	. . . . . . . . . . . . . 14 |- ( k = x -> ( k mod 6 ) = ( x mod 6 ) )
37	36	eleq1d 2307	. . . . . . . . . . . . 13 |- ( k = x -> ( ( k mod 6 ) e. { 1 , 5 } <-> ( x mod 6 ) e. { 1 , 5 } ) )
38	37	elrab 2982	. . . . . . . . . . . 12 |- ( x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } <-> ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) e. { 1 , 5 } ) )
39	38	dcbii 852	. . . . . . . . . . 11 |- (DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } <-> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) e. { 1 , 5 } ) )
40	35, 39	sylibr 134	. . . . . . . . . 10 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } )
41	40	ralrimiva 2623	. . . . . . . . 9 |- ( N e. QQ -> A. x e. ( 4 ... ( |_ ` N ) )DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } )
42		ssfidc 7245	. . . . . . . . 9 |- ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } C_ ( 4 ... ( |_ ` N ) ) /\ A. x e. ( 4 ... ( |_ ` N ) )DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin )
43	10, 12, 41, 42	syl3anc 1278	. . . . . . . 8 |- ( N e. QQ -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin )
44		hashcl 11236	. . . . . . . 8 |- ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. NN0 )
45	43, 44	syl 14	. . . . . . 7 |- ( N e. QQ -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. NN0 )
46	45	nn0red 9626	. . . . . 6 |- ( N e. QQ -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. RR )
47	46	adantr 276	. . . . 5 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) e. RR )
48		qre 10035	. . . . . . 7 |- ( N e. QQ -> N e. RR )
49		3nn 9472	. . . . . . 7 |- 3 e. NN
50		nndivre 9343	. . . . . . 7 |- ( ( N e. RR /\ 3 e. NN ) -> ( N / 3 ) e. RR )
51	48, 49, 50	sylancl 417	. . . . . 6 |- ( N e. QQ -> ( N / 3 ) e. RR )
52	51	adantr 276	. . . . 5 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N / 3 ) e. RR )
53		ppiqfl 16227	. . . . . . . . 9 |- ( N e. QQ -> (π ` ( |_ ` N ) ) = (π ` N ) )
54	53	adantr 276	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> (π ` ( |_ ` N ) ) = (π ` N ) )
55		ppi3 16236	. . . . . . . . 9 |- (π ` 3 ) = 2
56	55	a1i 9	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> (π ` 3 ) = 2 )
57	54, 56	oveq12d 6103	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` ( |_ ` N ) ) - (π ` 3 ) ) = ( (π ` N ) - 2 ) )
58		3z 9678	. . . . . . . . . . 11 |- 3 e. ZZ
59	58	a1i 9	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> 3 e. ZZ )
60	9	adantr 276	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` N ) e. ZZ )
61		flqge 10730	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ 3 e. ZZ ) -> ( 3 <_ N <-> 3 <_ ( |_ ` N ) ) )
62	58, 61	mpan2 429	. . . . . . . . . . 11 |- ( N e. QQ -> ( 3 <_ N <-> 3 <_ ( |_ ` N ) ) )
63	62	biimpa 296	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> 3 <_ ( |_ ` N ) )
64		eluz2 9937	. . . . . . . . . 10 |- ( ( |_ ` N ) e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ ( |_ ` N ) e. ZZ /\ 3 <_ ( |_ ` N ) ) )
65	59, 60, 63, 64	syl3anbrc 1212	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` N ) e. ( ZZ>= ` 3 ) )
66		ppidif 16230	. . . . . . . . 9 |- ( ( |_ ` N ) e. ( ZZ>= ` 3 ) -> ( (π ` ( |_ ` N ) ) - (π ` 3 ) ) = (♯ ` ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
67	65, 66	syl 14	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` ( |_ ` N ) ) - (π ` 3 ) ) = (♯ ` ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
68		df-4 9368	. . . . . . . . . . 11 |- 4 = ( 3 + 1 )
69	68	oveq1i 6095	. . . . . . . . . 10 |- ( 4 ... ( |_ ` N ) ) = ( ( 3 + 1 ) ... ( |_ ` N ) )
70	69	ineq1i 3428	. . . . . . . . 9 |- ( ( 4 ... ( |_ ` N ) ) i^i Prime ) = ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime )
71	70	fveq2i 5698	. . . . . . . 8 |- (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) = (♯ ` ( ( ( 3 + 1 ) ... ( |_ ` N ) ) i^i Prime ) )
72	67, 71	eqtr4di 2289	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` ( |_ ` N ) ) - (π ` 3 ) ) = (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) )
73	57, 72	eqtr3d 2273	. . . . . 6 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` N ) - 2 ) = (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) )
74		dfin5 3227	. . . . . . . . . 10 |- ( ( 4 ... ( |_ ` N ) ) i^i Prime ) = { k e. ( 4 ... ( |_ ` N ) ) | k e. Prime }
75		elfzle1 10442	. . . . . . . . . . . 12 |- ( k e. ( 4 ... ( |_ ` N ) ) -> 4 <_ k )
76		ppiublem2 16253	. . . . . . . . . . . . 13 |- ( ( k e. Prime /\ 4 <_ k ) -> ( k mod 6 ) e. { 1 , 5 } )
77	76	expcom 116	. . . . . . . . . . . 12 |- ( 4 <_ k -> ( k e. Prime -> ( k mod 6 ) e. { 1 , 5 } ) )
78	75, 77	syl 14	. . . . . . . . . . 11 |- ( k e. ( 4 ... ( |_ ` N ) ) -> ( k e. Prime -> ( k mod 6 ) e. { 1 , 5 } ) )
79	78	ss2rabi 3330	. . . . . . . . . 10 |- { k e. ( 4 ... ( |_ ` N ) ) | k e. Prime } C_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } }
80	74, 79	eqsstri 3280	. . . . . . . . 9 |- ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } }
81		ssdomg 7065	. . . . . . . . 9 |- ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin -> ( ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
82	43, 80, 81	mpisyl 1496	. . . . . . . 8 |- ( N e. QQ -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } )
83		inss1 3451	. . . . . . . . . . 11 |- ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ ( 4 ... ( |_ ` N ) )
84	83	a1i 9	. . . . . . . . . 10 |- ( N e. QQ -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ ( 4 ... ( |_ ` N ) ) )
85		prmdcz 12928	. . . . . . . . . . . . . 14 |- ( x e. ZZ -> DECID x e. Prime )
86	17, 85	syl 14	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID x e. Prime )
87	15, 86	dcand 945	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ x e. Prime ) )
88		elin 3412	. . . . . . . . . . . . 13 |- ( x e. ( ( 4 ... ( |_ ` N ) ) i^i Prime ) <-> ( x e. ( 4 ... ( |_ ` N ) ) /\ x e. Prime ) )
89	88	dcbii 852	. . . . . . . . . . . 12 |- (DECID x e. ( ( 4 ... ( |_ ` N ) ) i^i Prime ) <-> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ x e. Prime ) )
90	87, 89	sylibr 134	. . . . . . . . . . 11 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID x e. ( ( 4 ... ( |_ ` N ) ) i^i Prime ) )
91	90	ralrimiva 2623	. . . . . . . . . 10 |- ( N e. QQ -> A. x e. ( 4 ... ( |_ ` N ) )DECID x e. ( ( 4 ... ( |_ ` N ) ) i^i Prime ) )
92		ssfidc 7245	. . . . . . . . . 10 |- ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ ( ( 4 ... ( |_ ` N ) ) i^i Prime ) C_ ( 4 ... ( |_ ` N ) ) /\ A. x e. ( 4 ... ( |_ ` N ) )DECID x e. ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) e. Fin )
93	10, 84, 91, 92	syl3anc 1278	. . . . . . . . 9 |- ( N e. QQ -> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) e. Fin )
94		fihashdom 11259	. . . . . . . . 9 |- ( ( ( ( 4 ... ( |_ ` N ) ) i^i Prime ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } e. Fin ) -> ( (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) <-> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
95	93, 43, 94	syl2anc 415	. . . . . . . 8 |- ( N e. QQ -> ( (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) <-> ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ~<_ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
96	82, 95	mpbird 167	. . . . . . 7 |- ( N e. QQ -> (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
97	96	adantr 276	. . . . . 6 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` ( ( 4 ... ( |_ ` N ) ) i^i Prime ) ) <_ (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
98	73, 97	eqbrtrd 4152	. . . . 5 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` N ) - 2 ) <_ (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) )
99		peano2zm 9687	. . . . . . . . . . 11 |- ( ( |_ ` N ) e. ZZ -> ( ( |_ ` N ) - 1 ) e. ZZ )
100	60, 99	syl 14	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` N ) - 1 ) e. ZZ )
101		znq 10034	. . . . . . . . . 10 |- ( ( ( ( |_ ` N ) - 1 ) e. ZZ /\ 6 e. NN ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) e. QQ )
102	100, 18, 101	sylancl 417	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) e. QQ )
103	102	flqcld 10725	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. ZZ )
104	103	zred 9773	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. RR )
105	26	a1i 9	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ 3 <_ N ) -> 5 e. ZZ )
106	60, 105	zsubcld 9778	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` N ) - 5 ) e. ZZ )
107		znq 10034	. . . . . . . . . . 11 |- ( ( ( ( |_ ` N ) - 5 ) e. ZZ /\ 6 e. NN ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) e. QQ )
108	106, 18, 107	sylancl 417	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) e. QQ )
109	108	flqcld 10725	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. ZZ )
110	109	zred 9773	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. RR )
111		peano2re 8464	. . . . . . . 8 |- ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. RR -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) e. RR )
112	110, 111	syl 14	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) e. RR )
113		peano2rem 8595	. . . . . . . . . 10 |- ( N e. RR -> ( N - 1 ) e. RR )
114	48, 113	syl 14	. . . . . . . . 9 |- ( N e. QQ -> ( N - 1 ) e. RR )
115	114	adantr 276	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N - 1 ) e. RR )
116		nndivre 9343	. . . . . . . 8 |- ( ( ( N - 1 ) e. RR /\ 6 e. NN ) -> ( ( N - 1 ) / 6 ) e. RR )
117	115, 18, 116	sylancl 417	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( N - 1 ) / 6 ) e. RR )
118	48	adantr 276	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> N e. RR )
119		5re 9386	. . . . . . . . . 10 |- 5 e. RR
120		resubcl 8592	. . . . . . . . . 10 |- ( ( N e. RR /\ 5 e. RR ) -> ( N - 5 ) e. RR )
121	118, 119, 120	sylancl 417	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N - 5 ) e. RR )
122		nndivre 9343	. . . . . . . . 9 |- ( ( ( N - 5 ) e. RR /\ 6 e. NN ) -> ( ( N - 5 ) / 6 ) e. RR )
123	121, 18, 122	sylancl 417	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( N - 5 ) / 6 ) e. RR )
124		peano2re 8464	. . . . . . . 8 |- ( ( ( N - 5 ) / 6 ) e. RR -> ( ( ( N - 5 ) / 6 ) + 1 ) e. RR )
125	123, 124	syl 14	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( N - 5 ) / 6 ) + 1 ) e. RR )
126		qre 10035	. . . . . . . . 9 |- ( ( ( ( |_ ` N ) - 1 ) / 6 ) e. QQ -> ( ( ( |_ ` N ) - 1 ) / 6 ) e. RR )
127	102, 126	syl 14	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) e. RR )
128		flqle 10726	. . . . . . . . 9 |- ( ( ( ( |_ ` N ) - 1 ) / 6 ) e. QQ -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 1 ) / 6 ) )
129	102, 128	syl 14	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 1 ) / 6 ) )
130	60	zred 9773	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` N ) e. RR )
131		1red 8342	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> 1 e. RR )
132		flqle 10726	. . . . . . . . . . 11 |- ( N e. QQ -> ( |_ ` N ) <_ N )
133	132	adantr 276	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` N ) <_ N )
134	130, 118, 131, 133	lesub1dd 8891	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` N ) - 1 ) <_ ( N - 1 ) )
135	100	zred 9773	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` N ) - 1 ) e. RR )
136		6re 9388	. . . . . . . . . . 11 |- 6 e. RR
137	136	a1i 9	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> 6 e. RR )
138		6pos 9408	. . . . . . . . . . 11 |- 0 < 6
139	138	a1i 9	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> 0 < 6 )
140		lediv1 9202	. . . . . . . . . 10 |- ( ( ( ( |_ ` N ) - 1 ) e. RR /\ ( N - 1 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( ( |_ ` N ) - 1 ) <_ ( N - 1 ) <-> ( ( ( |_ ` N ) - 1 ) / 6 ) <_ ( ( N - 1 ) / 6 ) ) )
141	135, 115, 137, 139, 140	syl112anc 1282	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) <_ ( N - 1 ) <-> ( ( ( |_ ` N ) - 1 ) / 6 ) <_ ( ( N - 1 ) / 6 ) ) )
142	134, 141	mpbid 147	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 1 ) / 6 ) <_ ( ( N - 1 ) / 6 ) )
143	104, 127, 117, 129, 142	letrd 8452	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) <_ ( ( N - 1 ) / 6 ) )
144		resubcl 8592	. . . . . . . . . . 11 |- ( ( ( |_ ` N ) e. RR /\ 5 e. RR ) -> ( ( |_ ` N ) - 5 ) e. RR )
145	130, 119, 144	sylancl 417	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` N ) - 5 ) e. RR )
146		nndivre 9343	. . . . . . . . . 10 |- ( ( ( ( |_ ` N ) - 5 ) e. RR /\ 6 e. NN ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) e. RR )
147	145, 18, 146	sylancl 417	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) e. RR )
148		flqle 10726	. . . . . . . . . 10 |- ( ( ( ( |_ ` N ) - 5 ) / 6 ) e. QQ -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 5 ) / 6 ) )
149	108, 148	syl 14	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) <_ ( ( ( |_ ` N ) - 5 ) / 6 ) )
150	119	a1i 9	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> 5 e. RR )
151	130, 118, 150, 133	lesub1dd 8891	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` N ) - 5 ) <_ ( N - 5 ) )
152		lediv1 9202	. . . . . . . . . . 11 |- ( ( ( ( |_ ` N ) - 5 ) e. RR /\ ( N - 5 ) e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( ( |_ ` N ) - 5 ) <_ ( N - 5 ) <-> ( ( ( |_ ` N ) - 5 ) / 6 ) <_ ( ( N - 5 ) / 6 ) ) )
153	145, 121, 137, 139, 152	syl112anc 1282	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) <_ ( N - 5 ) <-> ( ( ( |_ ` N ) - 5 ) / 6 ) <_ ( ( N - 5 ) / 6 ) ) )
154	151, 153	mpbid 147	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( |_ ` N ) - 5 ) / 6 ) <_ ( ( N - 5 ) / 6 ) )
155	110, 147, 123, 149, 154	letrd 8452	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) <_ ( ( N - 5 ) / 6 ) )
156	110, 123, 131, 155	leadd1dd 8889	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) <_ ( ( ( N - 5 ) / 6 ) + 1 ) )
157	104, 112, 117, 125, 143, 156	le2addd 8894	. . . . . 6 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) + ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) ) <_ ( ( ( N - 1 ) / 6 ) + ( ( ( N - 5 ) / 6 ) + 1 ) ) )
158		elfzelz 10439	. . . . . . . . . . . . . 14 |- ( k e. ( 4 ... ( |_ ` N ) ) -> k e. ZZ )
159	18	a1i 9	. . . . . . . . . . . . . 14 |- ( k e. ( 4 ... ( |_ ` N ) ) -> 6 e. NN )
160	158, 159	zmodcld 10797	. . . . . . . . . . . . 13 |- ( k e. ( 4 ... ( |_ ` N ) ) -> ( k mod 6 ) e. NN0 )
161		elprg 3729	. . . . . . . . . . . . 13 |- ( ( k mod 6 ) e. NN0 -> ( ( k mod 6 ) e. { 1 , 5 } <-> ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) ) )
162	160, 161	syl 14	. . . . . . . . . . . 12 |- ( k e. ( 4 ... ( |_ ` N ) ) -> ( ( k mod 6 ) e. { 1 , 5 } <-> ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) ) )
163	162	rabbiia 2807	. . . . . . . . . . 11 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } = { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) }
164		unrab 3504	. . . . . . . . . . 11 |- ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 \/ ( k mod 6 ) = 5 ) }
165	163, 164	eqtr4i 2262	. . . . . . . . . 10 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } = ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } )
166	165	fveq2i 5698	. . . . . . . . 9 |- (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = (♯ ` ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) )
167		ssrab2 3333	. . . . . . . . . . . 12 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } C_ ( 4 ... ( |_ ` N ) )
168	167	a1i 9	. . . . . . . . . . 11 |- ( N e. QQ -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } C_ ( 4 ... ( |_ ` N ) ) )
169	15, 24	dcand 945	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) = 1 ) )
170	36	eqeq1d 2247	. . . . . . . . . . . . . . 15 |- ( k = x -> ( ( k mod 6 ) = 1 <-> ( x mod 6 ) = 1 ) )
171	170	elrab 2982	. . . . . . . . . . . . . 14 |- ( x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } <-> ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) = 1 ) )
172	171	dcbii 852	. . . . . . . . . . . . 13 |- (DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } <-> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) = 1 ) )
173	169, 172	sylibr 134	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } )
174	173	ralrimiva 2623	. . . . . . . . . . 11 |- ( N e. QQ -> A. x e. ( 4 ... ( |_ ` N ) )DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } )
175		ssfidc 7245	. . . . . . . . . . 11 |- ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } C_ ( 4 ... ( |_ ` N ) ) /\ A. x e. ( 4 ... ( |_ ` N ) )DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } e. Fin )
176	10, 168, 174, 175	syl3anc 1278	. . . . . . . . . 10 |- ( N e. QQ -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } e. Fin )
177		ssrab2 3333	. . . . . . . . . . . 12 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } C_ ( 4 ... ( |_ ` N ) )
178	177	a1i 9	. . . . . . . . . . 11 |- ( N e. QQ -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } C_ ( 4 ... ( |_ ` N ) ) )
179	15, 28	dcand 945	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) = 5 ) )
180	36	eqeq1d 2247	. . . . . . . . . . . . . . 15 |- ( k = x -> ( ( k mod 6 ) = 5 <-> ( x mod 6 ) = 5 ) )
181	180	elrab 2982	. . . . . . . . . . . . . 14 |- ( x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } <-> ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) = 5 ) )
182	181	dcbii 852	. . . . . . . . . . . . 13 |- (DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } <-> DECID ( x e. ( 4 ... ( |_ ` N ) ) /\ ( x mod 6 ) = 5 ) )
183	179, 182	sylibr 134	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ x e. ( 4 ... ( |_ ` N ) ) ) -> DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } )
184	183	ralrimiva 2623	. . . . . . . . . . 11 |- ( N e. QQ -> A. x e. ( 4 ... ( |_ ` N ) )DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } )
185		ssfidc 7245	. . . . . . . . . . 11 |- ( ( ( 4 ... ( |_ ` N ) ) e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } C_ ( 4 ... ( |_ ` N ) ) /\ A. x e. ( 4 ... ( |_ ` N ) )DECID x e. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } e. Fin )
186	10, 178, 184, 185	syl3anc 1278	. . . . . . . . . 10 |- ( N e. QQ -> { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } e. Fin )
187		inrab 3505	. . . . . . . . . . . 12 |- ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) }
188		rabeq0 3552	. . . . . . . . . . . . 13 |- ( { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) } = (/) <-> A. k e. ( 4 ... ( |_ ` N ) ) -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) )
189		1re 8326	. . . . . . . . . . . . . . . 16 |- 1 e. RR
190		1lt5 9488	. . . . . . . . . . . . . . . 16 |- 1 < 5
191	189, 190	ltneii 8424	. . . . . . . . . . . . . . 15 |- 1 =/= 5
192		eqtr2 2257	. . . . . . . . . . . . . . . 16 |- ( ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) -> 1 = 5 )
193	192	necon3ai 2469	. . . . . . . . . . . . . . 15 |- ( 1 =/= 5 -> -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) )
194	191, 193	ax-mp 5	. . . . . . . . . . . . . 14 |- -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 )
195	194	a1i 9	. . . . . . . . . . . . 13 |- ( k e. ( 4 ... ( |_ ` N ) ) -> -. ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) )
196	188, 195	mprgbir 2608	. . . . . . . . . . . 12 |- { k e. ( 4 ... ( |_ ` N ) ) | ( ( k mod 6 ) = 1 /\ ( k mod 6 ) = 5 ) } = (/)
197	187, 196	eqtri 2259	. . . . . . . . . . 11 |- ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = (/)
198	197	a1i 9	. . . . . . . . . 10 |- ( N e. QQ -> ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = (/) )
199		hashun 11261	. . . . . . . . . 10 |- ( ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } e. Fin /\ { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } e. Fin /\ ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } i^i { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = (/) ) -> (♯ ` ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) = ( (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) )
200	176, 186, 198, 199	syl3anc 1278	. . . . . . . . 9 |- ( N e. QQ -> (♯ ` ( { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } u. { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) = ( (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) )
201	166, 200	eqtrid 2283	. . . . . . . 8 |- ( N e. QQ -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = ( (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) )
202	201	adantr 276	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = ( (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) )
203		zq 10036	. . . . . . . . . . . . . . . . 17 |- ( 1 e. ZZ -> 1 e. QQ )
204	22, 203	ax-mp 5	. . . . . . . . . . . . . . . 16 |- 1 e. QQ
205		nnq 10043	. . . . . . . . . . . . . . . . 17 |- ( 6 e. NN -> 6 e. QQ )
206	18, 205	ax-mp 5	. . . . . . . . . . . . . . . 16 |- 6 e. QQ
207		0le1 8811	. . . . . . . . . . . . . . . 16 |- 0 <_ 1
208		1lt6 9493	. . . . . . . . . . . . . . . 16 |- 1 < 6
209		modqid 10801	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 e. QQ /\ 6 e. QQ ) /\ ( 0 <_ 1 /\ 1 < 6 ) ) -> ( 1 mod 6 ) = 1 )
210	204, 206, 207, 208, 209	mp4an 431	. . . . . . . . . . . . . . 15 |- ( 1 mod 6 ) = 1
211	210	eqeq2i 2249	. . . . . . . . . . . . . 14 |- ( ( k mod 6 ) = ( 1 mod 6 ) <-> ( k mod 6 ) = 1 )
212		moddvds 12585	. . . . . . . . . . . . . . 15 |- ( ( 6 e. NN /\ k e. ZZ /\ 1 e. ZZ ) -> ( ( k mod 6 ) = ( 1 mod 6 ) <-> 6 || ( k - 1 ) ) )
213	18, 22, 212	mp3an13 1369	. . . . . . . . . . . . . 14 |- ( k e. ZZ -> ( ( k mod 6 ) = ( 1 mod 6 ) <-> 6 || ( k - 1 ) ) )
214	211, 213	bitr3id 194	. . . . . . . . . . . . 13 |- ( k e. ZZ -> ( ( k mod 6 ) = 1 <-> 6 || ( k - 1 ) ) )
215	158, 214	syl 14	. . . . . . . . . . . 12 |- ( k e. ( 4 ... ( |_ ` N ) ) -> ( ( k mod 6 ) = 1 <-> 6 || ( k - 1 ) ) )
216	215	rabbiia 2807	. . . . . . . . . . 11 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } = { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 1 ) }
217	216	fveq2i 5698	. . . . . . . . . 10 |- (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) = (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 1 ) } )
218	18	a1i 9	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> 6 e. NN )
219	7	a1i 9	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> 4 e. ZZ )
220		4m1e3 9428	. . . . . . . . . . . . 13 |- ( 4 - 1 ) = 3
221	220	fveq2i 5698	. . . . . . . . . . . 12 |- ( ZZ>= ` ( 4 - 1 ) ) = ( ZZ>= ` 3 )
222	65, 221	eleqtrrdi 2332	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` N ) e. ( ZZ>= ` ( 4 - 1 ) ) )
223		1zzd 9676	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> 1 e. ZZ )
224	218, 219, 222, 223	hashdvds 13022	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 1 ) } ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) )
225	217, 224	eqtrid 2283	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) )
226		2cn 9378	. . . . . . . . . . . . . . 15 |- 2 e. CC
227		ax-1cn 8273	. . . . . . . . . . . . . . 15 |- 1 e. CC
228		df-3 9367	. . . . . . . . . . . . . . . 16 |- 3 = ( 2 + 1 )
229	220, 228	eqtri 2259	. . . . . . . . . . . . . . 15 |- ( 4 - 1 ) = ( 2 + 1 )
230	226, 227, 229	mvrraddi 8545	. . . . . . . . . . . . . 14 |- ( ( 4 - 1 ) - 1 ) = 2
231	230	oveq1i 6095	. . . . . . . . . . . . 13 |- ( ( ( 4 - 1 ) - 1 ) / 6 ) = ( 2 / 6 )
232	231	fveq2i 5698	. . . . . . . . . . . 12 |- ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) = ( |_ ` ( 2 / 6 ) )
233		0re 8327	. . . . . . . . . . . . . 14 |- 0 e. RR
234	136, 138	gt0ap0ii 8959	. . . . . . . . . . . . . . 15 |- 6 # 0
235	4, 136, 234	redivclapi 9112	. . . . . . . . . . . . . 14 |- ( 2 / 6 ) e. RR
236		2pos 9398	. . . . . . . . . . . . . . 15 |- 0 < 2
237	4, 136, 236, 138	divgt0ii 9252	. . . . . . . . . . . . . 14 |- 0 < ( 2 / 6 )
238	233, 235, 237	ltleii 8430	. . . . . . . . . . . . 13 |- 0 <_ ( 2 / 6 )
239		2lt6 9492	. . . . . . . . . . . . . . . 16 |- 2 < 6
240		6cn 9389	. . . . . . . . . . . . . . . . 17 |- 6 e. CC
241	240	mulridi 8329	. . . . . . . . . . . . . . . 16 |- ( 6 x. 1 ) = 6
242	239, 241	breqtrri 4157	. . . . . . . . . . . . . . 15 |- 2 < ( 6 x. 1 )
243	136, 138	pm3.2i 272	. . . . . . . . . . . . . . . 16 |- ( 6 e. RR /\ 0 < 6 )
244		ltdivmul 9209	. . . . . . . . . . . . . . . 16 |- ( ( 2 e. RR /\ 1 e. RR /\ ( 6 e. RR /\ 0 < 6 ) ) -> ( ( 2 / 6 ) < 1 <-> 2 < ( 6 x. 1 ) ) )
245	4, 189, 243, 244	mp3an 1378	. . . . . . . . . . . . . . 15 |- ( ( 2 / 6 ) < 1 <-> 2 < ( 6 x. 1 ) )
246	242, 245	mpbir 146	. . . . . . . . . . . . . 14 |- ( 2 / 6 ) < 1
247		1e0p1 9828	. . . . . . . . . . . . . 14 |- 1 = ( 0 + 1 )
248	246, 247	breqtri 4155	. . . . . . . . . . . . 13 |- ( 2 / 6 ) < ( 0 + 1 )
249		2z 9677	. . . . . . . . . . . . . . 15 |- 2 e. ZZ
250		znq 10034	. . . . . . . . . . . . . . 15 |- ( ( 2 e. ZZ /\ 6 e. NN ) -> ( 2 / 6 ) e. QQ )
251	249, 18, 250	mp2an 430	. . . . . . . . . . . . . 14 |- ( 2 / 6 ) e. QQ
252		0z 9660	. . . . . . . . . . . . . 14 |- 0 e. ZZ
253		flqbi 10740	. . . . . . . . . . . . . 14 |- ( ( ( 2 / 6 ) e. QQ /\ 0 e. ZZ ) -> ( ( |_ ` ( 2 / 6 ) ) = 0 <-> ( 0 <_ ( 2 / 6 ) /\ ( 2 / 6 ) < ( 0 + 1 ) ) ) )
254	251, 252, 253	mp2an 430	. . . . . . . . . . . . 13 |- ( ( |_ ` ( 2 / 6 ) ) = 0 <-> ( 0 <_ ( 2 / 6 ) /\ ( 2 / 6 ) < ( 0 + 1 ) ) )
255	238, 248, 254	mpbir2an 955	. . . . . . . . . . . 12 |- ( |_ ` ( 2 / 6 ) ) = 0
256	232, 255	eqtri 2259	. . . . . . . . . . 11 |- ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) = 0
257	256	oveq2i 6096	. . . . . . . . . 10 |- ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - 0 )
258	103	zcnd 9774	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) e. CC )
259	258	subid1d 8628	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - 0 ) = ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) )
260	257, 259	eqtrid 2283	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 1 ) / 6 ) ) ) = ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) )
261	225, 260	eqtrd 2271	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) = ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) )
262		nnq 10043	. . . . . . . . . . . . . . . . 17 |- ( 5 e. NN -> 5 e. QQ )
263	25, 262	ax-mp 5	. . . . . . . . . . . . . . . 16 |- 5 e. QQ
264		5pos 9407	. . . . . . . . . . . . . . . . 17 |- 0 < 5
265	233, 119, 264	ltleii 8430	. . . . . . . . . . . . . . . 16 |- 0 <_ 5
266		5lt6 9489	. . . . . . . . . . . . . . . 16 |- 5 < 6
267		modqid 10801	. . . . . . . . . . . . . . . 16 |- ( ( ( 5 e. QQ /\ 6 e. QQ ) /\ ( 0 <_ 5 /\ 5 < 6 ) ) -> ( 5 mod 6 ) = 5 )
268	263, 206, 265, 266, 267	mp4an 431	. . . . . . . . . . . . . . 15 |- ( 5 mod 6 ) = 5
269	268	eqeq2i 2249	. . . . . . . . . . . . . 14 |- ( ( k mod 6 ) = ( 5 mod 6 ) <-> ( k mod 6 ) = 5 )
270		moddvds 12585	. . . . . . . . . . . . . . 15 |- ( ( 6 e. NN /\ k e. ZZ /\ 5 e. ZZ ) -> ( ( k mod 6 ) = ( 5 mod 6 ) <-> 6 || ( k - 5 ) ) )
271	18, 26, 270	mp3an13 1369	. . . . . . . . . . . . . 14 |- ( k e. ZZ -> ( ( k mod 6 ) = ( 5 mod 6 ) <-> 6 || ( k - 5 ) ) )
272	269, 271	bitr3id 194	. . . . . . . . . . . . 13 |- ( k e. ZZ -> ( ( k mod 6 ) = 5 <-> 6 || ( k - 5 ) ) )
273	158, 272	syl 14	. . . . . . . . . . . 12 |- ( k e. ( 4 ... ( |_ ` N ) ) -> ( ( k mod 6 ) = 5 <-> 6 || ( k - 5 ) ) )
274	273	rabbiia 2807	. . . . . . . . . . 11 |- { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } = { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 5 ) }
275	274	fveq2i 5698	. . . . . . . . . 10 |- (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 5 ) } )
276	218, 219, 222, 105	hashdvds 13022	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | 6 || ( k - 5 ) } ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) )
277	275, 276	eqtrid 2283	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) )
278	220	oveq1i 6095	. . . . . . . . . . . . . . . 16 |- ( ( 4 - 1 ) - 5 ) = ( 3 - 5 )
279		5cn 9387	. . . . . . . . . . . . . . . . 17 |- 5 e. CC
280		3cn 9382	. . . . . . . . . . . . . . . . 17 |- 3 e. CC
281	279, 280	negsubdi2i 8614	. . . . . . . . . . . . . . . 16 |- -u ( 5 - 3 ) = ( 3 - 5 )
282		3p2e5 9449	. . . . . . . . . . . . . . . . . . 19 |- ( 3 + 2 ) = 5
283	282	oveq1i 6095	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 + 2 ) - 3 ) = ( 5 - 3 )
284		pncan2 8535	. . . . . . . . . . . . . . . . . . 19 |- ( ( 3 e. CC /\ 2 e. CC ) -> ( ( 3 + 2 ) - 3 ) = 2 )
285	280, 226, 284	mp2an 430	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 + 2 ) - 3 ) = 2
286	283, 285	eqtr3i 2261	. . . . . . . . . . . . . . . . 17 |- ( 5 - 3 ) = 2
287	286	negeqi 8522	. . . . . . . . . . . . . . . 16 |- -u ( 5 - 3 ) = -u 2
288	278, 281, 287	3eqtr2i 2265	. . . . . . . . . . . . . . 15 |- ( ( 4 - 1 ) - 5 ) = -u 2
289	288	oveq1i 6095	. . . . . . . . . . . . . 14 |- ( ( ( 4 - 1 ) - 5 ) / 6 ) = ( -u 2 / 6 )
290		divnegap 9039	. . . . . . . . . . . . . . 15 |- ( ( 2 e. CC /\ 6 e. CC /\ 6 # 0 ) -> -u ( 2 / 6 ) = ( -u 2 / 6 ) )
291	226, 240, 234, 290	mp3an 1378	. . . . . . . . . . . . . 14 |- -u ( 2 / 6 ) = ( -u 2 / 6 )
292	289, 291	eqtr4i 2262	. . . . . . . . . . . . 13 |- ( ( ( 4 - 1 ) - 5 ) / 6 ) = -u ( 2 / 6 )
293	292	fveq2i 5698	. . . . . . . . . . . 12 |- ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) = ( |_ ` -u ( 2 / 6 ) )
294	235, 189, 246	ltleii 8430	. . . . . . . . . . . . . 14 |- ( 2 / 6 ) <_ 1
295	235, 189	lenegi 8824	. . . . . . . . . . . . . 14 |- ( ( 2 / 6 ) <_ 1 <-> -u 1 <_ -u ( 2 / 6 ) )
296	294, 295	mpbi 145	. . . . . . . . . . . . 13 |- -u 1 <_ -u ( 2 / 6 )
297	233, 235	ltnegi 8823	. . . . . . . . . . . . . . 15 |- ( 0 < ( 2 / 6 ) <-> -u ( 2 / 6 ) < -u 0 )
298	237, 297	mpbi 145	. . . . . . . . . . . . . 14 |- -u ( 2 / 6 ) < -u 0
299		neg0 8574	. . . . . . . . . . . . . . . 16 |- -u 0 = 0
300		1pneg1e0 9418	. . . . . . . . . . . . . . . 16 |- ( 1 + -u 1 ) = 0
301	299, 300	eqtr4i 2262	. . . . . . . . . . . . . . 15 |- -u 0 = ( 1 + -u 1 )
302		neg1cn 9412	. . . . . . . . . . . . . . . 16 |- -u 1 e. CC
303	302, 227	addcomi 8472	. . . . . . . . . . . . . . 15 |- ( -u 1 + 1 ) = ( 1 + -u 1 )
304	301, 303	eqtr4i 2262	. . . . . . . . . . . . . 14 |- -u 0 = ( -u 1 + 1 )
305	298, 304	breqtri 4155	. . . . . . . . . . . . 13 |- -u ( 2 / 6 ) < ( -u 1 + 1 )
306		qnegcl 10046	. . . . . . . . . . . . . . 15 |- ( ( 2 / 6 ) e. QQ -> -u ( 2 / 6 ) e. QQ )
307	251, 306	ax-mp 5	. . . . . . . . . . . . . 14 |- -u ( 2 / 6 ) e. QQ
308		neg1z 9681	. . . . . . . . . . . . . 14 |- -u 1 e. ZZ
309		flqbi 10740	. . . . . . . . . . . . . 14 |- ( ( -u ( 2 / 6 ) e. QQ /\ -u 1 e. ZZ ) -> ( ( |_ ` -u ( 2 / 6 ) ) = -u 1 <-> ( -u 1 <_ -u ( 2 / 6 ) /\ -u ( 2 / 6 ) < ( -u 1 + 1 ) ) ) )
310	307, 308, 309	mp2an 430	. . . . . . . . . . . . 13 |- ( ( |_ ` -u ( 2 / 6 ) ) = -u 1 <-> ( -u 1 <_ -u ( 2 / 6 ) /\ -u ( 2 / 6 ) < ( -u 1 + 1 ) ) )
311	296, 305, 310	mpbir2an 955	. . . . . . . . . . . 12 |- ( |_ ` -u ( 2 / 6 ) ) = -u 1
312	293, 311	eqtri 2259	. . . . . . . . . . 11 |- ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) = -u 1
313	312	oveq2i 6096	. . . . . . . . . 10 |- ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - -u 1 )
314	109	zcnd 9774	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. CC )
315		subneg 8577	. . . . . . . . . . 11 |- ( ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) e. CC /\ 1 e. CC ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - -u 1 ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
316	314, 227, 315	sylancl 417	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - -u 1 ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
317	313, 316	eqtrid 2283	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) - ( |_ ` ( ( ( 4 - 1 ) - 5 ) / 6 ) ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
318	277, 317	eqtrd 2271	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) = ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) )
319	261, 318	oveq12d 6103	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 1 } ) + (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) = 5 } ) ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) + ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) ) )
320	202, 319	eqtrd 2271	. . . . . 6 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) = ( ( |_ ` ( ( ( |_ ` N ) - 1 ) / 6 ) ) + ( ( |_ ` ( ( ( |_ ` N ) - 5 ) / 6 ) ) + 1 ) ) )
321	118	recnd 8355	. . . . . . . . . . . . 13 |- ( ( N e. QQ /\ 3 <_ N ) -> N e. CC )
322	321	2timesd 9553	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ 3 <_ N ) -> ( 2 x. N ) = ( N + N ) )
323		df-6 9370	. . . . . . . . . . . . . 14 |- 6 = ( 5 + 1 )
324	279, 227	addcomi 8472	. . . . . . . . . . . . . 14 |- ( 5 + 1 ) = ( 1 + 5 )
325	323, 324	eqtri 2259	. . . . . . . . . . . . 13 |- 6 = ( 1 + 5 )
326	325	a1i 9	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ 3 <_ N ) -> 6 = ( 1 + 5 ) )
327	322, 326	oveq12d 6103	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( 2 x. N ) - 6 ) = ( ( N + N ) - ( 1 + 5 ) ) )
328		addsub4 8571	. . . . . . . . . . . . 13 |- ( ( ( N e. CC /\ N e. CC ) /\ ( 1 e. CC /\ 5 e. CC ) ) -> ( ( N + N ) - ( 1 + 5 ) ) = ( ( N - 1 ) + ( N - 5 ) ) )
329	227, 279, 328	mpanr12 443	. . . . . . . . . . . 12 |- ( ( N e. CC /\ N e. CC ) -> ( ( N + N ) - ( 1 + 5 ) ) = ( ( N - 1 ) + ( N - 5 ) ) )
330	321, 321, 329	syl2anc 415	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( N + N ) - ( 1 + 5 ) ) = ( ( N - 1 ) + ( N - 5 ) ) )
331	327, 330	eqtrd 2271	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( 2 x. N ) - 6 ) = ( ( N - 1 ) + ( N - 5 ) ) )
332	331	oveq1d 6100	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) )
333		mulcl 8307	. . . . . . . . . . . 12 |- ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) e. CC )
334	226, 321, 333	sylancr 418	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( 2 x. N ) e. CC )
335	240, 234	pm3.2i 272	. . . . . . . . . . . 12 |- ( 6 e. CC /\ 6 # 0 )
336		divsubdirap 9041	. . . . . . . . . . . 12 |- ( ( ( 2 x. N ) e. CC /\ 6 e. CC /\ ( 6 e. CC /\ 6 # 0 ) ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) )
337	240, 335, 336	mp3an23 1370	. . . . . . . . . . 11 |- ( ( 2 x. N ) e. CC -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) )
338	334, 337	syl 14	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) )
339		2t3e6 9465	. . . . . . . . . . . . 13 |- ( 2 x. 3 ) = 6
340	339	oveq2i 6096	. . . . . . . . . . . 12 |- ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( ( 2 x. N ) / 6 )
341		3ap0 9403	. . . . . . . . . . . . . . 15 |- 3 # 0
342	280, 341	pm3.2i 272	. . . . . . . . . . . . . 14 |- ( 3 e. CC /\ 3 # 0 )
343		2ap0 9400	. . . . . . . . . . . . . . 15 |- 2 # 0
344	226, 343	pm3.2i 272	. . . . . . . . . . . . . 14 |- ( 2 e. CC /\ 2 # 0 )
345		divcanap5 9047	. . . . . . . . . . . . . 14 |- ( ( N e. CC /\ ( 3 e. CC /\ 3 # 0 ) /\ ( 2 e. CC /\ 2 # 0 ) ) -> ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( N / 3 ) )
346	342, 344, 345	mp3an23 1370	. . . . . . . . . . . . 13 |- ( N e. CC -> ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( N / 3 ) )
347	321, 346	syl 14	. . . . . . . . . . . 12 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( 2 x. N ) / ( 2 x. 3 ) ) = ( N / 3 ) )
348	340, 347	eqtr3id 2285	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( 2 x. N ) / 6 ) = ( N / 3 ) )
349	240, 234	dividapi 9078	. . . . . . . . . . . 12 |- ( 6 / 6 ) = 1
350	349	a1i 9	. . . . . . . . . . 11 |- ( ( N e. QQ /\ 3 <_ N ) -> ( 6 / 6 ) = 1 )
351	348, 350	oveq12d 6103	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( 2 x. N ) / 6 ) - ( 6 / 6 ) ) = ( ( N / 3 ) - 1 ) )
352	338, 351	eqtrd 2271	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( 2 x. N ) - 6 ) / 6 ) = ( ( N / 3 ) - 1 ) )
353	115	recnd 8355	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N - 1 ) e. CC )
354	121	recnd 8355	. . . . . . . . . 10 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N - 5 ) e. CC )
355		divdirap 9030	. . . . . . . . . . 11 |- ( ( ( N - 1 ) e. CC /\ ( N - 5 ) e. CC /\ ( 6 e. CC /\ 6 # 0 ) ) -> ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
356	335, 355	mp3an3 1367	. . . . . . . . . 10 |- ( ( ( N - 1 ) e. CC /\ ( N - 5 ) e. CC ) -> ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
357	353, 354, 356	syl2anc 415	. . . . . . . . 9 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( N - 1 ) + ( N - 5 ) ) / 6 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
358	332, 352, 357	3eqtr3d 2279	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( N / 3 ) - 1 ) = ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) )
359	358	oveq1d 6100	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( N / 3 ) - 1 ) + 1 ) = ( ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) + 1 ) )
360	52	recnd 8355	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N / 3 ) e. CC )
361		npcan 8537	. . . . . . . 8 |- ( ( ( N / 3 ) e. CC /\ 1 e. CC ) -> ( ( ( N / 3 ) - 1 ) + 1 ) = ( N / 3 ) )
362	360, 227, 361	sylancl 417	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( N / 3 ) - 1 ) + 1 ) = ( N / 3 ) )
363	117	recnd 8355	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( N - 1 ) / 6 ) e. CC )
364	123	recnd 8355	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( N - 5 ) / 6 ) e. CC )
365	227	a1i 9	. . . . . . . 8 |- ( ( N e. QQ /\ 3 <_ N ) -> 1 e. CC )
366	363, 364, 365	addassd 8349	. . . . . . 7 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( ( ( N - 1 ) / 6 ) + ( ( N - 5 ) / 6 ) ) + 1 ) = ( ( ( N - 1 ) / 6 ) + ( ( ( N - 5 ) / 6 ) + 1 ) ) )
367	359, 362, 366	3eqtr3d 2279	. . . . . 6 |- ( ( N e. QQ /\ 3 <_ N ) -> ( N / 3 ) = ( ( ( N - 1 ) / 6 ) + ( ( ( N - 5 ) / 6 ) + 1 ) ) )
368	157, 320, 367	3brtr4d 4162	. . . . 5 |- ( ( N e. QQ /\ 3 <_ N ) -> (♯ ` { k e. ( 4 ... ( |_ ` N ) ) | ( k mod 6 ) e. { 1 , 5 } } ) <_ ( N / 3 ) )
369	6, 47, 52, 98, 368	letrd 8452	. . . 4 |- ( ( N e. QQ /\ 3 <_ N ) -> ( (π ` N ) - 2 ) <_ ( N / 3 ) )
370	4	a1i 9	. . . . 5 |- ( ( N e. QQ /\ 3 <_ N ) -> 2 e. RR )
371	3, 370, 52	lesubaddd 8872	. . . 4 |- ( ( N e. QQ /\ 3 <_ N ) -> ( ( (π ` N ) - 2 ) <_ ( N / 3 ) <-> (π ` N ) <_ ( ( N / 3 ) + 2 ) ) )
372	369, 371	mpbid 147	. . 3 |- ( ( N e. QQ /\ 3 <_ N ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )
373	372	adantlr 481	. 2 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ 3 <_ N ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )
374	2	ad2antrr 492	. . 3 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> (π ` N ) e. RR )
375	4	a1i 9	. . 3 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> 2 e. RR )
376	51	ad2antrr 492	. . . 4 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> ( N / 3 ) e. RR )
377		readdcl 8306	. . . 4 |- ( ( ( N / 3 ) e. RR /\ 2 e. RR ) -> ( ( N / 3 ) + 2 ) e. RR )
378	376, 4, 377	sylancl 417	. . 3 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> ( ( N / 3 ) + 2 ) e. RR )
379		zq 10036	. . . . . . 7 |- ( 3 e. ZZ -> 3 e. QQ )
380	58, 379	ax-mp 5	. . . . . 6 |- 3 e. QQ
381		ppiqwordi 16229	. . . . . 6 |- ( ( N e. QQ /\ 3 e. QQ /\ N <_ 3 ) -> (π ` N ) <_ (π ` 3 ) )
382	380, 381	mp3an2 1366	. . . . 5 |- ( ( N e. QQ /\ N <_ 3 ) -> (π ` N ) <_ (π ` 3 ) )
383	382	adantlr 481	. . . 4 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> (π ` N ) <_ (π ` 3 ) )
384	383, 55	breqtrdi 4171	. . 3 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> (π ` N ) <_ 2 )
385	48	adantr 276	. . . . . 6 |- ( ( N e. QQ /\ 0 <_ N ) -> N e. RR )
386		simpr 110	. . . . . 6 |- ( ( N e. QQ /\ 0 <_ N ) -> 0 <_ N )
387		3re 9381	. . . . . . 7 |- 3 e. RR
388	387	a1i 9	. . . . . 6 |- ( ( N e. QQ /\ 0 <_ N ) -> 3 e. RR )
389		3pos 9401	. . . . . . 7 |- 0 < 3
390	389	a1i 9	. . . . . 6 |- ( ( N e. QQ /\ 0 <_ N ) -> 0 < 3 )
391		divge0 9206	. . . . . 6 |- ( ( ( N e. RR /\ 0 <_ N ) /\ ( 3 e. RR /\ 0 < 3 ) ) -> 0 <_ ( N / 3 ) )
392	385, 386, 388, 390, 391	syl22anc 1279	. . . . 5 |- ( ( N e. QQ /\ 0 <_ N ) -> 0 <_ ( N / 3 ) )
393	392	adantr 276	. . . 4 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> 0 <_ ( N / 3 ) )
394		addge02 8803	. . . . 5 |- ( ( 2 e. RR /\ ( N / 3 ) e. RR ) -> ( 0 <_ ( N / 3 ) <-> 2 <_ ( ( N / 3 ) + 2 ) ) )
395	4, 376, 394	sylancr 418	. . . 4 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> ( 0 <_ ( N / 3 ) <-> 2 <_ ( ( N / 3 ) + 2 ) ) )
396	393, 395	mpbid 147	. . 3 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> 2 <_ ( ( N / 3 ) + 2 ) )
397	374, 375, 378, 384, 396	letrd 8452	. 2 |- ( ( ( N e. QQ /\ 0 <_ N ) /\ N <_ 3 ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )
398		simpl 109	. . 3 |- ( ( N e. QQ /\ 0 <_ N ) -> N e. QQ )
399		qletric 10687	. . 3 |- ( ( 3 e. QQ /\ N e. QQ ) -> ( 3 <_ N \/ N <_ 3 ) )
400	380, 398, 399	sylancr 418	. 2 |- ( ( N e. QQ /\ 0 <_ N ) -> ( 3 <_ N \/ N <_ 3 ) )
401	373, 397, 400	mpjaodan 810	1 |- ( ( N e. QQ /\ 0 <_ N ) -> (π ` N ) <_ ( ( N / 3 ) + 2 ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   =/= wne 2420   A.wral 2528   {crab 2532   u. cun 3218   i^i cin 3219   C_ wss 3220   (/)c0 3520   {cpr 3710   class class class wbr 4130   ` cfv 5377  (class class class)co 6085   ~<_ cdom 7021   Fincfn 7022   CCcc 8178   RRcr 8179   0cc0 8180   1c1 8181   + caddc 8183   x. cmul 8185   < clt 8361   <_ cle 8362   - cmin 8499   -ucneg 8500   # cap 8912   / cdiv 9005   NNcn 9307   2c2 9358   3c3 9359   4c4 9360   5c5 9361   6c6 9362   NN0cn0 9568   ZZcz 9649   ZZ>=cuz 9931   QQcq 10029   ...cfz 10422   |_cfl 10714   mod cmo 10774  ♯chash 11230   || cdvds 12573   Primecprime 12904  πcppi 16195

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6807  df-en 7023  df-dom 7024  df-fin 7025  df-sup 7325  df-inf 7326  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-5 9369  df-6 9370  df-n0 9569  df-z 9650  df-uz 9932  df-q 10030  df-rp 10066  df-icc 10308  df-fz 10423  df-fl 10716  df-mod 10775  df-seqfrec 10900  df-exp 10991  df-ihash 11231  df-cj 11623  df-re 11624  df-im 11625  df-rsqrt 11780  df-abs 11781  df-dvds 12574  df-prm 12905  df-ppi 16198

This theorem is used by:  bposlem5  16276