Theorem 1re 11207

Description: The number 1 is real. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 11157, by exploiting properties of the imaginary unit i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
1re	⊢ 1 ∈ ℝ

Proof of Theorem 1re

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1ne0 11168	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11157	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11204	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3026	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11197	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11204	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3027	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3186	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3186	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3186	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3186	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7430	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 418	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2985	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2978	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 876	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3026	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3027	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3603	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1137	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 759	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3026	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3027	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3603	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1137	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 758	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 872	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 35	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3228	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3213	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2791	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 417	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2985	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3026	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3590	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 418	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 36	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 87	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 495	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3026	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3590	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 418	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 496	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 51	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3047	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3213	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11171	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11184	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 727	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2857	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3172	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3164	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∃wrex 3095  (class class class)co 7411  ℂcc 11097  ℝcr 11098  0cc0 11099  1c1 11100  ici 11101   + caddc 11102   · cmul 11104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  1red  11208  pr01ssre  11211  1xr  11267  dedekind  11372  peano2re  11382  mul02lem2  11386  addrid  11389  renegcl  11520  peano2rem  11524  0reALT  11554  0lt1  11735  0le1  11736  relin01  11737  1le1  11841  eqneg  11934  ltp1  12054  ltm1  12056  recgt0  12060  ltmulgt11  12073  lemulge11  12076  reclt1  12109  recgt1  12110  recgt1i  12111  recp1lt1  12112  recreclt  12113  recgt0ii  12120  ledivp1i  12139  ltdivp1i  12140  neg1rr  12203  neg1lt0  12205  cju  12213  indf  12223  indfval  12224  nnssre  12236  nnge1  12263  nngt1ne1  12264  nnle1eq1  12265  nngt0  12266  nnnlt1  12267  nnne0  12269  nnrecre  12277  nnrecgt0  12278  nnsub  12279  1t1e1ALT  12290  2re  12314  3re  12320  4re  12324  5re  12327  6re  12330  7re  12333  8re  12336  9re  12339  0le2OLD  12343  2posOLD  12345  1lt2  12412  1lt3  12415  1lt4  12418  1lt5  12422  1lt6  12427  1lt7  12433  1lt8  12440  1lt9  12448  1ne2  12450  1le2  12451  1le3  12454  halflt1  12460  addltmul  12479  nnunb  12499  elnnnn0c  12548  nn0ge2m1nn  12573  elnnz1  12619  znnnlt1  12620  zltp1le  12643  zleltp1  12644  nn0lt2  12658  recnz  12670  gtndiv  12672  3halfnz  12674  10re  12733  1lt10  12855  1lt10OLD  12856  eluzp1m1  12887  eluzp1p1  12889  eluz2b2  12944  zbtwnre  12969  rebtwnz  12970  1rp  13019  divlt1lt  13086  divle1le  13087  nnledivrp  13129  qbtwnxr  13225  xmulrid  13304  xmulm1  13306  x2times  13324  xrub  13337  elicc01  13492  1elunit  13496  divelunit  13520  lincmb01cmp  13521  unitssre  13525  0nelfz1  13570  fzpreddisj  13600  fznatpl1  13605  fztpval  13613  fraclt1  13834  fracle1  13835  flbi2  13849  fldiv4p1lem1div2  13867  fldiv4lem1div2  13869  fldiv  13892  modid  13928  1mod  13935  m1modnnsub1  13952  modm1p1mod0  13957  seqf1olem1  14076  reexpcl  14113  reexpclz  14117  expge0  14133  expge1  14134  expgt1  14135  bernneq  14264  bernneq2  14265  expnbnd  14267  expnlbnd  14268  expnlbnd2  14269  expmulnbnd  14270  discr1  14274  facwordi  14324  faclbnd3  14327  faclbnd4lem1  14328  faclbnd4lem4  14331  faclbnd6  14334  facavg  14336  hashv01gt1  14380  hashnn0n0nn  14426  hashunsnggt  14429  hash1snb  14455  hashgt12el  14458  hashgt12el2  14459  hashfun  14473  hashge2el2dif  14516  tpf1ofv2  14534  lsw0  14601  f1oun2prg  14953  sgnclre  15138  sgnnbi  15140  sgnpbi  15141  cjexp  15200  re1  15204  im1  15205  rei  15206  imi  15207  01sqrexlem1  15292  01sqrexlem2  15293  01sqrexlem3  15294  01sqrexlem4  15295  01sqrexlem7  15298  resqrex  15300  sqrt1  15321  sqrt2gt1lt2  15324  sqrtm1  15325  abs1  15347  absrdbnd  15392  caubnd2  15408  mulcn2  15646  reccn2  15647  rlimno1  15704  o1fsum  15864  expcnv  15917  geolim  15923  geolim2  15924  georeclim  15925  geomulcvg  15929  geoisumr  15931  geoisum1c  15933  fprodge0  16046  fprodge1  16048  rerisefaccl  16070  refallfaccl  16071  ere  16142  ege2le3  16143  efgt1  16171  resin4p  16193  recos4p  16194  tanhbnd  16216  sinbnd  16235  cosbnd  16236  sinbnd2  16237  cosbnd2  16238  ef01bndlem  16239  sin01bnd  16240  cos01bnd  16241  cos1bnd  16242  cos2bnd  16243  sinltx  16244  sin01gt0  16245  cos01gt0  16246  sin02gt0  16247  sincos1sgn  16248  ene1  16265  rpnnen2lem2  16270  rpnnen2lem3  16271  rpnnen2lem4  16272  rpnnen2lem9  16277  rpnnen2lem12  16280  ruclem6  16290  ruclem11  16295  ruclem12  16296  3dvds  16388  flodddiv4  16472  sadcadd  16515  isprm3  16740  sqnprm  16760  coprm  16769  phibndlem  16828  pythagtriplem3  16877  pcmpt  16951  fldivp1  16956  pockthi  16966  infpn2  16972  basendxnmulrndx  17348  starvndxnbasendx  17356  scandxnbasendx  17368  vscandxnbasendx  17373  ipndxnbasendx  17384  basendxnocndx  17435  slotsbhcdif  17467  lt6abl  19964  srgbinomlem4  20310  0ringnnzr  20608  abvneg  20906  abvtrivd  20912  prmidl0  21446  xrsmcmn  21513  xrsnsgrp  21526  gzrngunitlem  21550  gzrngunit  21551  rge0srg  21556  psgnodpmr  21708  remulg  21725  resubdrg  21726  psdmvr  22300  dscmet  24697  dscopn  24698  nrginvrcnlem  24816  idnghm  24868  tgioo  24921  blcvx  24923  iicmp  25013  iiconn  25014  iirev  25056  iihalf1  25058  iihalf2  25060  elii1  25062  elii2  25063  iimulcl  25064  icopnfcnv  25069  icopnfhmeo  25070  iccpnfhmeo  25072  xrhmeo  25073  xrhmph  25074  evth  25086  xlebnum  25092  htpycc  25107  reparphti  25124  pcoval1  25140  pco1  25142  pcoval2  25143  pcocn  25144  pcohtpylem  25146  pcopt  25149  pcopt2  25150  pcoass  25151  pcorevlem  25153  nmhmcn  25247  ncvs1  25284  ovolunlem1a  25623  vitalilem2  25736  vitalilem4  25738  vitalilem5  25739  vitali  25740  i1f1  25817  itg11  25818  itg2const  25867  dveflem  26106  dvlipcn  26121  dvcvx  26147  ply1remlem  26290  fta1blem  26296  plyn0mulidp  26410  plymulidp  26411  vieta1lem2  26440  aalioulem3  26463  aalioulem5  26465  aaliou3lem2  26472  ulmbdd  26526  iblulm  26535  radcnvlem1  26541  dvradcnv  26549  abelthlem2  26560  abelthlem3  26561  abelthlem5  26563  abelthlem7  26566  abelth  26569  abelth2  26570  reeff1olem  26574  reeff1o  26575  sinhalfpilem  26593  tangtx  26635  sincos4thpi  26643  pige3ALT  26650  coskpi  26653  cos0pilt1  26662  recosf1o  26665  tanregt0  26669  efif1olem3  26674  efif1olem4  26675  loge  26716  logdivlti  26750  logcnlem4  26775  logf1o2  26780  logtayl  26790  logccv  26793  recxpcl  26805  cxplea  26826  cxpcn3lem  26877  cxpaddlelem  26881  loglesqrt  26891  ang180lem2  26940  angpined  26960  acosrecl  27033  atancj  27040  atanlogaddlem  27043  atantan  27053  atans2  27061  ressatans  27064  leibpi  27072  log2le1  27080  birthdaylem3  27083  cxp2lim  27106  cxploglim  27107  cxploglim2  27108  divsqrtsumlem  27109  cvxcl  27114  scvxcvx  27115  jensenlem2  27117  amgmlem  27119  emcllem2  27126  emcllem4  27128  emcllem6  27130  emcllem7  27131  emre  27135  emgt0  27136  harmonicbnd3  27137  harmonicubnd  27139  harmonicbnd4  27140  zetacvg  27144  ftalem1  27202  ftalem2  27203  ftalem5  27206  issqf  27265  cht1  27294  chp1  27296  ppiltx  27306  mumullem2  27309  ppiublem1  27331  ppiub  27333  chtublem  27340  chtub  27341  logfacbnd3  27352  logexprlim  27354  perfectlem2  27359  dchrinv  27390  dchr1re  27392  efexple  27410  bposlem1  27413  bposlem2  27414  bposlem5  27417  bposlem8  27420  lgsdir2lem1  27454  lgsdir2lem5  27458  lgsdir  27461  lgsne0  27464  lgsabs1  27465  lgsdinn0  27474  gausslemma2dlem0i  27493  lgseisen  27508  m1lgs  27517  2lgslem3  27533  addsq2nreurex  27573  2sqreultblem  27577  2sqreunnltblem  27580  chebbnd1lem3  27600  chebbnd1  27601  chtppilimlem1  27602  chtppilimlem2  27603  chtppilim  27604  chpchtlim  27608  vmadivsumb  27612  rplogsumlem2  27614  rpvmasumlem  27616  dchrmusumlema  27622  dchrmusum2  27623  dchrvmasumlem2  27627  dchrvmasumiflem1  27630  dchrisum0flblem1  27637  dchrisum0flblem2  27638  dchrisum0fno1  27640  rpvmasum2  27641  dchrisum0re  27642  dchrisum0lema  27643  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2a  27646  dchrisum0lem2  27647  logdivsum  27662  mulog2sumlem2  27664  2vmadivsumlem  27669  log2sumbnd  27673  selbergb  27678  selberg2b  27681  chpdifbndlem1  27682  selberg3lem1  27686  selberg3lem2  27687  selberg4lem1  27689  pntrmax  27693  pntrsumo1  27694  selbergsb  27704  pntrlog2bndlem3  27708  pntrlog2bndlem5  27710  pntpbnd1a  27714  pntpbnd2  27716  pntibndlem1  27718  pntibndlem3  27721  pntlemd  27723  pntlemc  27724  pntlemb  27726  pntlemr  27731  pntlemf  27734  pntlemk  27735  pntlemo  27736  pntlem3  27738  pntleml  27740  abvcxp  27744  ostth2lem1  27747  ostth1  27762  ostth2lem2  27763  ostth2lem3  27764  ostth2lem4  27765  ostth2  27766  ostth3  27767  ostth  27768  slotsinbpsd  28675  slotslnbpsd  28676  trgcgrg  28749  brbtwn2  29195  colinearalglem4  29199  ax5seglem2  29219  ax5seglem3  29221  axpaschlem  29230  axpasch  29231  axlowdimlem6  29237  axlowdimlem10  29241  axlowdimlem16  29247  axlowdim1  29249  axlowdim2  29250  axlowdim  29251  axcontlem2  29255  elntg2  29275  lfgrnloop  29415  lfuhgr1v0e  29544  usgrexmpldifpr  29548  usgrexmplef  29549  1loopgrvd2  29793  vdegp1bi  29827  lfgrwlkprop  29975  pthdlem1  30055  pthdlem2  30057  clwlkclwwlkf  30299  upgr4cycl4dv4e  30476  konigsberglem2  30544  konigsberglem3  30545  konigsberglem5  30547  frgrreg  30685  ex-dif  30714  ex-in  30716  ex-pss  30719  ex-res  30732  ex-fl  30738  nv1  30967  smcnlem  30989  ipidsq  31002  nmlno0lem  31085  norm-ii-i  31429  bcs2  31474  norm1  31541  nmopub2tALT  32201  nmfnleub2  32218  nmlnop0iALT  32287  unopbd  32307  nmopadjlem  32381  nmopcoadji  32393  pjnmopi  32440  pjbdlni  32441  hstle1  32518  hstle  32522  hstles  32523  stge1i  32530  stlesi  32533  staddi  32538  stadd3i  32540  strlem1  32542  strlem5  32547  jplem1  32560  cdj1i  32725  addltmulALT  32738  xlt2addrd  33044  sgnmulsgp  33116  dp2lt10  33143  dp2ltsuc  33145  dp2ltc  33146  dplti  33164  dpmul4  33173  cshw1s2  33220  xrsmulgzz  33269  rearchi  33608  xrge0slmod  33610  evl1deg3  33812  constrconj  34079  2sqr3minply  34114  submateqlem1  34141  xrge0iifcnv  34267  xrge0iifcv  34268  xrge0iifiso  34269  xrge0iifhom  34271  zrhre  34353  esumcst  34397  cntnevol  34562  omssubadd  34634  iwrdsplit  34721  dstfrvclim1  34812  coinfliprv  34817  ballotlem2  34823  ballotlem4  34833  ballotlemi1  34837  ballotlemic  34841  signswch  34892  signstf  34897  signsvfn  34913  itgexpif  34937  hgt750lemd  34979  logdivsqrle  34981  hgt750lem  34982  hgt750lem2  34983  hgt750leme  34989  tgoldbachgnn  34990  subfacp1lem1  35569  subfacp1lem5  35574  resconn  35636  iisconn  35642  iillysconn  35643  problem2  36056  problem3  36057  sinccvglem  36062  fz0n  36121  dnibndlem12  36966  knoppcnlem4  36973  knoppndvlem13  37001  cnndvlem1  37014  irrdiff  37857  relowlpssretop  37897  sin2h  38148  cos2h  38149  tan2h  38150  poimirlem7  38165  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem22  38180  poimirlem23  38181  poimirlem29  38187  poimirlem31  38189  itg2addnclem3  38211  asindmre  38241  dvasin  38242  dvacos  38243  dvreasin  38244  dvreacos  38245  fdc  38283  geomcau  38297  cntotbnd  38334  heiborlem8  38356  bfplem2  38361  bfp  38362  aks4d1p1p7  42730  ine1  42964  re1m1e0m0  43047  sn-00idlem1  43048  sn-00idlem2  43049  remul02  43055  sn-0ne2  43056  reixi  43073  rei4  43074  remullid  43084  ipiiie0  43088  sn-0tie0  43114  sn-nnne0  43123  mulgt0b1d  43135  sn-0lt1  43138  sn-ltp1  43139  reneg1lt0  43143  sn-inelr  43150  rabren3dioph  43433  pellexlem5  43451  pellexlem6  43452  pell1qrgaplem  43491  pell14qrgap  43493  pellqrex  43497  pellfundre  43499  pellfundlb  43502  pellfund14gap  43505  jm2.17a  43578  acongeq  43601  jm2.23  43614  jm3.1lem2  43636  sqrtcval  44258  sqrtcval2  44259  resqrtval  44260  imsqrtval  44261  relexp01min  44330  cvgdvgrat  44914  lhe4.4ex1a  44930  binomcxplemnotnn0  44957  isosctrlem1ALT  45533  supxrgelem  45944  xrlexaddrp  45959  infxr  45973  infleinflem2  45977  sumnnodd  46237  limsup10exlem  46377  limsup10ex  46378  dvnprodlem3  46553  stoweidlem1  46606  stoweidlem18  46623  stoweidlem19  46624  stoweidlem26  46631  stoweidlem34  46639  stoweidlem40  46645  stoweidlem41  46646  stoweidlem59  46664  stoweid  46668  stirlinglem10  46688  stirlinglem11  46689  dirkercncflem1  46708  fourierdlem16  46728  fourierdlem21  46733  fourierdlem22  46734  fourierdlem42  46754  fourierdlem68  46779  fourierdlem83  46794  fourierdlem103  46814  sqwvfourb  46834  fouriersw  46836  etransclem23  46862  salgencntex  46948  ovn0lem  47170  smfmullem3  47398  smfmullem4  47399  nthrucw  47493  cjnpoly  47514  zm1nn  47927  ceilhalf1  47963  m1mod0mod1  47985  muldvdsfacgt  48011  fmtnosqrt  48179  nprmdvdsfacm1lem4  48263  perfectALTVlem2  48375  2exp340mod341  48386  8exp8mod9  48389  nfermltl8rev  48395  nnsum3primesprm  48443  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  tgblthelfgott  48468  tgoldbach  48470  usgrexmpl1lem  48674  usgrexmpl2lem  48679  usgrexmpl2nb1  48685  usgrexmpl2nb3  48687  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  usgrexmpl2trifr  48690  gpg3kgrtriexlem3  48738  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  rege1logbrege0  49222  rege1logbzge0  49223  blennnelnn  49240  dignnld  49267  nn0sumshdiglemA  49283  nn0sumshdiglem1  49285  rrx2xpref1o  49382  rrxlines  49397  eenglngeehlnmlem1  49401  eenglngeehlnmlem2  49402  line2ylem  49415  line2x  49418  icccldii  49581  io1ii  49583  sepfsepc  49590