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

Theorem pige3 24561
 Description: π is greater than or equal to 3. This proof is based on the geometric observation that a hexagon of unit side length has perimeter 6, which is less than the unit-radius circumcircle, of perimeter 2π. We translate this to algebra by looking at the function e↑(i𝑥) as 𝑥 goes from 0 to π / 3; it moves at unit speed and travels distance 1, hence 1 ≤ π / 3. (Contributed by Mario Carneiro, 21-May-2016.)
Assertion
Ref Expression
pige3 3 ≤ π

Proof of Theorem pige3
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3cn 11353 . . 3 3 ∈ ℂ
21mulid2i 10299 . 2 (1 · 3) = 3
3 tru 1657 . . . . . 6
4 0xr 10340 . . . . . . . 8 0 ∈ ℝ*
5 pirp 24505 . . . . . . . . . 10 π ∈ ℝ+
6 3re 11352 . . . . . . . . . . 11 3 ∈ ℝ
7 3pos 11384 . . . . . . . . . . 11 0 < 3
86, 7elrpii 12031 . . . . . . . . . 10 3 ∈ ℝ+
9 rpdivcl 12054 . . . . . . . . . 10 ((π ∈ ℝ+ ∧ 3 ∈ ℝ+) → (π / 3) ∈ ℝ+)
105, 8, 9mp2an 683 . . . . . . . . 9 (π / 3) ∈ ℝ+
11 rpxr 12039 . . . . . . . . 9 ((π / 3) ∈ ℝ+ → (π / 3) ∈ ℝ*)
1210, 11ax-mp 5 . . . . . . . 8 (π / 3) ∈ ℝ*
13 rpge0 12043 . . . . . . . . 9 ((π / 3) ∈ ℝ+ → 0 ≤ (π / 3))
1410, 13ax-mp 5 . . . . . . . 8 0 ≤ (π / 3)
15 lbicc2 12492 . . . . . . . 8 ((0 ∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0 ≤ (π / 3)) → 0 ∈ (0[,](π / 3)))
164, 12, 14, 15mp3an 1585 . . . . . . 7 0 ∈ (0[,](π / 3))
17 ubicc2 12493 . . . . . . . 8 ((0 ∈ ℝ* ∧ (π / 3) ∈ ℝ* ∧ 0 ≤ (π / 3)) → (π / 3) ∈ (0[,](π / 3)))
184, 12, 14, 17mp3an 1585 . . . . . . 7 (π / 3) ∈ (0[,](π / 3))
1916, 18pm3.2i 462 . . . . . 6 (0 ∈ (0[,](π / 3)) ∧ (π / 3) ∈ (0[,](π / 3)))
20 0re 10295 . . . . . . . 8 0 ∈ ℝ
2120a1i 11 . . . . . . 7 (⊤ → 0 ∈ ℝ)
22 pire 24502 . . . . . . . . 9 π ∈ ℝ
23 3ne0 11385 . . . . . . . . 9 3 ≠ 0
2422, 6, 23redivcli 11046 . . . . . . . 8 (π / 3) ∈ ℝ
2524a1i 11 . . . . . . 7 (⊤ → (π / 3) ∈ ℝ)
26 efcn 24488 . . . . . . . . 9 exp ∈ (ℂ–cn→ℂ)
2726a1i 11 . . . . . . . 8 (⊤ → exp ∈ (ℂ–cn→ℂ))
28 iccssre 12457 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ (π / 3) ∈ ℝ) → (0[,](π / 3)) ⊆ ℝ)
2920, 24, 28mp2an 683 . . . . . . . . . . 11 (0[,](π / 3)) ⊆ ℝ
30 ax-resscn 10246 . . . . . . . . . . 11 ℝ ⊆ ℂ
3129, 30sstri 3770 . . . . . . . . . 10 (0[,](π / 3)) ⊆ ℂ
32 resmpt 5626 . . . . . . . . . 10 ((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) = (𝑥 ∈ (0[,](π / 3)) ↦ (i · 𝑥)))
3331, 32mp1i 13 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) = (𝑥 ∈ (0[,](π / 3)) ↦ (i · 𝑥)))
34 ssidd 3784 . . . . . . . . . . 11 (⊤ → ℂ ⊆ ℂ)
35 ax-icn 10248 . . . . . . . . . . . . 13 i ∈ ℂ
36 simpr 477 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
37 mulcl 10273 . . . . . . . . . . . . 13 ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
3835, 36, 37sylancr 581 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
3938fmpttd 6575 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ ℂ ↦ (i · 𝑥)):ℂ⟶ℂ)
40 cnelprrecn 10282 . . . . . . . . . . . . . . . 16 ℂ ∈ {ℝ, ℂ}
4140a1i 11 . . . . . . . . . . . . . . 15 (⊤ → ℂ ∈ {ℝ, ℂ})
42 ax-1cn 10247 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
4342a1i 11 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
4441dvmptid 24011 . . . . . . . . . . . . . . 15 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
4535a1i 11 . . . . . . . . . . . . . . 15 (⊤ → i ∈ ℂ)
4641, 36, 43, 44, 45dvmptcmul 24018 . . . . . . . . . . . . . 14 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ (i · 1)))
4735mulid1i 10298 . . . . . . . . . . . . . . 15 (i · 1) = i
4847mpteq2i 4900 . . . . . . . . . . . . . 14 (𝑥 ∈ ℂ ↦ (i · 1)) = (𝑥 ∈ ℂ ↦ i)
4946, 48syl6eq 2815 . . . . . . . . . . . . 13 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = (𝑥 ∈ ℂ ↦ i))
5049dmeqd 5494 . . . . . . . . . . . 12 (⊤ → dom (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = dom (𝑥 ∈ ℂ ↦ i))
5135elexi 3366 . . . . . . . . . . . . 13 i ∈ V
52 eqid 2765 . . . . . . . . . . . . 13 (𝑥 ∈ ℂ ↦ i) = (𝑥 ∈ ℂ ↦ i)
5351, 52dmmpti 6201 . . . . . . . . . . . 12 dom (𝑥 ∈ ℂ ↦ i) = ℂ
5450, 53syl6eq 2815 . . . . . . . . . . 11 (⊤ → dom (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = ℂ)
55 dvcn 23975 . . . . . . . . . . 11 (((ℂ ⊆ ℂ ∧ (𝑥 ∈ ℂ ↦ (i · 𝑥)):ℂ⟶ℂ ∧ ℂ ⊆ ℂ) ∧ dom (ℂ D (𝑥 ∈ ℂ ↦ (i · 𝑥))) = ℂ) → (𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ))
5634, 39, 34, 54, 55syl31anc 1492 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ))
57 rescncf 22979 . . . . . . . . . 10 ((0[,](π / 3)) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) ∈ ((0[,](π / 3))–cn→ℂ)))
5831, 56, 57mpsyl 68 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℂ ↦ (i · 𝑥)) ↾ (0[,](π / 3))) ∈ ((0[,](π / 3))–cn→ℂ))
5933, 58eqeltrrd 2845 . . . . . . . 8 (⊤ → (𝑥 ∈ (0[,](π / 3)) ↦ (i · 𝑥)) ∈ ((0[,](π / 3))–cn→ℂ))
6027, 59cncfmpt1f 22995 . . . . . . 7 (⊤ → (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))) ∈ ((0[,](π / 3))–cn→ℂ))
61 reelprrecn 10281 . . . . . . . . . . 11 ℝ ∈ {ℝ, ℂ}
6261a1i 11 . . . . . . . . . 10 (⊤ → ℝ ∈ {ℝ, ℂ})
63 recn 10279 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
64 efcl 15095 . . . . . . . . . . . 12 ((i · 𝑥) ∈ ℂ → (exp‘(i · 𝑥)) ∈ ℂ)
6538, 64syl 17 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → (exp‘(i · 𝑥)) ∈ ℂ)
6663, 65sylan2 586 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ) → (exp‘(i · 𝑥)) ∈ ℂ)
67 mulcl 10273 . . . . . . . . . . . 12 (((exp‘(i · 𝑥)) ∈ ℂ ∧ i ∈ ℂ) → ((exp‘(i · 𝑥)) · i) ∈ ℂ)
6865, 35, 67sylancl 580 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℂ) → ((exp‘(i · 𝑥)) · i) ∈ ℂ)
6963, 68sylan2 586 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ) → ((exp‘(i · 𝑥)) · i) ∈ ℂ)
70 eqid 2765 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
7170cnfldtopon 22865 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
72 toponmax 21010 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) → ℂ ∈ (TopOpen‘ℂfld))
7371, 72mp1i 13 . . . . . . . . . . 11 (⊤ → ℂ ∈ (TopOpen‘ℂfld))
7430a1i 11 . . . . . . . . . . . 12 (⊤ → ℝ ⊆ ℂ)
75 df-ss 3746 . . . . . . . . . . . 12 (ℝ ⊆ ℂ ↔ (ℝ ∩ ℂ) = ℝ)
7674, 75sylib 209 . . . . . . . . . . 11 (⊤ → (ℝ ∩ ℂ) = ℝ)
7735a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℂ) → i ∈ ℂ)
78 efcl 15095 . . . . . . . . . . . . 13 (𝑦 ∈ ℂ → (exp‘𝑦) ∈ ℂ)
7978adantl 473 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ ℂ) → (exp‘𝑦) ∈ ℂ)
80 dvef 24034 . . . . . . . . . . . . 13 (ℂ D exp) = exp
81 eff 15094 . . . . . . . . . . . . . . . 16 exp:ℂ⟶ℂ
8281a1i 11 . . . . . . . . . . . . . . 15 (⊤ → exp:ℂ⟶ℂ)
8382feqmptd 6438 . . . . . . . . . . . . . 14 (⊤ → exp = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
8483oveq2d 6858 . . . . . . . . . . . . 13 (⊤ → (ℂ D exp) = (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))))
8580, 84, 833eqtr3a 2823 . . . . . . . . . . . 12 (⊤ → (ℂ D (𝑦 ∈ ℂ ↦ (exp‘𝑦))) = (𝑦 ∈ ℂ ↦ (exp‘𝑦)))
86 fveq2 6375 . . . . . . . . . . . 12 (𝑦 = (i · 𝑥) → (exp‘𝑦) = (exp‘(i · 𝑥)))
8741, 41, 38, 77, 79, 79, 49, 85, 86, 86dvmptco 24026 . . . . . . . . . . 11 (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℂ ↦ ((exp‘(i · 𝑥)) · i)))
8870, 62, 73, 76, 65, 68, 87dvmptres3 24010 . . . . . . . . . 10 (⊤ → (ℝ D (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ ℝ ↦ ((exp‘(i · 𝑥)) · i)))
8929a1i 11 . . . . . . . . . 10 (⊤ → (0[,](π / 3)) ⊆ ℝ)
9070tgioo2 22885 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
91 iccntr 22903 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ (π / 3) ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(0[,](π / 3))) = (0(,)(π / 3)))
9220, 25, 91sylancr 581 . . . . . . . . . 10 (⊤ → ((int‘(topGen‘ran (,)))‘(0[,](π / 3))) = (0(,)(π / 3)))
9362, 66, 69, 88, 89, 90, 70, 92dvmptres2 24016 . . . . . . . . 9 (⊤ → (ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)))
9493dmeqd 5494 . . . . . . . 8 (⊤ → dom (ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = dom (𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)))
95 ovex 6874 . . . . . . . . 9 ((exp‘(i · 𝑥)) · i) ∈ V
96 eqid 2765 . . . . . . . . 9 (𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)) = (𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i))
9795, 96dmmpti 6201 . . . . . . . 8 dom (𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i)) = (0(,)(π / 3))
9894, 97syl6eq 2815 . . . . . . 7 (⊤ → dom (ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))) = (0(,)(π / 3)))
99 1re 10293 . . . . . . . 8 1 ∈ ℝ
10099a1i 11 . . . . . . 7 (⊤ → 1 ∈ ℝ)
10193fveq1d 6377 . . . . . . . . . . 11 (⊤ → ((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦) = ((𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i))‘𝑦))
102 oveq2 6850 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (i · 𝑥) = (i · 𝑦))
103102fveq2d 6379 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (exp‘(i · 𝑥)) = (exp‘(i · 𝑦)))
104103oveq1d 6857 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((exp‘(i · 𝑥)) · i) = ((exp‘(i · 𝑦)) · i))
105104, 96, 95fvmpt3i 6476 . . . . . . . . . . 11 (𝑦 ∈ (0(,)(π / 3)) → ((𝑥 ∈ (0(,)(π / 3)) ↦ ((exp‘(i · 𝑥)) · i))‘𝑦) = ((exp‘(i · 𝑦)) · i))
106101, 105sylan9eq 2819 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → ((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦) = ((exp‘(i · 𝑦)) · i))
107106fveq2d 6379 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦)) = (abs‘((exp‘(i · 𝑦)) · i)))
108 ioossre 12437 . . . . . . . . . . . . . . 15 (0(,)(π / 3)) ⊆ ℝ
109108a1i 11 . . . . . . . . . . . . . 14 (⊤ → (0(,)(π / 3)) ⊆ ℝ)
110109sselda 3761 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → 𝑦 ∈ ℝ)
111110recnd 10322 . . . . . . . . . . . 12 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → 𝑦 ∈ ℂ)
112 mulcl 10273 . . . . . . . . . . . 12 ((i ∈ ℂ ∧ 𝑦 ∈ ℂ) → (i · 𝑦) ∈ ℂ)
11335, 111, 112sylancr 581 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (i · 𝑦) ∈ ℂ)
114 efcl 15095 . . . . . . . . . . 11 ((i · 𝑦) ∈ ℂ → (exp‘(i · 𝑦)) ∈ ℂ)
115113, 114syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (exp‘(i · 𝑦)) ∈ ℂ)
116 absmul 14319 . . . . . . . . . 10 (((exp‘(i · 𝑦)) ∈ ℂ ∧ i ∈ ℂ) → (abs‘((exp‘(i · 𝑦)) · i)) = ((abs‘(exp‘(i · 𝑦))) · (abs‘i)))
117115, 35, 116sylancl 580 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (abs‘((exp‘(i · 𝑦)) · i)) = ((abs‘(exp‘(i · 𝑦))) · (abs‘i)))
118 absefi 15208 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → (abs‘(exp‘(i · 𝑦))) = 1)
119110, 118syl 17 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (abs‘(exp‘(i · 𝑦))) = 1)
120 absi 14311 . . . . . . . . . . . 12 (abs‘i) = 1
121120a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (abs‘i) = 1)
122119, 121oveq12d 6860 . . . . . . . . . 10 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) = (1 · 1))
12342mulid1i 10298 . . . . . . . . . 10 (1 · 1) = 1
124122, 123syl6eq 2815 . . . . . . . . 9 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → ((abs‘(exp‘(i · 𝑦))) · (abs‘i)) = 1)
125107, 117, 1243eqtrd 2803 . . . . . . . 8 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦)) = 1)
126 1le1 10909 . . . . . . . 8 1 ≤ 1
127125, 126syl6eqbr 4848 . . . . . . 7 ((⊤ ∧ 𝑦 ∈ (0(,)(π / 3))) → (abs‘((ℝ D (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))))‘𝑦)) ≤ 1)
12821, 25, 60, 98, 100, 127dvlip 24047 . . . . . 6 ((⊤ ∧ (0 ∈ (0[,](π / 3)) ∧ (π / 3) ∈ (0[,](π / 3)))) → (abs‘(((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3)))) ≤ (1 · (abs‘(0 − (π / 3)))))
1293, 19, 128mp2an 683 . . . . 5 (abs‘(((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3)))) ≤ (1 · (abs‘(0 − (π / 3))))
130 oveq2 6850 . . . . . . . . . . . . 13 (𝑥 = 0 → (i · 𝑥) = (i · 0))
131 it0e0 11500 . . . . . . . . . . . . 13 (i · 0) = 0
132130, 131syl6eq 2815 . . . . . . . . . . . 12 (𝑥 = 0 → (i · 𝑥) = 0)
133132fveq2d 6379 . . . . . . . . . . 11 (𝑥 = 0 → (exp‘(i · 𝑥)) = (exp‘0))
134 ef0 15103 . . . . . . . . . . 11 (exp‘0) = 1
135133, 134syl6eq 2815 . . . . . . . . . 10 (𝑥 = 0 → (exp‘(i · 𝑥)) = 1)
136 eqid 2765 . . . . . . . . . 10 (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥))) = (𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))
137 fvex 6388 . . . . . . . . . 10 (exp‘(i · 𝑥)) ∈ V
138135, 136, 137fvmpt3i 6476 . . . . . . . . 9 (0 ∈ (0[,](π / 3)) → ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) = 1)
13916, 138ax-mp 5 . . . . . . . 8 ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) = 1
140 oveq2 6850 . . . . . . . . . . 11 (𝑥 = (π / 3) → (i · 𝑥) = (i · (π / 3)))
141140fveq2d 6379 . . . . . . . . . 10 (𝑥 = (π / 3) → (exp‘(i · 𝑥)) = (exp‘(i · (π / 3))))
142141, 136, 137fvmpt3i 6476 . . . . . . . . 9 ((π / 3) ∈ (0[,](π / 3)) → ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3)) = (exp‘(i · (π / 3))))
14318, 142ax-mp 5 . . . . . . . 8 ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3)) = (exp‘(i · (π / 3)))
144139, 143oveq12i 6854 . . . . . . 7 (((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3))) = (1 − (exp‘(i · (π / 3))))
14524recni 10308 . . . . . . . . . 10 (π / 3) ∈ ℂ
14635, 145mulcli 10301 . . . . . . . . 9 (i · (π / 3)) ∈ ℂ
147 efcl 15095 . . . . . . . . 9 ((i · (π / 3)) ∈ ℂ → (exp‘(i · (π / 3))) ∈ ℂ)
148146, 147ax-mp 5 . . . . . . . 8 (exp‘(i · (π / 3))) ∈ ℂ
149 negicn 10536 . . . . . . . . . 10 -i ∈ ℂ
150149, 145mulcli 10301 . . . . . . . . 9 (-i · (π / 3)) ∈ ℂ
151 efcl 15095 . . . . . . . . 9 ((-i · (π / 3)) ∈ ℂ → (exp‘(-i · (π / 3))) ∈ ℂ)
152150, 151ax-mp 5 . . . . . . . 8 (exp‘(-i · (π / 3))) ∈ ℂ
153 cosval 15135 . . . . . . . . . . 11 ((π / 3) ∈ ℂ → (cos‘(π / 3)) = (((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) / 2))
154145, 153ax-mp 5 . . . . . . . . . 10 (cos‘(π / 3)) = (((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) / 2)
155 sincos3rdpi 24560 . . . . . . . . . . 11 ((sin‘(π / 3)) = ((√‘3) / 2) ∧ (cos‘(π / 3)) = (1 / 2))
156155simpri 479 . . . . . . . . . 10 (cos‘(π / 3)) = (1 / 2)
157154, 156eqtr3i 2789 . . . . . . . . 9 (((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) / 2) = (1 / 2)
158148, 152addcli 10300 . . . . . . . . . 10 ((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) ∈ ℂ
159 2cn 11347 . . . . . . . . . 10 2 ∈ ℂ
160 2ne0 11383 . . . . . . . . . 10 2 ≠ 0
161158, 42, 159, 160div11i 11038 . . . . . . . . 9 ((((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) / 2) = (1 / 2) ↔ ((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) = 1)
162157, 161mpbi 221 . . . . . . . 8 ((exp‘(i · (π / 3))) + (exp‘(-i · (π / 3)))) = 1
16342, 148, 152, 162subaddrii 10624 . . . . . . 7 (1 − (exp‘(i · (π / 3)))) = (exp‘(-i · (π / 3)))
164 mulneg12 10722 . . . . . . . . 9 ((i ∈ ℂ ∧ (π / 3) ∈ ℂ) → (-i · (π / 3)) = (i · -(π / 3)))
16535, 145, 164mp2an 683 . . . . . . . 8 (-i · (π / 3)) = (i · -(π / 3))
166165fveq2i 6378 . . . . . . 7 (exp‘(-i · (π / 3))) = (exp‘(i · -(π / 3)))
167144, 163, 1663eqtri 2791 . . . . . 6 (((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3))) = (exp‘(i · -(π / 3)))
168167fveq2i 6378 . . . . 5 (abs‘(((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘0) − ((𝑥 ∈ (0[,](π / 3)) ↦ (exp‘(i · 𝑥)))‘(π / 3)))) = (abs‘(exp‘(i · -(π / 3))))
169145absnegi 14424 . . . . . . . 8 (abs‘-(π / 3)) = (abs‘(π / 3))
170 df-neg 10523 . . . . . . . . 9 -(π / 3) = (0 − (π / 3))
171170fveq2i 6378 . . . . . . . 8 (abs‘-(π / 3)) = (abs‘(0 − (π / 3)))
172169, 171eqtr3i 2789 . . . . . . 7 (abs‘(π / 3)) = (abs‘(0 − (π / 3)))
173 rprege0 12045 . . . . . . . 8 ((π / 3) ∈ ℝ+ → ((π / 3) ∈ ℝ ∧ 0 ≤ (π / 3)))
174 absid 14321 . . . . . . . 8 (((π / 3) ∈ ℝ ∧ 0 ≤ (π / 3)) → (abs‘(π / 3)) = (π / 3))
17510, 173, 174mp2b 10 . . . . . . 7 (abs‘(π / 3)) = (π / 3)
176172, 175eqtr3i 2789 . . . . . 6 (abs‘(0 − (π / 3))) = (π / 3)
177176oveq2i 6853 . . . . 5 (1 · (abs‘(0 − (π / 3)))) = (1 · (π / 3))
178129, 168, 1773brtr3i 4838 . . . 4 (abs‘(exp‘(i · -(π / 3)))) ≤ (1 · (π / 3))
17924renegcli 10596 . . . . 5 -(π / 3) ∈ ℝ
180 absefi 15208 . . . . 5 (-(π / 3) ∈ ℝ → (abs‘(exp‘(i · -(π / 3)))) = 1)
181179, 180ax-mp 5 . . . 4 (abs‘(exp‘(i · -(π / 3)))) = 1
182145mulid2i 10299 . . . 4 (1 · (π / 3)) = (π / 3)
183178, 181, 1823brtr3i 4838 . . 3 1 ≤ (π / 3)
1846, 7pm3.2i 462 . . . 4 (3 ∈ ℝ ∧ 0 < 3)
185 lemuldiv 11157 . . . 4 ((1 ∈ ℝ ∧ π ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → ((1 · 3) ≤ π ↔ 1 ≤ (π / 3)))
18699, 22, 184, 185mp3an 1585 . . 3 ((1 · 3) ≤ π ↔ 1 ≤ (π / 3))
187183, 186mpbir 222 . 2 (1 · 3) ≤ π
1882, 187eqbrtrri 4832 1 3 ≤ π
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 197   ∧ wa 384   = wceq 1652  ⊤wtru 1653   ∈ wcel 2155   ∩ cin 3731   ⊆ wss 3732  {cpr 4336   class class class wbr 4809   ↦ cmpt 4888  dom cdm 5277  ran crn 5278   ↾ cres 5279  ⟶wf 6064  ‘cfv 6068  (class class class)co 6842  ℂcc 10187  ℝcr 10188  0cc0 10189  1c1 10190  ici 10191   + caddc 10192   · cmul 10194  ℝ*cxr 10327   < clt 10328   ≤ cle 10329   − cmin 10520  -cneg 10521   / cdiv 10938  2c2 11327  3c3 11328  ℝ+crp 12028  (,)cioo 12377  [,]cicc 12380  √csqrt 14258  abscabs 14259  expce 15074  sincsin 15076  cosccos 15077  πcpi 15079  TopOpenctopn 16348  topGenctg 16364  ℂfldccnfld 20019  TopOnctopon 20994  intcnt 21101  –cn→ccncf 22958   D cdv 23918 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269 This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-shft 14092  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-limsup 14487  df-clim 14504  df-rlim 14505  df-sum 14702  df-ef 15080  df-sin 15082  df-cos 15083  df-pi 15085  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-sca 16230  df-vsca 16231  df-ip 16232  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-hom 16238  df-cco 16239  df-rest 16349  df-topn 16350  df-0g 16368  df-gsum 16369  df-topgen 16370  df-pt 16371  df-prds 16374  df-xrs 16428  df-qtop 16433  df-imas 16434  df-xps 16436  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-mulg 17808  df-cntz 18013  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-fbas 20016  df-fg 20017  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cld 21103  df-ntr 21104  df-cls 21105  df-nei 21182  df-lp 21220  df-perf 21221  df-cn 21311  df-cnp 21312  df-haus 21399  df-cmp 21470  df-tx 21645  df-hmeo 21838  df-fil 21929  df-fm 22021  df-flim 22022  df-flf 22023  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-limc 23921  df-dv 23922 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator