The inner piece table on [3, 20]

The interval and coefficient data originate in gen_lean_inner.py. Each piece proves its minimum and maximum comparisons once, then reuses them in the interval-count formulas. This avoids repeated case splits and arithmetic preprocessing of earlier count equations.

theorem Zeta5Irrational.inPiece_0 (x : ℝ) (h1 : 3 ≤ x) (h2 : x < 70 / 23) : Ein x 2 = 18 / 5 * x + -6

theorem Zeta5Irrational.inPiece_1 (x : ℝ) (h1 : 70 / 23 ≤ x) (h2 : x < 120 / 37) : Ein x 3 = 49 / 20 * x + -5 / 2

theorem Zeta5Irrational.inPiece_2 (x : ℝ) (h1 : 120 / 37 ≤ x) (h2 : x < 10 / 3) : Ein x 3 = 283 / 40 * x + -35 / 2

theorem Zeta5Irrational.inPiece_3 (x : ℝ) (h1 : 10 / 3 ≤ x) (h2 : x < 80 / 23) : Ein x 4 = 277 / 40 * x + -17

theorem Zeta5Irrational.inPiece_4 (x : ℝ) (h1 : 80 / 23 ≤ x) (h2 : x < 7 / 2) : Ein x 5 = 231 / 40 * x + -13

theorem Zeta5Irrational.inPiece_5 (x : ℝ) (h1 : 7 / 2 ≤ x) (h2 : x < 160 / 43) : Ein x 5 = 271 / 40 * x + -33 / 2

theorem Zeta5Irrational.inPiece_6 (x : ℝ) (h1 : 160 / 43 ≤ x) (h2 : x < 140 / 37) : Ein x 5 = 71 / 20 * x + -9 / 2

theorem Zeta5Irrational.inPiece_7 (x : ℝ) (h1 : 140 / 37 ≤ x) (h2 : x < 90 / 23) : Ein x 5 = 27 / 5 * x + -23 / 2

theorem Zeta5Irrational.inPiece_8 (x : ℝ) (h1 : 90 / 23 ≤ x) (h2 : x < 4) : Ein x 6 = 17 / 4 * x + -7

theorem Zeta5Irrational.inPiece_9 (x : ℝ) (h1 : 4 ≤ x) (h2 : x < 160 / 37) : Ein x 6 = 17 / 5 * x + -11

theorem Zeta5Irrational.inPiece_10 (x : ℝ) (h1 : 160 / 37 ≤ x) (h2 : x < 100 / 23) : Ein x 6 = 321 / 40 * x + -31

theorem Zeta5Irrational.inPiece_11 (x : ℝ) (h1 : 100 / 23 ≤ x) (h2 : x < 9 / 2) : Ein x 7 = 55 / 8 * x + -26

theorem Zeta5Irrational.inPiece_12 (x : ℝ) (h1 : 9 / 2 ≤ x) (h2 : x < 200 / 43) : Ein x 7 = 63 / 8 * x + -61 / 2

theorem Zeta5Irrational.inPiece_13 (x : ℝ) (h1 : 200 / 43 ≤ x) (h2 : x < 110 / 23) : Ein x 7 = 93 / 20 * x + -31 / 2

theorem Zeta5Irrational.inPiece_14 (x : ℝ) (h1 : 110 / 23 ≤ x) (h2 : x < 180 / 37) : Ein x 8 = 7 / 2 * x + -10

theorem Zeta5Irrational.inPiece_15 (x : ℝ) (h1 : 180 / 37 ≤ x) (h2 : x < 5) : Ein x 8 = 107 / 20 * x + -19

theorem Zeta5Irrational.inPiece_16 (x : ℝ) (h1 : 5 ≤ x) (h2 : x < 120 / 23) : Ein x 8 = 9 / 2 * x + -24

theorem Zeta5Irrational.inPiece_17 (x : ℝ) (h1 : 120 / 23 ≤ x) (h2 : x < 200 / 37) : Ein x 9 = 67 / 20 * x + -18

theorem Zeta5Irrational.inPiece_18 (x : ℝ) (h1 : 200 / 37 ≤ x) (h2 : x < 11 / 2) : Ein x 9 = 319 / 40 * x + -43

theorem Zeta5Irrational.inPiece_19 (x : ℝ) (h1 : 11 / 2 ≤ x) (h2 : x < 240 / 43) : Ein x 9 = 359 / 40 * x + -97 / 2

