Proof of Theorem log2ub
Step | Hyp | Ref
| Expression |
1 | | 4m1e3 11848 |
. . . . . . . . 9
⊢ (4
− 1) = 3 |
2 | 1 | oveq2i 7184 |
. . . . . . . 8
⊢ (0...(4
− 1)) = (0...3) |
3 | 2 | sumeq1i 15151 |
. . . . . . 7
⊢
Σ𝑛 ∈
(0...(4 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) |
4 | 3 | oveq2i 7184 |
. . . . . 6
⊢
((log‘2) − Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛)))) =
((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) |
5 | | 4nn0 11998 |
. . . . . . 7
⊢ 4 ∈
ℕ0 |
6 | | log2tlbnd 25686 |
. . . . . . 7
⊢ (4 ∈
ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛))))
∈ (0[,](3 / ((4 · ((2 · 4) + 1)) ·
(9↑4))))) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
⊢
((log‘2) − Σ𝑛 ∈ (0...(4 − 1))(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛))))
∈ (0[,](3 / ((4 · ((2 · 4) + 1)) ·
(9↑4)))) |
8 | 4, 7 | eqeltrri 2831 |
. . . . 5
⊢
((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) ∈
(0[,](3 / ((4 · ((2 · 4) + 1)) ·
(9↑4)))) |
9 | | 0re 10724 |
. . . . . 6
⊢ 0 ∈
ℝ |
10 | | 3re 11799 |
. . . . . . 7
⊢ 3 ∈
ℝ |
11 | | 4nn 11802 |
. . . . . . . . 9
⊢ 4 ∈
ℕ |
12 | | 2nn0 11996 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
13 | | 1nn 11730 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ |
14 | 12, 5, 13 | numnncl 12192 |
. . . . . . . . 9
⊢ ((2
· 4) + 1) ∈ ℕ |
15 | 11, 14 | nnmulcli 11744 |
. . . . . . . 8
⊢ (4
· ((2 · 4) + 1)) ∈ ℕ |
16 | | 9nn 11817 |
. . . . . . . . 9
⊢ 9 ∈
ℕ |
17 | | nnexpcl 13537 |
. . . . . . . . 9
⊢ ((9
∈ ℕ ∧ 4 ∈ ℕ0) → (9↑4) ∈
ℕ) |
18 | 16, 5, 17 | mp2an 692 |
. . . . . . . 8
⊢
(9↑4) ∈ ℕ |
19 | 15, 18 | nnmulcli 11744 |
. . . . . . 7
⊢ ((4
· ((2 · 4) + 1)) · (9↑4)) ∈
ℕ |
20 | | nndivre 11760 |
. . . . . . 7
⊢ ((3
∈ ℝ ∧ ((4 · ((2 · 4) + 1)) · (9↑4))
∈ ℕ) → (3 / ((4 · ((2 · 4) + 1)) ·
(9↑4))) ∈ ℝ) |
21 | 10, 19, 20 | mp2an 692 |
. . . . . 6
⊢ (3 / ((4
· ((2 · 4) + 1)) · (9↑4))) ∈
ℝ |
22 | 9, 21 | elicc2i 12890 |
. . . . 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))))) |
23 | 8, 22 | mpbi 233 |
. . . 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)))) |
24 | 23 | simp3i 1142 |
. . 3
⊢
((log‘2) − Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) ≤ (3 / ((4
· ((2 · 4) + 1)) · (9↑4))) |
25 | | 2rp 12480 |
. . . . 5
⊢ 2 ∈
ℝ+ |
26 | | relogcl 25322 |
. . . . 5
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢
(log‘2) ∈ ℝ |
28 | | fzfid 13435 |
. . . . . 6
⊢ (⊤
→ (0...3) ∈ Fin) |
29 | | 2re 11793 |
. . . . . . 7
⊢ 2 ∈
ℝ |
30 | | 3nn 11798 |
. . . . . . . . 9
⊢ 3 ∈
ℕ |
31 | | elfznn0 13094 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (0...3) → 𝑛 ∈
ℕ0) |
32 | 31 | adantl 485 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → 𝑛
∈ ℕ0) |
33 | | nn0mulcl 12015 |
. . . . . . . . . . 11
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
34 | 12, 32, 33 | sylancr 590 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → (2 · 𝑛) ∈
ℕ0) |
35 | | nn0p1nn 12018 |
. . . . . . . . . 10
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → ((2 · 𝑛) + 1) ∈ ℕ) |
37 | | nnmulcl 11743 |
. . . . . . . . 9
⊢ ((3
∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2
· 𝑛) + 1)) ∈
ℕ) |
38 | 30, 36, 37 | sylancr 590 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ) |
39 | | nnexpcl 13537 |
. . . . . . . . 9
⊢ ((9
∈ ℕ ∧ 𝑛
∈ ℕ0) → (9↑𝑛) ∈ ℕ) |
40 | 16, 32, 39 | sylancr 590 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → (9↑𝑛) ∈ ℕ) |
41 | 38, 40 | nnmulcld 11772 |
. . . . . . 7
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) |
42 | | nndivre 11760 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛)))
∈ ℝ) |
43 | 29, 41, 42 | sylancr 590 |
. . . . . 6
⊢
((⊤ ∧ 𝑛
∈ (0...3)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ) |
44 | 28, 43 | fsumrecl 15187 |
. . . . 5
⊢ (⊤
→ Σ𝑛 ∈
(0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ) |
45 | 44 | mptru 1549 |
. . . 4
⊢
Σ𝑛 ∈
(0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ |
46 | 27, 45, 21 | lesubadd2i 11281 |
. . 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))))) |
47 | 24, 46 | mpbi 233 |
. 2
⊢
(log‘2) ≤ (Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) + (3 / ((4
· ((2 · 4) + 1)) · (9↑4)))) |
48 | | log2ublem3 25689 |
. . . . 5
⊢
(((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) ≤ ;;;;53056 |
49 | | 3nn0 11997 |
. . . . 5
⊢ 3 ∈
ℕ0 |
50 | | 5nn0 11999 |
. . . . . . . . 9
⊢ 5 ∈
ℕ0 |
51 | 50, 49 | deccl 12197 |
. . . . . . . 8
⊢ ;53 ∈
ℕ0 |
52 | | 0nn0 11994 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
53 | 51, 52 | deccl 12197 |
. . . . . . 7
⊢ ;;530 ∈ ℕ0 |
54 | 53, 50 | deccl 12197 |
. . . . . 6
⊢ ;;;5305
∈ ℕ0 |
55 | | 6nn0 12000 |
. . . . . 6
⊢ 6 ∈
ℕ0 |
56 | 54, 55 | deccl 12197 |
. . . . 5
⊢ ;;;;53056 ∈
ℕ0 |
57 | | 1nn0 11995 |
. . . . 5
⊢ 1 ∈
ℕ0 |
58 | | eqid 2739 |
. . . . 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)))) |
59 | | 6p1e7 11867 |
. . . . . 6
⊢ (6 + 1) =
7 |
60 | | eqid 2739 |
. . . . . 6
⊢ ;;;;53056 = ;;;;53056 |
61 | 54, 55, 59, 60 | decsuc 12213 |
. . . . 5
⊢ (;;;;53056 + 1) = ;;;;53057 |
62 | | 5nn 11805 |
. . . . . . . . . 10
⊢ 5 ∈
ℕ |
63 | | 7nn 11811 |
. . . . . . . . . 10
⊢ 7 ∈
ℕ |
64 | 62, 63 | nnmulcli 11744 |
. . . . . . . . 9
⊢ (5
· 7) ∈ ℕ |
65 | 64 | nnrei 11728 |
. . . . . . . 8
⊢ (5
· 7) ∈ ℝ |
66 | 15 | nnrei 11728 |
. . . . . . . 8
⊢ (4
· ((2 · 4) + 1)) ∈ ℝ |
67 | | 6nn 11808 |
. . . . . . . . . 10
⊢ 6 ∈
ℕ |
68 | | 5lt6 11900 |
. . . . . . . . . 10
⊢ 5 <
6 |
69 | 49, 50, 67, 68 | declt 12210 |
. . . . . . . . 9
⊢ ;35 < ;36 |
70 | | 7cn 11813 |
. . . . . . . . . 10
⊢ 7 ∈
ℂ |
71 | | 5cn 11807 |
. . . . . . . . . 10
⊢ 5 ∈
ℂ |
72 | | 7t5e35 12294 |
. . . . . . . . . 10
⊢ (7
· 5) = ;35 |
73 | 70, 71, 72 | mulcomli 10731 |
. . . . . . . . 9
⊢ (5
· 7) = ;35 |
74 | | 4cn 11804 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℂ |
75 | | 2cn 11794 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
76 | | 4t2e8 11887 |
. . . . . . . . . . . . . 14
⊢ (4
· 2) = 8 |
77 | 74, 75, 76 | mulcomli 10731 |
. . . . . . . . . . . . 13
⊢ (2
· 4) = 8 |
78 | 77 | oveq1i 7183 |
. . . . . . . . . . . 12
⊢ ((2
· 4) + 1) = (8 + 1) |
79 | | 8p1e9 11869 |
. . . . . . . . . . . 12
⊢ (8 + 1) =
9 |
80 | 78, 79 | eqtri 2762 |
. . . . . . . . . . 11
⊢ ((2
· 4) + 1) = 9 |
81 | 80 | oveq2i 7184 |
. . . . . . . . . 10
⊢ (4
· ((2 · 4) + 1)) = (4 · 9) |
82 | | 9cn 11819 |
. . . . . . . . . . 11
⊢ 9 ∈
ℂ |
83 | | 9t4e36 12306 |
. . . . . . . . . . 11
⊢ (9
· 4) = ;36 |
84 | 82, 74, 83 | mulcomli 10731 |
. . . . . . . . . 10
⊢ (4
· 9) = ;36 |
85 | 81, 84 | eqtri 2762 |
. . . . . . . . 9
⊢ (4
· ((2 · 4) + 1)) = ;36 |
86 | 69, 73, 85 | 3brtr4i 5061 |
. . . . . . . 8
⊢ (5
· 7) < (4 · ((2 · 4) + 1)) |
87 | 65, 66, 86 | ltleii 10844 |
. . . . . . 7
⊢ (5
· 7) ≤ (4 · ((2 · 4) + 1)) |
88 | 18 | nngt0i 11758 |
. . . . . . . 8
⊢ 0 <
(9↑4) |
89 | 18 | nnrei 11728 |
. . . . . . . . 9
⊢
(9↑4) ∈ ℝ |
90 | 65, 66, 89 | lemul2i 11644 |
. . . . . . . 8
⊢ (0 <
(9↑4) → ((5 · 7) ≤ (4 · ((2 · 4) + 1)) ↔
((9↑4) · (5 · 7)) ≤ ((9↑4) · (4 · ((2
· 4) + 1))))) |
91 | 88, 90 | ax-mp 5 |
. . . . . . 7
⊢ ((5
· 7) ≤ (4 · ((2 · 4) + 1)) ↔ ((9↑4) ·
(5 · 7)) ≤ ((9↑4) · (4 · ((2 · 4) +
1)))) |
92 | 87, 91 | mpbi 233 |
. . . . . 6
⊢
((9↑4) · (5 · 7)) ≤ ((9↑4) · (4
· ((2 · 4) + 1))) |
93 | | 7nn0 12001 |
. . . . . . . . . 10
⊢ 7 ∈
ℕ0 |
94 | | nnexpcl 13537 |
. . . . . . . . . 10
⊢ ((3
∈ ℕ ∧ 7 ∈ ℕ0) → (3↑7) ∈
ℕ) |
95 | 30, 93, 94 | mp2an 692 |
. . . . . . . . 9
⊢
(3↑7) ∈ ℕ |
96 | 95 | nncni 11729 |
. . . . . . . 8
⊢
(3↑7) ∈ ℂ |
97 | 64 | nncni 11729 |
. . . . . . . 8
⊢ (5
· 7) ∈ ℂ |
98 | | 3cn 11800 |
. . . . . . . 8
⊢ 3 ∈
ℂ |
99 | 96, 97, 98 | mul32i 10917 |
. . . . . . 7
⊢
(((3↑7) · (5 · 7)) · 3) = (((3↑7)
· 3) · (5 · 7)) |
100 | 74, 75 | mulcomi 10730 |
. . . . . . . . . . . 12
⊢ (4
· 2) = (2 · 4) |
101 | | df-8 11788 |
. . . . . . . . . . . 12
⊢ 8 = (7 +
1) |
102 | 76, 100, 101 | 3eqtr3i 2770 |
. . . . . . . . . . 11
⊢ (2
· 4) = (7 + 1) |
103 | 102 | oveq2i 7184 |
. . . . . . . . . 10
⊢
(3↑(2 · 4)) = (3↑(7 + 1)) |
104 | | expmul 13569 |
. . . . . . . . . . 11
⊢ ((3
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 4 ∈
ℕ0) → (3↑(2 · 4)) =
((3↑2)↑4)) |
105 | 98, 12, 5, 104 | mp3an 1462 |
. . . . . . . . . 10
⊢
(3↑(2 · 4)) = ((3↑2)↑4) |
106 | 103, 105 | eqtr3i 2764 |
. . . . . . . . 9
⊢
(3↑(7 + 1)) = ((3↑2)↑4) |
107 | | expp1 13531 |
. . . . . . . . . 10
⊢ ((3
∈ ℂ ∧ 7 ∈ ℕ0) → (3↑(7 + 1)) =
((3↑7) · 3)) |
108 | 98, 93, 107 | mp2an 692 |
. . . . . . . . 9
⊢
(3↑(7 + 1)) = ((3↑7) · 3) |
109 | | sq3 13656 |
. . . . . . . . . 10
⊢
(3↑2) = 9 |
110 | 109 | oveq1i 7183 |
. . . . . . . . 9
⊢
((3↑2)↑4) = (9↑4) |
111 | 106, 108,
110 | 3eqtr3i 2770 |
. . . . . . . 8
⊢
((3↑7) · 3) = (9↑4) |
112 | 111 | oveq1i 7183 |
. . . . . . 7
⊢
(((3↑7) · 3) · (5 · 7)) = ((9↑4) ·
(5 · 7)) |
113 | 99, 112 | eqtri 2762 |
. . . . . 6
⊢
(((3↑7) · (5 · 7)) · 3) = ((9↑4) ·
(5 · 7)) |
114 | 15 | nncni 11729 |
. . . . . . . . 9
⊢ (4
· ((2 · 4) + 1)) ∈ ℂ |
115 | 18 | nncni 11729 |
. . . . . . . . 9
⊢
(9↑4) ∈ ℂ |
116 | 114, 115 | mulcomi 10730 |
. . . . . . . 8
⊢ ((4
· ((2 · 4) + 1)) · (9↑4)) = ((9↑4) · (4
· ((2 · 4) + 1))) |
117 | 116 | oveq1i 7183 |
. . . . . . 7
⊢ (((4
· ((2 · 4) + 1)) · (9↑4)) · 1) = (((9↑4)
· (4 · ((2 · 4) + 1))) · 1) |
118 | 115, 114 | mulcli 10729 |
. . . . . . . 8
⊢
((9↑4) · (4 · ((2 · 4) + 1))) ∈
ℂ |
119 | 118 | mulid1i 10726 |
. . . . . . 7
⊢
(((9↑4) · (4 · ((2 · 4) + 1))) · 1) =
((9↑4) · (4 · ((2 · 4) + 1))) |
120 | 117, 119 | eqtri 2762 |
. . . . . 6
⊢ (((4
· ((2 · 4) + 1)) · (9↑4)) · 1) = ((9↑4)
· (4 · ((2 · 4) + 1))) |
121 | 92, 113, 120 | 3brtr4i 5061 |
. . . . 5
⊢
(((3↑7) · (5 · 7)) · 3) ≤ (((4 · ((2
· 4) + 1)) · (9↑4)) · 1) |
122 | 48, 45, 49, 19, 56, 57, 58, 61, 121 | log2ublem1 25687 |
. . . 4
⊢
(((3↑7) · (5 · 7)) · (Σ𝑛 ∈ (0...3)(2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛))) + (3
/ ((4 · ((2 · 4) + 1)) · (9↑4))))) ≤ ;;;;53057 |
123 | 45, 21 | readdcli 10737 |
. . . . 5
⊢
(Σ𝑛 ∈
(0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1))
· (9↑4)))) ∈ ℝ |
124 | 54, 93 | deccl 12197 |
. . . . . 6
⊢ ;;;;53057 ∈
ℕ0 |
125 | 124 | nn0rei 11990 |
. . . . 5
⊢ ;;;;53057 ∈ ℝ |
126 | 95, 64 | nnmulcli 11744 |
. . . . . . 7
⊢
((3↑7) · (5 · 7)) ∈ ℕ |
127 | 126 | nnrei 11728 |
. . . . . 6
⊢
((3↑7) · (5 · 7)) ∈ ℝ |
128 | 126 | nngt0i 11758 |
. . . . . 6
⊢ 0 <
((3↑7) · (5 · 7)) |
129 | 127, 128 | pm3.2i 474 |
. . . . 5
⊢
(((3↑7) · (5 · 7)) ∈ ℝ ∧ 0 <
((3↑7) · (5 · 7))) |
130 | | lemuldiv2 11602 |
. . . . 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))))) |
131 | 123, 125,
129, 130 | mp3an 1462 |
. . . 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)))) |
132 | 122, 131 | mpbi 233 |
. . 3
⊢
(Σ𝑛 ∈
(0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1))
· (9↑4)))) ≤ (;;;;53057 / ((3↑7) · (5 ·
7))) |
133 | | 8nn0 12002 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℕ0 |
134 | 49, 133 | deccl 12197 |
. . . . . . . . . . . 12
⊢ ;38 ∈
ℕ0 |
135 | 134, 93 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;;387 ∈ ℕ0 |
136 | 135, 49 | deccl 12197 |
. . . . . . . . . 10
⊢ ;;;3873
∈ ℕ0 |
137 | 136, 57 | deccl 12197 |
. . . . . . . . 9
⊢ ;;;;38731 ∈
ℕ0 |
138 | 137, 55 | deccl 12197 |
. . . . . . . 8
⊢ ;;;;;387316 ∈ ℕ0 |
139 | 137, 93 | deccl 12197 |
. . . . . . . 8
⊢ ;;;;;387317 ∈ ℕ0 |
140 | | 1lt10 12321 |
. . . . . . . 8
⊢ 1 <
;10 |
141 | | 6lt7 11905 |
. . . . . . . . 9
⊢ 6 <
7 |
142 | 137, 55, 63, 141 | declt 12210 |
. . . . . . . 8
⊢ ;;;;;387316 < ;;;;;387317 |
143 | 138, 139,
57, 93, 140, 142 | decltc 12211 |
. . . . . . 7
⊢ ;;;;;;3873161 < ;;;;;;3873177 |
144 | | eqid 2739 |
. . . . . . . 8
⊢ ;73 = ;73 |
145 | 57, 50 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;15 ∈
ℕ0 |
146 | | 9nn0 12003 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ0 |
147 | 145, 146 | deccl 12197 |
. . . . . . . . . 10
⊢ ;;159 ∈ ℕ0 |
148 | 147, 57 | deccl 12197 |
. . . . . . . . 9
⊢ ;;;1591
∈ ℕ0 |
149 | 148, 93 | deccl 12197 |
. . . . . . . 8
⊢ ;;;;15917 ∈
ℕ0 |
150 | | eqid 2739 |
. . . . . . . . 9
⊢ ;;;;53057 = ;;;;53057 |
151 | | eqid 2739 |
. . . . . . . . 9
⊢ ;;;;15917 = ;;;;15917 |
152 | | eqid 2739 |
. . . . . . . . . 10
⊢ ;;;5305 =
;;;5305 |
153 | | eqid 2739 |
. . . . . . . . . . 11
⊢ ;;;1591 =
;;;1591 |
154 | | ax-1cn 10676 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
155 | | 5p1e6 11866 |
. . . . . . . . . . . 12
⊢ (5 + 1) =
6 |
156 | 71, 154, 155 | addcomli 10913 |
. . . . . . . . . . 11
⊢ (1 + 5) =
6 |
157 | 147, 57, 50, 153, 156 | decaddi 12242 |
. . . . . . . . . 10
⊢ (;;;1591 +
5) = ;;;1596 |
158 | 57, 55 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;16 ∈
ℕ0 |
159 | | eqid 2739 |
. . . . . . . . . . 11
⊢ ;;530 = ;;530 |
160 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;;159 = ;;159 |
161 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ ;15 = ;15 |
162 | 57, 50, 155, 161 | decsuc 12213 |
. . . . . . . . . . . 12
⊢ (;15 + 1) = ;16 |
163 | | 9p4e13 12271 |
. . . . . . . . . . . 12
⊢ (9 + 4) =
;13 |
164 | 145, 146,
5, 160, 162, 49, 163 | decaddci 12243 |
. . . . . . . . . . 11
⊢ (;;159 + 4) = ;;163 |
165 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;53 = ;53 |
166 | 158 | nn0cni 11991 |
. . . . . . . . . . . . 13
⊢ ;16 ∈ ℂ |
167 | 166 | addid1i 10908 |
. . . . . . . . . . . 12
⊢ (;16 + 0) = ;16 |
168 | | 1p2e3 11862 |
. . . . . . . . . . . . . 14
⊢ (1 + 2) =
3 |
169 | 168 | oveq2i 7184 |
. . . . . . . . . . . . 13
⊢ ((5
· 7) + (1 + 2)) = ((5 · 7) + 3) |
170 | | 5p3e8 11876 |
. . . . . . . . . . . . . 14
⊢ (5 + 3) =
8 |
171 | 49, 50, 49, 73, 170 | decaddi 12242 |
. . . . . . . . . . . . 13
⊢ ((5
· 7) + 3) = ;38 |
172 | 169, 171 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((5
· 7) + (1 + 2)) = ;38 |
173 | | 7t3e21 12292 |
. . . . . . . . . . . . . 14
⊢ (7
· 3) = ;21 |
174 | 70, 98, 173 | mulcomli 10731 |
. . . . . . . . . . . . 13
⊢ (3
· 7) = ;21 |
175 | | 6cn 11810 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℂ |
176 | 175, 154,
59 | addcomli 10913 |
. . . . . . . . . . . . 13
⊢ (1 + 6) =
7 |
177 | 12, 57, 55, 174, 176 | decaddi 12242 |
. . . . . . . . . . . 12
⊢ ((3
· 7) + 6) = ;27 |
178 | 50, 49, 57, 55, 165, 167, 93, 93, 12, 172, 177 | decmac 12234 |
. . . . . . . . . . 11
⊢ ((;53 · 7) + (;16 + 0)) = ;;387 |
179 | 70 | mul02i 10910 |
. . . . . . . . . . . . 13
⊢ (0
· 7) = 0 |
180 | 179 | oveq1i 7183 |
. . . . . . . . . . . 12
⊢ ((0
· 7) + 3) = (0 + 3) |
181 | 98 | addid2i 10909 |
. . . . . . . . . . . . 13
⊢ (0 + 3) =
3 |
182 | 49 | dec0h 12204 |
. . . . . . . . . . . . 13
⊢ 3 = ;03 |
183 | 181, 182 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ (0 + 3) =
;03 |
184 | 180, 183 | eqtri 2762 |
. . . . . . . . . . 11
⊢ ((0
· 7) + 3) = ;03 |
185 | 51, 52, 158, 49, 159, 164, 93, 49, 52, 178, 184 | decmac 12234 |
. . . . . . . . . 10
⊢ ((;;530 · 7) + (;;159 +
4)) = ;;;3873 |
186 | | 3p1e4 11864 |
. . . . . . . . . . 11
⊢ (3 + 1) =
4 |
187 | | 6p5e11 12255 |
. . . . . . . . . . . 12
⊢ (6 + 5) =
;11 |
188 | 175, 71, 187 | addcomli 10913 |
. . . . . . . . . . 11
⊢ (5 + 6) =
;11 |
189 | 49, 50, 55, 73, 186, 57, 188 | decaddci 12243 |
. . . . . . . . . 10
⊢ ((5
· 7) + 6) = ;41 |
190 | 53, 50, 147, 55, 152, 157, 93, 57, 5, 185, 189 | decmac 12234 |
. . . . . . . . 9
⊢ ((;;;5305
· 7) + (;;;1591 +
5)) = ;;;;38731 |
191 | | 7t7e49 12296 |
. . . . . . . . . 10
⊢ (7
· 7) = ;49 |
192 | | 4p1e5 11865 |
. . . . . . . . . 10
⊢ (4 + 1) =
5 |
193 | | 9p7e16 12274 |
. . . . . . . . . 10
⊢ (9 + 7) =
;16 |
194 | 5, 146, 93, 191, 192, 55, 193 | decaddci 12243 |
. . . . . . . . 9
⊢ ((7
· 7) + 7) = ;56 |
195 | 54, 93, 148, 93, 150, 151, 93, 55, 50, 190, 194 | decmac 12234 |
. . . . . . . 8
⊢ ((;;;;53057 · 7) + ;;;;15917) = ;;;;;387316 |
196 | 12 | dec0h 12204 |
. . . . . . . . . 10
⊢ 2 = ;02 |
197 | 154 | addid2i 10909 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
198 | 57 | dec0h 12204 |
. . . . . . . . . . . 12
⊢ 1 = ;01 |
199 | 197, 198 | eqtri 2762 |
. . . . . . . . . . 11
⊢ (0 + 1) =
;01 |
200 | | 00id 10896 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
201 | 52 | dec0h 12204 |
. . . . . . . . . . . . 13
⊢ 0 = ;00 |
202 | 200, 201 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ (0 + 0) =
;00 |
203 | | 5t3e15 12283 |
. . . . . . . . . . . . . 14
⊢ (5
· 3) = ;15 |
204 | 203 | oveq1i 7183 |
. . . . . . . . . . . . 13
⊢ ((5
· 3) + 0) = (;15 +
0) |
205 | 145 | nn0cni 11991 |
. . . . . . . . . . . . . 14
⊢ ;15 ∈ ℂ |
206 | 205 | addid1i 10908 |
. . . . . . . . . . . . 13
⊢ (;15 + 0) = ;15 |
207 | 204, 206 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((5
· 3) + 0) = ;15 |
208 | | 3t3e9 11886 |
. . . . . . . . . . . . . 14
⊢ (3
· 3) = 9 |
209 | 208 | oveq1i 7183 |
. . . . . . . . . . . . 13
⊢ ((3
· 3) + 0) = (9 + 0) |
210 | 82 | addid1i 10908 |
. . . . . . . . . . . . 13
⊢ (9 + 0) =
9 |
211 | 209, 210 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((3
· 3) + 0) = 9 |
212 | 50, 49, 52, 52, 165, 202, 49, 207, 211 | decma 12233 |
. . . . . . . . . . 11
⊢ ((;53 · 3) + (0 + 0)) = ;;159 |
213 | 98 | mul02i 10910 |
. . . . . . . . . . . . 13
⊢ (0
· 3) = 0 |
214 | 213 | oveq1i 7183 |
. . . . . . . . . . . 12
⊢ ((0
· 3) + 1) = (0 + 1) |
215 | 214, 199 | eqtri 2762 |
. . . . . . . . . . 11
⊢ ((0
· 3) + 1) = ;01 |
216 | 51, 52, 52, 57, 159, 199, 49, 57, 52, 212, 215 | decmac 12234 |
. . . . . . . . . 10
⊢ ((;;530 · 3) + (0 + 1)) = ;;;1591 |
217 | | 5p2e7 11875 |
. . . . . . . . . . 11
⊢ (5 + 2) =
7 |
218 | 57, 50, 12, 203, 217 | decaddi 12242 |
. . . . . . . . . 10
⊢ ((5
· 3) + 2) = ;17 |
219 | 53, 50, 52, 12, 152, 196, 49, 93, 57, 216, 218 | decmac 12234 |
. . . . . . . . 9
⊢ ((;;;5305
· 3) + 2) = ;;;;15917 |
220 | 49, 54, 93, 150, 57, 12, 219, 173 | decmul1c 12247 |
. . . . . . . 8
⊢ (;;;;53057 · 3) = ;;;;;159171 |
221 | 124, 93, 49, 144, 57, 149, 195, 220 | decmul2c 12248 |
. . . . . . 7
⊢ (;;;;53057 · ;73) = ;;;;;;3873161 |
222 | 50, 50 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;55 ∈
ℕ0 |
223 | 222, 49 | deccl 12197 |
. . . . . . . . . 10
⊢ ;;553 ∈ ℕ0 |
224 | 223, 49 | deccl 12197 |
. . . . . . . . 9
⊢ ;;;5533
∈ ℕ0 |
225 | 224, 57 | deccl 12197 |
. . . . . . . 8
⊢ ;;;;55331 ∈
ℕ0 |
226 | 12, 50 | deccl 12197 |
. . . . . . . . . 10
⊢ ;25 ∈
ℕ0 |
227 | 226, 49 | deccl 12197 |
. . . . . . . . 9
⊢ ;;253 ∈ ℕ0 |
228 | 12, 57 | deccl 12197 |
. . . . . . . . . 10
⊢ ;21 ∈
ℕ0 |
229 | 228, 133 | deccl 12197 |
. . . . . . . . 9
⊢ ;;218 ∈ ℕ0 |
230 | 93, 12 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;72 ∈
ℕ0 |
231 | | 3t2e6 11885 |
. . . . . . . . . . . . 13
⊢ (3
· 2) = 6 |
232 | 98, 75, 231 | mulcomli 10731 |
. . . . . . . . . . . 12
⊢ (2
· 3) = 6 |
233 | | 3exp3 16531 |
. . . . . . . . . . . 12
⊢
(3↑3) = ;27 |
234 | 12, 93 | deccl 12197 |
. . . . . . . . . . . . 13
⊢ ;27 ∈
ℕ0 |
235 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ ;27 = ;27 |
236 | 57, 133 | deccl 12197 |
. . . . . . . . . . . . 13
⊢ ;18 ∈
ℕ0 |
237 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ ;18 = ;18 |
238 | | 2t2e4 11883 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 2) = 4 |
239 | 238, 168 | oveq12i 7185 |
. . . . . . . . . . . . . . 15
⊢ ((2
· 2) + (1 + 2)) = (4 + 3) |
240 | | 4p3e7 11873 |
. . . . . . . . . . . . . . 15
⊢ (4 + 3) =
7 |
241 | 239, 240 | eqtri 2762 |
. . . . . . . . . . . . . 14
⊢ ((2
· 2) + (1 + 2)) = 7 |
242 | | 7t2e14 12291 |
. . . . . . . . . . . . . . 15
⊢ (7
· 2) = ;14 |
243 | | 1p1e2 11844 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
2 |
244 | | 8cn 11816 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℂ |
245 | | 8p4e12 12264 |
. . . . . . . . . . . . . . . 16
⊢ (8 + 4) =
;12 |
246 | 244, 74, 245 | addcomli 10913 |
. . . . . . . . . . . . . . 15
⊢ (4 + 8) =
;12 |
247 | 57, 5, 133, 242, 243, 12, 246 | decaddci 12243 |
. . . . . . . . . . . . . 14
⊢ ((7
· 2) + 8) = ;22 |
248 | 12, 93, 57, 133, 235, 237, 12, 12, 12, 241, 247 | decmac 12234 |
. . . . . . . . . . . . 13
⊢ ((;27 · 2) + ;18) = ;72 |
249 | 70, 75, 242 | mulcomli 10731 |
. . . . . . . . . . . . . . 15
⊢ (2
· 7) = ;14 |
250 | | 4p4e8 11874 |
. . . . . . . . . . . . . . 15
⊢ (4 + 4) =
8 |
251 | 57, 5, 5, 249, 250 | decaddi 12242 |
. . . . . . . . . . . . . 14
⊢ ((2
· 7) + 4) = ;18 |
252 | 93, 12, 93, 235, 146, 5, 251, 191 | decmul1c 12247 |
. . . . . . . . . . . . 13
⊢ (;27 · 7) = ;;189 |
253 | 234, 12, 93, 235, 146, 236, 248, 252 | decmul2c 12248 |
. . . . . . . . . . . 12
⊢ (;27 · ;27) = ;;729 |
254 | 49, 49, 232, 233, 253 | numexp2x 16518 |
. . . . . . . . . . 11
⊢
(3↑6) = ;;729 |
255 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;72 = ;72 |
256 | 232 | oveq1i 7183 |
. . . . . . . . . . . . 13
⊢ ((2
· 3) + 2) = (6 + 2) |
257 | | 6p2e8 11878 |
. . . . . . . . . . . . 13
⊢ (6 + 2) =
8 |
258 | 256, 257 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((2
· 3) + 2) = 8 |
259 | 93, 12, 12, 255, 49, 173, 258 | decrmanc 12239 |
. . . . . . . . . . 11
⊢ ((;72 · 3) + 2) = ;;218 |
260 | | 9t3e27 12305 |
. . . . . . . . . . 11
⊢ (9
· 3) = ;27 |
261 | 49, 230, 146, 254, 93, 12, 259, 260 | decmul1c 12247 |
. . . . . . . . . 10
⊢
((3↑6) · 3) = ;;;2187 |
262 | 49, 55, 59, 261 | numexpp1 16517 |
. . . . . . . . 9
⊢
(3↑7) = ;;;2187 |
263 | 57, 93 | deccl 12197 |
. . . . . . . . . 10
⊢ ;17 ∈
ℕ0 |
264 | 263, 93 | deccl 12197 |
. . . . . . . . 9
⊢ ;;177 ∈ ℕ0 |
265 | | eqid 2739 |
. . . . . . . . . 10
⊢ ;;218 = ;;218 |
266 | | eqid 2739 |
. . . . . . . . . 10
⊢ ;;177 = ;;177 |
267 | 12, 52 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;20 ∈
ℕ0 |
268 | 267, 49 | deccl 12197 |
. . . . . . . . . 10
⊢ ;;203 ∈ ℕ0 |
269 | 12, 12 | deccl 12197 |
. . . . . . . . . . 11
⊢ ;22 ∈
ℕ0 |
270 | | eqid 2739 |
. . . . . . . . . . 11
⊢ ;21 = ;21 |
271 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;17 = ;17 |
272 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;;203 = ;;203 |
273 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ ;20 = ;20 |
274 | 75 | addid2i 10909 |
. . . . . . . . . . . . . 14
⊢ (0 + 2) =
2 |
275 | 154 | addid1i 10908 |
. . . . . . . . . . . . . 14
⊢ (1 + 0) =
1 |
276 | 52, 57, 12, 52, 198, 273, 274, 275 | decadd 12236 |
. . . . . . . . . . . . 13
⊢ (1 +
;20) = ;21 |
277 | 12, 57, 243, 276 | decsuc 12213 |
. . . . . . . . . . . 12
⊢ ((1 +
;20) + 1) = ;22 |
278 | | 7p3e10 12257 |
. . . . . . . . . . . 12
⊢ (7 + 3) =
;10 |
279 | 57, 93, 267, 49, 271, 272, 277, 278 | decaddc2 12238 |
. . . . . . . . . . 11
⊢ (;17 + ;;203) =
;;220 |
280 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;;253 = ;;253 |
281 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ ;22 = ;22 |
282 | | eqid 2739 |
. . . . . . . . . . . . 13
⊢ ;25 = ;25 |
283 | | 2p2e4 11854 |
. . . . . . . . . . . . 13
⊢ (2 + 2) =
4 |
284 | 71, 75, 217 | addcomli 10913 |
. . . . . . . . . . . . 13
⊢ (2 + 5) =
7 |
285 | 12, 12, 12, 50, 281, 282, 283, 284 | decadd 12236 |
. . . . . . . . . . . 12
⊢ (;22 + ;25) = ;47 |
286 | 50 | dec0h 12204 |
. . . . . . . . . . . . . 14
⊢ 5 = ;05 |
287 | 192, 286 | eqtri 2762 |
. . . . . . . . . . . . 13
⊢ (4 + 1) =
;05 |
288 | 238, 197 | oveq12i 7185 |
. . . . . . . . . . . . . 14
⊢ ((2
· 2) + (0 + 1)) = (4 + 1) |
289 | 288, 192 | eqtri 2762 |
. . . . . . . . . . . . 13
⊢ ((2
· 2) + (0 + 1)) = 5 |
290 | | 5t2e10 12282 |
. . . . . . . . . . . . . 14
⊢ (5
· 2) = ;10 |
291 | 71 | addid2i 10909 |
. . . . . . . . . . . . . 14
⊢ (0 + 5) =
5 |
292 | 57, 52, 50, 290, 291 | decaddi 12242 |
. . . . . . . . . . . . 13
⊢ ((5
· 2) + 5) = ;15 |
293 | 12, 50, 52, 50, 282, 287, 12, 50, 57, 289, 292 | decmac 12234 |
. . . . . . . . . . . 12
⊢ ((;25 · 2) + (4 + 1)) = ;55 |
294 | 231 | oveq1i 7183 |
. . . . . . . . . . . . 13
⊢ ((3
· 2) + 7) = (6 + 7) |
295 | | 7p6e13 12260 |
. . . . . . . . . . . . . 14
⊢ (7 + 6) =
;13 |
296 | 70, 175, 295 | addcomli 10913 |
. . . . . . . . . . . . 13
⊢ (6 + 7) =
;13 |
297 | 294, 296 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((3
· 2) + 7) = ;13 |
298 | 226, 49, 5, 93, 280, 285, 12, 49, 57, 293, 297 | decmac 12234 |
. . . . . . . . . . 11
⊢ ((;;253 · 2) + (;22 + ;25)) = ;;553 |
299 | 227 | nn0cni 11991 |
. . . . . . . . . . . . . 14
⊢ ;;253 ∈ ℂ |
300 | 299 | mulid1i 10726 |
. . . . . . . . . . . . 13
⊢ (;;253 · 1) = ;;253 |
301 | 300 | oveq1i 7183 |
. . . . . . . . . . . 12
⊢ ((;;253 · 1) + 0) = (;;253 +
0) |
302 | 299 | addid1i 10908 |
. . . . . . . . . . . 12
⊢ (;;253 + 0) = ;;253 |
303 | 301, 302 | eqtri 2762 |
. . . . . . . . . . 11
⊢ ((;;253 · 1) + 0) = ;;253 |
304 | 12, 57, 269, 52, 270, 279, 227, 49, 226, 298, 303 | decma2c 12235 |
. . . . . . . . . 10
⊢ ((;;253 · ;21) + (;17 + ;;203))
= ;;;5533 |
305 | 93 | dec0h 12204 |
. . . . . . . . . . 11
⊢ 7 = ;07 |
306 | 74 | addid2i 10909 |
. . . . . . . . . . . . . 14
⊢ (0 + 4) =
4 |
307 | 306 | oveq2i 7184 |
. . . . . . . . . . . . 13
⊢ ((2
· 8) + (0 + 4)) = ((2 · 8) + 4) |
308 | | 8t2e16 12297 |
. . . . . . . . . . . . . . 15
⊢ (8
· 2) = ;16 |
309 | 244, 75, 308 | mulcomli 10731 |
. . . . . . . . . . . . . 14
⊢ (2
· 8) = ;16 |
310 | | 6p4e10 12254 |
. . . . . . . . . . . . . 14
⊢ (6 + 4) =
;10 |
311 | 57, 55, 5, 309, 243, 310 | decaddci2 12244 |
. . . . . . . . . . . . 13
⊢ ((2
· 8) + 4) = ;20 |
312 | 307, 311 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((2
· 8) + (0 + 4)) = ;20 |
313 | | 8t5e40 12300 |
. . . . . . . . . . . . . 14
⊢ (8
· 5) = ;40 |
314 | 244, 71, 313 | mulcomli 10731 |
. . . . . . . . . . . . 13
⊢ (5
· 8) = ;40 |
315 | 5, 52, 49, 314, 181 | decaddi 12242 |
. . . . . . . . . . . 12
⊢ ((5
· 8) + 3) = ;43 |
316 | 12, 50, 52, 49, 282, 183, 133, 49, 5, 312, 315 | decmac 12234 |
. . . . . . . . . . 11
⊢ ((;25 · 8) + (0 + 3)) = ;;203 |
317 | | 8t3e24 12298 |
. . . . . . . . . . . . 13
⊢ (8
· 3) = ;24 |
318 | 244, 98, 317 | mulcomli 10731 |
. . . . . . . . . . . 12
⊢ (3
· 8) = ;24 |
319 | | 2p1e3 11861 |
. . . . . . . . . . . 12
⊢ (2 + 1) =
3 |
320 | | 7p4e11 12258 |
. . . . . . . . . . . . 13
⊢ (7 + 4) =
;11 |
321 | 70, 74, 320 | addcomli 10913 |
. . . . . . . . . . . 12
⊢ (4 + 7) =
;11 |
322 | 12, 5, 93, 318, 319, 57, 321 | decaddci 12243 |
. . . . . . . . . . 11
⊢ ((3
· 8) + 7) = ;31 |
323 | 226, 49, 52, 93, 280, 305, 133, 57, 49, 316, 322 | decmac 12234 |
. . . . . . . . . 10
⊢ ((;;253 · 8) + 7) = ;;;2031 |
324 | 228, 133,
263, 93, 265, 266, 227, 57, 268, 304, 323 | decma2c 12235 |
. . . . . . . . 9
⊢ ((;;253 · ;;218) +
;;177) = ;;;;55331 |
325 | 57, 5, 49, 249, 240 | decaddi 12242 |
. . . . . . . . . . 11
⊢ ((2
· 7) + 3) = ;17 |
326 | 49, 50, 12, 73, 217 | decaddi 12242 |
. . . . . . . . . . 11
⊢ ((5
· 7) + 2) = ;37 |
327 | 12, 50, 12, 282, 93, 93, 49, 325, 326 | decrmac 12240 |
. . . . . . . . . 10
⊢ ((;25 · 7) + 2) = ;;177 |
328 | 93, 226, 49, 280, 57, 12, 327, 174 | decmul1c 12247 |
. . . . . . . . 9
⊢ (;;253 · 7) = ;;;1771 |
329 | 227, 229,
93, 262, 57, 264, 324, 328 | decmul2c 12248 |
. . . . . . . 8
⊢ (;;253 · (3↑7)) = ;;;;;553311 |
330 | | eqid 2739 |
. . . . . . . . 9
⊢ ;;;;55331 = ;;;;55331 |
331 | | eqid 2739 |
. . . . . . . . . 10
⊢ ;;;5533 =
;;;5533 |
332 | | eqid 2739 |
. . . . . . . . . . 11
⊢ ;;553 = ;;553 |
333 | | eqid 2739 |
. . . . . . . . . . . 12
⊢ ;55 = ;55 |
334 | 274, 196 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ (0 + 2) =
;02 |
335 | 181 | oveq2i 7184 |
. . . . . . . . . . . . 13
⊢ ((5
· 7) + (0 + 3)) = ((5 · 7) + 3) |
336 | 335, 171 | eqtri 2762 |
. . . . . . . . . . . 12
⊢ ((5
· 7) + (0 + 3)) = ;38 |
337 | 50, 50, 52, 12, 333, 334, 93, 93, 49, 336, 326 | decmac 12234 |
. . . . . . . . . . 11
⊢ ((;55 · 7) + (0 + 2)) = ;;387 |
338 | 12, 57, 12, 174, 168 | decaddi 12242 |
. . . . . . . . . . 11
⊢ ((3
· 7) + 2) = ;23 |
339 | 222, 49, 52, 12, 332, 196, 93, 49, 12, 337, 338 | decmac 12234 |
. . . . . . . . . 10
⊢ ((;;553 · 7) + 2) = ;;;3873 |
340 | 93, 223, 49, 331, 57, 12, 339, 174 | decmul1c 12247 |
. . . . . . . . 9
⊢ (;;;5533
· 7) = ;;;;38731 |
341 | 70 | mulid2i 10727 |
. . . . . . . . 9
⊢ (1
· 7) = 7 |
342 | 93, 224, 57, 330, 340, 341 | decmul1 12246 |
. . . . . . . 8
⊢ (;;;;55331 · 7) = ;;;;;387317 |
343 | 93, 225, 57, 329, 342, 341 | decmul1 12246 |
. . . . . . 7
⊢ ((;;253 · (3↑7)) · 7) = ;;;;;;3873177 |
344 | 143, 221,
343 | 3brtr4i 5061 |
. . . . . 6
⊢ (;;;;53057 · ;73) < ((;;253
· (3↑7)) · 7) |
345 | 93, 49 | deccl 12197 |
. . . . . . . . 9
⊢ ;73 ∈
ℕ0 |
346 | 124, 345 | nn0mulcli 12017 |
. . . . . . . 8
⊢ (;;;;53057 · ;73) ∈ ℕ0 |
347 | 346 | nn0rei 11990 |
. . . . . . 7
⊢ (;;;;53057 · ;73) ∈ ℝ |
348 | 49, 93 | nn0expcli 13550 |
. . . . . . . . . 10
⊢
(3↑7) ∈ ℕ0 |
349 | 227, 348 | nn0mulcli 12017 |
. . . . . . . . 9
⊢ (;;253 · (3↑7)) ∈
ℕ0 |
350 | 349, 93 | nn0mulcli 12017 |
. . . . . . . 8
⊢ ((;;253 · (3↑7)) · 7) ∈
ℕ0 |
351 | 350 | nn0rei 11990 |
. . . . . . 7
⊢ ((;;253 · (3↑7)) · 7) ∈
ℝ |
352 | 62 | nnrei 11728 |
. . . . . . 7
⊢ 5 ∈
ℝ |
353 | 62 | nngt0i 11758 |
. . . . . . 7
⊢ 0 <
5 |
354 | 347, 351,
352, 353 | ltmul1ii 11649 |
. . . . . 6
⊢ ((;;;;53057 · ;73) < ((;;253
· (3↑7)) · 7) ↔ ((;;;;53057 · ;73) · 5) < (((;;253
· (3↑7)) · 7) · 5)) |
355 | 344, 354 | mpbi 233 |
. . . . 5
⊢ ((;;;;53057 · ;73) · 5) < (((;;253
· (3↑7)) · 7) · 5) |
356 | 124 | nn0cni 11991 |
. . . . . . 7
⊢ ;;;;53057 ∈ ℂ |
357 | 345 | nn0cni 11991 |
. . . . . . 7
⊢ ;73 ∈ ℂ |
358 | 356, 357,
71 | mulassi 10733 |
. . . . . 6
⊢ ((;;;;53057 · ;73) · 5) = (;;;;53057 · (;73 · 5)) |
359 | 49, 50, 155, 72 | decsuc 12213 |
. . . . . . . 8
⊢ ((7
· 5) + 1) = ;36 |
360 | 71, 98, 203 | mulcomli 10731 |
. . . . . . . 8
⊢ (3
· 5) = ;15 |
361 | 50, 93, 49, 144, 50, 57, 359, 360 | decmul1c 12247 |
. . . . . . 7
⊢ (;73 · 5) = ;;365 |
362 | 361 | oveq2i 7184 |
. . . . . 6
⊢ (;;;;53057 · (;73 · 5)) = (;;;;53057 · ;;365) |
363 | 358, 362 | eqtri 2762 |
. . . . 5
⊢ ((;;;;53057 · ;73) · 5) = (;;;;53057 · ;;365) |
364 | 299, 96 | mulcli 10729 |
. . . . . . 7
⊢ (;;253 · (3↑7)) ∈
ℂ |
365 | 364, 70, 71 | mulassi 10733 |
. . . . . 6
⊢ (((;;253 · (3↑7)) · 7) · 5) =
((;;253 · (3↑7)) · (7 ·
5)) |
366 | 70, 71 | mulcomi 10730 |
. . . . . . . 8
⊢ (7
· 5) = (5 · 7) |
367 | 366 | oveq2i 7184 |
. . . . . . 7
⊢ ((;;253 · (3↑7)) · (7 · 5)) =
((;;253 · (3↑7)) · (5 ·
7)) |
368 | 299, 96, 97 | mulassi 10733 |
. . . . . . 7
⊢ ((;;253 · (3↑7)) · (5 · 7)) =
(;;253 · ((3↑7) · (5 ·
7))) |
369 | 367, 368 | eqtri 2762 |
. . . . . 6
⊢ ((;;253 · (3↑7)) · (7 · 5)) =
(;;253 · ((3↑7) · (5 ·
7))) |
370 | 365, 369 | eqtri 2762 |
. . . . 5
⊢ (((;;253 · (3↑7)) · 7) · 5) =
(;;253 · ((3↑7) · (5 ·
7))) |
371 | 355, 363,
370 | 3brtr3i 5060 |
. . . 4
⊢ (;;;;53057 · ;;365)
< (;;253 · ((3↑7) · (5 ·
7))) |
372 | 49, 55 | deccl 12197 |
. . . . . . . 8
⊢ ;36 ∈
ℕ0 |
373 | 372, 62 | decnncl 12202 |
. . . . . . 7
⊢ ;;365 ∈ ℕ |
374 | 373 | nnrei 11728 |
. . . . . 6
⊢ ;;365 ∈ ℝ |
375 | 373 | nngt0i 11758 |
. . . . . 6
⊢ 0 <
;;365 |
376 | 374, 375 | pm3.2i 474 |
. . . . 5
⊢ (;;365 ∈ ℝ ∧ 0 < ;;365) |
377 | 227 | nn0rei 11990 |
. . . . 5
⊢ ;;253 ∈ ℝ |
378 | | lt2mul2div 11599 |
. . . . 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))) |
379 | 125, 376,
377, 129, 378 | mp4an 693 |
. . . 4
⊢ ((;;;;53057 · ;;365)
< (;;253 · ((3↑7) · (5 · 7)))
↔ (;;;;53057 / ((3↑7) · (5
· 7))) < (;;253 / ;;365)) |
380 | 371, 379 | mpbi 233 |
. . 3
⊢ (;;;;53057 / ((3↑7) · (5
· 7))) < (;;253 / ;;365) |
381 | | nndivre 11760 |
. . . . 5
⊢ ((;;;;53057 ∈ ℝ ∧ ((3↑7)
· (5 · 7)) ∈ ℕ) → (;;;;53057 / ((3↑7) · (5 · 7))) ∈
ℝ) |
382 | 125, 126,
381 | mp2an 692 |
. . . 4
⊢ (;;;;53057 / ((3↑7) · (5
· 7))) ∈ ℝ |
383 | | nndivre 11760 |
. . . . 5
⊢ ((;;253 ∈ ℝ ∧ ;;365
∈ ℕ) → (;;253 / ;;365)
∈ ℝ) |
384 | 377, 373,
383 | mp2an 692 |
. . . 4
⊢ (;;253 / ;;365)
∈ ℝ |
385 | 123, 382,
384 | lelttri 10848 |
. . 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)) |
386 | 132, 380,
385 | mp2an 692 |
. 2
⊢
(Σ𝑛 ∈
(0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (3 / ((4 · ((2 · 4) + 1))
· (9↑4)))) < (;;253 /
;;365) |
387 | 27, 123, 384 | lelttri 10848 |
. 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)) |
388 | 47, 386, 387 | mp2an 692 |
1
⊢
(log‘2) < (;;253 / ;;365) |