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

Theorem log2ub 24036
 Description: log2 is less than 253 / 365. If written in decimal, this is because log2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. (Contributed by Mario Carneiro, 7-Apr-2015.)
Assertion
Ref Expression
log2ub (log‘2) < (253 / 365)

Proof of Theorem log2ub
StepHypRef Expression
1 df-4 10759 . . . . . . . . . . 11 4 = (3 + 1)
21oveq1i 6373 . . . . . . . . . 10 (4 − 1) = ((3 + 1) − 1)
3 3cn 10773 . . . . . . . . . . 11 3 ∈ ℂ
4 ax-1cn 9682 . . . . . . . . . . 11 1 ∈ ℂ
53, 4pncan3oi 9978 . . . . . . . . . 10 ((3 + 1) − 1) = 3
62, 5eqtri 2527 . . . . . . . . 9 (4 − 1) = 3
76oveq2i 6374 . . . . . . . 8 (0...(4 − 1)) = (0...3)
87sumeq1i 13924 . . . . . . 7 Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
98oveq2i 6374 . . . . . 6 ((log‘2) − Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))
10 4nn0 10979 . . . . . . 7 4 ∈ ℕ0
11 log2tlbnd 24032 . . . . . . 7 (4 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 4) + 1)) · (9↑4)))))
1210, 11ax-mp 5 . . . . . 6 ((log‘2) − Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 4) + 1)) · (9↑4))))
139, 12eqeltrri 2580 . . . . 5 ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 4) + 1)) · (9↑4))))
14 0re 9728 . . . . . 6 0 ∈ ℝ
15 3re 10772 . . . . . . 7 3 ∈ ℝ
16 4nn 10859 . . . . . . . . 9 4 ∈ ℕ
17 2nn0 10977 . . . . . . . . . 10 2 ∈ ℕ0
18 1nn 10709 . . . . . . . . . 10 1 ∈ ℕ
1917, 10, 18numnncl 11149 . . . . . . . . 9 ((2 · 4) + 1) ∈ ℕ
2016, 19nnmulcli 10722 . . . . . . . 8 (4 · ((2 · 4) + 1)) ∈ ℕ
21 9nn 10864 . . . . . . . . 9 9 ∈ ℕ
22 nnexpcl 12399 . . . . . . . . 9 ((9 ∈ ℕ ∧ 4 ∈ ℕ0) → (9↑4) ∈ ℕ)
2321, 10, 22mp2an 695 . . . . . . . 8 (9↑4) ∈ ℕ
2420, 23nnmulcli 10722 . . . . . . 7 ((4 · ((2 · 4) + 1)) · (9↑4)) ∈ ℕ
25 nndivre 10734 . . . . . . 7 ((3 ∈ ℝ ∧ ((4 · ((2 · 4) + 1)) · (9↑4)) ∈ ℕ) → (3 / ((4 · ((2 · 4) + 1)) · (9↑4))) ∈ ℝ)
2615, 24, 25mp2an 695 . . . . . 6 (3 / ((4 · ((2 · 4) + 1)) · (9↑4))) ∈ ℝ
2714, 26elicc2i 11795 . . . . 5 (((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ↔ (((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ ℝ ∧ 0 ≤ ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∧ ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))))
2813, 27mpbi 215 . . . 4 (((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ ℝ ∧ 0 ≤ ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∧ ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (3 / ((4 · ((2 · 4) + 1)) · (9↑4))))
2928simp3i 1055 . . 3 ((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))
30 2rp 11398 . . . . 5 2 ∈ ℝ+
31 relogcl 23686 . . . . 5 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3230, 31ax-mp 5 . . . 4 (log‘2) ∈ ℝ
33 fzfid 12299 . . . . . 6 (⊤ → (0...3) ∈ Fin)
34 2re 10768 . . . . . . 7 2 ∈ ℝ
35 3nn 10858 . . . . . . . . 9 3 ∈ ℕ
36 elfznn0 11985 . . . . . . . . . . . 12 (𝑛 ∈ (0...3) → 𝑛 ∈ ℕ0)
3736adantl 475 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ (0...3)) → 𝑛 ∈ ℕ0)
38 nn0mulcl 10997 . . . . . . . . . . 11 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
3917, 37, 38sylancr 685 . . . . . . . . . 10 ((⊤ ∧ 𝑛 ∈ (0...3)) → (2 · 𝑛) ∈ ℕ0)
40 nn0p1nn 11000 . . . . . . . . . 10 ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
4139, 40syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑛 ∈ (0...3)) → ((2 · 𝑛) + 1) ∈ ℕ)
42 nnmulcl 10721 . . . . . . . . 9 ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
4335, 41, 42sylancr 685 . . . . . . . 8 ((⊤ ∧ 𝑛 ∈ (0...3)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
44 nnexpcl 12399 . . . . . . . . 9 ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
4521, 37, 44sylancr 685 . . . . . . . 8 ((⊤ ∧ 𝑛 ∈ (0...3)) → (9↑𝑛) ∈ ℕ)
4643, 45nnmulcld 10746 . . . . . . 7 ((⊤ ∧ 𝑛 ∈ (0...3)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
47 nndivre 10734 . . . . . . 7 ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
4834, 46, 47sylancr 685 . . . . . 6 ((⊤ ∧ 𝑛 ∈ (0...3)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
4933, 48fsumrecl 13960 . . . . 5 (⊤ → Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
5049trud 1477 . . . 4 Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ
5132, 50, 26lesubadd2i 10262 . . 3 (((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (3 / ((4 · ((2 · 4) + 1)) · (9↑4))) ↔ (log‘2) ≤ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))))
5229, 51mpbi 215 . 2 (log‘2) ≤ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4))))
53 log2ublem3 24035 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056
54 3nn0 10978 . . . . 5 3 ∈ ℕ0
55 5nn0 10980 . . . . . . . . 9 5 ∈ ℕ0
5655, 54deccl 11155 . . . . . . . 8 53 ∈ ℕ0
57 0nn0 10975 . . . . . . . 8 0 ∈ ℕ0
5856, 57deccl 11155 . . . . . . 7 530 ∈ ℕ0
5958, 55deccl 11155 . . . . . 6 5305 ∈ ℕ0
60 6nn0 10981 . . . . . 6 6 ∈ ℕ0
6159, 60deccl 11155 . . . . 5 53056 ∈ ℕ0
62 1nn0 10976 . . . . 5 1 ∈ ℕ0
63 eqid 2505 . . . . 5 𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) = (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4))))
64 6p1e7 10828 . . . . . 6 (6 + 1) = 7
65 eqid 2505 . . . . . 6 53056 = 53056
6659, 60, 64, 65decsuc 11164 . . . . 5 (53056 + 1) = 53057
67 5nn 10860 . . . . . . . . . 10 5 ∈ ℕ
68 7nn 10862 . . . . . . . . . 10 7 ∈ ℕ
6967, 68nnmulcli 10722 . . . . . . . . 9 (5 · 7) ∈ ℕ
7069nnrei 10707 . . . . . . . 8 (5 · 7) ∈ ℝ
7120nnrei 10707 . . . . . . . 8 (4 · ((2 · 4) + 1)) ∈ ℝ
72 6nn 10861 . . . . . . . . . 10 6 ∈ ℕ
73 5lt6 10876 . . . . . . . . . 10 5 < 6
7454, 55, 72, 73declt 11162 . . . . . . . . 9 35 < 36
75 7cn 10782 . . . . . . . . . 10 7 ∈ ℂ
76 5cn 10778 . . . . . . . . . 10 5 ∈ ℂ
77 7t5e35 11226 . . . . . . . . . 10 (7 · 5) = 35
7875, 76, 77mulcomli 9735 . . . . . . . . 9 (5 · 7) = 35
79 4cn 10776 . . . . . . . . . . . . . 14 4 ∈ ℂ
80 2cn 10769 . . . . . . . . . . . . . 14 2 ∈ ℂ
81 4t2e8 10853 . . . . . . . . . . . . . 14 (4 · 2) = 8
8279, 80, 81mulcomli 9735 . . . . . . . . . . . . 13 (2 · 4) = 8
8382oveq1i 6373 . . . . . . . . . . . 12 ((2 · 4) + 1) = (8 + 1)
84 8p1e9 10830 . . . . . . . . . . . 12 (8 + 1) = 9
8583, 84eqtri 2527 . . . . . . . . . . 11 ((2 · 4) + 1) = 9
8685oveq2i 6374 . . . . . . . . . 10 (4 · ((2 · 4) + 1)) = (4 · 9)
87 9cn 10786 . . . . . . . . . . 11 9 ∈ ℂ
88 9t4e36 11238 . . . . . . . . . . 11 (9 · 4) = 36
8987, 79, 88mulcomli 9735 . . . . . . . . . 10 (4 · 9) = 36
9086, 89eqtri 2527 . . . . . . . . 9 (4 · ((2 · 4) + 1)) = 36
9174, 78, 903brtr4i 4463 . . . . . . . 8 (5 · 7) < (4 · ((2 · 4) + 1))
9270, 71, 91ltleii 9842 . . . . . . 7 (5 · 7) ≤ (4 · ((2 · 4) + 1))
9323nngt0i 10732 . . . . . . . 8 0 < (9↑4)
9423nnrei 10707 . . . . . . . . 9 (9↑4) ∈ ℝ
9570, 71, 94lemul2i 10619 . . . . . . . 8 (0 < (9↑4) → ((5 · 7) ≤ (4 · ((2 · 4) + 1)) ↔ ((9↑4) · (5 · 7)) ≤ ((9↑4) · (4 · ((2 · 4) + 1)))))
9693, 95ax-mp 5 . . . . . . 7 ((5 · 7) ≤ (4 · ((2 · 4) + 1)) ↔ ((9↑4) · (5 · 7)) ≤ ((9↑4) · (4 · ((2 · 4) + 1))))
9792, 96mpbi 215 . . . . . 6 ((9↑4) · (5 · 7)) ≤ ((9↑4) · (4 · ((2 · 4) + 1)))
98 7nn0 10982 . . . . . . . . . 10 7 ∈ ℕ0
99 nnexpcl 12399 . . . . . . . . . 10 ((3 ∈ ℕ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℕ)
10035, 98, 99mp2an 695 . . . . . . . . 9 (3↑7) ∈ ℕ
101100nncni 10708 . . . . . . . 8 (3↑7) ∈ ℂ
10269nncni 10708 . . . . . . . 8 (5 · 7) ∈ ℂ
103101, 102, 3mul32i 9914 . . . . . . 7 (((3↑7) · (5 · 7)) · 3) = (((3↑7) · 3) · (5 · 7))
10479, 80mulcomi 9734 . . . . . . . . . . . 12 (4 · 2) = (2 · 4)
105 df-8 10763 . . . . . . . . . . . 12 8 = (7 + 1)
10681, 104, 1053eqtr3i 2535 . . . . . . . . . . 11 (2 · 4) = (7 + 1)
107106oveq2i 6374 . . . . . . . . . 10 (3↑(2 · 4)) = (3↑(7 + 1))
108 expmul 12431 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 4 ∈ ℕ0) → (3↑(2 · 4)) = ((3↑2)↑4))
1093, 17, 10, 108mp3an 1406 . . . . . . . . . 10 (3↑(2 · 4)) = ((3↑2)↑4)
110107, 109eqtr3i 2529 . . . . . . . . 9 (3↑(7 + 1)) = ((3↑2)↑4)
111 expp1 12393 . . . . . . . . . 10 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑(7 + 1)) = ((3↑7) · 3))
1123, 98, 111mp2an 695 . . . . . . . . 9 (3↑(7 + 1)) = ((3↑7) · 3)
113 sq3 12486 . . . . . . . . . 10 (3↑2) = 9
114113oveq1i 6373 . . . . . . . . 9 ((3↑2)↑4) = (9↑4)
115110, 112, 1143eqtr3i 2535 . . . . . . . 8 ((3↑7) · 3) = (9↑4)
116115oveq1i 6373 . . . . . . 7 (((3↑7) · 3) · (5 · 7)) = ((9↑4) · (5 · 7))
117103, 116eqtri 2527 . . . . . 6 (((3↑7) · (5 · 7)) · 3) = ((9↑4) · (5 · 7))
11820nncni 10708 . . . . . . . . 9 (4 · ((2 · 4) + 1)) ∈ ℂ
11923nncni 10708 . . . . . . . . 9 (9↑4) ∈ ℂ
120118, 119mulcomi 9734 . . . . . . . 8 ((4 · ((2 · 4) + 1)) · (9↑4)) = ((9↑4) · (4 · ((2 · 4) + 1)))
121120oveq1i 6373 . . . . . . 7 (((4 · ((2 · 4) + 1)) · (9↑4)) · 1) = (((9↑4) · (4 · ((2 · 4) + 1))) · 1)
122119, 118mulcli 9733 . . . . . . . 8 ((9↑4) · (4 · ((2 · 4) + 1))) ∈ ℂ
123122mulid1i 9730 . . . . . . 7 (((9↑4) · (4 · ((2 · 4) + 1))) · 1) = ((9↑4) · (4 · ((2 · 4) + 1)))
124121, 123eqtri 2527 . . . . . 6 (((4 · ((2 · 4) + 1)) · (9↑4)) · 1) = ((9↑4) · (4 · ((2 · 4) + 1)))
12597, 117, 1243brtr4i 4463 . . . . 5 (((3↑7) · (5 · 7)) · 3) ≤ (((4 · ((2 · 4) + 1)) · (9↑4)) · 1)
12653, 50, 54, 24, 61, 62, 63, 66, 125log2ublem1 24033 . . . 4 (((3↑7) · (5 · 7)) · (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4))))) ≤ 53057
12750, 26readdcli 9741 . . . . 5 𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ∈ ℝ
12859, 98deccl 11155 . . . . . 6 53057 ∈ ℕ0
129128nn0rei 10971 . . . . 5 53057 ∈ ℝ
130100, 69nnmulcli 10722 . . . . . . 7 ((3↑7) · (5 · 7)) ∈ ℕ
131130nnrei 10707 . . . . . 6 ((3↑7) · (5 · 7)) ∈ ℝ
132130nngt0i 10732 . . . . . 6 0 < ((3↑7) · (5 · 7))
133131, 132pm3.2i 464 . . . . 5 (((3↑7) · (5 · 7)) ∈ ℝ ∧ 0 < ((3↑7) · (5 · 7)))
134 lemuldiv2 10576 . . . . 5 (((Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ∈ ℝ ∧ 53057 ∈ ℝ ∧ (((3↑7) · (5 · 7)) ∈ ℝ ∧ 0 < ((3↑7) · (5 · 7)))) → ((((3↑7) · (5 · 7)) · (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4))))) ≤ 53057 ↔ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ≤ (53057 / ((3↑7) · (5 · 7)))))
135127, 129, 133, 134mp3an 1406 . . . 4 ((((3↑7) · (5 · 7)) · (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4))))) ≤ 53057 ↔ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ≤ (53057 / ((3↑7) · (5 · 7))))
136126, 135mpbi 215 . . 3 𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ≤ (53057 / ((3↑7) · (5 · 7)))
137 8nn0 10983 . . . . . . . . . . . . 13 8 ∈ ℕ0
13854, 137deccl 11155 . . . . . . . . . . . 12 38 ∈ ℕ0
139138, 98deccl 11155 . . . . . . . . . . 11 387 ∈ ℕ0
140139, 54deccl 11155 . . . . . . . . . 10 3873 ∈ ℕ0
141140, 62deccl 11155 . . . . . . . . 9 38731 ∈ ℕ0
142141, 60deccl 11155 . . . . . . . 8 387316 ∈ ℕ0
143141, 98deccl 11155 . . . . . . . 8 387317 ∈ ℕ0
144 1lt10 10910 . . . . . . . 8 1 < 10
145 6lt7 10881 . . . . . . . . 9 6 < 7
146141, 60, 68, 145declt 11162 . . . . . . . 8 387316 < 387317
147142, 143, 62, 98, 144, 146decltc 11163 . . . . . . 7 3873161 < 3873177
148 eqid 2505 . . . . . . . 8 73 = 73
14962, 55deccl 11155 . . . . . . . . . . 11 15 ∈ ℕ0
150 9nn0 10984 . . . . . . . . . . 11 9 ∈ ℕ0
151149, 150deccl 11155 . . . . . . . . . 10 159 ∈ ℕ0
152151, 62deccl 11155 . . . . . . . . 9 1591 ∈ ℕ0
153152, 98deccl 11155 . . . . . . . 8 15917 ∈ ℕ0
154 eqid 2505 . . . . . . . . 9 53057 = 53057
155 eqid 2505 . . . . . . . . 9 15917 = 15917
156 eqid 2505 . . . . . . . . . 10 5305 = 5305
157 eqid 2505 . . . . . . . . . . 11 1591 = 1591
158 5p1e6 10827 . . . . . . . . . . . 12 (5 + 1) = 6
15976, 4, 158addcomli 9910 . . . . . . . . . . 11 (1 + 5) = 6
160151, 62, 55, 157, 159decaddi 11185 . . . . . . . . . 10 (1591 + 5) = 1596
16162, 60deccl 11155 . . . . . . . . . . 11 16 ∈ ℕ0
162 eqid 2505 . . . . . . . . . . 11 530 = 530
163 eqid 2505 . . . . . . . . . . . 12 159 = 159
164 eqid 2505 . . . . . . . . . . . . 13 15 = 15
16562, 55, 158, 164decsuc 11164 . . . . . . . . . . . 12 (15 + 1) = 16
166 9p4e13 11205 . . . . . . . . . . . 12 (9 + 4) = 13
167149, 150, 10, 163, 165, 54, 166decaddci 11186 . . . . . . . . . . 11 (159 + 4) = 163
168 eqid 2505 . . . . . . . . . . . 12 53 = 53
169161nn0cni 10972 . . . . . . . . . . . . 13 16 ∈ ℂ
170169addid1i 9905 . . . . . . . . . . . 12 (16 + 0) = 16
171 1p2e3 10824 . . . . . . . . . . . . . 14 (1 + 2) = 3
172171oveq2i 6374 . . . . . . . . . . . . 13 ((5 · 7) + (1 + 2)) = ((5 · 7) + 3)
173 5p3e8 10838 . . . . . . . . . . . . . 14 (5 + 3) = 8
17454, 55, 54, 78, 173decaddi 11185 . . . . . . . . . . . . 13 ((5 · 7) + 3) = 38
175172, 174eqtri 2527 . . . . . . . . . . . 12 ((5 · 7) + (1 + 2)) = 38
176 7t3e21 11224 . . . . . . . . . . . . . 14 (7 · 3) = 21
17775, 3, 176mulcomli 9735 . . . . . . . . . . . . 13 (3 · 7) = 21
178 6cn 10780 . . . . . . . . . . . . . 14 6 ∈ ℂ
179178, 4, 64addcomli 9910 . . . . . . . . . . . . 13 (1 + 6) = 7
18017, 62, 60, 177, 179decaddi 11185 . . . . . . . . . . . 12 ((3 · 7) + 6) = 27
18155, 54, 62, 60, 168, 170, 98, 98, 17, 175, 180decmac 11180 . . . . . . . . . . 11 ((53 · 7) + (16 + 0)) = 387
18275mul02i 9907 . . . . . . . . . . . . 13 (0 · 7) = 0
183182oveq1i 6373 . . . . . . . . . . . 12 ((0 · 7) + 3) = (0 + 3)
1843addid2i 9906 . . . . . . . . . . . . 13 (0 + 3) = 3
18554dec0h 11157 . . . . . . . . . . . . 13 3 = 03
186184, 185eqtri 2527 . . . . . . . . . . . 12 (0 + 3) = 03
187183, 186eqtri 2527 . . . . . . . . . . 11 ((0 · 7) + 3) = 03
18856, 57, 161, 54, 162, 167, 98, 54, 57, 181, 187decmac 11180 . . . . . . . . . 10 ((530 · 7) + (159 + 4)) = 3873
189 3p1e4 10825 . . . . . . . . . . 11 (3 + 1) = 4
190 6p5e11 11191 . . . . . . . . . . . 12 (6 + 5) = 11
191178, 76, 190addcomli 9910 . . . . . . . . . . 11 (5 + 6) = 11
19254, 55, 60, 78, 189, 62, 191decaddci 11186 . . . . . . . . . 10 ((5 · 7) + 6) = 41
19358, 55, 151, 60, 156, 160, 98, 62, 10, 188, 192decmac 11180 . . . . . . . . 9 ((5305 · 7) + (1591 + 5)) = 38731
194 7t7e49 11228 . . . . . . . . . 10 (7 · 7) = 49
195 4p1e5 10826 . . . . . . . . . 10 (4 + 1) = 5
196 9p7e16 11208 . . . . . . . . . 10 (9 + 7) = 16
19710, 150, 98, 194, 195, 60, 196decaddci 11186 . . . . . . . . 9 ((7 · 7) + 7) = 56
19859, 98, 152, 98, 154, 155, 98, 60, 55, 193, 197decmac 11180 . . . . . . . 8 ((53057 · 7) + 15917) = 387316
19917dec0h 11157 . . . . . . . . . 10 2 = 02
2004addid2i 9906 . . . . . . . . . . . 12 (0 + 1) = 1
20162dec0h 11157 . . . . . . . . . . . 12 1 = 01
202200, 201eqtri 2527 . . . . . . . . . . 11 (0 + 1) = 01
203 00id 9893 . . . . . . . . . . . . 13 (0 + 0) = 0
20457dec0h 11157 . . . . . . . . . . . . 13 0 = 00
205203, 204eqtri 2527 . . . . . . . . . . . 12 (0 + 0) = 00
206 5t3e15 11215 . . . . . . . . . . . . . 14 (5 · 3) = 15
207206oveq1i 6373 . . . . . . . . . . . . 13 ((5 · 3) + 0) = (15 + 0)
208149nn0cni 10972 . . . . . . . . . . . . . 14 15 ∈ ℂ
209208addid1i 9905 . . . . . . . . . . . . 13 (15 + 0) = 15
210207, 209eqtri 2527 . . . . . . . . . . . 12 ((5 · 3) + 0) = 15
211 3t3e9 10852 . . . . . . . . . . . . . 14 (3 · 3) = 9
212211oveq1i 6373 . . . . . . . . . . . . 13 ((3 · 3) + 0) = (9 + 0)
21387addid1i 9905 . . . . . . . . . . . . 13 (9 + 0) = 9
214212, 213eqtri 2527 . . . . . . . . . . . 12 ((3 · 3) + 0) = 9
21555, 54, 57, 57, 168, 205, 54, 210, 214decma 11179 . . . . . . . . . . 11 ((53 · 3) + (0 + 0)) = 159
2163mul02i 9907 . . . . . . . . . . . . 13 (0 · 3) = 0
217216oveq1i 6373 . . . . . . . . . . . 12 ((0 · 3) + 1) = (0 + 1)
218217, 202eqtri 2527 . . . . . . . . . . 11 ((0 · 3) + 1) = 01
21956, 57, 57, 62, 162, 202, 54, 62, 57, 215, 218decmac 11180 . . . . . . . . . 10 ((530 · 3) + (0 + 1)) = 1591
220 5p2e7 10837 . . . . . . . . . . 11 (5 + 2) = 7
22162, 55, 17, 206, 220decaddi 11185 . . . . . . . . . 10 ((5 · 3) + 2) = 17
22258, 55, 57, 17, 156, 199, 54, 98, 62, 219, 221decmac 11180 . . . . . . . . 9 ((5305 · 3) + 2) = 15917
22354, 59, 98, 154, 62, 17, 222, 176decmul1c 11188 . . . . . . . 8 (53057 · 3) = 159171
224128, 98, 54, 148, 62, 153, 198, 223decmul2c 11189 . . . . . . 7 (53057 · 73) = 3873161
22555, 55deccl 11155 . . . . . . . . . . 11 55 ∈ ℕ0
226225, 54deccl 11155 . . . . . . . . . 10 553 ∈ ℕ0
227226, 54deccl 11155 . . . . . . . . 9 5533 ∈ ℕ0
228227, 62deccl 11155 . . . . . . . 8 55331 ∈ ℕ0
22917, 55deccl 11155 . . . . . . . . . 10 25 ∈ ℕ0
230229, 54deccl 11155 . . . . . . . . 9 253 ∈ ℕ0
23117, 62deccl 11155 . . . . . . . . . 10 21 ∈ ℕ0
232231, 137deccl 11155 . . . . . . . . 9 218 ∈ ℕ0
23398, 17deccl 11155 . . . . . . . . . . 11 72 ∈ ℕ0
234 3t2e6 10851 . . . . . . . . . . . . 13 (3 · 2) = 6
2353, 80, 234mulcomli 9735 . . . . . . . . . . . 12 (2 · 3) = 6
236 3exp3 15223 . . . . . . . . . . . 12 (3↑3) = 27
23717, 98deccl 11155 . . . . . . . . . . . . 13 27 ∈ ℕ0
238 eqid 2505 . . . . . . . . . . . . 13 27 = 27
23962, 137deccl 11155 . . . . . . . . . . . . 13 18 ∈ ℕ0
240 eqid 2505 . . . . . . . . . . . . . 14 18 = 18
241 2t2e4 10849 . . . . . . . . . . . . . . . 16 (2 · 2) = 4
242241, 171oveq12i 6375 . . . . . . . . . . . . . . 15 ((2 · 2) + (1 + 2)) = (4 + 3)
243 4p3e7 10835 . . . . . . . . . . . . . . 15 (4 + 3) = 7
244242, 243eqtri 2527 . . . . . . . . . . . . . 14 ((2 · 2) + (1 + 2)) = 7
245 7t2e14 11223 . . . . . . . . . . . . . . 15 (7 · 2) = 14
246 1p1e2 10812 . . . . . . . . . . . . . . 15 (1 + 1) = 2
247 8cn 10784 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
248 8p4e12 11198 . . . . . . . . . . . . . . . 16 (8 + 4) = 12
249247, 79, 248addcomli 9910 . . . . . . . . . . . . . . 15 (4 + 8) = 12
25062, 10, 137, 245, 246, 17, 249decaddci 11186 . . . . . . . . . . . . . 14 ((7 · 2) + 8) = 22
25117, 98, 62, 137, 238, 240, 17, 17, 17, 244, 250decmac 11180 . . . . . . . . . . . . 13 ((27 · 2) + 18) = 72
25275, 80, 245mulcomli 9735 . . . . . . . . . . . . . . 15 (2 · 7) = 14
253 4p4e8 10836 . . . . . . . . . . . . . . 15 (4 + 4) = 8
25462, 10, 10, 252, 253decaddi 11185 . . . . . . . . . . . . . 14 ((2 · 7) + 4) = 18
25598, 17, 98, 238, 150, 10, 254, 194decmul1c 11188 . . . . . . . . . . . . 13 (27 · 7) = 189
256237, 17, 98, 238, 150, 239, 251, 255decmul2c 11189 . . . . . . . . . . . 12 (27 · 27) = 729
25754, 54, 235, 236, 256numexp2x 15213 . . . . . . . . . . 11 (3↑6) = 729
258 eqid 2505 . . . . . . . . . . . 12 72 = 72
259176oveq1i 6373 . . . . . . . . . . . . 13 ((7 · 3) + 0) = (21 + 0)
260231nn0cni 10972 . . . . . . . . . . . . . 14 21 ∈ ℂ
261260addid1i 9905 . . . . . . . . . . . . 13 (21 + 0) = 21
262259, 261eqtri 2527 . . . . . . . . . . . 12 ((7 · 3) + 0) = 21
263235oveq1i 6373 . . . . . . . . . . . . 13 ((2 · 3) + 2) = (6 + 2)
264 6p2e8 10841 . . . . . . . . . . . . 13 (6 + 2) = 8
265263, 264eqtri 2527 . . . . . . . . . . . 12 ((2 · 3) + 2) = 8
26698, 17, 57, 17, 258, 199, 54, 262, 265decma 11179 . . . . . . . . . . 11 ((72 · 3) + 2) = 218
267 9t3e27 11237 . . . . . . . . . . 11 (9 · 3) = 27
26854, 233, 150, 257, 98, 17, 266, 267decmul1c 11188 . . . . . . . . . 10 ((3↑6) · 3) = 2187
26954, 60, 64, 268numexpp1 15212 . . . . . . . . 9 (3↑7) = 2187
27062, 98deccl 11155 . . . . . . . . . 10 17 ∈ ℕ0
271270, 98deccl 11155 . . . . . . . . 9 177 ∈ ℕ0
272 eqid 2505 . . . . . . . . . 10 218 = 218
273 eqid 2505 . . . . . . . . . 10 177 = 177
27417, 57deccl 11155 . . . . . . . . . . 11 20 ∈ ℕ0
275274, 54deccl 11155 . . . . . . . . . 10 203 ∈ ℕ0
27617, 17deccl 11155 . . . . . . . . . . 11 22 ∈ ℕ0
277 eqid 2505 . . . . . . . . . . 11 21 = 21
278 eqid 2505 . . . . . . . . . . . 12 17 = 17
279 eqid 2505 . . . . . . . . . . . 12 203 = 203
280 eqid 2505 . . . . . . . . . . . . . 14 20 = 20
28180addid2i 9906 . . . . . . . . . . . . . 14 (0 + 2) = 2
2824addid1i 9905 . . . . . . . . . . . . . 14 (1 + 0) = 1
28357, 62, 17, 57, 201, 280, 281, 282decadd 11182 . . . . . . . . . . . . 13 (1 + 20) = 21
28417, 62, 246, 283decsuc 11164 . . . . . . . . . . . 12 ((1 + 20) + 1) = 22
285 7p3e10 10845 . . . . . . . . . . . 12 (7 + 3) = 10
28662, 98, 274, 54, 278, 279, 284, 285decaddc2 11184 . . . . . . . . . . 11 (17 + 203) = 220
287 eqid 2505 . . . . . . . . . . . 12 253 = 253
288 eqid 2505 . . . . . . . . . . . . 13 22 = 22
289 eqid 2505 . . . . . . . . . . . . 13 25 = 25
290 2p2e4 10817 . . . . . . . . . . . . 13 (2 + 2) = 4
29176, 80, 220addcomli 9910 . . . . . . . . . . . . 13 (2 + 5) = 7
29217, 17, 17, 55, 288, 289, 290, 291decadd 11182 . . . . . . . . . . . 12 (22 + 25) = 47
29355dec0h 11157 . . . . . . . . . . . . . 14 5 = 05
294195, 293eqtri 2527 . . . . . . . . . . . . 13 (4 + 1) = 05
295241, 200oveq12i 6375 . . . . . . . . . . . . . 14 ((2 · 2) + (0 + 1)) = (4 + 1)
296295, 195eqtri 2527 . . . . . . . . . . . . 13 ((2 · 2) + (0 + 1)) = 5
297 5t2e10 10854 . . . . . . . . . . . . . . 15 (5 · 2) = 10
298 dec10 11171 . . . . . . . . . . . . . . 15 10 = 10
299297, 298eqtri 2527 . . . . . . . . . . . . . 14 (5 · 2) = 10
30076addid2i 9906 . . . . . . . . . . . . . 14 (0 + 5) = 5
30162, 57, 55, 299, 300decaddi 11185 . . . . . . . . . . . . 13 ((5 · 2) + 5) = 15
30217, 55, 57, 55, 289, 294, 17, 55, 62, 296, 301decmac 11180 . . . . . . . . . . . 12 ((25 · 2) + (4 + 1)) = 55
303234oveq1i 6373 . . . . . . . . . . . . 13 ((3 · 2) + 7) = (6 + 7)
304 7p6e13 11195 . . . . . . . . . . . . . 14 (7 + 6) = 13
30575, 178, 304addcomli 9910 . . . . . . . . . . . . 13 (6 + 7) = 13
306303, 305eqtri 2527 . . . . . . . . . . . 12 ((3 · 2) + 7) = 13
307229, 54, 10, 98, 287, 292, 17, 54, 62, 302, 306decmac 11180 . . . . . . . . . . 11 ((253 · 2) + (22 + 25)) = 553
308230nn0cni 10972 . . . . . . . . . . . . . 14 253 ∈ ℂ
309308mulid1i 9730 . . . . . . . . . . . . 13 (253 · 1) = 253
310309oveq1i 6373 . . . . . . . . . . . 12 ((253 · 1) + 0) = (253 + 0)
311308addid1i 9905 . . . . . . . . . . . 12 (253 + 0) = 253
312310, 311eqtri 2527 . . . . . . . . . . 11 ((253 · 1) + 0) = 253
31317, 62, 276, 57, 277, 286, 230, 54, 229, 307, 312decma2c 11181 . . . . . . . . . 10 ((253 · 21) + (17 + 203)) = 5533
31498dec0h 11157 . . . . . . . . . . 11 7 = 07
31579addid2i 9906 . . . . . . . . . . . . . 14 (0 + 4) = 4
316315oveq2i 6374 . . . . . . . . . . . . 13 ((2 · 8) + (0 + 4)) = ((2 · 8) + 4)
317 8t2e16 11229 . . . . . . . . . . . . . . 15 (8 · 2) = 16
318247, 80, 317mulcomli 9735 . . . . . . . . . . . . . 14 (2 · 8) = 16
319 6p4e10 10843 . . . . . . . . . . . . . 14 (6 + 4) = 10
32062, 60, 10, 318, 246, 319decaddci2 11187 . . . . . . . . . . . . 13 ((2 · 8) + 4) = 20
321316, 320eqtri 2527 . . . . . . . . . . . 12 ((2 · 8) + (0 + 4)) = 20
322 8t5e40 11232 . . . . . . . . . . . . . 14 (8 · 5) = 40
323247, 76, 322mulcomli 9735 . . . . . . . . . . . . 13 (5 · 8) = 40
32410, 57, 54, 323, 184decaddi 11185 . . . . . . . . . . . 12 ((5 · 8) + 3) = 43
32517, 55, 57, 54, 289, 186, 137, 54, 10, 321, 324decmac 11180 . . . . . . . . . . 11 ((25 · 8) + (0 + 3)) = 203
326 8t3e24 11230 . . . . . . . . . . . . 13 (8 · 3) = 24
327247, 3, 326mulcomli 9735 . . . . . . . . . . . 12 (3 · 8) = 24
328 2p1e3 10823 . . . . . . . . . . . 12 (2 + 1) = 3
329 7p4e11 11193 . . . . . . . . . . . . 13 (7 + 4) = 11
33075, 79, 329addcomli 9910 . . . . . . . . . . . 12 (4 + 7) = 11
33117, 10, 98, 327, 328, 62, 330decaddci 11186 . . . . . . . . . . 11 ((3 · 8) + 7) = 31
332229, 54, 57, 98, 287, 314, 137, 62, 54, 325, 331decmac 11180 . . . . . . . . . 10 ((253 · 8) + 7) = 2031
333231, 137, 270, 98, 272, 273, 230, 62, 275, 313, 332decma2c 11181 . . . . . . . . 9 ((253 · 218) + 177) = 55331
334184oveq2i 6374 . . . . . . . . . . . 12 ((2 · 7) + (0 + 3)) = ((2 · 7) + 3)
33562, 10, 54, 252, 243decaddi 11185 . . . . . . . . . . . 12 ((2 · 7) + 3) = 17
336334, 335eqtri 2527 . . . . . . . . . . 11 ((2 · 7) + (0 + 3)) = 17
33754, 55, 17, 78, 220decaddi 11185 . . . . . . . . . . 11 ((5 · 7) + 2) = 37
33817, 55, 57, 17, 289, 199, 98, 98, 54, 336, 337decmac 11180 . . . . . . . . . 10 ((25 · 7) + 2) = 177
33998, 229, 54, 287, 62, 17, 338, 177decmul1c 11188 . . . . . . . . 9 (253 · 7) = 1771
340230, 232, 98, 269, 62, 271, 333, 339decmul2c 11189 . . . . . . . 8 (253 · (3↑7)) = 553311
341 eqid 2505 . . . . . . . . . . 11 55331 = 55331
342 eqid 2505 . . . . . . . . . . . . . 14 5533 = 5533
343 eqid 2505 . . . . . . . . . . . . . . 15 553 = 553
344 eqid 2505 . . . . . . . . . . . . . . . 16 55 = 55
345281, 199eqtri 2527 . . . . . . . . . . . . . . . 16 (0 + 2) = 02
346184oveq2i 6374 . . . . . . . . . . . . . . . . 17 ((5 · 7) + (0 + 3)) = ((5 · 7) + 3)
347346, 174eqtri 2527 . . . . . . . . . . . . . . . 16 ((5 · 7) + (0 + 3)) = 38
34855, 55, 57, 17, 344, 345, 98, 98, 54, 347, 337decmac 11180 . . . . . . . . . . . . . . 15 ((55 · 7) + (0 + 2)) = 387
34917, 62, 17, 177, 171decaddi 11185 . . . . . . . . . . . . . . 15 ((3 · 7) + 2) = 23
350225, 54, 57, 17, 343, 199, 98, 54, 17, 348, 349decmac 11180 . . . . . . . . . . . . . 14 ((553 · 7) + 2) = 3873
35198, 226, 54, 342, 62, 17, 350, 177decmul1c 11188 . . . . . . . . . . . . 13 (5533 · 7) = 38731
352351oveq1i 6373 . . . . . . . . . . . 12 ((5533 · 7) + 0) = (38731 + 0)
353141nn0cni 10972 . . . . . . . . . . . . 13 38731 ∈ ℂ
354353addid1i 9905 . . . . . . . . . . . 12 (38731 + 0) = 38731
355352, 354eqtri 2527 . . . . . . . . . . 11 ((5533 · 7) + 0) = 38731
35675mulid2i 9731 . . . . . . . . . . . 12 (1 · 7) = 7
357356, 314eqtri 2527 . . . . . . . . . . 11 (1 · 7) = 07
35898, 227, 62, 341, 98, 57, 355, 357decmul1c 11188 . . . . . . . . . 10 (55331 · 7) = 387317
359358oveq1i 6373 . . . . . . . . 9 ((55331 · 7) + 0) = (387317 + 0)
360143nn0cni 10972 . . . . . . . . . 10 387317 ∈ ℂ
361360addid1i 9905 . . . . . . . . 9 (387317 + 0) = 387317
362359, 361eqtri 2527 . . . . . . . 8 ((55331 · 7) + 0) = 387317
36398, 228, 62, 340, 98, 57, 362, 357decmul1c 11188 . . . . . . 7 ((253 · (3↑7)) · 7) = 3873177
364147, 224, 3633brtr4i 4463 . . . . . 6 (53057 · 73) < ((253 · (3↑7)) · 7)
36598, 54deccl 11155 . . . . . . . . 9 73 ∈ ℕ0
366128, 365nn0mulcli 10999 . . . . . . . 8 (53057 · 73) ∈ ℕ0
367366nn0rei 10971 . . . . . . 7 (53057 · 73) ∈ ℝ
36854, 98nn0expcli 12412 . . . . . . . . . 10 (3↑7) ∈ ℕ0
369230, 368nn0mulcli 10999 . . . . . . . . 9 (253 · (3↑7)) ∈ ℕ0
370369, 98nn0mulcli 10999 . . . . . . . 8 ((253 · (3↑7)) · 7) ∈ ℕ0
371370nn0rei 10971 . . . . . . 7 ((253 · (3↑7)) · 7) ∈ ℝ
37267nnrei 10707 . . . . . . 7 5 ∈ ℝ
37367nngt0i 10732 . . . . . . 7 0 < 5
374367, 371, 372, 373ltmul1ii 10624 . . . . . 6 ((53057 · 73) < ((253 · (3↑7)) · 7) ↔ ((53057 · 73) · 5) < (((253 · (3↑7)) · 7) · 5))
375364, 374mpbi 215 . . . . 5 ((53057 · 73) · 5) < (((253 · (3↑7)) · 7) · 5)
376128nn0cni 10972 . . . . . . 7 53057 ∈ ℂ
377365nn0cni 10972 . . . . . . 7 73 ∈ ℂ
378376, 377, 76mulassi 9737 . . . . . 6 ((53057 · 73) · 5) = (53057 · (73 · 5))
37954, 55, 158, 77decsuc 11164 . . . . . . . 8 ((7 · 5) + 1) = 36
38076, 3, 206mulcomli 9735 . . . . . . . 8 (3 · 5) = 15
38155, 98, 54, 148, 55, 62, 379, 380decmul1c 11188 . . . . . . 7 (73 · 5) = 365
382381oveq2i 6374 . . . . . 6 (53057 · (73 · 5)) = (53057 · 365)
383378, 382eqtri 2527 . . . . 5 ((53057 · 73) · 5) = (53057 · 365)
384308, 101mulcli 9733 . . . . . . 7 (253 · (3↑7)) ∈ ℂ
385384, 75, 76mulassi 9737 . . . . . 6 (((253 · (3↑7)) · 7) · 5) = ((253 · (3↑7)) · (7 · 5))
38675, 76mulcomi 9734 . . . . . . . 8 (7 · 5) = (5 · 7)
387386oveq2i 6374 . . . . . . 7 ((253 · (3↑7)) · (7 · 5)) = ((253 · (3↑7)) · (5 · 7))
388308, 101, 102mulassi 9737 . . . . . . 7 ((253 · (3↑7)) · (5 · 7)) = (253 · ((3↑7) · (5 · 7)))
389387, 388eqtri 2527 . . . . . 6 ((253 · (3↑7)) · (7 · 5)) = (253 · ((3↑7) · (5 · 7)))
390385, 389eqtri 2527 . . . . 5 (((253 · (3↑7)) · 7) · 5) = (253 · ((3↑7) · (5 · 7)))
391375, 383, 3903brtr3i 4462 . . . 4 (53057 · 365) < (253 · ((3↑7) · (5 · 7)))
39254, 60deccl 11155 . . . . . . . 8 36 ∈ ℕ0
393392, 67decnncl 11154 . . . . . . 7 365 ∈ ℕ
394393nnrei 10707 . . . . . 6 365 ∈ ℝ
395393nngt0i 10732 . . . . . 6 0 < 365
396394, 395pm3.2i 464 . . . . 5 (365 ∈ ℝ ∧ 0 < 365)
397230nn0rei 10971 . . . . 5 253 ∈ ℝ
398 lt2mul2div 10572 . . . . 5 (((53057 ∈ ℝ ∧ (365 ∈ ℝ ∧ 0 < 365)) ∧ (253 ∈ ℝ ∧ (((3↑7) · (5 · 7)) ∈ ℝ ∧ 0 < ((3↑7) · (5 · 7))))) → ((53057 · 365) < (253 · ((3↑7) · (5 · 7))) ↔ (53057 / ((3↑7) · (5 · 7))) < (253 / 365)))
399129, 396, 397, 133, 398mp4an 696 . . . 4 ((53057 · 365) < (253 · ((3↑7) · (5 · 7))) ↔ (53057 / ((3↑7) · (5 · 7))) < (253 / 365))
400391, 399mpbi 215 . . 3 (53057 / ((3↑7) · (5 · 7))) < (253 / 365)
401 nndivre 10734 . . . . 5 ((53057 ∈ ℝ ∧ ((3↑7) · (5 · 7)) ∈ ℕ) → (53057 / ((3↑7) · (5 · 7))) ∈ ℝ)
402129, 130, 401mp2an 695 . . . 4 (53057 / ((3↑7) · (5 · 7))) ∈ ℝ
403 nndivre 10734 . . . . 5 ((253 ∈ ℝ ∧ 365 ∈ ℕ) → (253 / 365) ∈ ℝ)
404397, 393, 403mp2an 695 . . . 4 (253 / 365) ∈ ℝ
405127, 402, 404lelttri 9846 . . 3 (((Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ≤ (53057 / ((3↑7) · (5 · 7))) ∧ (53057 / ((3↑7) · (5 · 7))) < (253 / 365)) → (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) < (253 / 365))
406136, 400, 405mp2an 695 . 2 𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) < (253 / 365)
40732, 127, 404lelttri 9846 . 2 (((log‘2) ≤ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) ∧ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1)) · (9↑4)))) < (253 / 365)) → (log‘2) < (253 / 365))
40852, 406, 407mp2an 695 1 (log‘2) < (253 / 365)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 191   ∧ wa 378   ∧ w3a 1021   = wceq 1468  ⊤wtru 1469   ∈ wcel 1937   class class class wbr 4434  ‘cfv 5633  (class class class)co 6363  ℂcc 9622  ℝcr 9623  0cc0 9624  1c1 9625   + caddc 9627   · cmul 9629   < clt 9760   ≤ cle 9761   − cmin 9947   / cdiv 10358  ℕcn 10698  2c2 10748  3c3 10749  4c4 10750  5c5 10751  6c6 10752  7c7 10753  8c8 10754  9c9 10755  10c10 10756  ℕ0cn0 10960  ;cdc 11141  ℝ+crp 11393  [,]cicc 11733  ...cfz 11880  ↑cexp 12386  Σcsu 13912  logclog 23665 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-rep 4548  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680  ax-un 6659  ax-inf2 8231  ax-cnex 9680  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-mulcom 9688  ax-addass 9689  ax-mulass 9690  ax-distr 9691  ax-i2m1 9692  ax-1ne0 9693  ax-1rid 9694  ax-rnegex 9695  ax-rrecex 9696  ax-cnre 9697  ax-pre-lttri 9698  ax-pre-lttrn 9699  ax-pre-ltadd 9700  ax-pre-mulgt0 9701  ax-pre-sup 9702  ax-addf 9703  ax-mulf 9704 This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3or 1022  df-3an 1023  df-tru 1471  df-fal 1474  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-nel 2678  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3758  df-if 3909  df-pw 3980  df-sn 3996  df-pr 3998  df-tp 4000  df-op 4002  df-uni 4229  df-int 4265  df-iun 4309  df-iin 4310  df-br 4435  df-opab 4494  df-mpt 4495  df-tr 4531  df-eprel 4791  df-id 4795  df-po 4801  df-so 4802  df-fr 4839  df-se 4840  df-we 4841  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-pred 5431  df-ord 5477  df-on 5478  df-lim 5479  df-suc 5480  df-iota 5597  df-fun 5635  df-fn 5636  df-f 5637  df-f1 5638  df-fo 5639  df-f1o 5640  df-fv 5641  df-isom 5642  df-riota 6325  df-ov 6366  df-oprab 6367  df-mpt2 6368  df-of 6607  df-om 6770  df-1st 6870  df-2nd 6871  df-supp 6994  df-wrecs 7105  df-recs 7167  df-rdg 7205  df-1o 7259  df-2o 7260  df-oadd 7263  df-er 7440  df-map 7557  df-pm 7558  df-ixp 7606  df-en 7653  df-dom 7654  df-sdom 7655  df-fin 7656  df-fsupp 7969  df-fi 8010  df-sup 8041  df-inf 8042  df-oi 8108  df-card 8458  df-cda 8683  df-pnf 9762  df-mnf 9763  df-xr 9764  df-ltxr 9765  df-le 9766  df-sub 9949  df-neg 9950  df-div 10359  df-nn 10699  df-2 10757  df-3 10758  df-4 10759  df-5 10760  df-6 10761  df-7 10762  df-8 10763  df-9 10764  df-10 10765  df-n0 10961  df-z 11029  df-dec 11142  df-uz 11250  df-q 11356  df-rp 11394  df-xneg 11500  df-xadd 11501  df-xmul 11502  df-ioo 11734  df-ioc 11735  df-ico 11736  df-icc 11737  df-fz 11881  df-fzo 12017  df-fl 12136  df-mod 12205  df-seq 12328  df-exp 12387  df-fac 12574  df-bc 12602  df-hash 12630  df-shft 13290  df-cj 13322  df-re 13323  df-im 13324  df-sqrt 13458  df-abs 13459  df-limsup 13686  df-clim 13712  df-rlim 13713  df-sum 13913  df-ef 14281  df-sin 14283  df-cos 14284  df-tan 14285  df-pi 14286  df-dvds 14466  df-struct 15284  df-ndx 15285  df-slot 15286  df-base 15287  df-sets 15288  df-ress 15289  df-plusg 15368  df-mulr 15369  df-starv 15370  df-sca 15371  df-vsca 15372  df-ip 15373  df-tset 15374  df-ple 15375  df-ds 15377  df-unif 15378  df-hom 15379  df-cco 15380  df-rest 15486  df-topn 15487  df-0g 15505  df-gsum 15506  df-topgen 15507  df-pt 15508  df-prds 15511  df-xrs 15565  df-qtop 15571  df-imas 15572  df-xps 15575  df-mre 15657  df-mrc 15658  df-acs 15660  df-mgm 16653  df-sgrp 16692  df-mnd 16702  df-submnd 16743  df-mulg 16836  df-cntz 17132  df-cmn 17593  df-psmet 19120  df-xmet 19121  df-met 19122  df-bl 19123  df-mopn 19124  df-fbas 19125  df-fg 19126  df-cnfld 19129  df-top 20079  df-bases 20080  df-topon 20081  df-topsp 20082  df-cld 20191  df-ntr 20192  df-cls 20193  df-nei 20271  df-lp 20309  df-perf 20310  df-cn 20400  df-cnp 20401  df-haus 20488  df-cmp 20559  df-tx 20734  df-hmeo 20927  df-fil 21019  df-fm 21111  df-flim 21112  df-flf 21113  df-xms 21493  df-ms 21494  df-tms 21495  df-cncf 22068  df-limc 22982  df-dv 22983  df-ulm 23493  df-log 23667  df-atan 23954 This theorem is referenced by:  log2le1  24037  birthday  24041
 Copyright terms: Public domain W3C validator