theorem Zeta5Irrational.inPiece_20 (x : ℝ) (h1 : 240 / 43 ≤ x) (h2 : x < 130 / 23) : Ein x 9 = 23 / 4 * x + -61 / 2

theorem Zeta5Irrational.inPiece_21 (x : ℝ) (h1 : 130 / 23 ≤ x) (h2 : x < 220 / 37) : Ein x 10 = 23 / 5 * x + -24

theorem Zeta5Irrational.inPiece_22 (x : ℝ) (h1 : 220 / 37 ≤ x) (h2 : x < 6) : Ein x 10 = 129 / 20 * x + -35

theorem Zeta5Irrational.inPiece_23 (x : ℝ) (h1 : 6 ≤ x) (h2 : x < 140 / 23) : Ein x 10 = 28 / 5 * x + -41

theorem Zeta5Irrational.inPiece_24 (x : ℝ) (h1 : 140 / 23 ≤ x) (h2 : x < 240 / 37) : Ein x 11 = 89 / 20 * x + -34

theorem Zeta5Irrational.inPiece_25 (x : ℝ) (h1 : 240 / 37 ≤ x) (h2 : x < 13 / 2) : Ein x 11 = 363 / 40 * x + -64

theorem Zeta5Irrational.inPiece_26 (x : ℝ) (h1 : 13 / 2 ≤ x) (h2 : x < 280 / 43) : Ein x 11 = 403 / 40 * x + -141 / 2

theorem Zeta5Irrational.inPiece_27 (x : ℝ) (h1 : 280 / 43 ≤ x) (h2 : x < 150 / 23) : Ein x 11 = 137 / 20 * x + -99 / 2

theorem Zeta5Irrational.inPiece_28 (x : ℝ) (h1 : 150 / 23 ≤ x) (h2 : x < 20 / 3) : Ein x 12 = 57 / 10 * x + -42

theorem Zeta5Irrational.inPiece_29 (x : ℝ) (h1 : 20 / 3 ≤ x) (h2 : x < 160 / 23) : Ein x 13 = 69 / 10 * x + -50

theorem Zeta5Irrational.inPiece_30 (x : ℝ) (h1 : 160 / 23 ≤ x) (h2 : x < 7) : Ein x 14 = 23 / 4 * x + -42

theorem Zeta5Irrational.inPiece_31 (x : ℝ) (h1 : 7 ≤ x) (h2 : x < 260 / 37) : Ein x 14 = 49 / 10 * x + -49

theorem Zeta5Irrational.inPiece_32 (x : ℝ) (h1 : 260 / 37 ≤ x) (h2 : x < 170 / 23) : Ein x 14 = 27 / 4 * x + -62

theorem Zeta5Irrational.inPiece_33 (x : ℝ) (h1 : 170 / 23 ≤ x) (h2 : x < 320 / 43) : Ein x 15 = 28 / 5 * x + -107 / 2

theorem Zeta5Irrational.inPiece_34 (x : ℝ) (h1 : 320 / 43 ≤ x) (h2 : x < 15 / 2) : Ein x 15 = 19 / 8 * x + -59 / 2

theorem Zeta5Irrational.inPiece_35 (x : ℝ) (h1 : 15 / 2 ≤ x) (h2 : x < 280 / 37) : Ein x 15 = 27 / 8 * x + -37

theorem Zeta5Irrational.inPiece_36 (x : ℝ) (h1 : 280 / 37 ≤ x) (h2 : x < 180 / 23) : Ein x 15 = 8 * x + -72

theorem Zeta5Irrational.inPiece_37 (x : ℝ) (h1 : 180 / 23 ≤ x) (h2 : x < 8) : Ein x 16 = 137 / 20 * x + -63

theorem Zeta5Irrational.inPiece_38 (x : ℝ) (h1 : 8 ≤ x) (h2 : x < 300 / 37) : Ein x 16 = 6 * x + -71

theorem Zeta5Irrational.inPiece_39 (x : ℝ) (h1 : 300 / 37 ≤ x) (h2 : x < 190 / 23) : Ein x 16 = 157 / 20 * x + -86

theorem Zeta5Irrational.inPiece_40 (x : ℝ) (h1 : 190 / 23 ≤ x) (h2 : x < 360 / 43) : Ein x 17 = 67 / 10 * x + -153 / 2

