A1:
(364 + 1) ! = (364 !) * (364 + 1)
by NEWTON:15;
A2:
(363 + 1) ! = (363 !) * (363 + 1)
by NEWTON:15;
A3:
(362 + 1) ! = (362 !) * (362 + 1)
by NEWTON:15;
A4:
(361 + 1) ! = (361 !) * (361 + 1)
by NEWTON:15;
A5:
(360 + 1) ! = (360 !) * (360 + 1)
by NEWTON:15;
A6:
(359 + 1) ! = (359 !) * (359 + 1)
by NEWTON:15;
A7:
(358 + 1) ! = (358 !) * (358 + 1)
by NEWTON:15;
A8:
(357 + 1) ! = (357 !) * (357 + 1)
by NEWTON:15;
A9:
(356 + 1) ! = (356 !) * (356 + 1)
by NEWTON:15;
A10:
(355 + 1) ! = (355 !) * (355 + 1)
by NEWTON:15;
A11:
(354 + 1) ! = (354 !) * (354 + 1)
by NEWTON:15;
A12:
(353 + 1) ! = (353 !) * (353 + 1)
by NEWTON:15;
A13:
(352 + 1) ! = (352 !) * (352 + 1)
by NEWTON:15;
A14:
(351 + 1) ! = (351 !) * (351 + 1)
by NEWTON:15;
A15:
(350 + 1) ! = (350 !) * (350 + 1)
by NEWTON:15;
A16:
(349 + 1) ! = (349 !) * (349 + 1)
by NEWTON:15;
A17:
(348 + 1) ! = (348 !) * (348 + 1)
by NEWTON:15;
A18:
(347 + 1) ! = (347 !) * (347 + 1)
by NEWTON:15;
A19:
(346 + 1) ! = (346 !) * (346 + 1)
by NEWTON:15;
A20:
(345 + 1) ! = (345 !) * (345 + 1)
by NEWTON:15;
A21:
(344 + 1) ! = (344 !) * (344 + 1)
by NEWTON:15;
A22:
(343 + 1) ! = (343 !) * (343 + 1)
by NEWTON:15;
(342 + 1) ! = (342 !) * (342 + 1)
by NEWTON:15;
then
365 ! = (((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343)) * (342 !)
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22;
then A23:
(365 !) / (342 !) = ((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343)
by XCMPLX_1:89;
365 |^ 1 = 365
;
then A24:
365 |^ (1 + 1) = 365 * 365
by NEWTON:6;
then A25:
365 |^ (2 + 1) = (365 * 365) * 365
by NEWTON:6;
A26:
365 |^ (3 + 2) = (365 |^ 3) * (365 |^ 2)
by NEWTON:8;
A27:
365 |^ (3 + 3) = (365 |^ 3) * (365 |^ 3)
by NEWTON:8;
A28:
365 |^ (6 + 5) = (365 |^ 6) * (365 |^ 5)
by NEWTON:8;
A29:
365 |^ (6 + 6) = (365 |^ 6) * (365 |^ 6)
by NEWTON:8;
365 |^ (12 + 11) = (365 |^ 12) * (365 |^ 11)
by NEWTON:8;
then A30:
2 * ((365 |^ 23) - ((365 !) / (342 !))) > 365 |^ 23
by A28, A23, A29, A26, A24, A25, A27;
365 - 23 >= 0
;
hence
2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
by A30, XREAL_0:def 2; verum