Theorem 1re 11174

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 11126, 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 11137	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11126	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11171	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2987	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11166	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11171	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2988	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3148	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3148	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3148	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3148	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7395	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7406	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2946	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2939	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3601	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3601	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1121	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 859	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3194	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3179	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2751	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2946	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2987	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3588	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 413	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 490	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 2987	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3588	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 413	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 491	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3008	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3179	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11140	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11153	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2816	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3134	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3126	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  (class class class)co 7387  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069  ici 11070   + caddc 11071   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  1red  11175  1xr  11233  dedekind  11337  peano2re  11347  mul02lem2  11351  addrid  11354  renegcl  11485  peano2rem  11489  0reALT  11519  0lt1  11700  0le1  11701  relin01  11702  1le1  11806  eqneg  11902  ltp1  12022  ltm1  12024  recgt0  12028  mulgt1OLD  12041  ltmulgt11  12042  lemulge11  12045  reclt1  12078  recgt1  12079  recgt1i  12080  recp1lt1  12081  recreclt  12082  recgt0ii  12089  ledivp1i  12108  ltdivp1i  12109  neg1rr  12172  neg1lt0  12174  cju  12182  nnssre  12190  nnge1  12214  nngt1ne1  12215  nnle1eq1  12216  nngt0  12217  nnnlt1  12218  nnne0  12220  nnrecre  12228  nnrecgt0  12229  nnsub  12230  2re  12260  3re  12266  4re  12270  5re  12273  6re  12276  7re  12279  8re  12282  9re  12285  0le2  12288  2pos  12289  3pos  12291  4pos  12293  5pos  12295  6pos  12296  7pos  12297  8pos  12298  9pos  12299  1lt2  12352  1lt3  12354  1lt4  12357  1lt5  12361  1lt6  12366  1lt7  12372  1lt8  12379  1lt9  12387  1ne2  12389  1le2  12390  1le3  12393  halflt1  12399  addltmul  12418  nnunb  12438  elnnnn0c  12487  nn0ge2m1nn  12512  elnnz1  12559  znnnlt1  12560  zltp1le  12583  zleltp1  12584  nn0lt2  12597  recnz  12609  gtndiv  12611  3halfnz  12613  10re  12668  1lt10  12788  eluzp1m1  12819  eluzp1p1  12821  eluz2b2  12880  zbtwnre  12905  rebtwnz  12906  1rp  12955  divlt1lt  13022  divle1le  13023  nnledivrp  13065  qbtwnxr  13160  xmulrid  13239  xmulm1  13241  x2times  13259  xrub  13272  elicc01  13427  1elunit  13431  divelunit  13455  lincmb01cmp  13456  unitssre  13460  0nelfz1  13504  fzpreddisj  13534  fznatpl1  13539  fztpval  13547  fraclt1  13764  fracle1  13765  flbi2  13779  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  fldiv  13822  modid  13858  1mod  13865  m1modnnsub1  13882  modm1p1mod0  13887  seqf1olem1  14006  reexpcl  14043  reexpclz  14047  expge0  14063  expge1  14064  expgt1  14065  bernneq  14194  bernneq2  14195  expnbnd  14197  expnlbnd  14198  expnlbnd2  14199  expmulnbnd  14200  discr1  14204  facwordi  14254  faclbnd3  14257  faclbnd4lem1  14258  faclbnd4lem4  14261  faclbnd6  14264  facavg  14266  hashv01gt1  14310  hashnn0n0nn  14356  hashunsnggt  14359  hash1snb  14384  hashgt12el  14387  hashgt12el2  14388  hashfun  14402  hashge2el2dif  14445  tpf1ofv2  14463  lsw0  14530  f1oun2prg  14883  cjexp  15116  re1  15120  im1  15121  rei  15122  imi  15123  01sqrexlem1  15208  01sqrexlem2  15209  01sqrexlem3  15210  01sqrexlem4  15211  01sqrexlem7  15214  resqrex  15216  sqrt1  15237  sqrt2gt1lt2  15240  sqrtm1  15241  abs1  15263  absrdbnd  15308  caubnd2  15324  mulcn2  15562  reccn2  15563  rlimno1  15620  o1fsum  15779  expcnv  15830  geolim  15836  geolim2  15837  georeclim  15838  geomulcvg  15842  geoisumr  15844  geoisum1c  15846  fprodge0  15959  fprodge1  15961  rerisefaccl  15983  refallfaccl  15984  ere  16055  ege2le3  16056  efgt1  16084  resin4p  16106  recos4p  16107  tanhbnd  16129  sinbnd  16148  cosbnd  16149  sinbnd2  16150  cosbnd2  16151  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  cos1bnd  16155  cos2bnd  16156  sinltx  16157  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  sincos1sgn  16161  ene1  16178  rpnnen2lem2  16183  rpnnen2lem3  16184  rpnnen2lem4  16185  rpnnen2lem9  16190  rpnnen2lem12  16193  ruclem6  16203  ruclem11  16208  ruclem12  16209  3dvds  16301  flodddiv4  16385  sadcadd  16428  isprm3  16653  sqnprm  16672  coprm  16681  phibndlem  16740  pythagtriplem3  16789  pcmpt  16863  fldivp1  16868  pockthi  16878  infpn2  16884  basendxnmulrndx  17259  starvndxnbasendx  17267  scandxnbasendx  17279  vscandxnbasendx  17284  ipndxnbasendx  17295  basendxnocndx  17346  slotsbhcdif  17378  lt6abl  19825  srgbinomlem4  20138  0ringnnzr  20434  abvneg  20735  abvtrivd  20741  xrsmcmn  21303  xrsnsgrp  21319  gzrngunitlem  21349  gzrngunit  21350  rge0srg  21355  psgnodpmr  21499  remulg  21516  resubdrg  21517  psdmvr  22056  dscmet  24460  dscopn  24461  nrginvrcnlem  24579  idnghm  24631  tgioo  24684  blcvx  24686  iicmp  24779  iiconn  24780  iirev  24823  iihalf1  24825  iihalf2  24828  iihalf2cnOLD  24830  elii1  24831  elii2  24832  iimulcl  24833  icopnfcnv  24840  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  xrhmph  24845  evth  24858  xlebnum  24864  htpycc  24879  reparphti  24896  reparphtiOLD  24897  pcoval1  24913  pco1  24915  pcoval2  24916  pcocn  24917  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  nmhmcn  25020  ncvs1  25057  ovolunlem1a  25397  vitalilem2  25510  vitalilem4  25512  vitalilem5  25513  vitali  25514  i1f1  25591  itg11  25592  itg2const  25641  dveflem  25883  dvlipcn  25899  dvcvx  25925  ply1remlem  26070  fta1blem  26076  vieta1lem2  26219  aalioulem3  26242  aalioulem5  26244  aaliou3lem2  26251  ulmbdd  26307  iblulm  26316  radcnvlem1  26322  dvradcnv  26330  abelthlem2  26342  abelthlem3  26343  abelthlem5  26345  abelthlem7  26348  abelth  26351  abelth2  26352  reeff1olem  26356  reeff1o  26357  sinhalfpilem  26372  tangtx  26414  sincos4thpi  26422  pige3ALT  26429  coskpi  26432  cos0pilt1  26441  recosf1o  26444  tanregt0  26448  efif1olem3  26453  efif1olem4  26454  loge  26495  logdivlti  26529  logcnlem4  26554  logf1o2  26559  logtayl  26569  logccv  26572  recxpcl  26584  cxplea  26605  cxpcn3lem  26657  cxpaddlelem  26661  loglesqrt  26671  ang180lem2  26720  angpined  26740  acosrecl  26813  atancj  26820  atanlogaddlem  26823  atantan  26833  atans2  26841  ressatans  26844  leibpi  26852  log2le1  26860  birthdaylem3  26863  cxp2lim  26887  cxploglim  26888  cxploglim2  26889  divsqrtsumlem  26890  cvxcl  26895  scvxcvx  26896  jensenlem2  26898  amgmlem  26900  emcllem2  26907  emcllem4  26909  emcllem6  26911  emcllem7  26912  emre  26916  emgt0  26917  harmonicbnd3  26918  harmonicubnd  26920  harmonicbnd4  26921  zetacvg  26925  ftalem1  26983  ftalem2  26984  ftalem5  26987  issqf  27046  cht1  27075  chp1  27077  ppiltx  27087  mumullem2  27090  ppiublem1  27113  ppiub  27115  chtublem  27122  chtub  27123  logfacbnd3  27134  logexprlim  27136  perfectlem2  27141  dchrinv  27172  dchr1re  27174  efexple  27192  bposlem1  27195  bposlem2  27196  bposlem5  27199  bposlem8  27202  lgsdir2lem1  27236  lgsdir2lem5  27240  lgsdir  27243  lgsne0  27246  lgsabs1  27247  lgsdinn0  27256  gausslemma2dlem0i  27275  lgseisen  27290  m1lgs  27299  2lgslem3  27315  addsq2nreurex  27355  2sqreultblem  27359  2sqreunnltblem  27362  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chpchtlim  27390  vmadivsumb  27394  rplogsumlem2  27396  rpvmasumlem  27398  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0fno1  27422  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  logdivsum  27444  mulog2sumlem2  27446  2vmadivsumlem  27451  log2sumbnd  27455  selbergb  27460  selberg2b  27463  chpdifbndlem1  27464  selberg3lem1  27468  selberg3lem2  27469  selberg4lem1  27471  pntrmax  27475  pntrsumo1  27476  selbergsb  27486  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem1  27500  pntibndlem3  27503  pntlemd  27505  pntlemc  27506  pntlemb  27508  pntlemr  27513  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntlem3  27520  pntleml  27522  abvcxp  27526  ostth2lem1  27529  ostth1  27544  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth2  27548  ostth3  27549  ostth  27550  slotsinbpsd  28368  slotslnbpsd  28369  trgcgrg  28442  brbtwn2  28832  colinearalglem4  28836  ax5seglem2  28856  ax5seglem3  28858  axpaschlem  28867  axpasch  28868  axlowdimlem6  28874  axlowdimlem10  28878  axlowdimlem16  28884  axlowdim1  28886  axlowdim2  28887  axlowdim  28888  axcontlem2  28892  elntg2  28912  lfgrnloop  29052  lfuhgr1v0e  29181  usgrexmpldifpr  29185  usgrexmplef  29186  1loopgrvd2  29431  vdegp1bi  29465  lfgrwlkprop  29615  pthdlem1  29696  pthdlem2  29698  clwlkclwwlkf  29937  upgr4cycl4dv4e  30114  konigsberglem2  30182  konigsberglem3  30183  konigsberglem5  30185  frgrreg  30323  ex-dif  30352  ex-in  30354  ex-pss  30357  ex-res  30370  ex-fl  30376  nv1  30604  smcnlem  30626  ipidsq  30639  nmlno0lem  30722  norm-ii-i  31066  bcs2  31111  norm1  31178  nmopub2tALT  31838  nmfnleub2  31855  nmlnop0iALT  31924  unopbd  31944  nmopadjlem  32018  nmopcoadji  32030  pjnmopi  32077  pjbdlni  32078  hstle1  32155  hstle  32159  hstles  32160  stge1i  32167  stlesi  32170  staddi  32175  stadd3i  32177  strlem1  32179  strlem5  32184  jplem1  32197  cdj1i  32362  addltmulALT  32375  xlt2addrd  32682  pr01ssre  32749  sgnclre  32757  sgnnbi  32763  sgnpbi  32764  sgnmulsgp  32768  indf  32778  indfval  32779  dp2lt10  32804  dp2ltsuc  32806  dp2ltc  32807  dplti  32825  dpmul4  32834  cshw1s2  32882  xrsmulgzz  32947  rearchi  33317  xrge0slmod  33319  prmidl0  33421  evl1deg3  33547  constrconj  33735  2sqr3minply  33770  submateqlem1  33797  xrge0iifcnv  33923  xrge0iifcv  33924  xrge0iifiso  33925  xrge0iifhom  33927  zrhre  34009  esumcst  34053  cntnevol  34218  omssubadd  34291  iwrdsplit  34378  dstfrvclim1  34469  coinfliprv  34474  ballotlem2  34480  ballotlem4  34490  ballotlemi1  34494  ballotlemic  34498  plymulx0  34538  plymulx  34539  signswch  34552  signstf  34557  signsvfn  34573  itgexpif  34597  hgt750lemd  34639  logdivsqrle  34641  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  tgoldbachgnn  34650  subfacp1lem1  35166  subfacp1lem5  35171  resconn  35233  iisconn  35239  iillysconn  35240  problem2  35653  problem3  35654  sinccvglem  35659  fz0n  35718  dnibndlem12  36477  knoppcnlem4  36484  knoppndvlem13  36512  cnndvlem1  36525  irrdiff  37314  relowlpssretop  37352  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem7  37621  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem29  37643  poimirlem31  37645  itg2addnclem3  37667  asindmre  37697  dvasin  37698  dvacos  37699  dvreasin  37700  dvreacos  37701  fdc  37739  geomcau  37753  cntotbnd  37790  heiborlem8  37812  bfplem2  37817  bfp  37818  aks4d1p1p7  42062  1t1e1ALT  42243  ine1  42302  re1m1e0m0  42385  sn-00idlem1  42386  sn-00idlem2  42387  remul02  42393  sn-0ne2  42394  reixi  42411  rei4  42412  remullid  42422  ipiiie0  42426  sn-0tie0  42439  sn-nnne0  42448  mulgt0b1d  42460  sn-0lt1  42463  sn-ltp1  42464  reneg1lt0  42468  sn-inelr  42475  rabren3dioph  42803  pellexlem5  42821  pellexlem6  42822  pell1qrgaplem  42861  pell14qrgap  42863  pellqrex  42867  pellfundre  42869  pellfundlb  42872  pellfund14gap  42875  jm2.17a  42949  acongeq  42972  jm2.23  42985  jm3.1lem2  43007  sqrtcval  43630  sqrtcval2  43631  resqrtval  43632  imsqrtval  43633  relexp01min  43702  cvgdvgrat  44302  lhe4.4ex1a  44318  binomcxplemnotnn0  44345  isosctrlem1ALT  44923  supxrgelem  45333  xrlexaddrp  45348  infxr  45363  infleinflem2  45367  sumnnodd  45628  limsup10exlem  45770  limsup10ex  45771  dvnprodlem3  45946  stoweidlem1  45999  stoweidlem18  46016  stoweidlem19  46017  stoweidlem26  46024  stoweidlem34  46032  stoweidlem40  46038  stoweidlem41  46039  stoweidlem59  46057  stoweid  46061  stirlinglem10  46081  stirlinglem11  46082  dirkercncflem1  46101  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem42  46147  fourierdlem68  46172  fourierdlem83  46187  fourierdlem103  46207  sqwvfourb  46227  fouriersw  46229  etransclem23  46255  salgencntex  46341  ovn0lem  46563  smfmullem3  46791  smfmullem4  46792  cjnpoly  46890  zm1nn  47303  ceilhalf1  47335  m1mod0mod1  47355  fmtnosqrt  47540  perfectALTVlem2  47723  2exp340mod341  47734  8exp8mod9  47737  nfermltl8rev  47743  nnsum3primesprm  47791  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  tgblthelfgott  47816  tgoldbach  47818  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb1  48023  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpg3kgrtriexlem3  48076  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  rege1logbrege0  48547  rege1logbzge0  48548  blennnelnn  48565  dignnld  48592  nn0sumshdiglemA  48608  nn0sumshdiglem1  48610  rrx2xpref1o  48707  rrxlines  48722  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  line2ylem  48740  line2x  48743  icccldii  48907  io1ii  48909  sepfsepc  48916