theorem Zeta5Irrational.inPiece_41 (x : ℝ) (h1 : 360 / 43 ≤ x) (h2 : x < 17 / 2) : Ein x 17 = 139 / 40 * x + -99 / 2

theorem Zeta5Irrational.inPiece_42 (x : ℝ) (h1 : 17 / 2 ≤ x) (h2 : x < 320 / 37) : Ein x 17 = 179 / 40 * x + -58

theorem Zeta5Irrational.inPiece_43 (x : ℝ) (h1 : 320 / 37 ≤ x) (h2 : x < 200 / 23) : Ein x 17 = 91 / 10 * x + -98

theorem Zeta5Irrational.inPiece_44 (x : ℝ) (h1 : 200 / 23 ≤ x) (h2 : x < 9) : Ein x 18 = 159 / 20 * x + -88

theorem Zeta5Irrational.inPiece_45 (x : ℝ) (h1 : 9 ≤ x) (h2 : x < 210 / 23) : Ein x 18 = 71 / 10 * x + -97

theorem Zeta5Irrational.inPiece_46 (x : ℝ) (h1 : 210 / 23 ≤ x) (h2 : x < 340 / 37) : Ein x 19 = 119 / 20 * x + -173 / 2

theorem Zeta5Irrational.inPiece_47 (x : ℝ) (h1 : 340 / 37 ≤ x) (h2 : x < 400 / 43) : Ein x 19 = 39 / 5 * x + -207 / 2

theorem Zeta5Irrational.inPiece_48 (x : ℝ) (h1 : 400 / 43 ≤ x) (h2 : x < 19 / 2) : Ein x 19 = 183 / 40 * x + -147 / 2

theorem Zeta5Irrational.inPiece_49 (x : ℝ) (h1 : 19 / 2 ≤ x) (h2 : x < 220 / 23) : Ein x 19 = 223 / 40 * x + -83

theorem Zeta5Irrational.inPiece_50 (x : ℝ) (h1 : 220 / 23 ≤ x) (h2 : x < 360 / 37) : Ein x 20 = 177 / 40 * x + -72

theorem Zeta5Irrational.inPiece_51 (x : ℝ) (h1 : 360 / 37 ≤ x) (h2 : x < 10) : Ein x 20 = 181 / 20 * x + -117

theorem Zeta5Irrational.inPiece_52 (x : ℝ) (h1 : 10 ≤ x) (h2 : x < 440 / 43) : Ein x 22 = 69 / 10 * x + -114

theorem Zeta5Irrational.inPiece_53 (x : ℝ) (h1 : 440 / 43 ≤ x) (h2 : x < 380 / 37) : Ein x 22 = 147 / 40 * x + -81

theorem Zeta5Irrational.inPiece_54 (x : ℝ) (h1 : 380 / 37 ≤ x) (h2 : x < 240 / 23) : Ein x 22 = 221 / 40 * x + -100

theorem Zeta5Irrational.inPiece_55 (x : ℝ) (h1 : 240 / 23 ≤ x) (h2 : x < 21 / 2) : Ein x 23 = 35 / 8 * x + -88

theorem Zeta5Irrational.inPiece_56 (x : ℝ) (h1 : 21 / 2 ≤ x) (h2 : x < 400 / 37) : Ein x 23 = 43 / 8 * x + -197 / 2

theorem Zeta5Irrational.inPiece_57 (x : ℝ) (h1 : 400 / 37 ≤ x) (h2 : x < 250 / 23) : Ein x 23 = 10 * x + -297 / 2

theorem Zeta5Irrational.inPiece_58 (x : ℝ) (h1 : 250 / 23 ≤ x) (h2 : x < 11) : Ein x 24 = 177 / 20 * x + -136

theorem Zeta5Irrational.inPiece_59 (x : ℝ) (h1 : 11 ≤ x) (h2 : x < 480 / 43) : Ein x 24 = 8 * x + -147

theorem Zeta5Irrational.inPiece_60 (x : ℝ) (h1 : 480 / 43 ≤ x) (h2 : x < 260 / 23) : Ein x 24 = 191 / 40 * x + -111

theorem Zeta5Irrational.inPiece_61 (x : ℝ) (h1 : 260 / 23 ≤ x) (h2 : x < 420 / 37) : Ein x 25 = 29 / 8 * x + -98

