Z01:
(364 + 1) ! = (364 !) * (364 + 1)
by NEWTON:21;
Z02:
(363 + 1) ! = (363 !) * (363 + 1)
by NEWTON:21;
Z03:
(362 + 1) ! = (362 !) * (362 + 1)
by NEWTON:21;
Z04:
(361 + 1) ! = (361 !) * (361 + 1)
by NEWTON:21;
Z05:
(360 + 1) ! = (360 !) * (360 + 1)
by NEWTON:21;
Z06:
(359 + 1) ! = (359 !) * (359 + 1)
by NEWTON:21;
Z07:
(358 + 1) ! = (358 !) * (358 + 1)
by NEWTON:21;
Z08:
(357 + 1) ! = (357 !) * (357 + 1)
by NEWTON:21;
Z09:
(356 + 1) ! = (356 !) * (356 + 1)
by NEWTON:21;
Z10:
(355 + 1) ! = (355 !) * (355 + 1)
by NEWTON:21;
Z11:
(354 + 1) ! = (354 !) * (354 + 1)
by NEWTON:21;
Z12:
(353 + 1) ! = (353 !) * (353 + 1)
by NEWTON:21;
Z13:
(352 + 1) ! = (352 !) * (352 + 1)
by NEWTON:21;
Z14:
(351 + 1) ! = (351 !) * (351 + 1)
by NEWTON:21;
Z15:
(350 + 1) ! = (350 !) * (350 + 1)
by NEWTON:21;
Z16:
(349 + 1) ! = (349 !) * (349 + 1)
by NEWTON:21;
Z17:
(348 + 1) ! = (348 !) * (348 + 1)
by NEWTON:21;
Z18:
(347 + 1) ! = (347 !) * (347 + 1)
by NEWTON:21;
Z19:
(346 + 1) ! = (346 !) * (346 + 1)
by NEWTON:21;
Z20:
(345 + 1) ! = (345 !) * (345 + 1)
by NEWTON:21;
Z21:
(344 + 1) ! = (344 !) * (344 + 1)
by NEWTON:21;
Z22:
(343 + 1) ! = (343 !) * (343 + 1)
by NEWTON:21;
(342 + 1) ! = (342 !) * (342 + 1)
by NEWTON:21;
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 Z01, Z02, Z03, Z04, Z05, Z06, Z07, Z08, Z09, Z10, Z11, Z12, Z13, Z14, Z15, Z16, Z17, Z18, Z19, Z20, Z21, Z22;
then A4:
(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:90;
365 |^ 1 = 365
by NEWTON:10;
then P2:
365 |^ (1 + 1) = 365 * 365
by NEWTON:11;
then P3:
365 |^ (2 + 1) = (365 * 365) * 365
by NEWTON:11;
P4:
365 |^ (3 + 2) = (365 |^ 3) * (365 |^ 2)
by NEWTON:13;
P5:
365 |^ (3 + 3) = (365 |^ 3) * (365 |^ 3)
by NEWTON:13;
P6:
365 |^ (6 + 5) = (365 |^ 6) * (365 |^ 5)
by NEWTON:13;
P7:
365 |^ (6 + 6) = (365 |^ 6) * (365 |^ 6)
by NEWTON:13;
365 |^ (12 + 11) = (365 |^ 12) * (365 |^ 11)
by NEWTON:13;
then P9:
2 * ((365 |^ 23) - ((365 !) / (342 !))) > 365 |^ 23
by P6, A4, P7, P4, P2, P3, P5;
365 - 23 >= 0
;
hence
2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
by P9, XREAL_0:def 2; verum