Theorem taupi 13641

Description: Relationship between τ and π. This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019.) (Revised by AV, 1-Oct-2020.)

Assertion

Ref	Expression
taupi	⊢ τ = (2 · π)

Proof of Theorem taupi

Dummy variables 𝑓 𝑔 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-tau 11672	. 2 ⊢ τ = inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < )
2		lttri3 7957	. . . . 5 ⊢ ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
3	2	adantl 275	. . . 4 ⊢ ((⊤ ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (𝑓 = 𝑔 ↔ (¬ 𝑓 < 𝑔 ∧ ¬ 𝑔 < 𝑓)))
4		2re 8903	. . . . . 6 ⊢ 2 ∈ ℝ
5		pire 13107	. . . . . 6 ⊢ π ∈ ℝ
6	4, 5	remulcli 7892	. . . . 5 ⊢ (2 · π) ∈ ℝ
7	6	a1i 9	. . . 4 ⊢ (⊤ → (2 · π) ∈ ℝ)
8		2rp 9565	. . . . . . 7 ⊢ 2 ∈ ℝ+
9		pirp 13110	. . . . . . 7 ⊢ π ∈ ℝ+
10		rpmulcl 9585	. . . . . . 7 ⊢ ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
11	8, 9, 10	mp2an 423	. . . . . 6 ⊢ (2 · π) ∈ ℝ+
12	6	recni 7890	. . . . . . 7 ⊢ (2 · π) ∈ ℂ
13		cos2pi 13125	. . . . . . 7 ⊢ (cos‘(2 · π)) = 1
14		cosf 11602	. . . . . . . . 9 ⊢ cos:ℂ⟶ℂ
15		ffn 5319	. . . . . . . . 9 ⊢ (cos:ℂ⟶ℂ → cos Fn ℂ)
16	14, 15	ax-mp 5	. . . . . . . 8 ⊢ cos Fn ℂ
17		fniniseg 5587	. . . . . . . 8 ⊢ (cos Fn ℂ → ((2 · π) ∈ (◡cos “ {1}) ↔ ((2 · π) ∈ ℂ ∧ (cos‘(2 · π)) = 1)))
18	16, 17	ax-mp 5	. . . . . . 7 ⊢ ((2 · π) ∈ (◡cos “ {1}) ↔ ((2 · π) ∈ ℂ ∧ (cos‘(2 · π)) = 1))
19	12, 13, 18	mpbir2an 927	. . . . . 6 ⊢ (2 · π) ∈ (◡cos “ {1})
20	11, 19	elini 3291	. . . . 5 ⊢ (2 · π) ∈ (ℝ+ ∩ (◡cos “ {1}))
21	20	a1i 9	. . . 4 ⊢ (⊤ → (2 · π) ∈ (ℝ+ ∩ (◡cos “ {1})))
22		elinel2 3294	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → 𝑥 ∈ (◡cos “ {1}))
23		fniniseg 5587	. . . . . . . . . . 11 ⊢ (cos Fn ℂ → (𝑥 ∈ (◡cos “ {1}) ↔ (𝑥 ∈ ℂ ∧ (cos‘𝑥) = 1)))
24	16, 23	ax-mp 5	. . . . . . . . . 10 ⊢ (𝑥 ∈ (◡cos “ {1}) ↔ (𝑥 ∈ ℂ ∧ (cos‘𝑥) = 1))
25	22, 24	sylib 121	. . . . . . . . 9 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → (𝑥 ∈ ℂ ∧ (cos‘𝑥) = 1))
26	25	simprd 113	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → (cos‘𝑥) = 1)
27	26	adantr 274	. . . . . . 7 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → (cos‘𝑥) = 1)
28		elinel1 3293	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → 𝑥 ∈ ℝ+)
29	28	rpred 9603	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → 𝑥 ∈ ℝ)
30	29	adantr 274	. . . . . . . . 9 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → 𝑥 ∈ ℝ)
31	28	rpgt0d 9606	. . . . . . . . . 10 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → 0 < 𝑥)
32	31	adantr 274	. . . . . . . . 9 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → 0 < 𝑥)
33		simpr 109	. . . . . . . . 9 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → 𝑥 < (2 · π))
34		0xr 7924	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
35	6	rexri 7935	. . . . . . . . . 10 ⊢ (2 · π) ∈ ℝ*
36		elioo2 9825	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ (2 · π) ∈ ℝ*) → (𝑥 ∈ (0(,)(2 · π)) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 < (2 · π))))
37	34, 35, 36	mp2an 423	. . . . . . . . 9 ⊢ (𝑥 ∈ (0(,)(2 · π)) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥 ∧ 𝑥 < (2 · π)))
38	30, 32, 33, 37	syl3anbrc 1166	. . . . . . . 8 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → 𝑥 ∈ (0(,)(2 · π)))
39		cos02pilt1 13172	. . . . . . . 8 ⊢ (𝑥 ∈ (0(,)(2 · π)) → (cos‘𝑥) < 1)
40	38, 39	syl 14	. . . . . . 7 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → (cos‘𝑥) < 1)
41	27, 40	eqbrtrrd 3988	. . . . . 6 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → 1 < 1)
42		1red 7893	. . . . . . 7 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → 1 ∈ ℝ)
43	42	ltnrd 7988	. . . . . 6 ⊢ ((𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) ∧ 𝑥 < (2 · π)) → ¬ 1 < 1)
44	41, 43	pm2.65da 651	. . . . 5 ⊢ (𝑥 ∈ (ℝ+ ∩ (◡cos “ {1})) → ¬ 𝑥 < (2 · π))
45	44	adantl 275	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (ℝ+ ∩ (◡cos “ {1}))) → ¬ 𝑥 < (2 · π))
46	3, 7, 21, 45	infminti 6971	. . 3 ⊢ (⊤ → inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < ) = (2 · π))
47	46	mptru 1344	. 2 ⊢ inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < ) = (2 · π)
48	1, 47	eqtri 2178	1 ⊢ τ = (2 · π)

Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1335  ⊤wtru 1336   ∈ wcel 2128   ∩ cin 3101  {csn 3560   class class class wbr 3965  ^◡ccnv 4585   “ cima 4589   Fn wfn 5165  ⟶wf 5166  ‘cfv 5170  (class class class)co 5824  infcinf 6927  ℂcc 7730  ℝcr 7731  0cc0 7732  1c1 7733   · cmul 7737  ℝ^*cxr 7911   < clt 7912  2c2 8884  ℝ⁺crp 9560  (,)cioo 9792  cosccos 11542  πcpi 11544  τctau 11671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-iinf 4547  ax-cnex 7823  ax-resscn 7824  ax-1cn 7825  ax-1re 7826  ax-icn 7827  ax-addcl 7828  ax-addrcl 7829  ax-mulcl 7830  ax-mulrcl 7831  ax-addcom 7832  ax-mulcom 7833  ax-addass 7834  ax-mulass 7835  ax-distr 7836  ax-i2m1 7837  ax-0lt1 7838  ax-1rid 7839  ax-0id 7840  ax-rnegex 7841  ax-precex 7842  ax-cnre 7843  ax-pre-ltirr 7844  ax-pre-ltwlin 7845  ax-pre-lttrn 7846  ax-pre-apti 7847  ax-pre-ltadd 7848  ax-pre-mulgt0 7849  ax-pre-mulext 7850  ax-arch 7851  ax-caucvg 7852  ax-pre-suploc 7853  ax-addf 7854  ax-mulf 7855

This theorem depends on definitions:  df-bi 116  df-stab 817  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-disj 3943  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-ilim 4329  df-suc 4331  df-iom 4550  df-xp 4592  df-rel 4593  df-cnv 4594  df-co 4595  df-dm 4596  df-rn 4597  df-res 4598  df-ima 4599  df-iota 5135  df-fun 5172  df-fn 5173  df-f 5174  df-f1 5175  df-fo 5176  df-f1o 5177  df-fv 5178  df-isom 5179  df-riota 5780  df-ov 5827  df-oprab 5828  df-mpo 5829  df-of 6032  df-1st 6088  df-2nd 6089  df-recs 6252  df-irdg 6317  df-frec 6338  df-1o 6363  df-oadd 6367  df-er 6480  df-map 6595  df-pm 6596  df-en 6686  df-dom 6687  df-fin 6688  df-sup 6928  df-inf 6929  df-pnf 7914  df-mnf 7915  df-xr 7916  df-ltxr 7917  df-le 7918  df-sub 8048  df-neg 8049  df-reap 8450  df-ap 8457  df-div 8546  df-inn 8834  df-2 8892  df-3 8893  df-4 8894  df-5 8895  df-6 8896  df-7 8897  df-8 8898  df-9 8899  df-n0 9091  df-z 9168  df-uz 9440  df-q 9529  df-rp 9561  df-xneg 9679  df-xadd 9680  df-ioo 9796  df-ioc 9797  df-ico 9798  df-icc 9799  df-fz 9913  df-fzo 10042  df-seqfrec 10345  df-exp 10419  df-fac 10600  df-bc 10622  df-ihash 10650  df-shft 10715  df-cj 10742  df-re 10743  df-im 10744  df-rsqrt 10898  df-abs 10899  df-clim 11176  df-sumdc 11251  df-ef 11545  df-sin 11547  df-cos 11548  df-pi 11550  df-tau 11672  df-rest 12353  df-topgen 12372  df-psmet 12387  df-xmet 12388  df-met 12389  df-bl 12390  df-mopn 12391  df-top 12396  df-topon 12409  df-bases 12441  df-ntr 12496  df-cn 12588  df-cnp 12589  df-tx 12653  df-cncf 12958  df-limced 13025  df-dvap 13026

This theorem is referenced by: (None)