theorem Zeta5Irrational.inPiece_62 (x : ℝ) (h1 : 420 / 37 ≤ x) (h2 : x < 23 / 2) : Ein x 25 = 219 / 40 * x + -119

theorem Zeta5Irrational.inPiece_63 (x : ℝ) (h1 : 23 / 2 ≤ x) (h2 : x < 270 / 23) : Ein x 25 = 259 / 40 * x + -261 / 2

theorem Zeta5Irrational.inPiece_64 (x : ℝ) (h1 : 270 / 23 ≤ x) (h2 : x < 440 / 37) : Ein x 26 = 213 / 40 * x + -117

theorem Zeta5Irrational.inPiece_65 (x : ℝ) (h1 : 440 / 37 ≤ x) (h2 : x < 12) : Ein x 26 = 199 / 20 * x + -172

theorem Zeta5Irrational.inPiece_66 (x : ℝ) (h1 : 12 ≤ x) (h2 : x < 520 / 43) : Ein x 26 = 91 / 10 * x + -184

theorem Zeta5Irrational.inPiece_67 (x : ℝ) (h1 : 520 / 43 ≤ x) (h2 : x < 280 / 23) : Ein x 26 = 47 / 8 * x + -145

theorem Zeta5Irrational.inPiece_68 (x : ℝ) (h1 : 280 / 23 ≤ x) (h2 : x < 460 / 37) : Ein x 27 = 189 / 40 * x + -131

theorem Zeta5Irrational.inPiece_69 (x : ℝ) (h1 : 460 / 37 ≤ x) (h2 : x < 25 / 2) : Ein x 27 = 263 / 40 * x + -154

theorem Zeta5Irrational.inPiece_70 (x : ℝ) (h1 : 25 / 2 ≤ x) (h2 : x < 290 / 23) : Ein x 27 = 303 / 40 * x + -333 / 2

theorem Zeta5Irrational.inPiece_71 (x : ℝ) (h1 : 290 / 23 ≤ x) (h2 : x < 480 / 37) : Ein x 28 = 257 / 40 * x + -152

theorem Zeta5Irrational.inPiece_72 (x : ℝ) (h1 : 480 / 37 ≤ x) (h2 : x < 13) : Ein x 28 = 221 / 20 * x + -212

theorem Zeta5Irrational.inPiece_73 (x : ℝ) (h1 : 13 ≤ x) (h2 : x < 560 / 43) : Ein x 28 = 51 / 5 * x + -225

theorem Zeta5Irrational.inPiece_74 (x : ℝ) (h1 : 560 / 43 ≤ x) (h2 : x < 300 / 23) : Ein x 28 = 279 / 40 * x + -183

theorem Zeta5Irrational.inPiece_75 (x : ℝ) (h1 : 300 / 23 ≤ x) (h2 : x < 40 / 3) : Ein x 29 = 233 / 40 * x + -168

theorem Zeta5Irrational.inPiece_76 (x : ℝ) (h1 : 40 / 3 ≤ x) (h2 : x < 310 / 23) : Ein x 30 = 145 / 8 * x + -184

theorem Zeta5Irrational.inPiece_77 (x : ℝ) (h1 : 310 / 23 ≤ x) (h2 : x < 27 / 2) : Ein x 31 = 679 / 40 * x + -337 / 2

theorem Zeta5Irrational.inPiece_78 (x : ℝ) (h1 : 27 / 2 ≤ x) (h2 : x < 500 / 37) : Ein x 31 = 719 / 40 * x + -182

theorem Zeta5Irrational.inPiece_79 (x : ℝ) (h1 : 500 / 37 ≤ x) (h2 : x < 320 / 23) : Ein x 31 = 793 / 40 * x + -207

theorem Zeta5Irrational.inPiece_80 (x : ℝ) (h1 : 320 / 23 ≤ x) (h2 : x < 600 / 43) : Ein x 32 = 747 / 40 * x + -191

theorem Zeta5Irrational.inPiece_81 (x : ℝ) (h1 : 600 / 43 ≤ x) (h2 : x < 14) : Ein x 32 = 309 / 20 * x + -146

theorem Zeta5Irrational.inPiece_82 (x : ℝ) (h1 : 14 ≤ x) (h2 : x < 520 / 37) : Ein x 32 = 73 / 5 * x + -160

