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  19801  srgbinomlem4  20114  0ringnnzr  20410  abvneg  20711  abvtrivd  20717  xrsmcmn  21279  xrsnsgrp  21295  gzrngunitlem  21325  gzrngunit  21326  rge0srg  21331  psgnodpmr  21475  remulg  21492  resubdrg  21493  psdmvr  22032  dscmet  24436  dscopn  24437  nrginvrcnlem  24555  idnghm  24607  tgioo  24660  blcvx  24662  iicmp  24755  iiconn  24756  iirev  24799  iihalf1  24801  iihalf2  24804  iihalf2cnOLD  24806  elii1  24807  elii2  24808  iimulcl  24809  icopnfcnv  24816  icopnfhmeo  24817  iccpnfhmeo  24819  xrhmeo  24820  xrhmph  24821  evth  24834  xlebnum  24840  htpycc  24855  reparphti  24872  reparphtiOLD  24873  pcoval1  24889  pco1  24891  pcoval2  24892  pcocn  24893  pcohtpylem  24895  pcopt  24898  pcopt2  24899  pcoass  24900  pcorevlem  24902  nmhmcn  24996  ncvs1  25033  ovolunlem1a  25373  vitalilem2  25486  vitalilem4  25488  vitalilem5  25489  vitali  25490  i1f1  25567  itg11  25568  itg2const  25617  dveflem  25859  dvlipcn  25875  dvcvx  25901  ply1remlem  26046  fta1blem  26052  vieta1lem2  26195  aalioulem3  26218  aalioulem5  26220  aaliou3lem2  26227  ulmbdd  26283  iblulm  26292  radcnvlem1  26298  dvradcnv  26306  abelthlem2  26318  abelthlem3  26319  abelthlem5  26321  abelthlem7  26324  abelth  26327  abelth2  26328  reeff1olem  26332  reeff1o  26333  sinhalfpilem  26348  tangtx  26390  sincos4thpi  26398  pige3ALT  26405  coskpi  26408  cos0pilt1  26417  recosf1o  26420  tanregt0  26424  efif1olem3  26429  efif1olem4  26430  loge  26471  logdivlti  26505  logcnlem4  26530  logf1o2  26535  logtayl  26545  logccv  26548  recxpcl  26560  cxplea  26581  cxpcn3lem  26633  cxpaddlelem  26637  loglesqrt  26647  ang180lem2  26696  angpined  26716  acosrecl  26789  atancj  26796  atanlogaddlem  26799  atantan  26809  atans2  26817  ressatans  26820  leibpi  26828  log2le1  26836  birthdaylem3  26839  cxp2lim  26863  cxploglim  26864  cxploglim2  26865  divsqrtsumlem  26866  cvxcl  26871  scvxcvx  26872  jensenlem2  26874  amgmlem  26876  emcllem2  26883  emcllem4  26885  emcllem6  26887  emcllem7  26888  emre  26892  emgt0  26893  harmonicbnd3  26894  harmonicubnd  26896  harmonicbnd4  26897  zetacvg  26901  ftalem1  26959  ftalem2  26960  ftalem5  26963  issqf  27022  cht1  27051  chp1  27053  ppiltx  27063  mumullem2  27066  ppiublem1  27089  ppiub  27091  chtublem  27098  chtub  27099  logfacbnd3  27110  logexprlim  27112  perfectlem2  27117  dchrinv  27148  dchr1re  27150  efexple  27168  bposlem1  27171  bposlem2  27172  bposlem5  27175  bposlem8  27178  lgsdir2lem1  27212  lgsdir2lem5  27216  lgsdir  27219  lgsne0  27222  lgsabs1  27223  lgsdinn0  27232  gausslemma2dlem0i  27251  lgseisen  27266  m1lgs  27275  2lgslem3  27291  addsq2nreurex  27331  2sqreultblem  27335  2sqreunnltblem  27338  chebbnd1lem3  27358  chebbnd1  27359  chtppilimlem1  27360  chtppilimlem2  27361  chtppilim  27362  chpchtlim  27366  vmadivsumb  27370  rplogsumlem2  27372  rpvmasumlem  27374  dchrmusumlema  27380  dchrmusum2  27381  dchrvmasumlem2  27385  dchrvmasumiflem1  27388  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0fno1  27398  rpvmasum2  27399  dchrisum0re  27400  dchrisum0lema  27401  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0lem2  27405  logdivsum  27420  mulog2sumlem2  27422  2vmadivsumlem  27427  log2sumbnd  27431  selbergb  27436  selberg2b  27439  chpdifbndlem1  27440  selberg3lem1  27444  selberg3lem2  27445  selberg4lem1  27447  pntrmax  27451  pntrsumo1  27452  selbergsb  27462  pntrlog2bndlem3  27466  pntrlog2bndlem5  27468  pntpbnd1a  27472  pntpbnd2  27474  pntibndlem1  27476  pntibndlem3  27479  pntlemd  27481  pntlemc  27482  pntlemb  27484  pntlemr  27489  pntlemf  27492  pntlemk  27493  pntlemo  27494  pntlem3  27496  pntleml  27498  abvcxp  27502  ostth2lem1  27505  ostth1  27520  ostth2lem2  27521  ostth2lem3  27522  ostth2lem4  27523  ostth2  27524  ostth3  27525  ostth  27526  slotsinbpsd  28344  slotslnbpsd  28345  trgcgrg  28418  brbtwn2  28808  colinearalglem4  28812  ax5seglem2  28832  ax5seglem3  28834  axpaschlem  28843  axpasch  28844  axlowdimlem6  28850  axlowdimlem10  28854  axlowdimlem16  28860  axlowdim1  28862  axlowdim2  28863  axlowdim  28864  axcontlem2  28868  elntg2  28888  lfgrnloop  29028  lfuhgr1v0e  29157  usgrexmpldifpr  29161  usgrexmplef  29162  1loopgrvd2  29407  vdegp1bi  29441  lfgrwlkprop  29589  pthdlem1  29669  pthdlem2  29671  clwlkclwwlkf  29910  upgr4cycl4dv4e  30087  konigsberglem2  30155  konigsberglem3  30156  konigsberglem5  30158  frgrreg  30296  ex-dif  30325  ex-in  30327  ex-pss  30330  ex-res  30343  ex-fl  30349  nv1  30577  smcnlem  30599  ipidsq  30612  nmlno0lem  30695  norm-ii-i  31039  bcs2  31084  norm1  31151  nmopub2tALT  31811  nmfnleub2  31828  nmlnop0iALT  31897  unopbd  31917  nmopadjlem  31991  nmopcoadji  32003  pjnmopi  32050  pjbdlni  32051  hstle1  32128  hstle  32132  hstles  32133  stge1i  32140  stlesi  32143  staddi  32148  stadd3i  32150  strlem1  32152  strlem5  32157  jplem1  32170  cdj1i  32335  addltmulALT  32348  xlt2addrd  32655  pr01ssre  32722  sgnclre  32730  sgnnbi  32736  sgnpbi  32737  sgnmulsgp  32741  indf  32751  indfval  32752  dp2lt10  32777  dp2ltsuc  32779  dp2ltc  32780  dplti  32798  dpmul4  32807  cshw1s2  32855  xrsmulgzz  32920  rearchi  33290  xrge0slmod  33292  prmidl0  33394  evl1deg3  33520  constrconj  33708  2sqr3minply  33743  submateqlem1  33770  xrge0iifcnv  33896  xrge0iifcv  33897  xrge0iifiso  33898  xrge0iifhom  33900  zrhre  33982  esumcst  34026  cntnevol  34191  omssubadd  34264  iwrdsplit  34351  dstfrvclim1  34442  coinfliprv  34447  ballotlem2  34453  ballotlem4  34463  ballotlemi1  34467  ballotlemic  34471  plymulx0  34511  plymulx  34512  signswch  34525  signstf  34530  signsvfn  34546  itgexpif  34570  hgt750lemd  34612  logdivsqrle  34614  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  tgoldbachgnn  34623  subfacp1lem1  35139  subfacp1lem5  35144  resconn  35206  iisconn  35212  iillysconn  35213  problem2  35626  problem3  35627  sinccvglem  35632  fz0n  35691  dnibndlem12  36450  knoppcnlem4  36457  knoppndvlem13  36485  cnndvlem1  36498  irrdiff  37287  relowlpssretop  37325  sin2h  37577  cos2h  37578  tan2h  37579  poimirlem7  37594  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem22  37609  poimirlem23  37610  poimirlem29  37616  poimirlem31  37618  itg2addnclem3  37640  asindmre  37670  dvasin  37671  dvacos  37672  dvreasin  37673  dvreacos  37674  fdc  37712  geomcau  37726  cntotbnd  37763  heiborlem8  37785  bfplem2  37790  bfp  37791  aks4d1p1p7  42035  1t1e1ALT  42216  ine1  42275  re1m1e0m0  42358  sn-00idlem1  42359  sn-00idlem2  42360  remul02  42366  sn-0ne2  42367  reixi  42384  rei4  42385  remullid  42395  ipiiie0  42399  sn-0tie0  42412  sn-nnne0  42421  mulgt0b1d  42433  sn-0lt1  42436  sn-ltp1  42437  reneg1lt0  42441  sn-inelr  42448  rabren3dioph  42776  pellexlem5  42794  pellexlem6  42795  pell1qrgaplem  42834  pell14qrgap  42836  pellqrex  42840  pellfundre  42842  pellfundlb  42845  pellfund14gap  42848  jm2.17a  42922  acongeq  42945  jm2.23  42958  jm3.1lem2  42980  sqrtcval  43603  sqrtcval2  43604  resqrtval  43605  imsqrtval  43606  relexp01min  43675  cvgdvgrat  44275  lhe4.4ex1a  44291  binomcxplemnotnn0  44318  isosctrlem1ALT  44896  supxrgelem  45306  xrlexaddrp  45321  infxr  45336  infleinflem2  45340  sumnnodd  45601  limsup10exlem  45743  limsup10ex  45744  dvnprodlem3  45919  stoweidlem1  45972  stoweidlem18  45989  stoweidlem19  45990  stoweidlem26  45997  stoweidlem34  46005  stoweidlem40  46011  stoweidlem41  46012  stoweidlem59  46030  stoweid  46034  stirlinglem10  46054  stirlinglem11  46055  dirkercncflem1  46074  fourierdlem16  46094  fourierdlem21  46099  fourierdlem22  46100  fourierdlem42  46120  fourierdlem68  46145  fourierdlem83  46160  fourierdlem103  46180  sqwvfourb  46200  fouriersw  46202  etransclem23  46228  salgencntex  46314  ovn0lem  46536  smfmullem3  46764  smfmullem4  46765  cjnpoly  46863  zm1nn  47276  ceilhalf1  47308  m1mod0mod1  47328  fmtnosqrt  47513  perfectALTVlem2  47696  2exp340mod341  47707  8exp8mod9  47710  nfermltl8rev  47716  nnsum3primesprm  47764  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  tgblthelfgott  47789  tgoldbach  47791  usgrexmpl1lem  47985  usgrexmpl2lem  47990  usgrexmpl2nb1  47996  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  gpg3kgrtriexlem3  48049  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  rege1logbrege0  48520  rege1logbzge0  48521  blennnelnn  48538  dignnld  48565  nn0sumshdiglemA  48581  nn0sumshdiglem1  48583  rrx2xpref1o  48680  rrxlines  48695  eenglngeehlnmlem1  48699  eenglngeehlnmlem2  48700  line2ylem  48713  line2x  48716  icccldii  48880  io1ii  48882  sepfsepc  48889