MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem6 Structured version   Visualization version   GIF version

Theorem bposlem6 27029
Description: Lemma for bpos 27033. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)
Hypotheses
Ref Expression
bpos.1 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜5))
bpos.2 (πœ‘ β†’ Β¬ βˆƒπ‘ ∈ β„™ (𝑁 < 𝑝 ∧ 𝑝 ≀ (2 Β· 𝑁)))
bpos.3 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑(𝑛 pCnt ((2 Β· 𝑁)C𝑁))), 1))
bpos.4 𝐾 = (βŒŠβ€˜((2 Β· 𝑁) / 3))
bpos.5 𝑀 = (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁)))
Assertion
Ref Expression
bposlem6 (πœ‘ β†’ ((4↑𝑁) / 𝑁) < (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
Distinct variable groups:   𝐹,𝑝   𝑛,𝑝,𝐾   𝑀,𝑝   𝑛,𝑁,𝑝   πœ‘,𝑛,𝑝
Allowed substitution hints:   𝐹(𝑛)   𝑀(𝑛)

Proof of Theorem bposlem6
StepHypRef Expression
1 4nn 12300 . . . . 5 4 ∈ β„•
2 5nn 12303 . . . . . . 7 5 ∈ β„•
3 bpos.1 . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜5))
4 eluznn 12907 . . . . . . 7 ((5 ∈ β„• ∧ 𝑁 ∈ (β„€β‰₯β€˜5)) β†’ 𝑁 ∈ β„•)
52, 3, 4sylancr 586 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
65nnnn0d 12537 . . . . 5 (πœ‘ β†’ 𝑁 ∈ β„•0)
7 nnexpcl 14045 . . . . 5 ((4 ∈ β„• ∧ 𝑁 ∈ β„•0) β†’ (4↑𝑁) ∈ β„•)
81, 6, 7sylancr 586 . . . 4 (πœ‘ β†’ (4↑𝑁) ∈ β„•)
98nnred 12232 . . 3 (πœ‘ β†’ (4↑𝑁) ∈ ℝ)
109, 5nndivred 12271 . 2 (πœ‘ β†’ ((4↑𝑁) / 𝑁) ∈ ℝ)
11 fzctr 13618 . . . . 5 (𝑁 ∈ β„•0 β†’ 𝑁 ∈ (0...(2 Β· 𝑁)))
126, 11syl 17 . . . 4 (πœ‘ β†’ 𝑁 ∈ (0...(2 Β· 𝑁)))
13 bccl2 14288 . . . 4 (𝑁 ∈ (0...(2 Β· 𝑁)) β†’ ((2 Β· 𝑁)C𝑁) ∈ β„•)
1412, 13syl 17 . . 3 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) ∈ β„•)
1514nnred 12232 . 2 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) ∈ ℝ)
16 2nn 12290 . . . . . . 7 2 ∈ β„•
17 nnmulcl 12241 . . . . . . 7 ((2 ∈ β„• ∧ 𝑁 ∈ β„•) β†’ (2 Β· 𝑁) ∈ β„•)
1816, 5, 17sylancr 586 . . . . . 6 (πœ‘ β†’ (2 Β· 𝑁) ∈ β„•)
1918nnrpd 13019 . . . . 5 (πœ‘ β†’ (2 Β· 𝑁) ∈ ℝ+)
2018nnred 12232 . . . . . . . 8 (πœ‘ β†’ (2 Β· 𝑁) ∈ ℝ)
2119rpge0d 13025 . . . . . . . 8 (πœ‘ β†’ 0 ≀ (2 Β· 𝑁))
2220, 21resqrtcld 15369 . . . . . . 7 (πœ‘ β†’ (βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ)
23 3nn 12296 . . . . . . 7 3 ∈ β„•
24 nndivre 12258 . . . . . . 7 (((βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ ∧ 3 ∈ β„•) β†’ ((βˆšβ€˜(2 Β· 𝑁)) / 3) ∈ ℝ)
2522, 23, 24sylancl 585 . . . . . 6 (πœ‘ β†’ ((βˆšβ€˜(2 Β· 𝑁)) / 3) ∈ ℝ)
26 2re 12291 . . . . . 6 2 ∈ ℝ
27 readdcl 11196 . . . . . 6 ((((βˆšβ€˜(2 Β· 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) β†’ (((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2) ∈ ℝ)
2825, 26, 27sylancl 585 . . . . 5 (πœ‘ β†’ (((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2) ∈ ℝ)
2919, 28rpcxpcld 26478 . . . 4 (πœ‘ β†’ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) ∈ ℝ+)
3029rpred 13021 . . 3 (πœ‘ β†’ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) ∈ ℝ)
31 2rp 12984 . . . . 5 2 ∈ ℝ+
32 nnmulcl 12241 . . . . . . . . 9 ((4 ∈ β„• ∧ 𝑁 ∈ β„•) β†’ (4 Β· 𝑁) ∈ β„•)
331, 5, 32sylancr 586 . . . . . . . 8 (πœ‘ β†’ (4 Β· 𝑁) ∈ β„•)
3433nnred 12232 . . . . . . 7 (πœ‘ β†’ (4 Β· 𝑁) ∈ ℝ)
35 nndivre 12258 . . . . . . 7 (((4 Β· 𝑁) ∈ ℝ ∧ 3 ∈ β„•) β†’ ((4 Β· 𝑁) / 3) ∈ ℝ)
3634, 23, 35sylancl 585 . . . . . 6 (πœ‘ β†’ ((4 Β· 𝑁) / 3) ∈ ℝ)
37 5re 12304 . . . . . 6 5 ∈ ℝ
38 resubcl 11529 . . . . . 6 ((((4 Β· 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) β†’ (((4 Β· 𝑁) / 3) βˆ’ 5) ∈ ℝ)
3936, 37, 38sylancl 585 . . . . 5 (πœ‘ β†’ (((4 Β· 𝑁) / 3) βˆ’ 5) ∈ ℝ)
40 rpcxpcl 26421 . . . . 5 ((2 ∈ ℝ+ ∧ (((4 Β· 𝑁) / 3) βˆ’ 5) ∈ ℝ) β†’ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ∈ ℝ+)
4131, 39, 40sylancr 586 . . . 4 (πœ‘ β†’ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ∈ ℝ+)
4241rpred 13021 . . 3 (πœ‘ β†’ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ∈ ℝ)
4330, 42remulcld 11249 . 2 (πœ‘ β†’ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))) ∈ ℝ)
44 df-5 12283 . . . . 5 5 = (4 + 1)
45 4z 12601 . . . . . 6 4 ∈ β„€
46 uzid 12842 . . . . . 6 (4 ∈ β„€ β†’ 4 ∈ (β„€β‰₯β€˜4))
47 peano2uz 12890 . . . . . 6 (4 ∈ (β„€β‰₯β€˜4) β†’ (4 + 1) ∈ (β„€β‰₯β€˜4))
4845, 46, 47mp2b 10 . . . . 5 (4 + 1) ∈ (β„€β‰₯β€˜4)
4944, 48eqeltri 2828 . . . 4 5 ∈ (β„€β‰₯β€˜4)
50 eqid 2731 . . . . 5 (β„€β‰₯β€˜4) = (β„€β‰₯β€˜4)
5150uztrn2 12846 . . . 4 ((5 ∈ (β„€β‰₯β€˜4) ∧ 𝑁 ∈ (β„€β‰₯β€˜5)) β†’ 𝑁 ∈ (β„€β‰₯β€˜4))
5249, 3, 51sylancr 586 . . 3 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜4))
53 bclbnd 27020 . . 3 (𝑁 ∈ (β„€β‰₯β€˜4) β†’ ((4↑𝑁) / 𝑁) < ((2 Β· 𝑁)C𝑁))
5452, 53syl 17 . 2 (πœ‘ β†’ ((4↑𝑁) / 𝑁) < ((2 Β· 𝑁)C𝑁))
55 bpos.3 . . . . . . . 8 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑(𝑛 pCnt ((2 Β· 𝑁)C𝑁))), 1))
56 id 22 . . . . . . . . . 10 (𝑛 ∈ β„™ β†’ 𝑛 ∈ β„™)
57 pccl 16787 . . . . . . . . . 10 ((𝑛 ∈ β„™ ∧ ((2 Β· 𝑁)C𝑁) ∈ β„•) β†’ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
5856, 14, 57syl2anr 596 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„™) β†’ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
5958ralrimiva 3145 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘› ∈ β„™ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
6055, 59pcmptcl 16829 . . . . . . 7 (πœ‘ β†’ (𝐹:β„•βŸΆβ„• ∧ seq1( Β· , 𝐹):β„•βŸΆβ„•))
6160simprd 495 . . . . . 6 (πœ‘ β†’ seq1( Β· , 𝐹):β„•βŸΆβ„•)
62 bpos.2 . . . . . . . . 9 (πœ‘ β†’ Β¬ βˆƒπ‘ ∈ β„™ (𝑁 < 𝑝 ∧ 𝑝 ≀ (2 Β· 𝑁)))
63 bpos.4 . . . . . . . . 9 𝐾 = (βŒŠβ€˜((2 Β· 𝑁) / 3))
64 bpos.5 . . . . . . . . 9 𝑀 = (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁)))
653, 62, 55, 63, 64bposlem4 27027 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ (3...𝐾))
66 elfzuz 13502 . . . . . . . 8 (𝑀 ∈ (3...𝐾) β†’ 𝑀 ∈ (β„€β‰₯β€˜3))
6765, 66syl 17 . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜3))
68 eluznn 12907 . . . . . . 7 ((3 ∈ β„• ∧ 𝑀 ∈ (β„€β‰₯β€˜3)) β†’ 𝑀 ∈ β„•)
6923, 67, 68sylancr 586 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•)
7061, 69ffvelcdmd 7087 . . . . 5 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ β„•)
7170nnred 12232 . . . 4 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ)
72 2z 12599 . . . . . . . . 9 2 ∈ β„€
73 nndivre 12258 . . . . . . . . . . . 12 (((2 Β· 𝑁) ∈ ℝ ∧ 3 ∈ β„•) β†’ ((2 Β· 𝑁) / 3) ∈ ℝ)
7420, 23, 73sylancl 585 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· 𝑁) / 3) ∈ ℝ)
7574flcld 13768 . . . . . . . . . 10 (πœ‘ β†’ (βŒŠβ€˜((2 Β· 𝑁) / 3)) ∈ β„€)
7663, 75eqeltrid 2836 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ β„€)
77 zmulcl 12616 . . . . . . . . 9 ((2 ∈ β„€ ∧ 𝐾 ∈ β„€) β†’ (2 Β· 𝐾) ∈ β„€)
7872, 76, 77sylancr 586 . . . . . . . 8 (πœ‘ β†’ (2 Β· 𝐾) ∈ β„€)
792nnzi 12591 . . . . . . . 8 5 ∈ β„€
80 zsubcl 12609 . . . . . . . 8 (((2 Β· 𝐾) ∈ β„€ ∧ 5 ∈ β„€) β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ β„€)
8178, 79, 80sylancl 585 . . . . . . 7 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ β„€)
8281zred 12671 . . . . . 6 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ ℝ)
83 rpcxpcl 26421 . . . . . 6 ((2 ∈ ℝ+ ∧ ((2 Β· 𝐾) βˆ’ 5) ∈ ℝ) β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ+)
8431, 82, 83sylancr 586 . . . . 5 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ+)
8584rpred 13021 . . . 4 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ)
8671, 85remulcld 11249 . . 3 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ∈ ℝ)
873, 62, 55, 63bposlem3 27026 . . . 4 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) = ((2 Β· 𝑁)C𝑁))
88 elfzuz3 13503 . . . . . . . . . 10 (𝑀 ∈ (3...𝐾) β†’ 𝐾 ∈ (β„€β‰₯β€˜π‘€))
8965, 88syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ (β„€β‰₯β€˜π‘€))
9055, 59, 69, 89pcmptdvds 16832 . . . . . . . 8 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) βˆ₯ (seq1( Β· , 𝐹)β€˜πΎ))
9170nnzd 12590 . . . . . . . . 9 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ β„€)
9270nnne0d 12267 . . . . . . . . 9 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) β‰  0)
93 uztrn 12845 . . . . . . . . . . . . 13 ((𝐾 ∈ (β„€β‰₯β€˜π‘€) ∧ 𝑀 ∈ (β„€β‰₯β€˜3)) β†’ 𝐾 ∈ (β„€β‰₯β€˜3))
9489, 67, 93syl2anc 583 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐾 ∈ (β„€β‰₯β€˜3))
95 eluznn 12907 . . . . . . . . . . . 12 ((3 ∈ β„• ∧ 𝐾 ∈ (β„€β‰₯β€˜3)) β†’ 𝐾 ∈ β„•)
9623, 94, 95sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ β„•)
9761, 96ffvelcdmd 7087 . . . . . . . . . 10 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) ∈ β„•)
9897nnzd 12590 . . . . . . . . 9 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) ∈ β„€)
99 dvdsval2 16205 . . . . . . . . 9 (((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘€) β‰  0 ∧ (seq1( Β· , 𝐹)β€˜πΎ) ∈ β„€) β†’ ((seq1( Β· , 𝐹)β€˜π‘€) βˆ₯ (seq1( Β· , 𝐹)β€˜πΎ) ↔ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€))
10091, 92, 98, 99syl3anc 1370 . . . . . . . 8 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) βˆ₯ (seq1( Β· , 𝐹)β€˜πΎ) ↔ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€))
10190, 100mpbid 231 . . . . . . 7 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€)
102101zred 12671 . . . . . 6 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ ℝ)
10369nnred 12232 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ∈ ℝ)
10476zred 12671 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ ℝ)
105 eluzle 12840 . . . . . . . . . 10 (𝐾 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝐾)
10689, 105syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ≀ 𝐾)
107 efchtdvds 26900 . . . . . . . . 9 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀 ≀ 𝐾) β†’ (expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)))
108103, 104, 106, 107syl3anc 1370 . . . . . . . 8 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)))
109 efchtcl 26852 . . . . . . . . . . 11 (𝑀 ∈ ℝ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ β„•)
110103, 109syl 17 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ β„•)
111110nnzd 12590 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ β„€)
112110nnne0d 12267 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) β‰  0)
113 efchtcl 26852 . . . . . . . . . . 11 (𝐾 ∈ ℝ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„•)
114104, 113syl 17 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„•)
115114nnzd 12590 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„€)
116 dvdsval2 16205 . . . . . . . . 9 (((expβ€˜(ΞΈβ€˜π‘€)) ∈ β„€ ∧ (expβ€˜(ΞΈβ€˜π‘€)) β‰  0 ∧ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„€) β†’ ((expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€))
117111, 112, 115, 116syl3anc 1370 . . . . . . . 8 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€))
118108, 117mpbid 231 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€)
119118zred 12671 . . . . . 6 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ ℝ)
120 prmz 16617 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„€)
121 fllt 13776 . . . . . . . . . . . . . . . . . 18 (((βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ ∧ 𝑝 ∈ β„€) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁))) < 𝑝))
12222, 120, 121syl2an 595 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁))) < 𝑝))
12364breq1i 5155 . . . . . . . . . . . . . . . . 17 (𝑀 < 𝑝 ↔ (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁))) < 𝑝)
124122, 123bitr4di 289 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ 𝑀 < 𝑝))
125120zred 12671 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ β„™ β†’ 𝑝 ∈ ℝ)
126 ltnle 11298 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) β†’ (𝑀 < 𝑝 ↔ Β¬ 𝑝 ≀ 𝑀))
127103, 125, 126syl2an 595 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑀 < 𝑝 ↔ Β¬ 𝑝 ≀ 𝑀))
128124, 127bitrd 279 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ Β¬ 𝑝 ≀ 𝑀))
129 bposlem1 27024 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ β„• ∧ 𝑝 ∈ β„™) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁))
1305, 129sylan 579 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁))
131125adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝑝 ∈ ℝ)
132 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„™)
133 pccl 16787 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ β„™ ∧ ((2 Β· 𝑁)C𝑁) ∈ β„•) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
134132, 14, 133syl2anr 596 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
135131, 134reexpcld 14133 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ∈ ℝ)
13620adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (2 Β· 𝑁) ∈ ℝ)
137131resqcld 14095 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝↑2) ∈ ℝ)
138 lelttr 11309 . . . . . . . . . . . . . . . . . . . 20 (((𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ∈ ℝ ∧ (2 Β· 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) β†’ (((𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁) ∧ (2 Β· 𝑁) < (𝑝↑2)) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
139135, 136, 137, 138syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁) ∧ (2 Β· 𝑁) < (𝑝↑2)) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
140130, 139mpand 692 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((2 Β· 𝑁) < (𝑝↑2) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
141 resqrtth 15207 . . . . . . . . . . . . . . . . . . . . 21 (((2 Β· 𝑁) ∈ ℝ ∧ 0 ≀ (2 Β· 𝑁)) β†’ ((βˆšβ€˜(2 Β· 𝑁))↑2) = (2 Β· 𝑁))
14220, 21, 141syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((βˆšβ€˜(2 Β· 𝑁))↑2) = (2 Β· 𝑁))
143142breq1d 5158 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) ↔ (2 Β· 𝑁) < (𝑝↑2)))
144143adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) ↔ (2 Β· 𝑁) < (𝑝↑2)))
145134nn0zd 12589 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„€)
14672a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 2 ∈ β„€)
147 prmgt1 16639 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ β„™ β†’ 1 < 𝑝)
148147adantl 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 1 < 𝑝)
149131, 145, 146, 148ltexp2d 14219 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
150140, 144, 1493imtr4d 294 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < 2))
151 df-2 12280 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
152151breq2i 5156 . . . . . . . . . . . . . . . . 17 ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1))
153150, 152imbitrdi 250 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1)))
15422adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ)
15520, 21sqrtge0d 15372 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 0 ≀ (βˆšβ€˜(2 Β· 𝑁)))
156155adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 0 ≀ (βˆšβ€˜(2 Β· 𝑁)))
157 prmnn 16616 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„•)
158157nnrpd 13019 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ β„™ β†’ 𝑝 ∈ ℝ+)
159158rpge0d 13025 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ β„™ β†’ 0 ≀ 𝑝)
160159adantl 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 0 ≀ 𝑝)
161154, 131, 156, 160lt2sqd 14224 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ ((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2)))
162 1z 12597 . . . . . . . . . . . . . . . . 17 1 ∈ β„€
163 zleltp1 12618 . . . . . . . . . . . . . . . . 17 (((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„€ ∧ 1 ∈ β„€) β†’ ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1 ↔ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1)))
164145, 162, 163sylancl 585 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1 ↔ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1)))
165153, 161, 1643imtr4d 294 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1))
166128, 165sylbird 260 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (Β¬ 𝑝 ≀ 𝑀 β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1))
167166imp 406 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ Β¬ 𝑝 ≀ 𝑀) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1)
168167adantrl 713 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1)
169 iftrue 4534 . . . . . . . . . . . . 13 ((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 Β· 𝑁)C𝑁)))
170169adantl 481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 Β· 𝑁)C𝑁)))
171 iftrue 4534 . . . . . . . . . . . . 13 ((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) = 1)
172171adantl 481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) = 1)
173168, 170, 1723brtr4d 5180 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
174 0le0 12318 . . . . . . . . . . . . 13 0 ≀ 0
175 iffalse 4537 . . . . . . . . . . . . . 14 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) = 0)
176 iffalse 4537 . . . . . . . . . . . . . 14 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) = 0)
177175, 176breq12d 5161 . . . . . . . . . . . . 13 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ (if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) ↔ 0 ≀ 0))
178174, 177mpbiri 258 . . . . . . . . . . . 12 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
179178adantl 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
180173, 179pm2.61dan 810 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
18159adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ βˆ€π‘› ∈ β„™ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
18269adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝑀 ∈ β„•)
183 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝑝 ∈ β„™)
184 oveq1 7419 . . . . . . . . . . 11 (𝑛 = 𝑝 β†’ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) = (𝑝 pCnt ((2 Β· 𝑁)C𝑁)))
18589adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝐾 ∈ (β„€β‰₯β€˜π‘€))
18655, 181, 182, 183, 184, 185pcmpt2 16831 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) = if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0))
187 eqid 2731 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1))
188187prmorcht 26919 . . . . . . . . . . . . . . 15 (𝐾 ∈ β„• β†’ (expβ€˜(ΞΈβ€˜πΎ)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ))
18996, 188syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ))
190187prmorcht 26919 . . . . . . . . . . . . . . 15 (𝑀 ∈ β„• β†’ (expβ€˜(ΞΈβ€˜π‘€)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))
19169, 190syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))
192189, 191oveq12d 7430 . . . . . . . . . . . . 13 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) = ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€)))
193192adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) = ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€)))
194193oveq2d 7428 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))) = (𝑝 pCnt ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))))
195 nncn 12225 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚)
196195exp1d 14111 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (𝑛↑1) = 𝑛)
197196ifeq1d 4547 . . . . . . . . . . . . . 14 (𝑛 ∈ β„• β†’ if(𝑛 ∈ β„™, (𝑛↑1), 1) = if(𝑛 ∈ β„™, 𝑛, 1))
198197mpteq2ia 5251 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑1), 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1))
199198eqcomi 2740 . . . . . . . . . . . 12 (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑1), 1))
200 1nn0 12493 . . . . . . . . . . . . . . 15 1 ∈ β„•0
201200a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„™) β†’ 1 ∈ β„•0)
202201ralrimiva 3145 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 1 ∈ β„•0)
203202adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 1 ∈ β„•0)
204 eqidd 2732 . . . . . . . . . . . 12 (𝑛 = 𝑝 β†’ 1 = 1)
205199, 203, 182, 183, 204, 185pcmpt2 16831 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))) = if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
206194, 205eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))) = if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
207180, 186, 2063brtr4d 5180 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
208207ralrimiva 3145 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
209 pc2dvds 16817 . . . . . . . . 9 ((((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€ ∧ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€) β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ↔ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))))
210101, 118, 209syl2anc 583 . . . . . . . 8 (πœ‘ β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ↔ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))))
211208, 210mpbird 257 . . . . . . 7 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))
212114nnred 12232 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ)
213110nnred 12232 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ ℝ)
214114nngt0d 12266 . . . . . . . . . 10 (πœ‘ β†’ 0 < (expβ€˜(ΞΈβ€˜πΎ)))
215110nngt0d 12266 . . . . . . . . . 10 (πœ‘ β†’ 0 < (expβ€˜(ΞΈβ€˜π‘€)))
216212, 213, 214, 215divgt0d 12154 . . . . . . . . 9 (πœ‘ β†’ 0 < ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))
217 elnnz 12573 . . . . . . . . 9 (((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„• ↔ (((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€ ∧ 0 < ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
218118, 216, 217sylanbrc 582 . . . . . . . 8 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„•)
219 dvdsle 16258 . . . . . . . 8 ((((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€ ∧ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„•) β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ≀ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
220101, 218, 219syl2anc 583 . . . . . . 7 (πœ‘ β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ≀ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
221211, 220mpd 15 . . . . . 6 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ≀ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))
222 nndivre 12258 . . . . . . . 8 (((expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ ∧ 4 ∈ β„•) β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / 4) ∈ ℝ)
223212, 1, 222sylancl 585 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / 4) ∈ ℝ)
224 4re 12301 . . . . . . . . . 10 4 ∈ ℝ
225224a1i 11 . . . . . . . . 9 (πœ‘ β†’ 4 ∈ ℝ)
226 6re 12307 . . . . . . . . . 10 6 ∈ ℝ
227226a1i 11 . . . . . . . . 9 (πœ‘ β†’ 6 ∈ ℝ)
228 4lt6 12399 . . . . . . . . . 10 4 < 6
229228a1i 11 . . . . . . . . 9 (πœ‘ β†’ 4 < 6)
230 cht3 26914 . . . . . . . . . . . 12 (ΞΈβ€˜3) = (logβ€˜6)
231230fveq2i 6894 . . . . . . . . . . 11 (expβ€˜(ΞΈβ€˜3)) = (expβ€˜(logβ€˜6))
232 6pos 12327 . . . . . . . . . . . . 13 0 < 6
233226, 232elrpii 12982 . . . . . . . . . . . 12 6 ∈ ℝ+
234 reeflog 26326 . . . . . . . . . . . 12 (6 ∈ ℝ+ β†’ (expβ€˜(logβ€˜6)) = 6)
235233, 234ax-mp 5 . . . . . . . . . . 11 (expβ€˜(logβ€˜6)) = 6
236231, 235eqtri 2759 . . . . . . . . . 10 (expβ€˜(ΞΈβ€˜3)) = 6
237 3re 12297 . . . . . . . . . . . . 13 3 ∈ ℝ
238237a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 3 ∈ ℝ)
239 eluzle 12840 . . . . . . . . . . . . 13 (𝑀 ∈ (β„€β‰₯β€˜3) β†’ 3 ≀ 𝑀)
24067, 239syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 3 ≀ 𝑀)
241 chtwordi 26897 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 3 ≀ 𝑀) β†’ (ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€))
242238, 103, 240, 241syl3anc 1370 . . . . . . . . . . 11 (πœ‘ β†’ (ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€))
243 chtcl 26850 . . . . . . . . . . . . 13 (3 ∈ ℝ β†’ (ΞΈβ€˜3) ∈ ℝ)
244237, 243ax-mp 5 . . . . . . . . . . . 12 (ΞΈβ€˜3) ∈ ℝ
245 chtcl 26850 . . . . . . . . . . . . 13 (𝑀 ∈ ℝ β†’ (ΞΈβ€˜π‘€) ∈ ℝ)
246103, 245syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (ΞΈβ€˜π‘€) ∈ ℝ)
247 efle 16066 . . . . . . . . . . . 12 (((ΞΈβ€˜3) ∈ ℝ ∧ (ΞΈβ€˜π‘€) ∈ ℝ) β†’ ((ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€) ↔ (expβ€˜(ΞΈβ€˜3)) ≀ (expβ€˜(ΞΈβ€˜π‘€))))
248244, 246, 247sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ ((ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€) ↔ (expβ€˜(ΞΈβ€˜3)) ≀ (expβ€˜(ΞΈβ€˜π‘€))))
249242, 248mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜3)) ≀ (expβ€˜(ΞΈβ€˜π‘€)))
250236, 249eqbrtrrid 5184 . . . . . . . . 9 (πœ‘ β†’ 6 ≀ (expβ€˜(ΞΈβ€˜π‘€)))
251225, 227, 213, 229, 250ltletrd 11379 . . . . . . . 8 (πœ‘ β†’ 4 < (expβ€˜(ΞΈβ€˜π‘€)))
252 4pos 12324 . . . . . . . . . 10 0 < 4
253252a1i 11 . . . . . . . . 9 (πœ‘ β†’ 0 < 4)
254 ltdiv2 12105 . . . . . . . . 9 (((4 ∈ ℝ ∧ 0 < 4) ∧ ((expβ€˜(ΞΈβ€˜π‘€)) ∈ ℝ ∧ 0 < (expβ€˜(ΞΈβ€˜π‘€))) ∧ ((expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ ∧ 0 < (expβ€˜(ΞΈβ€˜πΎ)))) β†’ (4 < (expβ€˜(ΞΈβ€˜π‘€)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < ((expβ€˜(ΞΈβ€˜πΎ)) / 4)))
255225, 253, 213, 215, 212, 214, 254syl222anc 1385 . . . . . . . 8 (πœ‘ β†’ (4 < (expβ€˜(ΞΈβ€˜π‘€)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < ((expβ€˜(ΞΈβ€˜πΎ)) / 4)))
256251, 255mpbid 231 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < ((expβ€˜(ΞΈβ€˜πΎ)) / 4))
25726a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 2 ∈ ℝ)
258 2lt3 12389 . . . . . . . . . . . . . 14 2 < 3
259258a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 2 < 3)
260238, 103, 104, 240, 106letrd 11376 . . . . . . . . . . . . 13 (πœ‘ β†’ 3 ≀ 𝐾)
261257, 238, 104, 259, 260ltletrd 11379 . . . . . . . . . . . 12 (πœ‘ β†’ 2 < 𝐾)
262 chtub 26952 . . . . . . . . . . . 12 ((𝐾 ∈ ℝ ∧ 2 < 𝐾) β†’ (ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
263104, 261, 262syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ (ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
264 chtcl 26850 . . . . . . . . . . . . 13 (𝐾 ∈ ℝ β†’ (ΞΈβ€˜πΎ) ∈ ℝ)
265104, 264syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (ΞΈβ€˜πΎ) ∈ ℝ)
266 relogcl 26321 . . . . . . . . . . . . . 14 (2 ∈ ℝ+ β†’ (logβ€˜2) ∈ ℝ)
26731, 266ax-mp 5 . . . . . . . . . . . . 13 (logβ€˜2) ∈ ℝ
268 3z 12600 . . . . . . . . . . . . . . 15 3 ∈ β„€
269 zsubcl 12609 . . . . . . . . . . . . . . 15 (((2 Β· 𝐾) ∈ β„€ ∧ 3 ∈ β„€) β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€)
27078, 268, 269sylancl 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€)
271270zred 12671 . . . . . . . . . . . . 13 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ ℝ)
272 remulcl 11198 . . . . . . . . . . . . 13 (((logβ€˜2) ∈ ℝ ∧ ((2 Β· 𝐾) βˆ’ 3) ∈ ℝ) β†’ ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ∈ ℝ)
273267, 271, 272sylancr 586 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ∈ ℝ)
274 eflt 16065 . . . . . . . . . . . 12 (((ΞΈβ€˜πΎ) ∈ ℝ ∧ ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ∈ ℝ) β†’ ((ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))))
275265, 273, 274syl2anc 583 . . . . . . . . . . 11 (πœ‘ β†’ ((ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))))
276263, 275mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) < (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3))))
277 reexplog 26340 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€) β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = (expβ€˜(((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2))))
27831, 270, 277sylancr 586 . . . . . . . . . . 11 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = (expβ€˜(((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2))))
279270zcnd 12672 . . . . . . . . . . . . 13 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ β„‚)
280267recni 11233 . . . . . . . . . . . . 13 (logβ€˜2) ∈ β„‚
281 mulcom 11199 . . . . . . . . . . . . 13 ((((2 Β· 𝐾) βˆ’ 3) ∈ β„‚ ∧ (logβ€˜2) ∈ β„‚) β†’ (((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2)) = ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
282279, 280, 281sylancl 585 . . . . . . . . . . . 12 (πœ‘ β†’ (((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2)) = ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
283282fveq2d 6895 . . . . . . . . . . 11 (πœ‘ β†’ (expβ€˜(((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2))) = (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3))))
284278, 283eqtrd 2771 . . . . . . . . . 10 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3))))
285276, 284breqtrrd 5176 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) < (2↑((2 Β· 𝐾) βˆ’ 3)))
286 3p2e5 12368 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
287286oveq1i 7422 . . . . . . . . . . . . . . 15 ((3 + 2) βˆ’ 2) = (5 βˆ’ 2)
288 3cn 12298 . . . . . . . . . . . . . . . 16 3 ∈ β„‚
289 2cn 12292 . . . . . . . . . . . . . . . 16 2 ∈ β„‚
290288, 289pncan3oi 11481 . . . . . . . . . . . . . . 15 ((3 + 2) βˆ’ 2) = 3
291287, 290eqtr3i 2761 . . . . . . . . . . . . . 14 (5 βˆ’ 2) = 3
292291oveq2i 7423 . . . . . . . . . . . . 13 ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = ((2 Β· 𝐾) βˆ’ 3)
29378zcnd 12672 . . . . . . . . . . . . . 14 (πœ‘ β†’ (2 Β· 𝐾) ∈ β„‚)
294 5cn 12305 . . . . . . . . . . . . . . 15 5 ∈ β„‚
295 subsub 11495 . . . . . . . . . . . . . . 15 (((2 Β· 𝐾) ∈ β„‚ ∧ 5 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = (((2 Β· 𝐾) βˆ’ 5) + 2))
296294, 289, 295mp3an23 1452 . . . . . . . . . . . . . 14 ((2 Β· 𝐾) ∈ β„‚ β†’ ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = (((2 Β· 𝐾) βˆ’ 5) + 2))
297293, 296syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = (((2 Β· 𝐾) βˆ’ 5) + 2))
298292, 297eqtr3id 2785 . . . . . . . . . . . 12 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) = (((2 Β· 𝐾) βˆ’ 5) + 2))
299298oveq2d 7428 . . . . . . . . . . 11 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 3)) = (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)))
300 2ne0 12321 . . . . . . . . . . . 12 2 β‰  0
301 cxpexpz 26412 . . . . . . . . . . . 12 ((2 ∈ β„‚ ∧ 2 β‰  0 ∧ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€) β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 3)) = (2↑((2 Β· 𝐾) βˆ’ 3)))
302289, 300, 270, 301mp3an12i 1464 . . . . . . . . . . 11 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 3)) = (2↑((2 Β· 𝐾) βˆ’ 3)))
30381zcnd 12672 . . . . . . . . . . . 12 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ β„‚)
304 2cnne0 12427 . . . . . . . . . . . . 13 (2 ∈ β„‚ ∧ 2 β‰  0)
305 cxpadd 26424 . . . . . . . . . . . . 13 (((2 ∈ β„‚ ∧ 2 β‰  0) ∧ ((2 Β· 𝐾) βˆ’ 5) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
306304, 289, 305mp3an13 1451 . . . . . . . . . . . 12 (((2 Β· 𝐾) βˆ’ 5) ∈ β„‚ β†’ (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
307303, 306syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
308299, 302, 3073eqtr3d 2779 . . . . . . . . . 10 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
309 2nn0 12494 . . . . . . . . . . . . 13 2 ∈ β„•0
310 cxpexp 26413 . . . . . . . . . . . . 13 ((2 ∈ β„‚ ∧ 2 ∈ β„•0) β†’ (2↑𝑐2) = (2↑2))
311289, 309, 310mp2an 689 . . . . . . . . . . . 12 (2↑𝑐2) = (2↑2)
312 sq2 14166 . . . . . . . . . . . 12 (2↑2) = 4
313311, 312eqtri 2759 . . . . . . . . . . 11 (2↑𝑐2) = 4
314313oveq2i 7423 . . . . . . . . . 10 ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4)
315308, 314eqtrdi 2787 . . . . . . . . 9 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4))
316285, 315breqtrd 5174 . . . . . . . 8 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) < ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4))
317224, 252pm3.2i 470 . . . . . . . . . 10 (4 ∈ ℝ ∧ 0 < 4)
318317a1i 11 . . . . . . . . 9 (πœ‘ β†’ (4 ∈ ℝ ∧ 0 < 4))
319 ltdivmul2 12096 . . . . . . . . 9 (((expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ ∧ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) β†’ (((expβ€˜(ΞΈβ€˜πΎ)) / 4) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4)))
320212, 85, 318, 319syl3anc 1370 . . . . . . . 8 (πœ‘ β†’ (((expβ€˜(ΞΈβ€˜πΎ)) / 4) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4)))
321316, 320mpbird 257 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / 4) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))
322119, 223, 85, 256, 321lttrd 11380 . . . . . 6 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))
323102, 119, 85, 221, 322lelttrd 11377 . . . . 5 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))
32497nnred 12232 . . . . . 6 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) ∈ ℝ)
325 nnre 12224 . . . . . . . 8 ((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ)
326 nngt0 12248 . . . . . . . 8 ((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„• β†’ 0 < (seq1( Β· , 𝐹)β€˜π‘€))
327325, 326jca 511 . . . . . . 7 ((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ ∧ 0 < (seq1( Β· , 𝐹)β€˜π‘€)))
32870, 327syl 17 . . . . . 6 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ ∧ 0 < (seq1( Β· , 𝐹)β€˜π‘€)))
329 ltdivmul 12094 . . . . . 6 (((seq1( Β· , 𝐹)β€˜πΎ) ∈ ℝ ∧ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ ∧ ((seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ ∧ 0 < (seq1( Β· , 𝐹)β€˜π‘€))) β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (seq1( Β· , 𝐹)β€˜πΎ) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))))
330324, 85, 328, 329syl3anc 1370 . . . . 5 (πœ‘ β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (seq1( Β· , 𝐹)β€˜πΎ) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))))
331323, 330mpbid 231 . . . 4 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))))
33287, 331eqbrtrrd 5172 . . 3 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))))
33330, 85remulcld 11249 . . . 4 (πœ‘ β†’ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ∈ ℝ)
3343, 62, 55, 63, 64bposlem5 27028 . . . . 5 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ≀ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)))
33571, 30, 84lemul1d 13064 . . . . 5 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) ≀ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) ↔ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))))
336334, 335mpbid 231 . . . 4 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))))
33778zred 12671 . . . . . . 7 (πœ‘ β†’ (2 Β· 𝐾) ∈ ℝ)
33837a1i 11 . . . . . . 7 (πœ‘ β†’ 5 ∈ ℝ)
339 flle 13769 . . . . . . . . . . 11 (((2 Β· 𝑁) / 3) ∈ ℝ β†’ (βŒŠβ€˜((2 Β· 𝑁) / 3)) ≀ ((2 Β· 𝑁) / 3))
34074, 339syl 17 . . . . . . . . . 10 (πœ‘ β†’ (βŒŠβ€˜((2 Β· 𝑁) / 3)) ≀ ((2 Β· 𝑁) / 3))
34163, 340eqbrtrid 5183 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ≀ ((2 Β· 𝑁) / 3))
342 2pos 12320 . . . . . . . . . . . 12 0 < 2
34326, 342pm3.2i 470 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 < 2)
344343a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (2 ∈ ℝ ∧ 0 < 2))
345 lemul2 12072 . . . . . . . . . 10 ((𝐾 ∈ ℝ ∧ ((2 Β· 𝑁) / 3) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ (𝐾 ≀ ((2 Β· 𝑁) / 3) ↔ (2 Β· 𝐾) ≀ (2 Β· ((2 Β· 𝑁) / 3))))
346104, 74, 344, 345syl3anc 1370 . . . . . . . . 9 (πœ‘ β†’ (𝐾 ≀ ((2 Β· 𝑁) / 3) ↔ (2 Β· 𝐾) ≀ (2 Β· ((2 Β· 𝑁) / 3))))
347341, 346mpbid 231 . . . . . . . 8 (πœ‘ β†’ (2 Β· 𝐾) ≀ (2 Β· ((2 Β· 𝑁) / 3)))
34818nncnd 12233 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· 𝑁) ∈ β„‚)
349 3ne0 12323 . . . . . . . . . . . 12 3 β‰  0
350288, 349pm3.2i 470 . . . . . . . . . . 11 (3 ∈ β„‚ ∧ 3 β‰  0)
351 divass 11895 . . . . . . . . . . 11 ((2 ∈ β„‚ ∧ (2 Β· 𝑁) ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((2 Β· (2 Β· 𝑁)) / 3) = (2 Β· ((2 Β· 𝑁) / 3)))
352289, 350, 351mp3an13 1451 . . . . . . . . . 10 ((2 Β· 𝑁) ∈ β„‚ β†’ ((2 Β· (2 Β· 𝑁)) / 3) = (2 Β· ((2 Β· 𝑁) / 3)))
353348, 352syl 17 . . . . . . . . 9 (πœ‘ β†’ ((2 Β· (2 Β· 𝑁)) / 3) = (2 Β· ((2 Β· 𝑁) / 3)))
3545nncnd 12233 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„‚)
355 mulass 11201 . . . . . . . . . . . 12 ((2 ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 𝑁 ∈ β„‚) β†’ ((2 Β· 2) Β· 𝑁) = (2 Β· (2 Β· 𝑁)))
356289, 289, 354, 355mp3an12i 1464 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· 2) Β· 𝑁) = (2 Β· (2 Β· 𝑁)))
357 2t2e4 12381 . . . . . . . . . . . 12 (2 Β· 2) = 4
358357oveq1i 7422 . . . . . . . . . . 11 ((2 Β· 2) Β· 𝑁) = (4 Β· 𝑁)
359356, 358eqtr3di 2786 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· (2 Β· 𝑁)) = (4 Β· 𝑁))
360359oveq1d 7427 . . . . . . . . 9 (πœ‘ β†’ ((2 Β· (2 Β· 𝑁)) / 3) = ((4 Β· 𝑁) / 3))
361353, 360eqtr3d 2773 . . . . . . . 8 (πœ‘ β†’ (2 Β· ((2 Β· 𝑁) / 3)) = ((4 Β· 𝑁) / 3))
362347, 361breqtrd 5174 . . . . . . 7 (πœ‘ β†’ (2 Β· 𝐾) ≀ ((4 Β· 𝑁) / 3))
363337, 36, 338, 362lesub1dd 11835 . . . . . 6 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ≀ (((4 Β· 𝑁) / 3) βˆ’ 5))
364 1lt2 12388 . . . . . . . 8 1 < 2
365364a1i 11 . . . . . . 7 (πœ‘ β†’ 1 < 2)
366257, 365, 82, 39cxpled 26465 . . . . . 6 (πœ‘ β†’ (((2 Β· 𝐾) βˆ’ 5) ≀ (((4 Β· 𝑁) / 3) βˆ’ 5) ↔ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ≀ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
367363, 366mpbid 231 . . . . 5 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ≀ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)))
36885, 42, 29lemul2d 13065 . . . . 5 (πœ‘ β†’ ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ≀ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ↔ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)))))
369367, 368mpbid 231 . . . 4 (πœ‘ β†’ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
37086, 333, 43, 336, 369letrd 11376 . . 3 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
37115, 86, 43, 332, 370ltletrd 11379 . 2 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) < (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
37210, 15, 43, 54, 371lttrd 11380 1 (πœ‘ β†’ ((4↑𝑁) / 𝑁) < (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7412  β„‚cc 11111  β„cr 11112  0cc0 11113  1c1 11114   + caddc 11116   Β· cmul 11118   < clt 11253   ≀ cle 11254   βˆ’ cmin 11449   / cdiv 11876  β„•cn 12217  2c2 12272  3c3 12273  4c4 12274  5c5 12275  6c6 12276  β„•0cn0 12477  β„€cz 12563  β„€β‰₯cuz 12827  β„+crp 12979  ...cfz 13489  βŒŠcfl 13760  seqcseq 13971  β†‘cexp 14032  Ccbc 14267  βˆšcsqrt 15185  expce 16010   βˆ₯ cdvds 16202  β„™cprime 16613   pCnt cpc 16774  logclog 26300  β†‘𝑐ccxp 26301  ΞΈccht 26832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7728  ax-inf2 9639  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191  ax-addf 11192
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7673  df-om 7859  df-1st 7978  df-2nd 7979  df-supp 8150  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-2o 8470  df-oadd 8473  df-er 8706  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9365  df-fi 9409  df-sup 9440  df-inf 9441  df-oi 9508  df-dju 9899  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-xnn0 12550  df-z 12564  df-dec 12683  df-uz 12828  df-q 12938  df-rp 12980  df-xneg 13097  df-xadd 13098  df-xmul 13099  df-ioo 13333  df-ioc 13334  df-ico 13335  df-icc 13336  df-fz 13490  df-fzo 13633  df-fl 13762  df-mod 13840  df-seq 13972  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15019  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-limsup 15420  df-clim 15437  df-rlim 15438  df-sum 15638  df-ef 16016  df-sin 16018  df-cos 16019  df-pi 16021  df-dvds 16203  df-gcd 16441  df-prm 16614  df-pc 16775  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-submnd 18707  df-mulg 18988  df-cntz 19223  df-cmn 19692  df-psmet 21137  df-xmet 21138  df-met 21139  df-bl 21140  df-mopn 21141  df-fbas 21142  df-fg 21143  df-cnfld 21146  df-top 22617  df-topon 22634  df-topsp 22656  df-bases 22670  df-cld 22744  df-ntr 22745  df-cls 22746  df-nei 22823  df-lp 22861  df-perf 22862  df-cn 22952  df-cnp 22953  df-haus 23040  df-tx 23287  df-hmeo 23480  df-fil 23571  df-fm 23663  df-flim 23664  df-flf 23665  df-xms 24047  df-ms 24048  df-tms 24049  df-cncf 24619  df-limc 25616  df-dv 25617  df-log 26302  df-cxp 26303  df-cht 26838  df-ppi 26841
This theorem is referenced by:  bposlem9  27032
  Copyright terms: Public domain W3C validator