theorem Zeta5Irrational.inPiece_83 (x : ℝ) (h1 : 520 / 37 ≤ x) (h2 : x < 330 / 23) : Ein x 32 = 769 / 40 * x + -225

theorem Zeta5Irrational.inPiece_84 (x : ℝ) (h1 : 330 / 23 ≤ x) (h2 : x < 29 / 2) : Ein x 33 = 723 / 40 * x + -417 / 2

theorem Zeta5Irrational.inPiece_85 (x : ℝ) (h1 : 29 / 2 ≤ x) (h2 : x < 540 / 37) : Ein x 33 = 763 / 40 * x + -223

theorem Zeta5Irrational.inPiece_86 (x : ℝ) (h1 : 540 / 37 ≤ x) (h2 : x < 340 / 23) : Ein x 33 = 837 / 40 * x + -250

theorem Zeta5Irrational.inPiece_87 (x : ℝ) (h1 : 340 / 23 ≤ x) (h2 : x < 640 / 43) : Ein x 34 = 791 / 40 * x + -233

theorem Zeta5Irrational.inPiece_88 (x : ℝ) (h1 : 640 / 43 ≤ x) (h2 : x < 15) : Ein x 34 = 331 / 20 * x + -185

theorem Zeta5Irrational.inPiece_89 (x : ℝ) (h1 : 15 ≤ x) (h2 : x < 560 / 37) : Ein x 34 = 157 / 10 * x + -200

theorem Zeta5Irrational.inPiece_90 (x : ℝ) (h1 : 560 / 37 ≤ x) (h2 : x < 350 / 23) : Ein x 34 = 813 / 40 * x + -270

theorem Zeta5Irrational.inPiece_91 (x : ℝ) (h1 : 350 / 23 ≤ x) (h2 : x < 31 / 2) : Ein x 35 = 767 / 40 * x + -505 / 2

theorem Zeta5Irrational.inPiece_92 (x : ℝ) (h1 : 31 / 2 ≤ x) (h2 : x < 360 / 23) : Ein x 35 = 807 / 40 * x + -268

theorem Zeta5Irrational.inPiece_93 (x : ℝ) (h1 : 360 / 23 ≤ x) (h2 : x < 580 / 37) : Ein x 36 = 761 / 40 * x + -250

theorem Zeta5Irrational.inPiece_94 (x : ℝ) (h1 : 580 / 37 ≤ x) (h2 : x < 680 / 43) : Ein x 36 = 167 / 8 * x + -279

theorem Zeta5Irrational.inPiece_95 (x : ℝ) (h1 : 680 / 43 ≤ x) (h2 : x < 16) : Ein x 36 = 353 / 20 * x + -228

theorem Zeta5Irrational.inPiece_96 (x : ℝ) (h1 : 16 ≤ x) (h2 : x < 370 / 23) : Ein x 36 = 84 / 5 * x + -244

theorem Zeta5Irrational.inPiece_97 (x : ℝ) (h1 : 370 / 23 ≤ x) (h2 : x < 600 / 37) : Ein x 37 = 313 / 20 * x + -451 / 2

theorem Zeta5Irrational.inPiece_98 (x : ℝ) (h1 : 600 / 37 ≤ x) (h2 : x < 33 / 2) : Ein x 37 = 811 / 40 * x + -601 / 2

theorem Zeta5Irrational.inPiece_99 (x : ℝ) (h1 : 33 / 2 ≤ x) (h2 : x < 380 / 23) : Ein x 37 = 851 / 40 * x + -317

theorem Zeta5Irrational.inPiece_100 (x : ℝ) (h1 : 380 / 23 ≤ x) (h2 : x < 50 / 3) : Ein x 38 = 161 / 8 * x + -298

theorem Zeta5Irrational.inPiece_101 (x : ℝ) (h1 : 50 / 3 ≤ x) (h2 : x < 720 / 43) : Ein x 39 = 799 / 40 * x + -591 / 2

theorem Zeta5Irrational.inPiece_102 (x : ℝ) (h1 : 720 / 43 ≤ x) (h2 : x < 620 / 37) : Ein x 39 = 67 / 4 * x + -483 / 2

theorem Zeta5Irrational.inPiece_103 (x : ℝ) (h1 : 620 / 37 ≤ x) (h2 : x < 390 / 23) : Ein x 39 = 93 / 5 * x + -545 / 2

