Theorem 1re 11150

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 11102, 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 11113	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11102	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11147	. . . . 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 11142	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11147	. . . . . . . 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 7377	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7388	. . . . . . . . . . 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 3598	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3598	. . . . . . . . 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 3192	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3177	. . 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 3585	. . . . . . . 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 3585	. . . . . . 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 3177	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11116	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11129	. . . . . . 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 7369  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045  ici 11046   + caddc 11047   · cmul 11049

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 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  1red  11151  1xr  11209  dedekind  11313  peano2re  11323  mul02lem2  11327  addrid  11330  renegcl  11461  peano2rem  11465  0reALT  11495  0lt1  11676  0le1  11677  relin01  11678  1le1  11782  eqneg  11878  ltp1  11998  ltm1  12000  recgt0  12004  mulgt1OLD  12017  ltmulgt11  12018  lemulge11  12021  reclt1  12054  recgt1  12055  recgt1i  12056  recp1lt1  12057  recreclt  12058  recgt0ii  12065  ledivp1i  12084  ltdivp1i  12085  neg1rr  12148  neg1lt0  12150  cju  12158  nnssre  12166  nnge1  12190  nngt1ne1  12191  nnle1eq1  12192  nngt0  12193  nnnlt1  12194  nnne0  12196  nnrecre  12204  nnrecgt0  12205  nnsub  12206  2re  12236  3re  12242  4re  12246  5re  12249  6re  12252  7re  12255  8re  12258  9re  12261  0le2  12264  2pos  12265  3pos  12267  4pos  12269  5pos  12271  6pos  12272  7pos  12273  8pos  12274  9pos  12275  1lt2  12328  1lt3  12330  1lt4  12333  1lt5  12337  1lt6  12342  1lt7  12348  1lt8  12355  1lt9  12363  1ne2  12365  1le2  12366  1le3  12369  halflt1  12375  addltmul  12394  nnunb  12414  elnnnn0c  12463  nn0ge2m1nn  12488  elnnz1  12535  znnnlt1  12536  zltp1le  12559  zleltp1  12560  nn0lt2  12573  recnz  12585  gtndiv  12587  3halfnz  12589  10re  12644  1lt10  12764  eluzp1m1  12795  eluzp1p1  12797  eluz2b2  12856  zbtwnre  12881  rebtwnz  12882  1rp  12931  divlt1lt  12998  divle1le  12999  nnledivrp  13041  qbtwnxr  13136  xmulrid  13215  xmulm1  13217  x2times  13235  xrub  13248  elicc01  13403  1elunit  13407  divelunit  13431  lincmb01cmp  13432  unitssre  13436  0nelfz1  13480  fzpreddisj  13510  fznatpl1  13515  fztpval  13523  fraclt1  13740  fracle1  13741  flbi2  13755  fldiv4p1lem1div2  13773  fldiv4lem1div2  13775  fldiv  13798  modid  13834  1mod  13841  m1modnnsub1  13858  modm1p1mod0  13863  seqf1olem1  13982  reexpcl  14019  reexpclz  14023  expge0  14039  expge1  14040  expgt1  14041  bernneq  14170  bernneq2  14171  expnbnd  14173  expnlbnd  14174  expnlbnd2  14175  expmulnbnd  14176  discr1  14180  facwordi  14230  faclbnd3  14233  faclbnd4lem1  14234  faclbnd4lem4  14237  faclbnd6  14240  facavg  14242  hashv01gt1  14286  hashnn0n0nn  14332  hashunsnggt  14335  hash1snb  14360  hashgt12el  14363  hashgt12el2  14364  hashfun  14378  hashge2el2dif  14421  tpf1ofv2  14439  lsw0  14506  f1oun2prg  14859  cjexp  15092  re1  15096  im1  15097  rei  15098  imi  15099  01sqrexlem1  15184  01sqrexlem2  15185  01sqrexlem3  15186  01sqrexlem4  15187  01sqrexlem7  15190  resqrex  15192  sqrt1  15213  sqrt2gt1lt2  15216  sqrtm1  15217  abs1  15239  absrdbnd  15284  caubnd2  15300  mulcn2  15538  reccn2  15539  rlimno1  15596  o1fsum  15755  expcnv  15806  geolim  15812  geolim2  15813  georeclim  15814  geomulcvg  15818  geoisumr  15820  geoisum1c  15822  fprodge0  15935  fprodge1  15937  rerisefaccl  15959  refallfaccl  15960  ere  16031  ege2le3  16032  efgt1  16060  resin4p  16082  recos4p  16083  tanhbnd  16105  sinbnd  16124  cosbnd  16125  sinbnd2  16126  cosbnd2  16127  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  cos1bnd  16131  cos2bnd  16132  sinltx  16133  sin01gt0  16134  cos01gt0  16135  sin02gt0  16136  sincos1sgn  16137  ene1  16154  rpnnen2lem2  16159  rpnnen2lem3  16160  rpnnen2lem4  16161  rpnnen2lem9  16166  rpnnen2lem12  16169  ruclem6  16179  ruclem11  16184  ruclem12  16185  3dvds  16277  flodddiv4  16361  sadcadd  16404  isprm3  16629  sqnprm  16648  coprm  16657  phibndlem  16716  pythagtriplem3  16765  pcmpt  16839  fldivp1  16844  pockthi  16854  infpn2  16860  basendxnmulrndx  17235  starvndxnbasendx  17243  scandxnbasendx  17255  vscandxnbasendx  17260  ipndxnbasendx  17271  basendxnocndx  17322  slotsbhcdif  17354  lt6abl  19809  srgbinomlem4  20149  0ringnnzr  20445  abvneg  20746  abvtrivd  20752  xrsmcmn  21333  xrsnsgrp  21349  gzrngunitlem  21374  gzrngunit  21375  rge0srg  21380  psgnodpmr  21532  remulg  21549  resubdrg  21550  psdmvr  22089  dscmet  24493  dscopn  24494  nrginvrcnlem  24612  idnghm  24664  tgioo  24717  blcvx  24719  iicmp  24812  iiconn  24813  iirev  24856  iihalf1  24858  iihalf2  24861  iihalf2cnOLD  24863  elii1  24864  elii2  24865  iimulcl  24866  icopnfcnv  24873  icopnfhmeo  24874  iccpnfhmeo  24876  xrhmeo  24877  xrhmph  24878  evth  24891  xlebnum  24897  htpycc  24912  reparphti  24929  reparphtiOLD  24930  pcoval1  24946  pco1  24948  pcoval2  24949  pcocn  24950  pcohtpylem  24952  pcopt  24955  pcopt2  24956  pcoass  24957  pcorevlem  24959  nmhmcn  25053  ncvs1  25090  ovolunlem1a  25430  vitalilem2  25543  vitalilem4  25545  vitalilem5  25546  vitali  25547  i1f1  25624  itg11  25625  itg2const  25674  dveflem  25916  dvlipcn  25932  dvcvx  25958  ply1remlem  26103  fta1blem  26109  vieta1lem2  26252  aalioulem3  26275  aalioulem5  26277  aaliou3lem2  26284  ulmbdd  26340  iblulm  26349  radcnvlem1  26355  dvradcnv  26363  abelthlem2  26375  abelthlem3  26376  abelthlem5  26378  abelthlem7  26381  abelth  26384  abelth2  26385  reeff1olem  26389  reeff1o  26390  sinhalfpilem  26405  tangtx  26447  sincos4thpi  26455  pige3ALT  26462  coskpi  26465  cos0pilt1  26474  recosf1o  26477  tanregt0  26481  efif1olem3  26486  efif1olem4  26487  loge  26528  logdivlti  26562  logcnlem4  26587  logf1o2  26592  logtayl  26602  logccv  26605  recxpcl  26617  cxplea  26638  cxpcn3lem  26690  cxpaddlelem  26694  loglesqrt  26704  ang180lem2  26753  angpined  26773  acosrecl  26846  atancj  26853  atanlogaddlem  26856  atantan  26866  atans2  26874  ressatans  26877  leibpi  26885  log2le1  26893  birthdaylem3  26896  cxp2lim  26920  cxploglim  26921  cxploglim2  26922  divsqrtsumlem  26923  cvxcl  26928  scvxcvx  26929  jensenlem2  26931  amgmlem  26933  emcllem2  26940  emcllem4  26942  emcllem6  26944  emcllem7  26945  emre  26949  emgt0  26950  harmonicbnd3  26951  harmonicubnd  26953  harmonicbnd4  26954  zetacvg  26958  ftalem1  27016  ftalem2  27017  ftalem5  27020  issqf  27079  cht1  27108  chp1  27110  ppiltx  27120  mumullem2  27123  ppiublem1  27146  ppiub  27148  chtublem  27155  chtub  27156  logfacbnd3  27167  logexprlim  27169  perfectlem2  27174  dchrinv  27205  dchr1re  27207  efexple  27225  bposlem1  27228  bposlem2  27229  bposlem5  27232  bposlem8  27235  lgsdir2lem1  27269  lgsdir2lem5  27273  lgsdir  27276  lgsne0  27279  lgsabs1  27280  lgsdinn0  27289  gausslemma2dlem0i  27308  lgseisen  27323  m1lgs  27332  2lgslem3  27348  addsq2nreurex  27388  2sqreultblem  27392  2sqreunnltblem  27395  chebbnd1lem3  27415  chebbnd1  27416  chtppilimlem1  27417  chtppilimlem2  27418  chtppilim  27419  chpchtlim  27423  vmadivsumb  27427  rplogsumlem2  27429  rpvmasumlem  27431  dchrmusumlema  27437  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumiflem1  27445  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0fno1  27455  rpvmasum2  27456  dchrisum0re  27457  dchrisum0lema  27458  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  logdivsum  27477  mulog2sumlem2  27479  2vmadivsumlem  27484  log2sumbnd  27488  selbergb  27493  selberg2b  27496  chpdifbndlem1  27497  selberg3lem1  27501  selberg3lem2  27502  selberg4lem1  27504  pntrmax  27508  pntrsumo1  27509  selbergsb  27519  pntrlog2bndlem3  27523  pntrlog2bndlem5  27525  pntpbnd1a  27529  pntpbnd2  27531  pntibndlem1  27533  pntibndlem3  27536  pntlemd  27538  pntlemc  27539  pntlemb  27541  pntlemr  27546  pntlemf  27549  pntlemk  27550  pntlemo  27551  pntlem3  27553  pntleml  27555  abvcxp  27559  ostth2lem1  27562  ostth1  27577  ostth2lem2  27578  ostth2lem3  27579  ostth2lem4  27580  ostth2  27581  ostth3  27582  ostth  27583  slotsinbpsd  28421  slotslnbpsd  28422  trgcgrg  28495  brbtwn2  28885  colinearalglem4  28889  ax5seglem2  28909  ax5seglem3  28911  axpaschlem  28920  axpasch  28921  axlowdimlem6  28927  axlowdimlem10  28931  axlowdimlem16  28937  axlowdim1  28939  axlowdim2  28940  axlowdim  28941  axcontlem2  28945  elntg2  28965  lfgrnloop  29105  lfuhgr1v0e  29234  usgrexmpldifpr  29238  usgrexmplef  29239  1loopgrvd2  29484  vdegp1bi  29518  lfgrwlkprop  29666  pthdlem1  29746  pthdlem2  29748  clwlkclwwlkf  29987  upgr4cycl4dv4e  30164  konigsberglem2  30232  konigsberglem3  30233  konigsberglem5  30235  frgrreg  30373  ex-dif  30402  ex-in  30404  ex-pss  30407  ex-res  30420  ex-fl  30426  nv1  30654  smcnlem  30676  ipidsq  30689  nmlno0lem  30772  norm-ii-i  31116  bcs2  31161  norm1  31228  nmopub2tALT  31888  nmfnleub2  31905  nmlnop0iALT  31974  unopbd  31994  nmopadjlem  32068  nmopcoadji  32080  pjnmopi  32127  pjbdlni  32128  hstle1  32205  hstle  32209  hstles  32210  stge1i  32217  stlesi  32220  staddi  32225  stadd3i  32227  strlem1  32229  strlem5  32234  jplem1  32247  cdj1i  32412  addltmulALT  32425  xlt2addrd  32732  pr01ssre  32799  sgnclre  32807  sgnnbi  32813  sgnpbi  32814  sgnmulsgp  32818  indf  32828  indfval  32829  dp2lt10  32854  dp2ltsuc  32856  dp2ltc  32857  dplti  32875  dpmul4  32884  cshw1s2  32932  xrsmulgzz  32993  rearchi  33310  xrge0slmod  33312  prmidl0  33414  evl1deg3  33540  constrconj  33728  2sqr3minply  33763  submateqlem1  33790  xrge0iifcnv  33916  xrge0iifcv  33917  xrge0iifiso  33918  xrge0iifhom  33920  zrhre  34002  esumcst  34046  cntnevol  34211  omssubadd  34284  iwrdsplit  34371  dstfrvclim1  34462  coinfliprv  34467  ballotlem2  34473  ballotlem4  34483  ballotlemi1  34487  ballotlemic  34491  plymulx0  34531  plymulx  34532  signswch  34545  signstf  34550  signsvfn  34566  itgexpif  34590  hgt750lemd  34632  logdivsqrle  34634  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  tgoldbachgnn  34643  subfacp1lem1  35159  subfacp1lem5  35164  resconn  35226  iisconn  35232  iillysconn  35233  problem2  35646  problem3  35647  sinccvglem  35652  fz0n  35711  dnibndlem12  36470  knoppcnlem4  36477  knoppndvlem13  36505  cnndvlem1  36518  irrdiff  37307  relowlpssretop  37345  sin2h  37597  cos2h  37598  tan2h  37599  poimirlem7  37614  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem23  37630  poimirlem29  37636  poimirlem31  37638  itg2addnclem3  37660  asindmre  37690  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  fdc  37732  geomcau  37746  cntotbnd  37783  heiborlem8  37805  bfplem2  37810  bfp  37811  aks4d1p1p7  42055  1t1e1ALT  42236  ine1  42295  re1m1e0m0  42378  sn-00idlem1  42379  sn-00idlem2  42380  remul02  42386  sn-0ne2  42387  reixi  42404  rei4  42405  remullid  42415  ipiiie0  42419  sn-0tie0  42432  sn-nnne0  42441  mulgt0b1d  42453  sn-0lt1  42456  sn-ltp1  42457  reneg1lt0  42461  sn-inelr  42468  rabren3dioph  42796  pellexlem5  42814  pellexlem6  42815  pell1qrgaplem  42854  pell14qrgap  42856  pellqrex  42860  pellfundre  42862  pellfundlb  42865  pellfund14gap  42868  jm2.17a  42942  acongeq  42965  jm2.23  42978  jm3.1lem2  43000  sqrtcval  43623  sqrtcval2  43624  resqrtval  43625  imsqrtval  43626  relexp01min  43695  cvgdvgrat  44295  lhe4.4ex1a  44311  binomcxplemnotnn0  44338  isosctrlem1ALT  44916  supxrgelem  45326  xrlexaddrp  45341  infxr  45356  infleinflem2  45360  sumnnodd  45621  limsup10exlem  45763  limsup10ex  45764  dvnprodlem3  45939  stoweidlem1  45992  stoweidlem18  46009  stoweidlem19  46010  stoweidlem26  46017  stoweidlem34  46025  stoweidlem40  46031  stoweidlem41  46032  stoweidlem59  46050  stoweid  46054  stirlinglem10  46074  stirlinglem11  46075  dirkercncflem1  46094  fourierdlem16  46114  fourierdlem21  46119  fourierdlem22  46120  fourierdlem42  46140  fourierdlem68  46165  fourierdlem83  46180  fourierdlem103  46200  sqwvfourb  46220  fouriersw  46222  etransclem23  46248  salgencntex  46334  ovn0lem  46556  smfmullem3  46784  smfmullem4  46785  cjnpoly  46883  zm1nn  47296  ceilhalf1  47328  m1mod0mod1  47348  fmtnosqrt  47533  perfectALTVlem2  47716  2exp340mod341  47727  8exp8mod9  47730  nfermltl8rev  47736  nnsum3primesprm  47784  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  tgblthelfgott  47809  tgoldbach  47811  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb1  48016  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpg3kgrtriexlem3  48069  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  rege1logbrege0  48540  rege1logbzge0  48541  blennnelnn  48558  dignnld  48585  nn0sumshdiglemA  48601  nn0sumshdiglem1  48603  rrx2xpref1o  48700  rrxlines  48715  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720  line2ylem  48733  line2x  48736  icccldii  48900  io1ii  48902  sepfsepc  48909