Theorem 1re 11233

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 11183, 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 11194	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11183	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11230	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3017	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11223	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11230	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3018	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3177	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3177	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3177	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3177	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7422	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7433	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 419	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2976	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2969	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 877	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3017	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3018	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3589	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1139	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 760	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3017	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3018	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3589	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1139	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 759	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 873	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 35	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3219	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3204	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2782	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 418	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2976	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3017	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3576	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 419	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 36	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 87	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 496	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3017	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3576	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 419	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 497	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 51	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3038	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3204	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11197	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11210	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 728	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2848	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3163	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3155	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∃wrex 3086  (class class class)co 7414  ℂcc 11123  ℝcr 11124  0cc0 11125  1c1 11126  ici 11127   + caddc 11128   · cmul 11130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-mulcl 11187  ax-mulrcl 11188  ax-i2m1 11193  ax-1ne0 11194  ax-rrecex 11197  ax-cnre 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417

This theorem is used by:  1red  11234  pr01ssre  11237  1xr  11293  dedekind  11398  peano2re  11408  mul02lem2  11412  addrid  11415  renegcl  11546  peano2rem  11550  0reALT  11580  0lt1  11761  0le1  11762  relin01  11763  1le1  11867  eqneg  11960  ltp1  12080  ltm1  12082  recgt0  12086  ltmulgt11  12099  lemulge11  12102  reclt1  12135  recgt1  12136  recgt1i  12137  recp1lt1  12138  recreclt  12139  recgt0ii  12146  ledivp1i  12165  ltdivp1i  12166  neg1rr  12229  neg1lt0  12231  cju  12239  indf  12249  indfval  12250  nnssre  12262  nnge1  12289  nngt1ne1  12290  nnle1eq1  12291  nngt0  12292  nnnlt1  12293  nnne0  12295  nnrecre  12303  nnrecgt0  12304  nnsub  12305  1t1e1ALT  12316  2re  12340  3re  12346  4re  12350  5re  12353  6re  12356  7re  12359  8re  12362  9re  12365  0le2OLD  12369  2posOLD  12371  1lt2  12438  1lt3  12441  1lt4  12444  1lt5  12448  1lt6  12453  1lt7  12459  1lt8  12466  1lt9  12474  1ne2  12476  1le2  12477  1le3  12480  halflt1  12486  addltmul  12505  nnunb  12525  elnnnn0c  12574  nn0ge2m1nn  12599  elnnz1  12645  znnnlt1  12646  zltp1le  12669  zleltp1  12670  nn0lt2  12685  recnz  12697  gtndiv  12699  3halfnz  12701  10re  12760  1lt10  12882  1lt10OLD  12883  eluzp1m1  12914  eluzp1p1  12916  eluz2b2  12971  zbtwnre  12996  rebtwnz  12997  1rp  13047  divlt1lt  13114  divle1le  13115  nnledivrp  13157  qbtwnxr  13253  xmulrid  13332  xmulm1  13334  x2times  13352  xrub  13365  elicc01  13520  1elunit  13524  divelunit  13548  lincmb01cmp  13549  unitssre  13553  0nelfz1  13598  fzpreddisj  13629  fznatpl1  13634  fztpval  13642  fraclt1  13864  fracle1  13865  flbi2  13879  fldiv4p1lem1div2  13897  fldiv4lem1div2  13899  fldiv  13922  modid  13958  1mod  13965  m1modnnsub1  13982  modm1p1mod0  13987  seqf1olem1  14106  reexpcl  14143  reexpclz  14147  expge0  14163  expge1  14164  expgt1  14165  bernneq  14294  bernneq2  14295  expnbnd  14297  expnlbnd  14298  expnlbnd2  14299  expmulnbnd  14300  discr1  14304  facwordi  14354  faclbnd3  14357  faclbnd4lem1  14358  faclbnd4lem4  14361  faclbnd6  14364  facavg  14366  hashv01gt1  14410  hashnn0n0nn  14456  hashunsnggt  14459  hash1snb  14485  hashgt12el  14488  hashgt12el2  14489  hashfun  14503  hashge2el2dif  14546  tpf1ofv2  14564  lsw0  14631  f1oun2prg  14989  sgnclre  15176  sgnnbi  15178  sgnpbi  15179  cjexp  15238  re1  15242  im1  15243  rei  15244  imi  15245  01sqrexlem1  15330  01sqrexlem2  15331  01sqrexlem3  15332  01sqrexlem4  15333  01sqrexlem7  15336  resqrex  15338  sqrt1  15359  sqrt2gt1lt2  15362  sqrtm1  15363  abs1  15385  absrdbnd  15430  caubnd2  15446  mulcn2  15684  reccn2  15685  rlimno1  15742  o1fsum  15901  expcnv  15954  geolim  15960  geolim2  15961  georeclim  15962  geomulcvg  15966  geoisumr  15968  geoisum1c  15970  fprodge0  16081  fprodge1  16083  rerisefaccl  16105  refallfaccl  16106  ere  16176  ege2le3  16177  efgt1  16205  resin4p  16227  recos4p  16228  tanhbnd  16250  sinbnd  16269  cosbnd  16270  sinbnd2  16271  cosbnd2  16272  ef01bndlem  16273  sin01bnd  16274  cos01bnd  16275  cos1bnd  16276  cos2bnd  16277  sinltx  16278  sin01gt0  16279  cos01gt0  16280  sin02gt0  16281  sincos1sgn  16282  ene1  16299  rpnnen2lem2  16304  rpnnen2lem3  16305  rpnnen2lem4  16306  rpnnen2lem9  16311  rpnnen2lem12  16314  ruclem6  16324  ruclem11  16329  ruclem12  16330  3dvds  16422  flodddiv4  16506  sadcadd  16549  isprm3  16774  sqnprm  16794  coprm  16803  phibndlem  16862  pythagtriplem3  16911  pcmpt  16985  fldivp1  16990  pockthi  17000  infpn2  17006  basendxnmulrndx  17382  starvndxnbasendx  17390  scandxnbasendx  17402  vscandxnbasendx  17407  ipndxnbasendx  17418  basendxnocndx  17469  slotsbhcdif  17501  lt6abl  20023  srgbinomlem4  20369  0ringnnzr  20687  abvneg  20993  abvtrivd  20999  prmidl0  21542  xrsmcmn  21609  xrsnsgrp  21622  gzrngunitlem  21646  gzrngunit  21647  rge0srg  21652  psgnodpmr  21804  remulg  21821  resubdrg  21822  psdmvr  22398  dscmet  24799  dscopn  24800  nrginvrcnlem  24918  idnghm  24970  tgioo  25023  blcvx  25025  iicmp  25115  iiconn  25116  iirev  25158  iihalf1  25160  iihalf2  25162  elii1  25164  elii2  25165  iimulcl  25166  icopnfcnv  25171  icopnfhmeo  25172  iccpnfhmeo  25174  xrhmeo  25175  xrhmph  25176  evth  25188  xlebnum  25194  htpycc  25209  reparphti  25226  pcoval1  25242  pco1  25244  pcoval2  25245  pcocn  25246  pcohtpylem  25248  pcopt  25251  pcopt2  25252  pcoass  25253  pcorevlem  25255  nmhmcn  25349  ncvs1  25386  ovolunlem1a  25725  vitalilem2  25838  vitalilem4  25840  vitalilem5  25841  vitali  25842  i1f1  25919  itg11  25920  itg2const  25969  dveflem  26207  dvlipcn  26222  dvcvx  26248  ply1remlem  26391  fta1blem  26397  plyn0mulidp  26512  plymulidp  26513  vieta1lem2  26544  aalioulem3  26571  aalioulem5  26573  aaliou3lem2  26580  ulmbdd  26635  iblulm  26644  radcnvlem1  26650  dvradcnv  26658  abelthlem2  26669  abelthlem3  26670  abelthlem5  26672  abelthlem7  26675  abelth  26678  abelth2  26679  reeff1olem  26683  reeff1o  26684  sinhalfpilem  26702  tangtx  26744  sincos4thpi  26752  pige3ALT  26758  coskpi  26761  cos0pilt1  26770  recosf1o  26773  tanregt0  26777  efif1olem3  26782  efif1olem4  26783  loge  26824  logdivlti  26858  logcnlem4  26883  logf1o2  26888  logtayl  26898  logccv  26901  recxpcl  26913  cxplea  26934  cxpcn3lem  26985  cxpaddlelem  26989  loglesqrt  26999  ang180lem2  27048  angpined  27068  acosrecl  27141  atancj  27148  atanlogaddlem  27151  atantan  27161  atans2  27169  ressatans  27172  leibpi  27180  log2le1  27188  birthdaylem3  27191  cxp2lim  27214  cxploglim  27215  cxploglim2  27216  divsqrtsumlem  27217  cvxcl  27222  scvxcvx  27223  jensenlem2  27225  amgmlem  27227  emcllem2  27234  emcllem4  27236  emcllem6  27238  emcllem7  27239  emre  27243  emgt0  27244  harmonicbnd3  27245  harmonicubnd  27247  harmonicbnd4  27248  zetacvg  27252  ftalem1  27310  ftalem2  27311  ftalem5  27314  issqf  27373  cht1  27402  chp1  27404  ppiltx  27414  mumullem2  27417  ppiublem1  27439  ppiub  27441  chtublem  27448  chtub  27449  logfacbnd3  27460  logexprlim  27462  perfectlem2  27467  dchrinv  27498  dchr1re  27500  efexple  27518  bposlem1  27521  bposlem2  27522  bposlem5  27525  bposlem8  27528  lgsdir2lem1  27562  lgsdir2lem5  27566  lgsdir  27569  lgsne0  27572  lgsabs1  27573  lgsdinn0  27582  gausslemma2dlem0i  27601  lgseisen  27616  m1lgs  27625  2lgslem3  27641  addsq2nreurex  27681  2sqreultblem  27685  2sqreunnltblem  27688  chebbnd1lem3  27708  chebbnd1  27709  chtppilimlem1  27710  chtppilimlem2  27711  chtppilim  27712  chpchtlim  27716  vmadivsumb  27720  rplogsumlem2  27722  rpvmasumlem  27724  dchrmusumlema  27730  dchrmusum2  27731  dchrvmasumlem2  27735  dchrvmasumiflem1  27738  dchrisum0flblem1  27745  dchrisum0flblem2  27746  dchrisum0fno1  27748  rpvmasum2  27749  dchrisum0re  27750  dchrisum0lema  27751  dchrisum0lem1b  27752  dchrisum0lem1  27753  dchrisum0lem2a  27754  dchrisum0lem2  27755  logdivsum  27770  mulog2sumlem2  27772  2vmadivsumlem  27777  log2sumbnd  27781  selbergb  27786  selberg2b  27789  chpdifbndlem1  27790  selberg3lem1  27794  selberg3lem2  27795  selberg4lem1  27797  pntrmax  27801  pntrsumo1  27802  selbergsb  27812  pntrlog2bndlem3  27816  pntrlog2bndlem5  27818  pntpbnd1a  27822  pntpbnd2  27824  pntibndlem1  27826  pntibndlem3  27829  pntlemd  27831  pntlemc  27832  pntlemb  27834  pntlemr  27839  pntlemf  27842  pntlemk  27843  pntlemo  27844  pntlem3  27846  pntleml  27848  abvcxp  27852  ostth2lem1  27855  ostth1  27870  ostth2lem2  27871  ostth2lem3  27872  ostth2lem4  27873  ostth2  27874  ostth3  27875  ostth  27876  slotsinbpsd  28783  slotslnbpsd  28784  trgcgrg  28858  brbtwn2  29363  colinearalglem4  29367  ax5seglem2  29387  ax5seglem3  29389  axpaschlem  29398  axpasch  29399  axlowdimlem6  29405  axlowdimlem10  29409  axlowdimlem16  29415  axlowdim1  29417  axlowdim2  29418  axlowdim  29419  axcontlem2  29423  elntg2  29443  lfgrnloop  29583  lfuhgr1v0e  29715  usgrexmpldifpr  29719  usgrexmplef  29720  1loopgrvd2  29964  vdegp1bi  29998  lfgrwlkprop  30150  pthdlem1  30232  pthdlem2  30234  clwlkclwwlkf  30479  upgr4cycl4dv4e  30666  konigsberglem2  30734  konigsberglem3  30735  konigsberglem5  30737  frgrreg  30875  ex-dif  30904  ex-in  30906  ex-pss  30909  ex-res  30922  ex-fl  30928  nv1  31157  smcnlem  31179  ipidsq  31192  nmlno0lem  31275  norm-ii-i  31619  bcs2  31664  norm1  31731  nmopub2tALT  32391  nmfnleub2  32408  nmlnop0iALT  32477  unopbd  32497  nmopadjlem  32571  nmopcoadji  32583  pjnmopi  32630  pjbdlni  32631  hstle1  32708  hstle  32712  hstles  32713  stge1i  32720  stlesi  32723  staddi  32728  stadd3i  32730  strlem1  32732  strlem5  32737  jplem1  32750  cdj1i  32915  addltmulALT  32928  xlt2addrd  33231  sgnmulsgp  33303  dp2lt10  33330  dp2ltsuc  33332  dp2ltc  33333  dplti  33351  dpmul4  33360  cshw1s2  33401  xrsmulgzz  33450  rearchi  33787  xrge0slmod  33789  evl1deg3  33989  constrconj  34256  2sqr3minply  34291  submateqlem1  34318  xrge0iifcnv  34444  xrge0iifcv  34445  xrge0iifiso  34446  xrge0iifhom  34448  zrhre  34530  esumcst  34574  cntnevol  34740  omssubadd  34812  iwrdsplit  34899  dstfrvclim1  34990  coinfliprv  34995  ballotlem2  35001  ballotlem4  35011  ballotlemi1  35015  ballotlemic  35019  signswch  35070  signstf  35075  signsvfn  35091  itgexpif  35115  hgt750lemd  35157  logdivsqrle  35159  hgt750lem  35160  hgt750lem2  35161  hgt750leme  35167  tgoldbachgnn  35168  subfacp1lem1  35759  subfacp1lem5  35764  resconn  35826  iisconn  35832  iillysconn  35833  problem2  36246  problem3  36247  sinccvglem  36252  fz0n  36311  dnibndlem12  37187  knoppcnlem4  37194  knoppndvlem13  37222  cnndvlem1  37235  irrdiff  38079  relowlpssretop  38119  sin2h  38365  cos2h  38366  tan2h  38367  poimirlem7  38377  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem22  38392  poimirlem23  38393  poimirlem29  38399  poimirlem31  38401  itg2addnclem3  38423  asindmre  38453  dvasin  38454  dvacos  38455  dvreasin  38456  dvreacos  38457  fdc  38496  geomcau  38510  cntotbnd  38547  heiborlem8  38569  bfplem2  38574  bfp  38575  aks4d1p1p7  42941  ine1  43190  re1m1e0m0  43273  sn-00idlem1  43274  sn-00idlem2  43275  remul02  43281  sn-0ne2  43282  reixi  43299  rei4  43300  remullid  43310  ipiiie0  43314  sn-0tie0  43340  sn-nnne0  43349  mulgt0b1d  43361  sn-0lt1  43364  sn-ltp1  43365  reneg1lt0  43369  sn-inelr  43376  rabren3dioph  43657  pellexlem5  43675  pellexlem6  43676  pell1qrgaplem  43715  pell14qrgap  43717  pellqrex  43721  pellfundre  43723  pellfundlb  43726  pellfund14gap  43729  jm2.17a  43802  acongeq  43825  jm2.23  43838  jm3.1lem2  43860  sqrtcval  44482  sqrtcval2  44483  resqrtval  44484  imsqrtval  44485  relexp01min  44554  cvgdvgrat  45138  lhe4.4ex1a  45154  binomcxplemnotnn0  45181  isosctrlem1ALT  45757  supxrgelem  46168  xrlexaddrp  46183  infxr  46197  infleinflem2  46201  sumnnodd  46461  limsup10exlem  46601  limsup10ex  46602  dvnprodlem3  46777  stoweidlem1  46830  stoweidlem18  46847  stoweidlem19  46848  stoweidlem26  46855  stoweidlem34  46863  stoweidlem40  46869  stoweidlem41  46870  stoweidlem59  46888  stoweid  46892  stirlinglem10  46912  stirlinglem11  46913  dirkercncflem1  46932  fourierdlem16  46952  fourierdlem21  46957  fourierdlem22  46958  fourierdlem42  46978  fourierdlem68  47003  fourierdlem83  47018  fourierdlem103  47038  sqwvfourb  47058  fouriersw  47060  etransclem23  47086  salgencntex  47172  ovn0lem  47394  smfmullem3  47622  smfmullem4  47623  numtowerdt  47735  goldratval  47755  cjnpoly  47758  zm1nn  48191  ceilhalf1  48227  m1mod0mod1  48249  muldvdsfacgt  48275  fmtnosqrt  48443  nprmdvdsfacm1lem4  48527  perfectALTVlem2  48639  2exp340mod341  48650  8exp8mod9  48653  nfermltl8rev  48659  nnsum3primesprm  48707  nnsum4primesodd  48713  nnsum4primesoddALTV  48714  nnsum4primeseven  48717  nnsum4primesevenALTV  48718  tgblthelfgott  48732  tgoldbach  48734  usgrexmpl1lem  48938  usgrexmpl2lem  48943  usgrexmpl2nb1  48949  usgrexmpl2nb3  48951  usgrexmpl2nb4  48952  usgrexmpl2nb5  48953  usgrexmpl2trifr  48954  gpg3kgrtriexlem3  49002  pgnbgreunbgrlem2lem1  49031  pgnbgreunbgrlem2lem2  49032  rege1logbrege0  49489  rege1logbzge0  49490  blennnelnn  49507  dignnld  49534  nn0sumshdiglemA  49550  nn0sumshdiglem1  49552  rrx2xpref1o  49649  rrxlines  49664  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  line2ylem  49682  line2x  49685  icccldii  49846  io1ii  49848  sepfsepc  49855  1ne3  50775  veronesev1lem  50807  veronesev4lem  50810  veronesev5lem  50811  veronesev6lem  50812  veronesevrowd  50813  veronesematrowd  50815  veroquadgsumlem  50817  veroquadmodzerod  50818  veroquadnolindfd  50819