theorem Zeta5Irrational.inPiece_104 (x : ℝ) (h1 : 390 / 23 ≤ x) (h2 : x < 17) : Ein x 40 = 349 / 20 * x + -253

theorem Zeta5Irrational.inPiece_105 (x : ℝ) (h1 : 17 ≤ x) (h2 : x < 640 / 37) : Ein x 40 = 83 / 5 * x + -270

theorem Zeta5Irrational.inPiece_106 (x : ℝ) (h1 : 640 / 37 ≤ x) (h2 : x < 400 / 23) : Ein x 40 = 849 / 40 * x + -350

theorem Zeta5Irrational.inPiece_107 (x : ℝ) (h1 : 400 / 23 ≤ x) (h2 : x < 35 / 2) : Ein x 41 = 803 / 40 * x + -330

theorem Zeta5Irrational.inPiece_108 (x : ℝ) (h1 : 35 / 2 ≤ x) (h2 : x < 760 / 43) : Ein x 41 = 843 / 40 * x + -695 / 2

theorem Zeta5Irrational.inPiece_109 (x : ℝ) (h1 : 760 / 43 ≤ x) (h2 : x < 410 / 23) : Ein x 41 = 357 / 20 * x + -581 / 2

theorem Zeta5Irrational.inPiece_110 (x : ℝ) (h1 : 410 / 23 ≤ x) (h2 : x < 660 / 37) : Ein x 42 = 167 / 10 * x + -270

theorem Zeta5Irrational.inPiece_111 (x : ℝ) (h1 : 660 / 37 ≤ x) (h2 : x < 18) : Ein x 42 = 371 / 20 * x + -303

theorem Zeta5Irrational.inPiece_112 (x : ℝ) (h1 : 18 ≤ x) (h2 : x < 420 / 23) : Ein x 42 = 177 / 10 * x + -321

theorem Zeta5Irrational.inPiece_113 (x : ℝ) (h1 : 420 / 23 ≤ x) (h2 : x < 680 / 37) : Ein x 43 = 331 / 20 * x + -300

theorem Zeta5Irrational.inPiece_114 (x : ℝ) (h1 : 680 / 37 ≤ x) (h2 : x < 37 / 2) : Ein x 43 = 847 / 40 * x + -385

theorem Zeta5Irrational.inPiece_115 (x : ℝ) (h1 : 37 / 2 ≤ x) (h2 : x < 800 / 43) : Ein x 43 = 887 / 40 * x + -807 / 2

theorem Zeta5Irrational.inPiece_116 (x : ℝ) (h1 : 800 / 43 ≤ x) (h2 : x < 430 / 23) : Ein x 43 = 379 / 20 * x + -687 / 2

theorem Zeta5Irrational.inPiece_117 (x : ℝ) (h1 : 430 / 23 ≤ x) (h2 : x < 700 / 37) : Ein x 44 = 89 / 5 * x + -322

theorem Zeta5Irrational.inPiece_118 (x : ℝ) (h1 : 700 / 37 ≤ x) (h2 : x < 19) : Ein x 44 = 393 / 20 * x + -357

theorem Zeta5Irrational.inPiece_119 (x : ℝ) (h1 : 19 ≤ x) (h2 : x < 440 / 23) : Ein x 44 = 94 / 5 * x + -376

theorem Zeta5Irrational.inPiece_120 (x : ℝ) (h1 : 440 / 23 ≤ x) (h2 : x < 720 / 37) : Ein x 45 = 353 / 20 * x + -354

theorem Zeta5Irrational.inPiece_121 (x : ℝ) (h1 : 720 / 37 ≤ x) (h2 : x < 39 / 2) : Ein x 45 = 891 / 40 * x + -444

theorem Zeta5Irrational.inPiece_122 (x : ℝ) (h1 : 39 / 2 ≤ x) (h2 : x < 840 / 43) : Ein x 45 = 931 / 40 * x + -927 / 2

theorem Zeta5Irrational.inPiece_123 (x : ℝ) (h1 : 840 / 43 ≤ x) (h2 : x < 450 / 23) : Ein x 45 = 401 / 20 * x + -801 / 2

theorem Zeta5Irrational.inPiece_124 (x : ℝ) (h1 : 450 / 23 ≤ x) (h2 : x < 20) : Ein x 46 = 189 / 10 * x + -378