Step 63 / 64

High school

Contradiction with the same object

Evidence for f ≠ 0 and f = 0 cannot both hold for the same f.

Start with a concrete example

“This same box contains zero sweets” and “this box contains a nonzero number of sweets” cannot both be true. Two different boxes with different amounts would cause no contradiction. The same object matters.

A small check: try the idea

Think with the concrete example above. You can try again.

Is “f=0 and g≠0” a contradiction if f and g are different objects?

Read the answer and reasoning

No; the objects may differ. Two different boxes may hold different amounts. A contradiction requires incompatible statements about the same object under the same conditions.

Build the idea in three steps

  1. A negation such as f ≠ 0 means evidence for f = 0 would yield False, a contradiction.
  2. Both statements must concern exactly the same object in the same space. Two different forms can behave differently.
  3. Applying the nonzero evidence to the zero evidence closes the impossible branch, ruling out its original assumption.

A small example

One f cannot satisfy both f ≠ 0 and f = 0. A nonzero f and a different zero g would not be a contradiction.

Use in Lean · original excerpt

FLT · aa2d8b3 · S_FreyPackage_no_frey_package.lean

  hf (ModularForm.S2_Gamma0_2_eq_zero f)

How to read this Lean

hf is the nonzero evidence; the argument supplied to it proves the same form is zero. The source shows the contradiction’s application, not a new axiom.

Where this idea is used

2. The case of three7. The veterans’ cabinet15. The concert of absolute silence16. The room with no room
I’m lost · Help

Mika’s help desk

Contradiction with the same object

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Evidence for f ≠ 0 and f = 0 cannot both hold for the same f.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

One f cannot satisfy both f ≠ 0 and f = 0. A nonzero f and a different zero g would not be a contradiction.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →